awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
P2 : Type u_6
V3 : Type u_7
P3 : Type u_8
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : AddCommGroup V2
inst_4 : AffineSpace V2 P2
inst_5 : AddCommGroup V3
inst_6 : AffineSpace V3 P3
inst_7 : Module k V1
inst_8 : Module k V2
inst_9 : Module k V3
inst_10 : Semiring R
inst_11 : Module R V2
inst_12 : SMulCommClass k R V2
f : V1 →ᵃ[k] V2
⊢ (fun (p : V2 × (V1 →ₗ[k] V2)) ↦ p.2.toAffineMap + const k V1 p.1)
      ((fun (f : V1 →ᵃ[k] V2) ↦ (((f : (a : V1) → V2) 0, f.linear) : V2 × (V1 →ₗ[k] V2))) f) =
    f
have h : ∀ (p : V1),
  Eq.{u_5 + 1} (α := V2)
    (((fun (p : V2 × (V1 →ₗ[k] V2)) ↦ p.2.toAffineMap + const k V1 p.1)
            ((fun (f : V1 →ᵃ[k] V2) ↦ (((f : (a : V1) → V2) 0, f.linear) : V2 × (V1 →ₗ[k] V2))) f) :
          (a : V1) → V2)
        p :
      V2)
    ((f : (a : V1) → V2) p : V2)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
P2 : Type u_6
V3 : Type u_7
P3 : Type u_8
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : AddCommGroup V2
inst_4 : AffineSpace V2 P2
inst_5 : AddCommGroup V3
inst_6 : AffineSpace V3 P3
inst_7 : Module k V1
inst_8 : Module k V2
inst_9 : Module k V3
inst_10 : Semiring R
inst_11 : Module R V2
inst_12 : SMulCommClass k R V2
f : V1 →ᵃ[k] V2
p : V1
⊢ Eq.{u_5 + 1} (α := V2)
    (((fun (p : V2 × (V1 →ₗ[k] V2)) ↦ p.2.toAffineMap + const k V1 p.1)
            ((fun (f : V1 →ᵃ[k] V2) ↦ (((f : (a : V1) → V2) 0, f.linear) : V2 × (V1 →ₗ[k] V2))) f) :
          (a : V1) → V2)
        p :
      V2)
    ((f : (a : V1) → V2) p : V2)
have h : ((fun (p : V2 × (V1 →ₗ[k] V2)) ↦ p.2.toAffineMap + const k V1 p.1)
        ((fun (f : V1 →ᵃ[k] V2) ↦ (((f : (a : V1) → V2) 0, f.linear) : V2 × (V1 →ₗ[k] V2))) f) :
      (a : V1) → V2)
    p =
  HAdd.hAdd (α := (a : V1) → V2) (β := V1 → V2) (⇑f.linear : (a : V1) → V2) (fun (x : V1) ↦ (f : (a : V1) → V2) 0) p
