awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst_7 : AddCommGroup V3
inst_8 : Module k V3
inst_9 : AffineSpace V3 P3
inst_10 : AddCommGroup V4
inst_11 : Module k V4
inst_12 : AffineSpace V4 P4
f : P1 → P2
f' : V1 →ₗ[k] V2
p : P1
h : ∀ (p' : P1), f p' = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) (p' -ᵥ p) : V2) (f p)
p' : P1
v : V1
rw :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) ((v +ᵥ p') -ᵥ p) : V2) (f p) =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) v : V2) (f p')
rw₁ :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) ((v +ᵥ p') -ᵥ p) : V2) (f p) =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) v : V2)
      (HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) (p' -ᵥ p) : V2) (f p))
rw₂ :
  HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) (v + (p' -ᵥ p)) : V2) (f p) =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) v : V2)
      (HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) (p' -ᵥ p) : V2) (f p))
rw₃ :
  HAdd.hAdd (α := V2) (β := V2) ((f' : (a : V1) → V2) v : V2) ((f' : (a : V1) → V2) (p' -ᵥ p) : V2) +ᵥ f p =
    HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) v : V2)
      (HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) (p' -ᵥ p) : V2) (f p))
⊢ f (v +ᵥ p') = HVAdd.hVAdd.{u_4, u_5, u_5} (α := V2) ((f' : (a : V1) → V2) v : V2) (f p')
have rw₄ : HAdd.hAdd (α := V2) (β := V2) ((f' : (a : V1) → V2) v : V2) ((f' : (a : V1) → V2) (p' -ᵥ p) : V2) +ᵥ f p =
  HAdd.hAdd (α := V2) (β := V2) ((f' : (a : V1) → V2) v : V2) ((f' : (a : V1) → V2) (p' -ᵥ p) : V2) +ᵥ f p
Tactic: rw [h, h p', vadd_vsub_assoc, f'.map_add, vadd_vadd]
-- 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
V3 : Type u_6
P3 : Type u_7
V4 : Type u_8
P4 : Type u_9
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
inst_7 : AddCommGroup V3
inst_8 : Module k V3
inst_9 : AffineSpace V3 P3
inst_10 : AddCommGroup V4
inst_11 : Module k V4
inst_12 : AffineSpace V4 P4
f : P2 →ᵃ[k] P3
g : P1 →ᵃ[k] P2
p : P1
v : V1
⊢ Function.comp.{u_3 + 1, u_5 + 1, u_7 + 1} (β := P2) (⇑f : (a : P2) → P3) (⇑g : (a : P1) → P2) (v +ᵥ p) =
    HVAdd.hVAdd.{u_6, u_7, u_7} (α := V3) (β := P3) ((f.linear ∘ₗ g.linear : (a : V1) → V3) v : V3)
      (Function.comp.{u_3 + 1, u_5 + 1, u_7 + 1} (β := P2) (⇑f : (a : P2) → P3) (⇑g : (a : P1) → P2) p)
have rw : HVAdd.hVAdd.{u_6, u_7, u_7} (α := V3) (β := P3) ((f.linear : (a : V2) → V3) ((g.linear : (a : V1) → V2) v : V2) : V3)
    ((f : (a : P2) → P3) ((g : (a : P1) → P2) p : P2) : P3) =
  HVAdd.hVAdd.{u_6, u_7, u_7} (α := V3) (β := P3) ((f.linear ∘ₗ g.linear : (a : V1) → V3) v : V3)
    (Function.comp.{u_3 + 1, u_5 + 1, u_7 + 1} (β := P2) (⇑f : (a : P2) → P3) (⇑g : (a : P1) → P2) p)
Tactic: rw [Function.comp_apply, g.map_vadd, f.map_vadd]
-- 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
f : P1 →ᵃ[k] P2
⊢ Function.Injective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2) (⇑f.linear : (a : V1) → V2) ↔
    Function.Injective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
have obtain : ∀ (p : P1),
  Function.Injective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2) (⇑f.linear : (a : V1) → V2) ↔
    Function.Injective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
Tactic: obtain ⟨p⟩ := (inferInstance : 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
f : P1 →ᵃ[k] P2
p : P1
⊢ Eq (α := (a : V1) → V2) (⇑f.linear : (a : V1) → V2)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := P2)
      (⇑(Equiv.symm (Equiv.vaddConst ((f : (a : P1) → P2) p)) : P2 ≃ V2) : (a : P2) → V2)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2) (⇑(Equiv.vaddConst p) : (a : V1) → P1)))
have h : ∀ (v : V1),
  Eq.{u_4 + 1} (α := V2) ((f.linear : (a : V1) → V2) v : V2)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := P2)
        (⇑(Equiv.symm (Equiv.vaddConst ((f : (a : P1) → P2) p)) : P2 ≃ V2) : (a : P2) → V2)
        (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2)
          (⇑(Equiv.vaddConst p) : (a : V1) → P1))
        v :
      V2)
Tactic: ext v
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (hypothesis)
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
f : P1 →ᵃ[k] P2
p : P1
⊢ Function.Injective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2) (⇑f.linear : (a : V1) → V2) ↔
    Function.Injective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
have h : Eq (α := (a : V1) → V2) (⇑f.linear : (a : V1) → V2)
  (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := P2)
    (⇑(Equiv.symm (Equiv.vaddConst ((f : (a : P1) → P2) p)) : P2 ≃ V2) : (a : P2) → V2)
    (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2) (⇑(Equiv.vaddConst p) : (a : V1) → P1)))
