awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
⊢ Eq (α := (a : P1 × P2) → P1) (⇑fst : (a : P1 × P2) → P1) Prod.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
⊢ Eq (α := V1 × V2 →ₗ[k] V1) (linear (k := k) (P1 := P1 × P2) fst) (LinearMap.fst k V1 V2)

Tactic:
rfl

Premises used: LinearMap.fst, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
⊢ Eq (α := (a : P1 × P2) → P2) (⇑snd : (a : P1 × P2) → P2) Prod.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
⊢ Eq (α := V1 × V2 →ₗ[k] V2) (linear (k := k) (P1 := P1 × P2) snd) (LinearMap.snd k V1 V2)

Tactic:
rfl

Premises used: LinearMap.snd, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
⊢ Eq.{u_3 + 1} (α := (a : P1) → P1) (⇑(id k P1) : (a : P1) → P1) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
⊢ Eq (α := V1 →ₗ[k] V1) (linear (id k P1)) LinearMap.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
⊢ (id k P1 : (a : P1) → P1) p = p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
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)
⊢ 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)

Tactic:
rw [Function.comp_apply, g.map_vadd, f.map_vadd]

Premises used: AffineMap.map_vadd, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
⊢ 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:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
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
f : P2 →ᵃ[k] P3
g : P1 →ᵃ[k] P2
⊢ Eq (α := (a : P1) → P3) (⇑(f.comp g) : (a : P1) → P3)
    (Function.comp.{u_3 + 1, u_5 + 1, u_7 + 1} (β := P2) (⇑f : (a : P2) → P3) (⇑g : (a : P1) → P2))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
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
f : P2 →ᵃ[k] P3
g : P1 →ᵃ[k] P2
p : P1
⊢ Eq.{u_7 + 1} (α := P3) ((f.comp g : (a : P1) → P3) p : P3) ((f : (a : P2) → P3) ((g : (a : P1) → P2) p : P2) : P3)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
⊢ f.comp (id k P1) = f

Tactic:
ext fun _ => rfl

Premises used: AffineMap.ext, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
⊢ comp (id k P2) f = f

Tactic:
ext fun _ => rfl

Premises used: AffineMap.ext, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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₃₄ : P3 →ᵃ[k] P4
f₂₃ : P2 →ᵃ[k] P3
f₁₂ : P1 →ᵃ[k] P2
⊢ (f₃₄.comp f₂₃).comp f₁₂ = f₃₄.comp (f₂₃.comp f₁₂)

Tactic:
rfl

Premises used: AffineMap.comp, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
f g : P1 →ᵃ[k] P1
⊢ Eq.{u_3 + 1} (α := (a : P1) → P1) (⇑(f * g) : (a : P1) → P1)
    (Function.comp (β := P1) (⇑f : (a : P1) → P1) (⇑g : (a : P1) → P1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
⊢ Eq.{u_3 + 1} (α := (a : P1) → P1) (⇑1 : (a : P1) → P1) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
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)
⊢ 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)

Premises used: inferInstance
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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 :
  ∀ (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)
⊢ 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:
ext v
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
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:
simp [f.map_vadd]

Premises used: AffineMap.map_vadd
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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)))

Tactic:
have h : ⇑f.linear = (Equiv.vaddConst (f p)).symm ∘ f ∘ Equiv.vaddConst p := by
    ext v
    simp [f.map_vadd]
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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)
rw₂ 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)
⊢ 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:
rw [h, Equiv.comp_injective, Equiv.injective_comp]

Premises used: Equiv.injective_comp, Equiv.comp_injective
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
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)
⊢ 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)

Premises used: inferInstance
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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)
rw₂ 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)
⊢ 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:
rw [h, Equiv.comp_surjective, Equiv.surjective_comp]

Premises used: Equiv.comp_surjective, Equiv.surjective_comp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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.Bijective.{u_2 + 1, u_4 + 1} (α := V1) (β := V2) (⇑f.linear : (a : V1) → V2) ↔
    Function.Bijective.{u_3 + 1, u_5 + 1} (α := P1) (β := P2) (⇑f : (a : P1) → P2)

Tactic:
and_congr f.linear_injective_iff f.linear_surjective_iff