Tactic: rw [f.decomp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
P2 : Type u_6
V3 : Type u_7
P3 : Type u_8
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : AddCommGroup V2
inst_4 : AffineSpace V2 P2
inst_5 : AddCommGroup V3
inst_6 : AffineSpace V3 P3
inst_7 : Module k V1
inst_8 : Module k V2
inst_9 : Module k V3
inst_10 : Semiring R
inst_11 : Module R V2
inst_12 : SMulCommClass k R V2
v : V2
f : V1 →ₗ[k] V2
⊢ (fun (f : V1 →ᵃ[k] V2) ↦ (((f : (a : V1) → V2) 0, f.linear) : V2 × (V1 →ₗ[k] V2)))
      ((fun (p : V2 × (V1 →ₗ[k] V2)) ↦ p.2.toAffineMap + const k V1 p.1) (v, f)) =
    (v, f)
have fst : ((fun (f : V1 →ᵃ[k] V2) ↦ (((f : (a : V1) → V2) 0, f.linear) : V2 × (V1 →ₗ[k] V2)))
      ((fun (p : V2 × (V1 →ₗ[k] V2)) ↦ p.2.toAffineMap + const k V1 p.1) (v, f))).1 =
  (v, f).1
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
R : Type u_1
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
P2 : Type u_6
V3 : Type u_7
P3 : Type u_8
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : AddCommGroup V2
inst_4 : AffineSpace V2 P2
inst_5 : AddCommGroup V3
inst_6 : AffineSpace V3 P3
inst_7 : Module k V1
inst_8 : Module k V2
inst_9 : Module k V3
inst_10 : Semiring R
inst_11 : Module R V2
inst_12 : SMulCommClass k R V2
v : V2
f : V1 →ₗ[k] V2
fst :
  ((fun (f : V1 →ᵃ[k] V2) ↦ (((f : (a : V1) → V2) 0, f.linear) : V2 × (V1 →ₗ[k] V2)))
        ((fun (p : V2 × (V1 →ₗ[k] V2)) ↦ p.2.toAffineMap + const k V1 p.1) (v, f))).1 =
    (v, f).1
⊢ (fun (f : V1 →ᵃ[k] V2) ↦ (((f : (a : V1) → V2) 0, f.linear) : V2 × (V1 →ₗ[k] V2)))
      ((fun (p : V2 × (V1 →ₗ[k] V2)) ↦ p.2.toAffineMap + const k V1 p.1) (v, f)) =
    (v, f)
have snd : ∀ (x : V1),
  Eq.{u_5 + 1} (α := V2)
    ((((fun (f : V1 →ᵃ[k] V2) ↦ (((f : (a : V1) → V2) 0, f.linear) : V2 × (V1 →ₗ[k] V2)))
              ((fun (p : V2 × (V1 →ₗ[k] V2)) ↦ p.2.toAffineMap + const k V1 p.1) (v, f))).2 :
          (a : V1) → V2)
        x :
      V2)
    (((v, f).2 : (a : V1) → V2) x : V2)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
ι : Type u_9
φv : ι → Type u_10
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
fv : (i : ι) → P1 →ᵃ[k] φv i
⊢ pi (φv := φv) (φp := φv) fv = 0 ↔ ∀ (i : ι), fv i = 0
have simp : (∀ (p : P1) (x : ι),
    Eq.{u_10 + 1} (α := φv x) ((fv x : (a : P1) → φv x) p : φv x) ((0 : (a : P1) → (i : ι) → φv i) p x : φv x)) ↔
  ∀ (i : ι) (p : P1), Eq.{u_10 + 1} (α := φv i) ((fv i : (a : P1) → φv i) p : φv i) ((0 : (a : P1) → φv i) p : φv i)
Tactic: simp only [AffineMap.ext_iff, funext_iff, pi_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
ι : Type u_9
φv : ι → Type u_10
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
⊢ Eq (α := P1 →ᵃ[k] (i : ι) → φv i) (pi (φv := φv) (φp := φv) fun (x : ι) ↦ 0) 0
have h : ∀ (p : P1) (x : ι),
  Eq.{u_10 + 1} (α := φv x) ((pi (φv := φv) (φp := φv) fun (x : ι) ↦ 0 : (a : P1) → (i : ι) → φv i) p x : φv x)
    ((0 : (a : P1) → (i : ι) → φv i) p x : φv x)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst : Ring k
inst_1 : AddCommGroup V2
inst_2 : AffineSpace V2 P2
inst_3 : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_6 : Finite ι
inst_7 : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h :
  ∀ (i : ι) (x : φv i),
    Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
      ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
h₂ : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
⊢ f = g
have h₁ : f.linear = g.linear
Tactic: apply ext_linear
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst : Ring k
inst_1 : AddCommGroup V2
inst_2 : AffineSpace V2 P2
inst_3 : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_6 : Finite ι
inst_7 : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h :
  ∀ (i : ι) (x : φv i),
    Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
      ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
h₂ : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
h₁ : f.linear = g.linear
h₃ : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
⊢ f = g
have p : (i : ι) → φv i
Tactic: apply ext_linear
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst : Ring k
inst_1 : AddCommGroup V2
inst_2 : AffineSpace V2 P2
inst_3 : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_6 : Finite ι
inst_7 : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h :
  ∀ (i : ι) (x : φv i),
    Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
      ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
h₂ : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
⊢ f.linear = g.linear
have h₁ : ∀ (i : ι) (x : φv i),
  Eq.{u_5 + 1} (α := V2) ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
    ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
Tactic: apply LinearMap.pi_ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (hypothesis)
Goal:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst : Ring k
inst_1 : AddCommGroup V2
inst_2 : AffineSpace V2 P2
inst_3 : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_6 : Finite ι
inst_7 : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h :
  ∀ (i : ι) (x : φv i),
    Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
      ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
h₂ : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
i : ι
x : φv i
⊢ Eq.{u_5 + 1} (α := V2) ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
    ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
have s₁ : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
  ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
Tactic: have s₁ := h i x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (hypothesis)
Goal:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst : Ring k
inst_1 : AddCommGroup V2
inst_2 : AffineSpace V2 P2
inst_3 : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_6 : Finite ι
inst_7 : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h :
  ∀ (i : ι) (x : φv i),
    Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
      ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
h₂ : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
i : ι
x : φv i
s₁ :
  Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
    ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
⊢ Eq.{u_5 + 1} (α := V2) ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
    ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
have s₂ : (f : (a : (i : ι) → φv i) → P2) (HVAdd.hVAdd (β := (i : ι) → φv i) (Pi.single (M := φv) i x) 0) =
  HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
    ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2)
Tactic: have s₂ := f.map_vadd 0 (Pi.single i x)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (hypothesis)
Goal:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst : Ring k
inst_1 : AddCommGroup V2
inst_2 : AffineSpace V2 P2
inst_3 : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_6 : Finite ι
inst_7 : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h :
  ∀ (i : ι) (x : φv i),
    Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
      ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
h₂ : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
i : ι
x : φv i
s₁ :
  Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
    ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
s₂ :
  (f : (a : (i : ι) → φv i) → P2) (HVAdd.hVAdd (β := (i : ι) → φv i) (Pi.single (M := φv) i x) 0) =
    HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
      ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2)