Tactic: have h : ⇑f.linear = (Equiv.vaddConst (f p)).symm ∘ f ∘ Equiv.vaddConst p := by
    ext v
    simp [f.map_vadd]
-- 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
f : P1 →ᵃ[k] P2
p : P1
h :
  Eq (α := (a : V1) → V2) (⇑f.linear : (a : V1) → V2)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := P2)
      (⇑(Equiv.symm (Equiv.vaddConst ((f : (a : P1) → P2) p)) : P2 ≃ V2) : (a : P2) → V2)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2) (⇑(Equiv.vaddConst p) : (a : V1) → P1)))
⊢ Function.Injective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2) (⇑f.linear : (a : V1) → V2) ↔
    Function.Injective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
have rw : Function.Injective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := P2)
      (⇑(Equiv.symm (Equiv.vaddConst ((f : (a : P1) → P2) p)) : P2 ≃ V2) : (a : P2) → V2)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2)
        (⇑(Equiv.vaddConst p) : (a : V1) → P1))) ↔
  Function.Injective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
Tactic: rw [h, Equiv.comp_injective, Equiv.injective_comp]
-- 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
f : P1 →ᵃ[k] P2
p : P1
h :
  Eq (α := (a : V1) → V2) (⇑f.linear : (a : V1) → V2)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := P2)
      (⇑(Equiv.symm (Equiv.vaddConst ((f : (a : P1) → P2) p)) : P2 ≃ V2) : (a : P2) → V2)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2) (⇑(Equiv.vaddConst p) : (a : V1) → P1)))
rw :
  Function.Injective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2)
      (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := P2)
        (⇑(Equiv.symm (Equiv.vaddConst ((f : (a : P1) → P2) p)) : P2 ≃ V2) : (a : P2) → V2)
        (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2)
          (⇑(Equiv.vaddConst p) : (a : V1) → P1))) ↔
    Function.Injective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
⊢ Function.Injective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2) (⇑f.linear : (a : V1) → V2) ↔
    Function.Injective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
have rw₁ : Function.Injective.{u_2 + 1, u_5 + 1} (α := V1) (β := P2)
    (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2) (⇑(Equiv.vaddConst p) : (a : V1) → P1)) ↔
  Function.Injective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
