-- Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean
theorem toAffineMap_injective : Injective (toAffineMap : (P₁ ≃ᵃ[k] P₂) → P₁ →ᵃ[k] P₂)

Proof state:
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
⊢ Injective toAffineMap

Tactic:
rintro ⟨e, el, h⟩ ⟨e', el', h'⟩ H

Result:
case mk.mk
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
e : P₁ ≃ P₂
el : V₁ ≃ₗ[k] V₂
h : ∀ (p : P₁) (v : V₁), e (v +ᵥ p) = el v +ᵥ e p
e' : P₁ ≃ P₂
el' : V₁ ≃ₗ[k] V₂
h' : ∀ (p : P₁) (v : V₁), e' (v +ᵥ p) = el' v +ᵥ e' p
H : ↑{ toEquiv := e, linear := el, map_vadd' := h } = ↑{ toEquiv := e', linear := el', map_vadd' := h' }
⊢ { toEquiv := e, linear := el, map_vadd' := h } = { toEquiv := e', linear := el', map_vadd' := h' }

Proof state:
case mk.mk.e_toEquiv
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
e : P₁ ≃ P₂
el : V₁ ≃ₗ[k] V₂
h : ∀ (p : P₁) (v : V₁), e (v +ᵥ p) = el v +ᵥ e p
e' : P₁ ≃ P₂
el' : V₁ ≃ₗ[k] V₂
h' : ∀ (p : P₁) (v : V₁), e' (v +ᵥ p) = el' v +ᵥ e' p
H : e = e' ∧ el = el'
⊢ e = e'

case mk.mk.e_linear
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
e : P₁ ≃ P₂
el : V₁ ≃ₗ[k] V₂
h : ∀ (p : P₁) (v : V₁), e (v +ᵥ p) = el v +ᵥ e p
e' : P₁ ≃ P₂
el' : V₁ ≃ₗ[k] V₂
h' : ∀ (p : P₁) (v : V₁), e' (v +ᵥ p) = el' v +ᵥ e' p
H : e = e' ∧ el = el'
⊢ el = el'

Tactic:
exacts [H.1, H.2]

Result:
no goals

Proof state:
case mk.mk
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
e : P₁ ≃ P₂
el : V₁ ≃ₗ[k] V₂
h : ∀ (p : P₁) (v : V₁), e (v +ᵥ p) = el v +ᵥ e p
e' : P₁ ≃ P₂
el' : V₁ ≃ₗ[k] V₂
h' : ∀ (p : P₁) (v : V₁), e' (v +ᵥ p) = el' v +ᵥ e' p
H : ↑{ toEquiv := e, linear := el, map_vadd' := h } = ↑{ toEquiv := e', linear := el', map_vadd' := h' }
⊢ { toEquiv := e, linear := el, map_vadd' := h } = { toEquiv := e', linear := el', map_vadd' := h' }

Tactic:
simp only [toAffineMap_mk, AffineMap.mk.injEq, Equiv.coe_inj,
  LinearEquiv.toLinearMap_inj] at H

Result:
case mk.mk
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
e : P₁ ≃ P₂
el : V₁ ≃ₗ[k] V₂
h : ∀ (p : P₁) (v : V₁), e (v +ᵥ p) = el v +ᵥ e p
e' : P₁ ≃ P₂
el' : V₁ ≃ₗ[k] V₂
h' : ∀ (p : P₁) (v : V₁), e' (v +ᵥ p) = el' v +ᵥ e' p
H : e = e' ∧ el = el'
⊢ { toEquiv := e, linear := el, map_vadd' := h } = { toEquiv := e', linear := el', map_vadd' := h' }

Proof state:
case mk.mk
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
e : P₁ ≃ P₂
el : V₁ ≃ₗ[k] V₂
h : ∀ (p : P₁) (v : V₁), e (v +ᵥ p) = el v +ᵥ e p
e' : P₁ ≃ P₂
el' : V₁ ≃ₗ[k] V₂
h' : ∀ (p : P₁) (v : V₁), e' (v +ᵥ p) = el' v +ᵥ e' p
H : e = e' ∧ el = el'
⊢ { toEquiv := e, linear := el, map_vadd' := h } = { toEquiv := e', linear := el', map_vadd' := h' }

Tactic:
congr

Result:
case mk.mk.e_toEquiv
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
e : P₁ ≃ P₂
el : V₁ ≃ₗ[k] V₂
h : ∀ (p : P₁) (v : V₁), e (v +ᵥ p) = el v +ᵥ e p
e' : P₁ ≃ P₂
el' : V₁ ≃ₗ[k] V₂
h' : ∀ (p : P₁) (v : V₁), e' (v +ᵥ p) = el' v +ᵥ e' p
H : e = e' ∧ el = el'
⊢ e = e'

case mk.mk.e_linear
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module k V₁
inst✝³ : AffineSpace V₁ P₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module k V₂
inst✝ : AffineSpace V₂ P₂
e : P₁ ≃ P₂
el : V₁ ≃ₗ[k] V₂
h : ∀ (p : P₁) (v : V₁), e (v +ᵥ p) = el v +ᵥ e p
e' : P₁ ≃ P₂
el' : V₁ ≃ₗ[k] V₂
h' : ∀ (p : P₁) (v : V₁), e' (v +ᵥ p) = el' v +ᵥ e' p
H : e = e' ∧ el = el'
⊢ el = el'