⊢ Eq.{u_5 + 1} (α := V2) ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
    ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
have s₃ : (g : (a : (i : ι) → φv i) → P2) (HVAdd.hVAdd (β := (i : ι) → φv i) (Pi.single (M := φv) i x) 0) =
  HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
    ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
Tactic: have s₃ := g.map_vadd 0 (Pi.single i x)
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (hypothesis)
Goal:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst : Ring k
inst_1 : AddCommGroup V2
inst_2 : AffineSpace V2 P2
inst_3 : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_6 : Finite ι
inst_7 : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h :
  ∀ (i : ι) (x : φv i),
    Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
      ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
h₂ : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
i : ι
x : φv i
s₁ :
  Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
    ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
s₂ :
  (f : (a : (i : ι) → φv i) → P2) (HVAdd.hVAdd (β := (i : ι) → φv i) (Pi.single (M := φv) i x) 0) =
    HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
      ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2)
s₃ :
  (g : (a : (i : ι) → φv i) → P2) (HVAdd.hVAdd (β := (i : ι) → φv i) (Pi.single (M := φv) i x) 0) =
    HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
      ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
⊢ Eq.{u_5 + 1} (α := V2) ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
    ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
have s₄ : (f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) =
  HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
    ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2)
Tactic: rw [vadd_eq_add, add_zero] at s₂ s₃
Cleared hypotheses: s₂, s₃
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (hypothesis)
Goal:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst : Ring k
inst_1 : AddCommGroup V2
inst_2 : AffineSpace V2 P2
inst_3 : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_6 : Finite ι
inst_7 : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h :
  ∀ (i : ι) (x : φv i),
    Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
      ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
h₂ : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
i : ι
x : φv i
s₁ :
  Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
    ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
s₂ :
  (f : (a : (i : ι) → φv i) → P2) (HVAdd.hVAdd (β := (i : ι) → φv i) (Pi.single (M := φv) i x) 0) =
    HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
      ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2)