Tactic: rw [h, Equiv.comp_injective, Equiv.injective_comp]
-- 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
f : P1 →ᵃ[k] P2
p : P1
h :
  Eq (α := (a : V1) → V2) (⇑f.linear : (a : V1) → V2)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := P2)
      (⇑(Equiv.symm (Equiv.vaddConst ((f : (a : P1) → P2) p)) : P2 ≃ V2) : (a : P2) → V2)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2) (⇑(Equiv.vaddConst p) : (a : V1) → P1)))
rw :
  Function.Injective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2)
      (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := P2)
        (⇑(Equiv.symm (Equiv.vaddConst ((f : (a : P1) → P2) p)) : P2 ≃ V2) : (a : P2) → V2)
        (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2)
          (⇑(Equiv.vaddConst p) : (a : V1) → P1))) ↔
    Function.Injective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
rw₁ :
  Function.Injective.{u_2 + 1, u_5 + 1} (α := V1) (β := P2)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2)
        (⇑(Equiv.vaddConst p) : (a : V1) → P1)) ↔
    Function.Injective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
⊢ Function.Injective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2) (⇑f.linear : (a : V1) → V2) ↔
    Function.Injective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
have rw₂ : Function.Injective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2) ↔
  Function.Injective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
Tactic: rw [h, Equiv.comp_injective, Equiv.injective_comp]
-- 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
f : P1 →ᵃ[k] P2
⊢ Function.Surjective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2) (⇑f.linear : (a : V1) → V2) ↔
    Function.Surjective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
have obtain : ∀ (p : P1),
  Function.Surjective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2) (⇑f.linear : (a : V1) → V2) ↔
    Function.Surjective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
Tactic: obtain ⟨p⟩ := (inferInstance : Nonempty P1)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (hypothesis)
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
f : P1 →ᵃ[k] P2
p : P1
⊢ Function.Surjective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2) (⇑f.linear : (a : V1) → V2) ↔
    Function.Surjective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
have h : Eq (α := (a : V1) → V2) (⇑f.linear : (a : V1) → V2)
  (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := P2)
    (⇑(Equiv.symm (Equiv.vaddConst ((f : (a : P1) → P2) p)) : P2 ≃ V2) : (a : P2) → V2)
    (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2) (⇑(Equiv.vaddConst p) : (a : V1) → P1)))
Tactic: have h : ⇑f.linear = (Equiv.vaddConst (f p)).symm ∘ f ∘ Equiv.vaddConst p := by
    ext v
    simp [f.map_vadd]
-- 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
f : P1 →ᵃ[k] P2
p : P1
h :
  Eq (α := (a : V1) → V2) (⇑f.linear : (a : V1) → V2)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := P2)
      (⇑(Equiv.symm (Equiv.vaddConst ((f : (a : P1) → P2) p)) : P2 ≃ V2) : (a : P2) → V2)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2) (⇑(Equiv.vaddConst p) : (a : V1) → P1)))
⊢ Function.Surjective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2) (⇑f.linear : (a : V1) → V2) ↔
    Function.Surjective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
have rw : Function.Surjective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := P2)
      (⇑(Equiv.symm (Equiv.vaddConst ((f : (a : P1) → P2) p)) : P2 ≃ V2) : (a : P2) → V2)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2)
        (⇑(Equiv.vaddConst p) : (a : V1) → P1))) ↔
  Function.Surjective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
Tactic: rw [h, Equiv.comp_surjective, Equiv.surjective_comp]
-- 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
f : P1 →ᵃ[k] P2
p : P1
h :
  Eq (α := (a : V1) → V2) (⇑f.linear : (a : V1) → V2)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := P2)
      (⇑(Equiv.symm (Equiv.vaddConst ((f : (a : P1) → P2) p)) : P2 ≃ V2) : (a : P2) → V2)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2) (⇑(Equiv.vaddConst p) : (a : V1) → P1)))