Premises used: AffineMap.linear_injective_iff, AffineMap.linear_surjective_iff, Function.Bijective, and_congr
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
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
⊢ 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)

Tactic:
ext v
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
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
⊢ 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:
simp only [Set.mem_vsub, Set.mem_image,
    exists_exists_and_eq_and, ← f.linearMap_vsub]

Premises used: Set.mem_vsub, Set.mem_image, AffineMap.linearMap_vsub, exists_exists_and_eq_and
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
⊢ (∃ 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:
grind
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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 →ᵃ[k] P2
g : P1 →ᵃ[k] P3
⊢ ∀ (p : P1) (v : V1),
    Function.prod (α := fun (a : P1) ↦ P2) (β := fun (a : P1) ↦ P3) (⇑f : (a : P1) → P2) (⇑g : (a : P1) → P3) (v +ᵥ p) =
      HVAdd.hVAdd (α := V2 × V3) (β := P2 × P3) ((f.linear.prod g.linear : (a : V1) → V2 × V3) v : V2 × V3)
        (Function.prod (α := fun (a : P1) ↦ P2) (β := fun (a : P1) ↦ P3) (⇑f : (a : P1) → P2) (⇑g : (a : P1) → P3) p :
          P2 × P3)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
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
f : P1 →ᵃ[k] P2
g : P1 →ᵃ[k] P3
⊢ Eq (α := (a : P1) → P2 × P3) (⇑(f.prod g) : (a : P1) → P2 × P3)
    (Function.prod (α := fun (a : P1) ↦ P2) (β := fun (a : P1) ↦ P3) (⇑f : (a : P1) → P2) (⇑g : (a : P1) → P3))

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
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
f : P1 →ᵃ[k] P2
g : P1 →ᵃ[k] P3
p : P1
⊢ Eq (α := P2 × P3) ((f.prod g : (a : P1) → P2 × P3) p : P2 × P3)
    (((f : (a : P1) → P2) p, (g : (a : P1) → P3) p) : P2 × P3)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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 →ᵃ[k] P2
g : P3 →ᵃ[k] P4
⊢ ∀ (p : P1 × P3) (v : V1 × V3),
    Prod.map (⇑f : (a : P1) → P2) (⇑g : (a : P3) → P4) (v +ᵥ p) =
      HVAdd.hVAdd (α := V2 × V4) (β := P2 × P4) ((f.linear.prodMap g.linear : (a : V1 × V3) → V2 × V4) v : V2 × V4)
        (Prod.map (⇑f : (a : P1) → P2) (⇑g : (a : P3) → P4) p)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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 →ᵃ[k] P2
g : P3 →ᵃ[k] P4
⊢ Eq (α := (a : P1 × P3) → P2 × P4) (⇑(f.prodMap g) : (a : P1 × P3) → P2 × P4)
    (Prod.map (⇑f : (a : P1) → P2) (⇑g : (a : P3) → P4))

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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 →ᵃ[k] P2
g : P3 →ᵃ[k] P4
x : P1 × P3
⊢ Eq (α := P2 × P4) ((f.prodMap g : (a : P1 × P3) → P2 × P4) x : P2 × P4)
    (((f : (a : P1) → P2) x.1, (g : (a : P3) → P4) x.2) : P2 × P4)

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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₀ p₁ : P1
⊢ Eq (α := (a : k) → P1) (⇑(lineMap p₀ p₁) : (a : k) → P1) fun (c : k) ↦ c • (p₁ -ᵥ p₀) +ᵥ p₀

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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₀ p₁ : P1
c : k
⊢ (lineMap p₀ p₁ : (a : k) → P1) c = c • (p₁ -ᵥ p₀) +ᵥ p₀

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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 = c • (p₁ - p₀) + p₀

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
simp : c • p₁ - c • p₀ + p₀ = p₀ - c • p₀ + c • p₁
⊢ (lineMap p₀ p₁ : (a : k) → V1) c = (1 - c) • p₀ + c • p₁

Tactic:
simp [lineMap_apply_module', smul_sub, sub_smul]

Premises used: sub_smul, AffineMap.lineMap_apply_module', smul_sub
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
⊢ c • p₁ - c • p₀ + p₀ = p₀ - c • p₀ + c • p₁

Tactic:
abel