s₃ :
  (g : (a : (i : ι) → φv i) → P2) (HVAdd.hVAdd (β := (i : ι) → φv i) (Pi.single (M := φv) i x) 0) =
    HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
      ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
s₄ :
  (f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) =
    HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
      ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2)
⊢ Eq.{u_5 + 1} (α := V2) ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
    ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
have s₅ : (g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) =
  HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
    ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
Tactic: rw [vadd_eq_add, add_zero] at s₂ s₃
Cleared hypotheses: s₂, s₃
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (hypothesis)
Goal:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst : Ring k
inst_1 : AddCommGroup V2
inst_2 : AffineSpace V2 P2
inst_3 : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_6 : Finite ι
inst_7 : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h :
  ∀ (i : ι) (x : φv i),
    Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
      ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
h₂ : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
i : ι
x : φv i
s₁ :
  Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
    ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
s₂ :
  (f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) =
    HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
      ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2)
s₃ :
  (g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) =
    HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
      ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
⊢ Eq.{u_5 + 1} (α := V2) ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
    ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
have h₃ : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i 0) : P2)
  ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i 0) : P2)
Tactic: replace h₂ := h i 0
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (hypothesis)
Goal:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst : Ring k
inst_1 : AddCommGroup V2
inst_2 : AffineSpace V2 P2
inst_3 : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_6 : Finite ι
inst_7 : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h :
  ∀ (i : ι) (x : φv i),
    Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
      ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
i : ι
x : φv i
s₁ :
  Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
    ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
s₂ :
  (f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) =
    HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
      ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2)
s₃ :
  (g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) =
    HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
      ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
h₂ :
  Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i 0) : P2)
    ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i 0) : P2)
⊢ Eq.{u_5 + 1} (α := V2) ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
    ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
have h₃ : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
Tactic: simp only [Pi.single_zero] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst : Ring k
inst_1 : AddCommGroup V2
inst_2 : AffineSpace V2 P2
inst_3 : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_6 : Finite ι
inst_7 : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
h :
  ∀ (i : ι) (x : φv i),
    Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
      ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
i : ι
x : φv i
s₁ :
  Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
    ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
s₂ :
  (f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) =
    HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
      ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2)
s₃ :
  (g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) =
    HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
      ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
h₂ : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
⊢ Eq.{u_5 + 1} (α := V2) ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
    ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
have h₁ : ∀
  (s₁ :
    HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
        ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
        ((f : (a : (i : ι) → φv i) → P2) 0 : P2) =
      (g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x))
  (s₂ :
    (f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) =
      HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
        ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
        ((f : (a : (i : ι) → φv i) → P2) 0 : P2))
  (s₃ :
    (g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) =
      HVAdd.hVAdd.{u_5, u_6, u_6} (α := V2) (β := P2)
        ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
        ((g : (a : (i : ι) → φv i) → P2) 0 : P2))
  (h₂ : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)),
  Eq.{u_5 + 1} (α := V2) ((f.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
    ((g.linear : (a : (i : ι) → φv i) → V2) (Pi.single (M := φv) i x) : V2)
Tactic: rwa [s₂, s₃, h₂, vadd_right_cancel_iff] at s₁
Cleared hypotheses: s₁, s₂, s₃, h₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst : Ring k
inst_1 : AddCommGroup V2
inst_2 : AffineSpace V2 P2
inst_3 : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_6 : Finite ι
inst_7 : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
inst_8 : Nonempty ι
h :
  ∀ (i : ι) (x : φv i),
    Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
      ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
⊢ f = g
have apply : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
Tactic: apply pi_ext_zero h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_2
V2 : Type u_5
P2 : Type u_6
inst : Ring k
inst_1 : AddCommGroup V2
inst_2 : AffineSpace V2 P2
inst_3 : Module k V2
ι : Type u_9
φv : ι → Type u_10
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_6 : Finite ι
inst_7 : DecidableEq ι
f g : ((i : ι) → φv i) →ᵃ[k] P2
inst_8 : Nonempty ι
h :
  ∀ (i : ι) (x : φv i),
    Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
      ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) i x) : P2)
⊢ Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
have inhabit : ∀ (inhabited_h : Inhabited ι),
  Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
Tactic: inhabit ι