rw :
  Function.Surjective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2)
      (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := P2)
        (⇑(Equiv.symm (Equiv.vaddConst ((f : (a : P1) → P2) p)) : P2 ≃ V2) : (a : P2) → V2)
        (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2)
          (⇑(Equiv.vaddConst p) : (a : V1) → P1))) ↔
    Function.Surjective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
⊢ Function.Surjective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2) (⇑f.linear : (a : V1) → V2) ↔
    Function.Surjective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
have rw₁ : Function.Surjective.{u_2 + 1, u_5 + 1} (α := V1) (β := P2)
    (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2) (⇑(Equiv.vaddConst p) : (a : V1) → P1)) ↔
  Function.Surjective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
Tactic: rw [h, Equiv.comp_surjective, Equiv.surjective_comp]
-- 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
f : P1 →ᵃ[k] P2
p : P1
h :
  Eq (α := (a : V1) → V2) (⇑f.linear : (a : V1) → V2)
    (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := P2)
      (⇑(Equiv.symm (Equiv.vaddConst ((f : (a : P1) → P2) p)) : P2 ≃ V2) : (a : P2) → V2)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2) (⇑(Equiv.vaddConst p) : (a : V1) → P1)))
rw :
  Function.Surjective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2)
      (Function.comp.{u_2 + 1, u_5 + 1, u_4 + 1} (β := P2)
        (⇑(Equiv.symm (Equiv.vaddConst ((f : (a : P1) → P2) p)) : P2 ≃ V2) : (a : P2) → V2)
        (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2)
          (⇑(Equiv.vaddConst p) : (a : V1) → P1))) ↔
    Function.Surjective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
rw₁ :
  Function.Surjective.{u_2 + 1, u_5 + 1} (α := V1) (β := P2)
      (Function.comp.{u_2 + 1, u_3 + 1, u_5 + 1} (β := P1) (⇑f : (a : P1) → P2)
        (⇑(Equiv.vaddConst p) : (a : V1) → P1)) ↔
    Function.Surjective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
⊢ Function.Surjective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2) (⇑f.linear : (a : V1) → V2) ↔
    Function.Surjective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
have rw₂ : Function.Surjective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2) ↔
  Function.Surjective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)
Tactic: rw [h, Equiv.comp_surjective, Equiv.surjective_comp]
-- 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
s t : Set P1
f : P1 →ᵃ[k] P2
⊢ VSub.vsub.{u_4, u_5} (P := Set P2) ((⇑f : (a : P1) → P2) '' s) ((⇑f : (a : P1) → P2) '' t) =
    (⇑f.linear : (a : V1) → V2) '' (s -ᵥ t)
have h : ∀ (v : V2),
  v ∈ VSub.vsub.{u_4, u_5} (P := Set P2) ((⇑f : (a : P1) → P2) '' s) ((⇑f : (a : P1) → P2) '' t) ↔
    Membership.mem (γ := Set V2) ((⇑f.linear : (a : V1) → V2) '' (s -ᵥ t)) v
Tactic: ext 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
s t : Set P1
f : P1 →ᵃ[k] P2
v : V2
⊢ v ∈ VSub.vsub.{u_4, u_5} (P := Set P2) ((⇑f : (a : P1) → P2) '' s) ((⇑f : (a : P1) → P2) '' t) ↔
    Membership.mem (γ := Set V2) ((⇑f.linear : (a : V1) → V2) '' (s -ᵥ t)) v
have h : (∃ a ∈ s, ∃ a_1 ∈ t, (f.linear : (a : V1) → V2) (a -ᵥ a_1) = v) ↔
  ∃ (x : V1), (∃ x_1 ∈ s, ∃ y ∈ t, x_1 -ᵥ y = x) ∧ (f.linear : (a : V1) → V2) x = v
