[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
a₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
h : { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }
⊢ a₁ = a₂ ∧ HEq b₁ b₂
[PROOFSTEP]
cases h
[GOAL]
case refl
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
a₁ : α
b₁ : β a₁
⊢ a₁ = a₁ ∧ HEq b₁ b₁
[PROOFSTEP]
exact ⟨rfl, heq_of_eq rfl⟩
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
a₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
x✝ : a₁ = a₂ ∧ HEq b₁ b₂
h₁ : a₁ = a₂
h₂ : HEq b₁ b₂
⊢ { fst := a₁, snd := b₁ } = { fst := a₂, snd := b₂ }
[PROOFSTEP]
subst h₁
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
a₁ : α
b₁ b₂ : β a₁
x✝ : a₁ = a₁ ∧ HEq b₁ b₂
h₂ : HEq b₁ b₂
⊢ { fst := a₁, snd := b₁ } = { fst := a₁, snd := b₂ }
[PROOFSTEP]
rw [eq_of_heq h₂]
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
x₀ x₁ : Sigma β
h₀ : x₀.fst = x₁.fst
h₁ : HEq x₀.snd x₁.snd
⊢ x₀ = x₁
[PROOFSTEP]
cases x₀
[GOAL]
case mk
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
x₁ : Sigma β
fst✝ : α
snd✝ : β fst✝
h₀ : { fst := fst✝, snd := snd✝ }.fst = x₁.fst
h₁ : HEq { fst := fst✝, snd := snd✝ }.snd x₁.snd
⊢ { fst := fst✝, snd := snd✝ } = x₁
[PROOFSTEP]
cases x₁
[GOAL]
case mk.mk
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
fst✝¹ : α
snd✝¹ : β fst✝¹
fst✝ : α
snd✝ : β fst✝
h₀ : { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst
h₁ : HEq { fst := fst✝¹, snd := snd✝¹ }.snd { fst := fst✝, snd := snd✝ }.snd
⊢ { fst := fst✝¹, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
cases h₀
[GOAL]
case mk.mk.refl
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
fst✝ : α
snd✝¹ snd✝ : β fst✝
h₁ : HEq { fst := fst✝, snd := snd✝¹ }.snd { fst := fst✝, snd := snd✝ }.snd
⊢ { fst := fst✝, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
cases h₁
[GOAL]
case mk.mk.refl.refl
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝, snd := snd✝ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
x₀ x₁ : Sigma β
⊢ x₀ = x₁ ↔ x₀.fst = x₁.fst ∧ HEq x₀.snd x₁.snd
[PROOFSTEP]
cases x₀
[GOAL]
case mk
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
x₁ : Sigma β
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝, snd := snd✝ } = x₁ ↔
    { fst := fst✝, snd := snd✝ }.fst = x₁.fst ∧ HEq { fst := fst✝, snd := snd✝ }.snd x₁.snd
[PROOFSTEP]
cases x₁
[GOAL]
case mk.mk
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
fst✝¹ : α
snd✝¹ : β fst✝¹
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝¹, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ } ↔
    { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst ∧
      HEq { fst := fst✝¹, snd := snd✝¹ }.snd { fst := fst✝, snd := snd✝ }.snd
[PROOFSTEP]
exact Sigma.mk.inj_iff
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
γ : Type u_7
inst✝ : Nonempty γ
a b : α
f : γ → β a
g : γ → β b
h : mk a ∘ f = mk b ∘ g
⊢ a = b ∧ HEq f g
[PROOFSTEP]
rcases‹Nonempty γ› with ⟨i⟩
[GOAL]
case intro
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
γ : Type u_7
inst✝ : Nonempty γ
a b : α
f : γ → β a
g : γ → β b
h : mk a ∘ f = mk b ∘ g
i : γ
⊢ a = b ∧ HEq f g
[PROOFSTEP]
obtain rfl : a = b := congr_arg Sigma.fst (congr_fun h i)
[GOAL]
case intro
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
γ : Type u_7
inst✝ : Nonempty γ
a : α
f : γ → β a
i : γ
g : γ → β a
h : mk a ∘ f = mk a ∘ g
⊢ a = a ∧ HEq f g
[PROOFSTEP]
simpa [Function.funext_iff] using h
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x : β₁ i
j : α₁
y : β₁ j
h : Sigma.map f₁ f₂ { fst := i, snd := x } = Sigma.map f₁ f₂ { fst := j, snd := y }
⊢ { fst := i, snd := x } = { fst := j, snd := y }
[PROOFSTEP]
obtain rfl : i = j := h₁ (Sigma.mk.inj_iff.mp h).1
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x y : β₁ i
h : Sigma.map f₁ f₂ { fst := i, snd := x } = Sigma.map f₁ f₂ { fst := i, snd := y }
⊢ { fst := i, snd := x } = { fst := i, snd := y }
[PROOFSTEP]
obtain rfl : x = y := h₂ i (sigma_mk_injective h)
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Injective f₁
h₂ : ∀ (a : α₁), Injective (f₂ a)
i : α₁
x : β₁ i
h : Sigma.map f₁ f₂ { fst := i, snd := x } = Sigma.map f₁ f₂ { fst := i, snd := x }
⊢ { fst := i, snd := x } = { fst := i, snd := x }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
⊢ Surjective (Sigma.map f₁ f₂)
[PROOFSTEP]
simp only [Function.Surjective, Sigma.forall, h₁.forall]
[GOAL]
α : Type u_1
α₁ : Type u_2
α₂ : Type u_3
β : α → Type u_4
β₁ : α₁ → Type u_5
β₂ : α₂ → Type u_6
f₁ : α₁ → α₂
f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)
h₁ : Surjective f₁
h₂ : ∀ (a : α₁), Surjective (f₂ a)
⊢ ∀ (x : α₁) (b : β₂ (f₁ x)), ∃ a, Sigma.map f₁ f₂ a = { fst := f₁ x, snd := b }
[PROOFSTEP]
exact fun i ↦ (h₂ _).forall.2 fun x ↦ ⟨⟨i, x⟩, rfl⟩
[GOAL]
α : Sort u_1
β : α → Sort u_2
x₀ x₁ : PSigma β
h₀ : x₀.fst = x₁.fst
h₁ : HEq x₀.snd x₁.snd
⊢ x₀ = x₁
[PROOFSTEP]
cases x₀
[GOAL]
case mk
α : Sort u_1
β : α → Sort u_2
x₁ : PSigma β
fst✝ : α
snd✝ : β fst✝
h₀ : { fst := fst✝, snd := snd✝ }.fst = x₁.fst
h₁ : HEq { fst := fst✝, snd := snd✝ }.snd x₁.snd
⊢ { fst := fst✝, snd := snd✝ } = x₁
[PROOFSTEP]
cases x₁
[GOAL]
case mk.mk
α : Sort u_1
β : α → Sort u_2
fst✝¹ : α
snd✝¹ : β fst✝¹
fst✝ : α
snd✝ : β fst✝
h₀ : { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst
h₁ : HEq { fst := fst✝¹, snd := snd✝¹ }.snd { fst := fst✝, snd := snd✝ }.snd
⊢ { fst := fst✝¹, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
cases h₀
[GOAL]
case mk.mk.refl
α : Sort u_1
β : α → Sort u_2
fst✝ : α
snd✝¹ snd✝ : β fst✝
h₁ : HEq { fst := fst✝, snd := snd✝¹ }.snd { fst := fst✝, snd := snd✝ }.snd
⊢ { fst := fst✝, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
cases h₁
[GOAL]
case mk.mk.refl.refl
α : Sort u_1
β : α → Sort u_2
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝, snd := snd✝ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
β : α → Sort u_2
x₀ x₁ : PSigma β
⊢ x₀ = x₁ ↔ x₀.fst = x₁.fst ∧ HEq x₀.snd x₁.snd
[PROOFSTEP]
cases x₀
[GOAL]
case mk
α : Sort u_1
β : α → Sort u_2
x₁ : PSigma β
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝, snd := snd✝ } = x₁ ↔
    { fst := fst✝, snd := snd✝ }.fst = x₁.fst ∧ HEq { fst := fst✝, snd := snd✝ }.snd x₁.snd
[PROOFSTEP]
cases x₁
[GOAL]
case mk.mk
α : Sort u_1
β : α → Sort u_2
fst✝¹ : α
snd✝¹ : β fst✝¹
fst✝ : α
snd✝ : β fst✝
⊢ { fst := fst✝¹, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ } ↔
    { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst ∧
      HEq { fst := fst✝¹, snd := snd✝¹ }.snd { fst := fst✝, snd := snd✝ }.snd
[PROOFSTEP]
exact PSigma.mk.inj_iff
