α : Type ?u.6398
α₁ : Type u_1
α₂ : Type u_2
β : α → Type ?u.6409
β₁ : α₁ → Type u_3
β₂ : α₂ → Type u_4
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 }
α : Type ?u.6398
α₁ : Type u_1
α₂ : Type u_2
β : α → Type ?u.6409
β₁ : α₁ → Type u_3
β₂ : α₂ → Type u_4
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 }
obtain rfl : i = j := h₁ (Sigma.mk.inj_iff.mp h).1
α : Type ?u.6398
α₁ : Type u_1
α₂ : Type u_2
β : α → Type ?u.6409
β₁ : α₁ → Type u_3
β₂ : α₂ → Type u_4
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 }
α : Type ?u.6398
α₁ : Type u_1
α₂ : Type u_2
β : α → Type ?u.6409
β₁ : α₁ → Type u_3
β₂ : α₂ → Type u_4
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 }
obtain rfl : x = y := h₂ i (sigma_mk_injective h)
no goals
α : Type ?u.6398
α₁ : Type u_1
α₂ : Type u_2
β : α → Type ?u.6409
β₁ : α₁ → Type u_3
β₂ : α₂ → Type u_4
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 }
rfl