Tactic: simp only [Set.mem_vsub, Set.mem_image,
    exists_exists_and_eq_and, ← f.linearMap_vsub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_1
V1 : Type u_2
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
p₀ p₁ : V1
c : k
⊢ (lineMap p₀ p₁ : (a : k) → V1) c = (1 - c) • p₀ + c • p₁
have simp : c • p₁ - c • p₀ + p₀ = p₀ - c • p₀ + c • p₁
Tactic: simp [lineMap_apply_module', smul_sub, sub_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
p : P1
v : V1
c : k
⊢ (lineMap p (v +ᵥ p) : (a : k) → P1) c = c • v +ᵥ p
have rw : c • ((v +ᵥ p) -ᵥ p) +ᵥ p = c • v +ᵥ p
Tactic: rw [lineMap_apply, vadd_vsub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
p : P1
v : V1
c : k
rw : c • ((v +ᵥ p) -ᵥ p) +ᵥ p = c • v +ᵥ p
⊢ (lineMap p (v +ᵥ p) : (a : k) → P1) c = c • v +ᵥ p
have rw₁ : c • v +ᵥ p = c • v +ᵥ p
Tactic: rw [lineMap_apply, vadd_vsub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : IsDomain k
inst_5 : IsTorsionFree k V1
p₀ p₁ : P1
c₁ c₂ : k
⊢ Eq.{u_3 + 1} (α := P1) ((lineMap p₀ p₁ : (a : k) → P1) c₁ : P1) ((lineMap p₀ p₁ : (a : k) → P1) c₂ : P1) ↔
    p₀ = p₁ ∨ c₁ = c₂
have rw : c₁ • (p₁ -ᵥ p₀) +ᵥ p₀ = (lineMap p₀ p₁ : (a : k) → P1) c₂ ↔ p₀ = p₁ ∨ c₁ = c₂
Tactic: rw [lineMap_apply, lineMap_apply, ← @vsub_eq_zero_iff_eq V1, vadd_vsub_vadd_cancel_right, ←
    sub_smul, smul_eq_zero, sub_eq_zero, vsub_eq_zero_iff_eq, or_comm, eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : IsDomain k
inst_5 : IsTorsionFree k V1
p₀ p₁ : P1
c₁ c₂ : k
rw : c₁ • (p₁ -ᵥ p₀) +ᵥ p₀ = (lineMap p₀ p₁ : (a : k) → P1) c₂ ↔ p₀ = p₁ ∨ c₁ = c₂
⊢ Eq.{u_3 + 1} (α := P1) ((lineMap p₀ p₁ : (a : k) → P1) c₁ : P1) ((lineMap p₀ p₁ : (a : k) → P1) c₂ : P1) ↔
    p₀ = p₁ ∨ c₁ = c₂
have rw₁ : c₁ • (p₁ -ᵥ p₀) +ᵥ p₀ = c₂ • (p₁ -ᵥ p₀) +ᵥ p₀ ↔ p₀ = p₁ ∨ c₁ = c₂
Tactic: rw [lineMap_apply, lineMap_apply, ← @vsub_eq_zero_iff_eq V1, vadd_vsub_vadd_cancel_right, ←
    sub_smul, smul_eq_zero, sub_eq_zero, vsub_eq_zero_iff_eq, or_comm, eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : IsDomain k
inst_5 : IsTorsionFree k V1
p₀ p₁ : P1
c₁ c₂ : k
rw : c₁ • (p₁ -ᵥ p₀) +ᵥ p₀ = (lineMap p₀ p₁ : (a : k) → P1) c₂ ↔ p₀ = p₁ ∨ c₁ = c₂
rw₁ : c₁ • (p₁ -ᵥ p₀) +ᵥ p₀ = c₂ • (p₁ -ᵥ p₀) +ᵥ p₀ ↔ p₀ = p₁ ∨ c₁ = c₂
⊢ Eq.{u_3 + 1} (α := P1) ((lineMap p₀ p₁ : (a : k) → P1) c₁ : P1) ((lineMap p₀ p₁ : (a : k) → P1) c₂ : P1) ↔
    p₀ = p₁ ∨ c₁ = c₂
have rw₂ : (c₁ • (p₁ -ᵥ p₀) +ᵥ p₀) -ᵥ (c₂ • (p₁ -ᵥ p₀) +ᵥ p₀) = 0 ↔ p₀ = p₁ ∨ c₁ = c₂
Tactic: rw [lineMap_apply, lineMap_apply, ← @vsub_eq_zero_iff_eq V1, vadd_vsub_vadd_cancel_right, ←
    sub_smul, smul_eq_zero, sub_eq_zero, vsub_eq_zero_iff_eq, or_comm, eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : IsDomain k
inst_5 : IsTorsionFree k V1
p₀ p₁ : P1
c₁ c₂ : k
rw : c₁ • (p₁ -ᵥ p₀) +ᵥ p₀ = (lineMap p₀ p₁ : (a : k) → P1) c₂ ↔ p₀ = p₁ ∨ c₁ = c₂
rw₁ : c₁ • (p₁ -ᵥ p₀) +ᵥ p₀ = c₂ • (p₁ -ᵥ p₀) +ᵥ p₀ ↔ p₀ = p₁ ∨ c₁ = c₂
rw₂ : (c₁ • (p₁ -ᵥ p₀) +ᵥ p₀) -ᵥ (c₂ • (p₁ -ᵥ p₀) +ᵥ p₀) = 0 ↔ p₀ = p₁ ∨ c₁ = c₂
⊢ Eq.{u_3 + 1} (α := P1) ((lineMap p₀ p₁ : (a : k) → P1) c₁ : P1) ((lineMap p₀ p₁ : (a : k) → P1) c₂ : P1) ↔
    p₀ = p₁ ∨ c₁ = c₂
have rw₃ : c₁ • (p₁ -ᵥ p₀) - c₂ • (p₁ -ᵥ p₀) = 0 ↔ p₀ = p₁ ∨ c₁ = c₂
Tactic: rw [lineMap_apply, lineMap_apply, ← @vsub_eq_zero_iff_eq V1, vadd_vsub_vadd_cancel_right, ←
    sub_smul, smul_eq_zero, sub_eq_zero, vsub_eq_zero_iff_eq, or_comm, eq_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_1
V1 : Type u_2
P1 : Type u_3
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AffineSpace V1 P1
inst_4 : IsDomain k
inst_5 : IsTorsionFree k V1
p₀ p₁ : P1
c₁ c₂ : k
rw : c₁ • (p₁ -ᵥ p₀) +ᵥ p₀ = (lineMap p₀ p₁ : (a : k) → P1) c₂ ↔ p₀ = p₁ ∨ c₁ = c₂
rw₁ : c₁ • (p₁ -ᵥ p₀) +ᵥ p₀ = c₂ • (p₁ -ᵥ p₀) +ᵥ p₀ ↔ p₀ = p₁ ∨ c₁ = c₂
rw₂ : (c₁ • (p₁ -ᵥ p₀) +ᵥ p₀) -ᵥ (c₂ • (p₁ -ᵥ p₀) +ᵥ p₀) = 0 ↔ p₀ = p₁ ∨ c₁ = c₂
rw₃ : c₁ • (p₁ -ᵥ p₀) - c₂ • (p₁ -ᵥ p₀) = 0 ↔ p₀ = p₁ ∨ c₁ = c₂
⊢ Eq.{u_3 + 1} (α := P1) ((lineMap p₀ p₁ : (a : k) → P1) c₁ : P1) ((lineMap p₀ p₁ : (a : k) → P1) c₂ : P1) ↔
    p₀ = p₁ ∨ c₁ = c₂
have rw₄ : (c₁ - c₂) • (p₁ -ᵥ p₀) = 0 ↔ p₀ = p₁ ∨ c₁ = c₂
Tactic: rw [lineMap_apply, lineMap_apply, ← @vsub_eq_zero_iff_eq V1, vadd_vsub_vadd_cancel_right, ←
    sub_smul, smul_eq_zero, sub_eq_zero, vsub_eq_zero_iff_eq, or_comm, eq_comm]