awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Lean.Meta.CongrTheorems (hypothesis)
Goal:
α β : Sort u
inst : FastSubsingleton α
h₂ : α = β
a : α
b : β
⊢ a ≍ b
have this : Subsingleton α
Tactic: have : Subsingleton α := FastSubsingleton.inst
-- Lean 4 proof step from Mathlib.Lean.Thunk (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
a b : Thunk α
x : a = b
⊢ a.get = b.get
have rw : b.get = b.get
Tactic: rw [x]
-- Lean 4 proof step from Mathlib.Lean.Thunk (hypothesis)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
a b : Thunk α
⊢ Decidable (a = b)
have this : a = b ↔ a.get = b.get
Tactic: have : a = b ↔ a.get = b.get := ⟨by intro x; rw [x], by intro; ext; assumption⟩
-- Lean 4 proof step from Mathlib.Lean.Thunk (goal)
Goal:
α : Type u
β : Type v
inst : DecidableEq α
a b : Thunk α
this : a = b ↔ a.get = b.get
⊢ Decidable (a = b)
have rw : Decidable (a.get = b.get)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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₂
p : P₂
v : V₂
⊢ v +ᵥ p =
    (e.symm.symm : (a : P₁) → P₂)
      (HVAdd.hVAdd.{u_6, u_2, u_2} (α := V₁) (β := P₁) ((e.linear.symm : (a : V₂) → V₁) v : V₁)
        ((e.symm : (a : P₂) → P₁) p : P₁))
have rw : v +ᵥ p =
  (e.toEquiv : (a : P₁) → P₂)
    (HVAdd.hVAdd.{u_6, u_2, u_2} (α := V₁) (β := P₁) ((e.linear.symm : (a : V₂) → V₁) v : V₁)
      ((e.symm : (a : P₂) → P₁) p : P₁))
Tactic: 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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₂
p : P₂
v : V₂
rw :
  v +ᵥ p =
    (e.toEquiv : (a : P₁) → P₂)
      (HVAdd.hVAdd.{u_6, u_2, u_2} (α := V₁) (β := P₁) ((e.linear.symm : (a : V₂) → V₁) v : V₁)
        ((e.symm : (a : P₂) → P₁) p : P₁))
⊢ v +ᵥ p =
    (e.symm.symm : (a : P₁) → P₂)
      (HVAdd.hVAdd.{u_6, u_2, u_2} (α := V₁) (β := P₁) ((e.linear.symm : (a : V₂) → V₁) v : V₁)
        ((e.symm : (a : P₂) → P₁) p : P₁))
have rw₁ : v +ᵥ p =
  HVAdd.hVAdd.{u_7, u_3, u_3} (α := V₂) (β := P₂)
    ((e.linear : (a : V₁) → V₂) ((e.linear.symm : (a : V₂) → V₁) v : V₁) : V₂)
    ((e.toEquiv : (a : P₁) → P₂) ((e.symm : (a : P₂) → P₁) p : P₁) : P₂)
Tactic: 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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₂
p : P₂
v : V₂
rw :
  v +ᵥ p =
    (e.toEquiv : (a : P₁) → P₂)
      (HVAdd.hVAdd.{u_6, u_2, u_2} (α := V₁) (β := P₁) ((e.linear.symm : (a : V₂) → V₁) v : V₁)
        ((e.symm : (a : P₂) → P₁) p : P₁))
rw₁ :
  v +ᵥ p =
    HVAdd.hVAdd.{u_7, u_3, u_3} (α := V₂) (β := P₂)
      ((e.linear : (a : V₁) → V₂) ((e.linear.symm : (a : V₂) → V₁) v : V₁) : V₂)
      ((e.toEquiv : (a : P₁) → P₂) ((e.symm : (a : P₂) → P₁) p : P₁) : P₂)
⊢ v +ᵥ p =
    (e.symm.symm : (a : P₁) → P₂)
      (HVAdd.hVAdd.{u_6, u_2, u_2} (α := V₁) (β := P₁) ((e.linear.symm : (a : V₂) → V₁) v : V₁)
        ((e.symm : (a : P₂) → P₁) p : P₁))
have rw₂ : v +ᵥ p = HVAdd.hVAdd (β := P₂) v ((e.toEquiv : (a : P₁) → P₂) ((e.symm : (a : P₂) → P₁) p : P₁) : P₂)
Tactic: 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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₂
p : P₂
v : V₂
rw :
  v +ᵥ p =
    (e.toEquiv : (a : P₁) → P₂)
      (HVAdd.hVAdd.{u_6, u_2, u_2} (α := V₁) (β := P₁) ((e.linear.symm : (a : V₂) → V₁) v : V₁)
        ((e.symm : (a : P₂) → P₁) p : P₁))
rw₁ :
  v +ᵥ p =
    HVAdd.hVAdd.{u_7, u_3, u_3} (α := V₂) (β := P₂)
      ((e.linear : (a : V₁) → V₂) ((e.linear.symm : (a : V₂) → V₁) v : V₁) : V₂)
      ((e.toEquiv : (a : P₁) → P₂) ((e.symm : (a : P₂) → P₁) p : P₁) : P₂)
rw₂ : v +ᵥ p = HVAdd.hVAdd (β := P₂) v ((e.toEquiv : (a : P₁) → P₂) ((e.symm : (a : P₂) → P₁) p : P₁) : P₂)
⊢ v +ᵥ p =
    (e.symm.symm : (a : P₁) → P₂)
      (HVAdd.hVAdd.{u_6, u_2, u_2} (α := V₁) (β := P₁) ((e.linear.symm : (a : V₂) → V₁) v : V₁)
        ((e.symm : (a : P₂) → P₁) p : P₁))
have rw₃ : v +ᵥ p = v +ᵥ p
Tactic: 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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
⊢ x = y
have rwa : ∀ (h : x + x = HSMul.hSMul (α := ℕ) 2 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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
⊢ x = y
have rwa₁ : ∀ (h : x + x = y + 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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
⊢ x = y
have rwa₂ : ∀ (h : HSMul.hSMul.{u_1, u_6, u_6} (α := k) 2 x = y + 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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
⊢ x = y
have 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
Tactic: rwa [two_nsmul, two_nsmul, ← two_smul k x, ← two_smul k y,
      (isUnit_of_invertible (2 : k)).smul_left_cancel] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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
⊢ x = y
have rwa₄ : ∀ (h : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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
⊢ Eq (α := P ≃ᵃ[k] P) (ofLinearEquiv (LinearEquiv.refl k V) p p) (refl k P)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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
⊢ Eq (α := P ≃ᵃ[k] P) (trans (ofLinearEquiv A p₀ p₁) (ofLinearEquiv B p₁ p₂)) (ofLinearEquiv (A ≪≫ₗ B) p₀ p₂)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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₃
⊢ (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
have 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₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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₄
⊢ (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
have 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₄)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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₃
⊢ (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun (x + x_1) =
    (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x + (e₁.arrowCongrEquiv e₂.toAffineEquiv).toFun x_1
have 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₄)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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₃
⊢ (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)
have 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₄)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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₃
⊢ (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₄)
have 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₄)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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
W : Type u_11
inst_13 : Ring R
inst_14 : AddCommGroup W
inst_15 : Module k W
inst_16 : Module R W
inst_17 : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
x x_1 : P₁ →ᵃ[k] W
⊢ Equiv.toFun (e.arrowCongrEquiv (refl k W)) (x + x_1) =
    Equiv.toFun (e.arrowCongrEquiv (refl k W)) x + Equiv.toFun (e.arrowCongrEquiv (refl k W)) x_1
have h : ∀ (p : P₂),
  Eq.{u_11 + 1} (α := W) ((Equiv.toFun (e.arrowCongrEquiv (refl k W)) (x + x_1) : (a : P₂) → W) p : W)
    ((Equiv.toFun (e.arrowCongrEquiv (refl k W)) x + Equiv.toFun (e.arrowCongrEquiv (refl k W)) x_1 : (a : P₂) → W) p :
      W)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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
W : Type u_11
inst_13 : Ring R
inst_14 : AddCommGroup W
inst_15 : Module k W
inst_16 : Module R W
inst_17 : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
x : R
x_1 : P₁ →ᵃ[k] W
⊢ Equiv.toFun (e.arrowCongrEquiv (refl k W)) (x • x_1) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (Equiv.toFun (e.arrowCongrEquiv (refl k W)) x_1)
have h : ∀ (p : P₂),
  Eq.{u_11 + 1} (α := W) ((Equiv.toFun (e.arrowCongrEquiv (refl k W)) (x • x_1) : (a : P₂) → W) p : W)
    ((HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) (Equiv.toFun (e.arrowCongrEquiv (refl k W)) x_1) :
          (a : P₂) → W)
        p :
      W)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineEquiv (goal)
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
W : Type u_11
inst_13 : Ring R
inst_14 : AddCommGroup W
inst_15 : Module k W
inst_16 : Module R W
inst_17 : SMulCommClass k R W
e : P₁ ≃ᵃ[k] P₂
Q : Type u_12
inst_18 : AffineSpace W Q
x : P₁ →ᵃ[k] Q
x_1 : P₁ →ᵃ[k] W
⊢ (e.arrowCongrEquiv (refl k Q) : (a : P₁ →ᵃ[k] Q) → P₂ →ᵃ[k] Q) (x_1 +ᵥ x) =
    HVAdd.hVAdd (α := P₂ →ᵃ[k] W) (β := P₂ →ᵃ[k] Q)
      ((congrLeftₗ R W e : (a : P₁ →ᵃ[k] W) → P₂ →ᵃ[k] W) x_1 : P₂ →ᵃ[k] W)
      ((e.arrowCongrEquiv (refl k Q) : (a : P₁ →ᵃ[k] Q) → P₂ →ᵃ[k] Q) x : P₂ →ᵃ[k] Q)
have h : ∀ (p : P₂),
  Eq.{u_12 + 1} (α := Q)
    ((((e.arrowCongrEquiv (refl k Q) : (a : P₁ →ᵃ[k] Q) → P₂ →ᵃ[k] Q) (x_1 +ᵥ x) : P₂ →ᵃ[k] Q) : (a : P₂) → Q) p : Q)
    ((HVAdd.hVAdd (α := P₂ →ᵃ[k] W) (β := P₂ →ᵃ[k] Q)
            ((congrLeftₗ R W e : (a : P₁ →ᵃ[k] W) → P₂ →ᵃ[k] W) x_1 : P₂ →ᵃ[k] W)
            ((e.arrowCongrEquiv (refl k Q) : (a : P₁ →ᵃ[k] Q) → P₂ →ᵃ[k] Q) x : P₂ →ᵃ[k] Q) :
          (a : P₂) → Q)
        p :
      Q)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
x x_1 : P1 →ᵃ[k] P2
f : P1 → P2
f_linear : V1 →ₗ[k] V2
f_add :
  ∀ (p : P1) (v : V1), f (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f_linear : (a : V1) → V2) v : V2) (f p)
g : P1 → P2
g_linear : V1 →ₗ[k] V2
g_add :
  ∀ (p : P1) (v : V1), g (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((g_linear : (a : V1) → V2) v : V2) (g p)
h : f = g
⊢ { toFun := f, linear := f_linear, map_vadd' := f_add : P1 →ᵃ[k] P2 } =
    { toFun := g, linear := g_linear, map_vadd' := g_add }
have obtain : ∀ (p : P1),
  { toFun := f, linear := f_linear, map_vadd' := f_add : P1 →ᵃ[k] P2 } =
    { toFun := g, linear := g_linear, map_vadd' := g_add }
Tactic: obtain ⟨p⟩ := (AddTorsor.nonempty : Nonempty P1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
x x_1 : P1 →ᵃ[k] P2
f : P1 → P2
f_linear : V1 →ₗ[k] V2
f_add :
  ∀ (p : P1) (v : V1), f (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f_linear : (a : V1) → V2) v : V2) (f p)
g : P1 → P2
g_linear : V1 →ₗ[k] V2
g_add :
  ∀ (p : P1) (v : V1), g (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((g_linear : (a : V1) → V2) v : V2) (g p)
h : f = g
p : P1
⊢ { toFun := f, linear := f_linear, map_vadd' := f_add : P1 →ᵃ[k] P2 } =
    { toFun := g, linear := g_linear, map_vadd' := g_add }
have e_linear : ∀ (v : V1), Eq.{u_4 + 1} (α := V2) ((f_linear : (a : V1) → V2) v : V2) ((g_linear : (a : V1) → V2) v : V2)
Tactic: congr with v
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
x x_1 : P1 →ᵃ[k] P2
f : P1 → P2
f_linear : V1 →ₗ[k] V2
f_add :
  ∀ (p : P1) (v : V1), f (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f_linear : (a : V1) → V2) v : V2) (f p)
g : P1 → P2
g_linear : V1 →ₗ[k] V2
g_add :
  ∀ (p : P1) (v : V1), g (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((g_linear : (a : V1) → V2) v : V2) (g p)
h : f = g
p : P1
v : V1
⊢ Eq.{u_4 + 1} (α := V2) ((f_linear : (a : V1) → V2) v : V2) ((g_linear : (a : V1) → V2) v : V2)
have e_linear : HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f_linear : (a : V1) → V2) v : V2) (f p) =
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((g_linear : (a : V1) → V2) v : V2) (f p)
Tactic: apply vadd_right_cancel (f p)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
V2 : Type u_4
P2 : Type u_5
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : AddCommGroup V2
inst_5 : Module k V2
inst_6 : AffineSpace V2 P2
x x_1 : P1 →ᵃ[k] P2
f : P1 → P2
f_linear : V1 →ₗ[k] V2
f_add :
  ∀ (p : P1) (v : V1), f (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f_linear : (a : V1) → V2) v : V2) (f p)
g : P1 → P2
g_linear : V1 →ₗ[k] V2
g_add :
  ∀ (p : P1) (v : V1), g (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((g_linear : (a : V1) → V2) v : V2) (g p)
h : f = g
p : P1
v : V1
⊢ HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f_linear : (a : V1) → V2) v : V2) (f p) =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((g_linear : (a : V1) → V2) v : V2) (f p)
have e_linear : f (v +ᵥ p) = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((g_linear : (a : V1) → V2) v : V2) (f p)
Tactic: rw [← f_add, h, ← g_add]