awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
R : Type u_10
V : Type u_11
P : Type u_12
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
p : P
t : Rˣ
⊢ Eq.{u_12 + 1} (α := (a : P) → P) (⇑((homothetyUnitsMulHom p : (a : Rˣ) → P ≃ᵃ[R] P) t : P ≃ᵃ[R] P) : (a : P) → P)
    (⇑(AffineMap.homothety p (↑t : R)) : (a : P) → P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
R : Type u_10
V : Type u_11
P : Type u_12
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
p : P
t : Rˣ
⊢ Eq.{u_12 + 1} (α := (a : P) → P) (⇑(symm ((homothetyUnitsMulHom p : (a : Rˣ) → P ≃ᵃ[R] P) t)) : (a : P) → P)
    (⇑(AffineMap.homothety p (↑t⁻¹ : R)) : (a : P) → P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
R : Type u_10
V : Type u_11
P : Type u_12
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : AffineSpace V P
p : P
⊢ Eq (α := Rˣ → P →ᵃ[R] P) (toAffineMap ∘ (⇑(homothetyUnitsMulHom p) : (a : Rˣ) → P ≃ᵃ[R] P))
    ((⇑(AffineMap.homothetyHom p) : (a : R) → P →ᵃ[R] P) ∘ Units.val)

Tactic:
funext fun _ => rfl

Premises used: funext, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
x y : P₁
⊢ Eq (α := P₁) ((pointReflection k x : (a : P₁) → P₁) y : P₁) ((Equiv.pointReflection x : (a : P₁) → P₁) y : P₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
x y : P₁
⊢ (pointReflection k x : (a : P₁) → P₁) y = (x -ᵥ y) +ᵥ x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
x : P₁
⊢ Eq (α := P₁ ≃ᵃ[k] P₁) (symm (pointReflection k x)) (pointReflection k x)

Tactic:
toEquiv_injective <| Equiv.pointReflection_symm x

Premises used: Equiv.pointReflection_symm, AffineEquiv.toEquiv_injective
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
x : P₁
⊢ toEquiv (pointReflection k x) = Equiv.pointReflection x

Tactic:
rfl

Premises used: Equiv.trans, Equiv.pointReflection, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
x : P₁
⊢ (pointReflection k x : (a : P₁) → P₁) x = x

Tactic:
vsub_vadd _ _

Premises used: vsub_vadd
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
x : P₁
⊢ Involutive.{u_2 + 1} (α := P₁) (⇑(pointReflection k x) : (a : P₁) → P₁)

Tactic:
Equiv.pointReflection_involutive x

Premises used: Equiv.vaddConst, Equiv.pointReflection_involutive, Equiv.constVSub
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
x y : P₁
h : Injective (β := V₁) fun (x : V₁) ↦ HSMul.hSMul (α := ℕ) 2 x
⊢ (pointReflection k x : (a : P₁) → P₁) y = y ↔ y = x

Tactic:
Equiv.pointReflection_fixed_iff_of_injective_two_nsmul h

Premises used: Equiv.pointReflection_fixed_iff_of_injective_two_nsmul
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
h : Injective (β := V₁) fun (x : V₁) ↦ HSMul.hSMul (α := ℕ) 2 x
y : P₁
⊢ Injective (β := P₁) fun (x : P₁) ↦ (pointReflection k x : (a : P₁) → P₁) y

Tactic:
Equiv.injective_pointReflection_left_of_injective_two_nsmul h y

Premises used: Equiv.injective_pointReflection_left_of_injective_two_nsmul
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : Invertible (α := k) 2
x y : V₁
h : HSMul.hSMul (α := ℕ) 2 x = HSMul.hSMul (α := ℕ) 2 y
rwa : ∀ (h : x + x = HSMul.hSMul (α := ℕ) 2 y), x = y
rwa₁ : ∀ (h : x + x = y + y), x = y
rwa₂ : ∀ (h : HSMul.hSMul.{u_1, u_6, u_6} (α := k) 2 x = y + y), x = y
rwa₃ : ∀ (h : HSMul.hSMul.{u_1, u_6, u_6} (α := k) 2 x = HSMul.hSMul.{u_1, u_6, u_6} (α := k) 2 y), x = y
rwa₄ rwa₅ rwa₆ rwa₇ : ∀ (h : x = y), x = y
⊢ x = y

Tactic:
rwa [two_nsmul, two_nsmul, ← two_smul k x, ← two_smul k y,
      (isUnit_of_invertible (2 : k)).smul_left_cancel] at h

Premises used: isUnit_of_invertible, two_smul, IsUnit.smul_left_cancel, OfNat.ofNat, two_nsmul
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
P₁ : Type u_2
V₁ : Type u_6
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : Invertible (α := k) 2
x y : P₁
⊢ (pointReflection k x : (a : P₁) → P₁) y = y ↔ y = x

Tactic:
((injective_pointReflection_left_of_module k y).eq_iff' (pointReflection_self k y)).trans eq_comm

Premises used: Function.Injective.eq_iff', eq_comm, AffineEquiv.injective_pointReflection_left_of_module, Iff.trans, AffineEquiv.pointReflection_self
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_1
V₁ : Type u_6
V₂ : Type u_7
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
e : V₁ ≃ₗ[k] V₂
⊢ Eq (α := (a : V₁) → V₂) (⇑e.toAffineEquiv : (a : V₁) → V₂) (⇑e : (a : V₁) → V₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_10
V : Type u_11
P : Type u_12
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
A : V ≃ₗ[k] V
p₀ p₁ x : P
⊢ (ofLinearEquiv A p₀ p₁ : (a : P) → P) x = HVAdd.hVAdd (α := V) ((A : (a : V) → V) (x -ᵥ p₀) : V) p₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_10
V : Type u_11
P : Type u_12
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
A : V ≃ₗ[k] V
p₀ p₁ : P
⊢ linear (ofLinearEquiv A p₀ p₁) = A

Tactic:
rfl

Premises used: LinearEquiv.trans, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_10
V : Type u_11
P : Type u_12
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p : P
h :
  ∀ (x : P),
    Eq (α := P) ((ofLinearEquiv (LinearEquiv.refl k V) p p : (a : P) → P) x : P) ((refl k P : (a : P) → P) x : P)
⊢ Eq (α := P ≃ᵃ[k] P) (ofLinearEquiv (LinearEquiv.refl k V) p p) (refl k P)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_10
V : Type u_11
P : Type u_12
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
p x : P
⊢ Eq (α := P) ((ofLinearEquiv (LinearEquiv.refl k V) p p : (a : P) → P) x : P) ((refl k P : (a : P) → P) x : P)

Tactic:
simp [ofLinearEquiv_apply]

Premises used: AffineEquiv.ofLinearEquiv_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_10
V : Type u_11
P : Type u_12
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
A B : V ≃ₗ[k] V
p₀ p₁ p₂ : P
h :
  ∀ (x : P),
    Eq (α := P) ((trans (ofLinearEquiv A p₀ p₁) (ofLinearEquiv B p₁ p₂) : (a : P) → P) x : P)
      ((ofLinearEquiv (A ≪≫ₗ B) p₀ p₂ : (a : P) → P) x : P)
⊢ Eq (α := P ≃ᵃ[k] P) (trans (ofLinearEquiv A p₀ p₁) (ofLinearEquiv B p₁ p₂)) (ofLinearEquiv (A ≪≫ₗ B) p₀ p₂)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
k : Type u_10
V : Type u_11
P : Type u_12
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
A B : V ≃ₗ[k] V
p₀ p₁ p₂ x : P
⊢ Eq (α := P) ((trans (ofLinearEquiv A p₀ p₁) (ofLinearEquiv B p₁ p₂) : (a : P) → P) x : P)
    ((ofLinearEquiv (A ≪≫ₗ B) p₀ p₂ : (a : P) → P) x : P)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
e₁ : P₁ ≃ᵃ[k] P₂
e₂ : P₃ ≃ᵃ[k] P₄
x : P₁ →ᵃ[k] P₃
h :
  ∀ (p : P₁),
    Eq.{u_4 + 1} (α := P₃)
      (((fun (f : P₂ →ᵃ[k] P₄) ↦ (↑e₂.symm : P₄ →ᵃ[k] P₃).comp (f.comp (↑e₁ : P₁ →ᵃ[k] P₂)))
              ((fun (f : P₁ →ᵃ[k] P₃) ↦ (↑e₂ : P₃ →ᵃ[k] P₄).comp (f.comp (↑e₁.symm : P₂ →ᵃ[k] P₁))) x) :
            (a : P₁) → P₃)
          p :
        P₃)
      ((x : (a : P₁) → P₃) p : P₃)
⊢ (fun (f : P₂ →ᵃ[k] P₄) ↦ (↑e₂.symm : P₄ →ᵃ[k] P₃).comp (f.comp (↑e₁ : P₁ →ᵃ[k] P₂)))
      ((fun (f : P₁ →ᵃ[k] P₃) ↦ (↑e₂ : P₃ →ᵃ[k] P₄).comp (f.comp (↑e₁.symm : P₂ →ᵃ[k] P₁))) x) =
    x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
e₁ : P₁ ≃ᵃ[k] P₂
e₂ : P₃ ≃ᵃ[k] P₄
x : P₁ →ᵃ[k] P₃
p : P₁
⊢ Eq.{u_4 + 1} (α := P₃)
    (((fun (f : P₂ →ᵃ[k] P₄) ↦ (↑e₂.symm : P₄ →ᵃ[k] P₃).comp (f.comp (↑e₁ : P₁ →ᵃ[k] P₂)))
            ((fun (f : P₁ →ᵃ[k] P₃) ↦ (↑e₂ : P₃ →ᵃ[k] P₄).comp (f.comp (↑e₁.symm : P₂ →ᵃ[k] P₁))) x) :
          (a : P₁) → P₃)
        p :
      P₃)
    ((x : (a : P₁) → P₃) p : P₃)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
e₁ : P₁ ≃ᵃ[k] P₂
e₂ : P₃ ≃ᵃ[k] P₄
x : P₂ →ᵃ[k] P₄
h :
  ∀ (p : P₂),
    Eq.{u_5 + 1} (α := P₄)
      (((fun (f : P₁ →ᵃ[k] P₃) ↦ (↑e₂ : P₃ →ᵃ[k] P₄).comp (f.comp (↑e₁.symm : P₂ →ᵃ[k] P₁)))
              ((fun (f : P₂ →ᵃ[k] P₄) ↦ (↑e₂.symm : P₄ →ᵃ[k] P₃).comp (f.comp (↑e₁ : P₁ →ᵃ[k] P₂))) x) :
            (a : P₂) → P₄)
          p :
        P₄)
      ((x : (a : P₂) → P₄) p : P₄)
⊢ (fun (f : P₁ →ᵃ[k] P₃) ↦ (↑e₂ : P₃ →ᵃ[k] P₄).comp (f.comp (↑e₁.symm : P₂ →ᵃ[k] P₁)))
      ((fun (f : P₂ →ᵃ[k] P₄) ↦ (↑e₂.symm : P₄ →ᵃ[k] P₃).comp (f.comp (↑e₁ : P₁ →ᵃ[k] P₂))) x) =
    x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
e₁ : P₁ ≃ᵃ[k] P₂
e₂ : P₃ ≃ᵃ[k] P₄
x : P₂ →ᵃ[k] P₄
p : P₂
⊢ Eq.{u_5 + 1} (α := P₄)
    (((fun (f : P₁ →ᵃ[k] P₃) ↦ (↑e₂ : P₃ →ᵃ[k] P₄).comp (f.comp (↑e₁.symm : P₂ →ᵃ[k] P₁)))
            ((fun (f : P₂ →ᵃ[k] P₄) ↦ (↑e₂.symm : P₄ →ᵃ[k] P₃).comp (f.comp (↑e₁ : P₁ →ᵃ[k] P₂))) x) :
          (a : P₂) → P₄)
        p :
      P₄)
    ((x : (a : P₂) → P₄) p : P₄)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
e₁ : P₁ ≃ᵃ[k] P₂
e₂ : P₃ ≃ᵃ[k] P₄
f : P₁ →ᵃ[k] P₃
x : P₂
⊢ Eq.{u_5 + 1} (α := P₄)
    ((((e₁.arrowCongrEquiv e₂ : (a : P₁ →ᵃ[k] P₃) → P₂ →ᵃ[k] P₄) f : P₂ →ᵃ[k] P₄) : (a : P₂) → P₄) x : P₄)
    ((e₂ : (a : P₃) → P₄) ((f : (a : P₁) → P₃) ((e₁.symm : (a : P₂) → P₁) x : P₁) : P₃) : P₄)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
e₁ : P₁ ≃ᵃ[k] P₂
e₂ : P₃ ≃ᵃ[k] P₄
f : P₂ →ᵃ[k] P₄
x : P₁
⊢ Eq.{u_4 + 1} (α := P₃)
    (((((e₁.arrowCongrEquiv e₂).symm : (a : P₂ →ᵃ[k] P₄) → P₁ →ᵃ[k] P₃) f : P₁ →ᵃ[k] P₃) : (a : P₁) → P₃) x : P₃)
    ((e₂.symm : (a : P₄) → P₃) ((f : (a : P₂) → P₄) ((e₁ : (a : P₁) → P₂) x : P₂) : P₄) : P₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
R : Type u_10
inst_13 : CommRing R
inst_14 : Module R V₁
inst_15 : Module R V₂
inst_16 : Module R V₃
inst_17 : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : V₃ ≃ₗ[R] V₄
x x_1 : P₁ →ᵃ[R] V₃
h :
  ∀ (p : P₂),
    Eq.{u_9 + 1} (α := V₄) (((e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun (x + x_1) : (a : P₂) → V₄) p : V₄)
      (((e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x + (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x_1 : (a : P₂) → V₄)
          p :
        V₄)
⊢ (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun (x + x_1) =
    (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x + (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x_1

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
R : Type u_10
inst_13 : CommRing R
inst_14 : Module R V₁
inst_15 : Module R V₂
inst_16 : Module R V₃
inst_17 : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : V₃ ≃ₗ[R] V₄
x x_1 : P₁ →ᵃ[R] V₃
p : P₂
⊢ Eq.{u_9 + 1} (α := V₄) (((e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun (x + x_1) : (a : P₂) → V₄) p : V₄)
    (((e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x + (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x_1 : (a : P₂) → V₄)
        p :
      V₄)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
R : Type u_10
inst_13 : CommRing R
inst_14 : Module R V₁
inst_15 : Module R V₂
inst_16 : Module R V₃
inst_17 : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : V₃ ≃ₗ[R] V₄
x : R
x_1 : P₁ →ᵃ[R] V₃
h :
  ∀ (p : P₂),
    Eq.{u_9 + 1} (α := V₄) (((e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun (x • x_1) : (a : P₂) → V₄) p : V₄)
      ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) ((e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x_1) :
            (a : P₂) → V₄)
          p :
        V₄)
⊢ (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun (x • x_1) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) ((e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x_1)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
R : Type u_10
inst_13 : CommRing R
inst_14 : Module R V₁
inst_15 : Module R V₂
inst_16 : Module R V₃
inst_17 : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : V₃ ≃ₗ[R] V₄
x : R
x_1 : P₁ →ᵃ[R] V₃
p : P₂
⊢ Eq.{u_9 + 1} (α := V₄) (((e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun (x • x_1) : (a : P₂) → V₄) p : V₄)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) ((e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x_1) :
          (a : P₂) → V₄)
        p :
      V₄)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst : AddCommGroup V₁
inst_1 : AddCommGroup V₂
inst_2 : AddCommGroup V₃
inst_3 : AddCommGroup V₄
inst_4 : AffineSpace V₁ P₁
inst_5 : AffineSpace V₂ P₂
R : Type u_10
inst_6 : CommRing R
inst_7 : Module R V₁
inst_8 : Module R V₂
inst_9 : Module R V₃
inst_10 : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : V₃ ≃ₗ[R] V₄
f : P₁ →ᵃ[R] V₃
x : P₂
⊢ Eq.{u_9 + 1} (α := V₄)
    ((((e₁.arrowCongrₗ e₂ : (a : P₁ →ᵃ[R] V₃) → P₂ →ᵃ[R] V₄) f : P₂ →ᵃ[R] V₄) : (a : P₂) → V₄) x : V₄)
    ((e₂ : (a : V₃) → V₄) ((f : (a : P₁) → V₃) ((e₁.symm : (a : P₂) → P₁) x : P₁) : V₃) : V₄)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
P₁ : Type u_2
P₂ : Type u_3
V₁ : Type u_6
V₂ : Type u_7
V₃ : Type u_8
V₄ : Type u_9
inst : AddCommGroup V₁
inst_1 : AddCommGroup V₂
inst_2 : AddCommGroup V₃
inst_3 : AddCommGroup V₄
inst_4 : AffineSpace V₁ P₁
inst_5 : AffineSpace V₂ P₂
R : Type u_10
inst_6 : CommRing R
inst_7 : Module R V₁
inst_8 : Module R V₂
inst_9 : Module R V₃
inst_10 : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : V₃ ≃ₗ[R] V₄
f : P₂ →ᵃ[R] V₄
x : P₁
⊢ Eq.{u_8 + 1} (α := V₃)
    (((((e₁.arrowCongrₗ e₂).symm : (a : P₂ →ᵃ[R] V₄) → P₁ →ᵃ[R] V₃) f : P₁ →ᵃ[R] V₃) : (a : P₁) → V₃) x : V₃)
    ((e₂.symm : (a : V₄) → V₃) ((f : (a : P₂) → V₄) ((e₁ : (a : P₁) → P₂) x : P₂) : V₄) : V₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
R : Type u_10
inst_13 : CommRing R
inst_14 : Module R V₁
inst_15 : Module R V₂
inst_16 : Module R V₃
inst_17 : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : P₃ ≃ᵃ[R] P₄
x : P₁ →ᵃ[R] P₃
x_1 : P₁ →ᵃ[R] V₃
h :
  ∀ (p : P₂),
    Eq.{u_5 + 1} (α := P₄)
      ((((e₁.arrowCongrEquiv e₂ : (a : P₁ →ᵃ[R] P₃) → P₂ →ᵃ[R] P₄) (x_1 +ᵥ x) : P₂ →ᵃ[R] P₄) : (a : P₂) → P₄) p : P₄)
      ((HVAdd.hVAdd (α := P₂ →ᵃ[R] V₄) (β := P₂ →ᵃ[R] P₄)
              ((e₁.arrowCongrₗ e₂.linear : (a : P₁ →ᵃ[R] V₃) → P₂ →ᵃ[R] V₄) x_1 : P₂ →ᵃ[R] V₄)
              ((e₁.arrowCongrEquiv e₂ : (a : P₁ →ᵃ[R] P₃) → P₂ →ᵃ[R] P₄) x : P₂ →ᵃ[R] P₄) :
            (a : P₂) → P₄)
          p :
        P₄)
⊢ (e₁.arrowCongrEquiv e₂ : (a : P₁ →ᵃ[R] P₃) → P₂ →ᵃ[R] P₄) (x_1 +ᵥ x) =
    HVAdd.hVAdd (α := P₂ →ᵃ[R] V₄) (β := P₂ →ᵃ[R] P₄)
      ((e₁.arrowCongrₗ e₂.linear : (a : P₁ →ᵃ[R] V₃) → P₂ →ᵃ[R] V₄) x_1 : P₂ →ᵃ[R] V₄)
      ((e₁.arrowCongrEquiv e₂ : (a : P₁ →ᵃ[R] P₃) → P₂ →ᵃ[R] P₄) x : P₂ →ᵃ[R] P₄)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
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_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : AddCommGroup V₃
inst_4 : AddCommGroup V₄
inst_5 : Module k V₁
inst_6 : Module k V₂
inst_7 : Module k V₃
inst_8 : Module k V₄
inst_9 : AffineSpace V₁ P₁
inst_10 : AffineSpace V₂ P₂
inst_11 : AffineSpace V₃ P₃
inst_12 : AffineSpace V₄ P₄
R : Type u_10
inst_13 : CommRing R
inst_14 : Module R V₁
inst_15 : Module R V₂
inst_16 : Module R V₃
inst_17 : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : P₃ ≃ᵃ[R] P₄
x : P₁ →ᵃ[R] P₃
x_1 : P₁ →ᵃ[R] V₃
p : P₂
⊢ Eq.{u_5 + 1} (α := P₄)
    ((((e₁.arrowCongrEquiv e₂ : (a : P₁ →ᵃ[R] P₃) → P₂ →ᵃ[R] P₄) (x_1 +ᵥ x) : P₂ →ᵃ[R] P₄) : (a : P₂) → P₄) p : P₄)
    ((HVAdd.hVAdd (α := P₂ →ᵃ[R] V₄) (β := P₂ →ᵃ[R] P₄)
            ((e₁.arrowCongrₗ e₂.linear : (a : P₁ →ᵃ[R] V₃) → P₂ →ᵃ[R] V₄) x_1 : P₂ →ᵃ[R] V₄)
            ((e₁.arrowCongrEquiv e₂ : (a : P₁ →ᵃ[R] P₃) → P₂ →ᵃ[R] P₄) x : P₂ →ᵃ[R] P₄) :
          (a : P₂) → P₄)
        p :
      P₄)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
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 : AddCommGroup V₁
inst_1 : AddCommGroup V₂
inst_2 : AddCommGroup V₃
inst_3 : AddCommGroup V₄
inst_4 : AffineSpace V₁ P₁
inst_5 : AffineSpace V₂ P₂
inst_6 : AffineSpace V₃ P₃
inst_7 : AffineSpace V₄ P₄
R : Type u_10
inst_8 : CommRing R
inst_9 : Module R V₁
inst_10 : Module R V₂
inst_11 : Module R V₃
inst_12 : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : P₃ ≃ᵃ[R] P₄
f : P₁ →ᵃ[R] P₃
x : P₂
⊢ Eq.{u_5 + 1} (α := P₄)
    ((((e₁.arrowCongr e₂ : (a : P₁ →ᵃ[R] P₃) → P₂ →ᵃ[R] P₄) f : P₂ →ᵃ[R] P₄) : (a : P₂) → P₄) x : P₄)
    ((e₂ : (a : P₃) → P₄) ((f : (a : P₁) → P₃) ((e₁.symm : (a : P₂) → P₁) x : P₁) : P₃) : P₄)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
Goal:
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 : AddCommGroup V₁
inst_1 : AddCommGroup V₂
inst_2 : AddCommGroup V₃
inst_3 : AddCommGroup V₄
inst_4 : AffineSpace V₁ P₁
inst_5 : AffineSpace V₂ P₂
inst_6 : AffineSpace V₃ P₃
inst_7 : AffineSpace V₄ P₄
R : Type u_10
inst_8 : CommRing R
inst_9 : Module R V₁
inst_10 : Module R V₂
inst_11 : Module R V₃
inst_12 : Module R V₄
e₁ : P₁ ≃ᵃ[R] P₂
e₂ : P₃ ≃ᵃ[R] P₄
f : P₂ →ᵃ[R] P₄
x : P₁
⊢ Eq.{u_4 + 1} (α := P₃)
    (((((e₁.arrowCongr e₂).symm : (a : P₂ →ᵃ[R] P₄) → P₁ →ᵃ[R] P₃) f : P₁ →ᵃ[R] P₃) : (a : P₁) → P₃) x : P₃)
    ((e₂.symm : (a : P₄) → P₃) ((f : (a : P₂) → P₄) ((e₁ : (a : P₁) → P₂) x : P₂) : P₄) : P₃)

Tactic:
rfl

Premises used: rfl