[GOAL]
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
inst✝⁵ : AddCommGroup V₃
inst✝⁴ : Module k V₃
inst✝³ : AffineSpace V₃ P₃
inst✝² : AddCommGroup V₄
inst✝¹ : Module k V₄
inst✝ : AffineSpace V₄ P₄
⊢ Injective toAffineMap
[PROOFSTEP]
rintro ⟨e, el, h⟩ ⟨e', el', h'⟩ H
[GOAL]
case mk.mk
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
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' }
[PROOFSTEP]
simp only [(toAffineMap_mk), (AffineMap.mk.injEq), Equiv.coe_inj, LinearEquiv.toLinearMap_inj] at H
[GOAL]
case mk.mk
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
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' }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toEquiv
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
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
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
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'
[PROOFSTEP]
exacts [H.1, H.2]
[GOAL]
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
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₂
e' : V₁ ≃ₗ[k] V₂
p : P₁
h : ∀ (p' : P₁), e p' = ↑e' (p' -ᵥ p) +ᵥ e p
p' : P₁
⊢ (fun q' => ↑(LinearEquiv.symm e') (q' -ᵥ e p) +ᵥ p) (e p') = p'
[PROOFSTEP]
simp [h p', (vadd_vsub), (vsub_vadd)]
  -- Porting note: `simp` needs `()`
[GOAL]
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
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₂
e' : V₁ ≃ₗ[k] V₂
p : P₁
h : ∀ (p' : P₁), e p' = ↑e' (p' -ᵥ p) +ᵥ e p
q' : P₂
⊢ e ((fun q' => ↑(LinearEquiv.symm e') (q' -ᵥ e p) +ᵥ p) q') = q'
[PROOFSTEP]
simp [h (e'.symm (q' -ᵥ e p) +ᵥ p), (vadd_vsub), (vsub_vadd)]
[GOAL]
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
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₂
e' : V₁ ≃ₗ[k] V₂
p : P₁
h : ∀ (p' : P₁), e p' = ↑e' (p' -ᵥ p) +ᵥ e p
p' : P₁
v : V₁
⊢ ↑{ toFun := e, invFun := fun q' => ↑(LinearEquiv.symm e') (q' -ᵥ e p) +ᵥ p,
          left_inv := (_ : ∀ (p' : P₁), ↑(LinearEquiv.symm e') (e p' -ᵥ e p) +ᵥ p = p'),
          right_inv := (_ : ∀ (q' : P₂), e (↑(LinearEquiv.symm e') (q' -ᵥ e p) +ᵥ p) = q') }
      (v +ᵥ p') =
    ↑e' v +ᵥ
      ↑{ toFun := e, invFun := fun q' => ↑(LinearEquiv.symm e') (q' -ᵥ e p) +ᵥ p,
            left_inv := (_ : ∀ (p' : P₁), ↑(LinearEquiv.symm e') (e p' -ᵥ e p) +ᵥ p = p'),
            right_inv := (_ : ∀ (q' : P₂), e (↑(LinearEquiv.symm e') (q' -ᵥ e p) +ᵥ p) = q') }
        p'
[PROOFSTEP]
simp [h p', h (v +ᵥ p'), (vadd_vsub_assoc), (vadd_vadd)]
[GOAL]
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
inst✝⁵ : AddCommGroup V₃
inst✝⁴ : Module k V₃
inst✝³ : AffineSpace V₃ P₃
inst✝² : AddCommGroup V₄
inst✝¹ : Module k V₄
inst✝ : AffineSpace V₄ P₄
e : P₁ ≃ᵃ[k] P₂
p : P₂
v : V₂
⊢ v +ᵥ p = ↑e.symm.symm (↑(LinearEquiv.symm e.linear) v +ᵥ ↑e.symm p)
[PROOFSTEP]
rw [Equiv.symm_symm, e.map_vadd' ((Equiv.symm e.toEquiv) p) ((LinearEquiv.symm e.linear) v),
  LinearEquiv.apply_symm_apply, Equiv.apply_symm_apply]
[GOAL]
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
inst✝⁵ : AddCommGroup V₃
inst✝⁴ : Module k V₃
inst✝³ : AffineSpace V₃ P₃
inst✝² : AddCommGroup V₄
inst✝¹ : Module k V₄
inst✝ : AffineSpace V₄ P₄
e : P₁ ≃ᵃ[k] P₂
e' : P₂ ≃ᵃ[k] P₃
p : P₁
v : V₁
⊢ ↑(e.trans e'.toEquiv) (v +ᵥ p) = ↑(LinearEquiv.trans e.linear e'.linear) v +ᵥ ↑(e.trans e'.toEquiv) p
[PROOFSTEP]
simp only [LinearEquiv.trans_apply, (coe_toEquiv), (· ∘ ·), Equiv.coe_trans, (map_vadd)]
[GOAL]
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
inst✝⁵ : AddCommGroup V₃
inst✝⁴ : Module k V₃
inst✝³ : AffineSpace V₃ P₃
inst✝² : AddCommGroup V₄
inst✝¹ : Module k V₄
inst✝ : AffineSpace V₄ P₄
p p' : P₁
v : V₁
⊢ ↑(Equiv.constVSub p) (v +ᵥ p') = ↑(LinearEquiv.neg k) v +ᵥ ↑(Equiv.constVSub p) p'
[PROOFSTEP]
simp [(Equiv.coe_constVSub), (vsub_vadd_eq_vsub_sub), neg_add_eq_sub]
[GOAL]
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
inst✝⁶ : AddCommGroup V₃
inst✝⁵ : Module k V₃
inst✝⁴ : AffineSpace V₃ P₃
inst✝³ : AddCommGroup V₄
inst✝² : Module k V₄
inst✝¹ : AffineSpace V₄ P₄
inst✝ : Invertible 2
x y : V₁
h : bit0 x = bit0 y
⊢ x = y
[PROOFSTEP]
rwa [bit0, bit0, ← two_smul k x, ← two_smul k y, (isUnit_of_invertible (2 : k)).smul_left_cancel] at h
[GOAL]
k : Type u_1
P₁ : Type u_2
P₂ : Type u_3
P₃ : Type u_4
P₄ : Type u_5
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
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₂
inst✝⁷ : AddCommGroup V₃
inst✝⁶ : Module k V₃
inst✝⁵ : AffineSpace V₃ P₃
inst✝⁴ : AddCommGroup V₄
inst✝³ : Module k V₄
inst✝² : AffineSpace V₄ P₄
R' : Type u_10
inst✝¹ : CommRing R'
inst✝ : Module R' V₁
c p : P₁
⊢ ↑(homothety c (-1)) p = ↑(pointReflection R' c) p
[PROOFSTEP]
simp [(homothety_apply), pointReflection_apply _, (neg_vsub_eq_vsub_rev)]