awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_10
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
f : k →ᵃ[k] k
a b : k
⊢ Eq (α := (a : k) → k) (⇑f : (a : k) → k)
    ((fun (x : k) ↦ HAdd.hAdd (β := k) x ((f : (a : k) → k) 0 : k)) ∘ fun (x : k) ↦
      x * HSub.hSub (α := k) (β := k) ((f : (a : k) → k) 1 : k) ((f : (a : k) → k) 0 : k))

Tactic:
have : ⇑f = (fun x => x + f 0) ∘ fun x => x * (f 1 - f 0) := by
    ext x
    change f x = x • (f 1 -ᵥ f 0) +ᵥ f 0
    rw [← f.linearMap_vsub, ← f.linear.map_smul, ← f.map_vadd]
    simp only [vsub_eq_sub, add_zero, mul_one, vadd_eq_add, sub_zero, smul_eq_mul]
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_10
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
f : k →ᵃ[k] k
a b : k
this :
  Eq (α := (a : k) → k) (⇑f : (a : k) → k)
    ((fun (x : k) ↦ HAdd.hAdd (β := k) x ((f : (a : k) → k) 0 : k)) ∘ fun (x : k) ↦
      x * HSub.hSub (α := k) (β := k) ((f : (a : k) → k) 1 : k) ((f : (a : k) → k) 0 : k))
rw :
  Eq (α := Set k)
    ((fun (x : k) ↦ HAdd.hAdd (β := k) x ((f : (a : k) → k) 0 : k)) ''
      (fun (x : k) ↦ x * HSub.hSub (α := k) (β := k) ((f : (a : k) → k) 1 : k) ((f : (a : k) → k) 0 : k)) ''
        Set.uIcc a b)
    (Set.uIcc
      (((fun (x : k) ↦ HAdd.hAdd (β := k) x ((f : (a : k) → k) 0 : k)) ∘ fun (x : k) ↦
          x * HSub.hSub (α := k) (β := k) ((f : (a : k) → k) 1 : k) ((f : (a : k) → k) 0 : k))
        a)
      (((fun (x : k) ↦ HAdd.hAdd (β := k) x ((f : (a : k) → k) 0 : k)) ∘ fun (x : k) ↦
          x * HSub.hSub (α := k) (β := k) ((f : (a : k) → k) 1 : k) ((f : (a : k) → k) 0 : k))
        b))
⊢ Eq (α := Set k) ((⇑f : (a : k) → k) '' Set.uIcc a b : Set k)
    (Set.uIcc ((f : (a : k) → k) a) ((f : (a : k) → k) b) : Set k)

Tactic:
rw [this, Set.image_comp]

Premises used: Set.image_comp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_10
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
f : k →ᵃ[k] k
a b : k
this :
  Eq (α := (a : k) → k) (⇑f : (a : k) → k)
    ((fun (x : k) ↦ HAdd.hAdd (β := k) x ((f : (a : k) → k) 0 : k)) ∘ fun (x : k) ↦
      x * HSub.hSub (α := k) (β := k) ((f : (a : k) → k) 1 : k) ((f : (a : k) → k) 0 : k))
⊢ Eq (α := Set k)
    ((fun (x : k) ↦ HAdd.hAdd (β := k) x ((f : (a : k) → k) 0 : k)) ''
      (fun (x : k) ↦ x * HSub.hSub (α := k) (β := k) ((f : (a : k) → k) 1 : k) ((f : (a : k) → k) 0 : k)) ''
        Set.uIcc a b)
    (Set.uIcc
      (((fun (x : k) ↦ HAdd.hAdd (β := k) x ((f : (a : k) → k) 0 : k)) ∘ fun (x : k) ↦
          x * HSub.hSub (α := k) (β := k) ((f : (a : k) → k) 1 : k) ((f : (a : k) → k) 0 : k))
        a)
      (((fun (x : k) ↦ HAdd.hAdd (β := k) x ((f : (a : k) → k) 0 : k)) ∘ fun (x : k) ↦
          x * HSub.hSub (α := k) (β := k) ((f : (a : k) → k) 1 : k) ((f : (a : k) → k) 0 : k))
        b))

Tactic:
simp only [Set.image_add_const_uIcc, Set.image_mul_const_uIcc, Function.comp_apply]

Premises used: Set.image_mul_const_uIcc, Set.image_add_const_uIcc, Function.comp_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
inst : Ring k
ι : Type u_10
V : ι → Type u_11
P : ι → Type u_12
inst_1 : (i : ι) → AddCommGroup (V i)
inst_2 : (i : ι) → Module.{u_1, u_11} k (V i)
inst_3 : (i : ι) → AddTorsor.{u_11, u_12} (V i) (P i)
i : ι
f : (i : ι) → P i
⊢ (proj (V := V) (P := P) i : (a : (i : ι) → P i) → P i) f = f i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
inst : Ring k
ι : Type u_10
V : ι → Type u_11
P : ι → Type u_12
inst_1 : (i : ι) → AddCommGroup (V i)
inst_2 : (i : ι) → Module.{u_1, u_11} k (V i)
inst_3 : (i : ι) → AddTorsor.{u_11, u_12} (V i) (P i)
i : ι
⊢ Eq (α := ((i : ι) → V i) →ₗ[k] V i) (linear (k := k) (P1 := (i : ι) → P i) (proj (V := V) (P := P) i))
    (LinearMap.proj (φ := V) i)

Tactic:
rfl

Premises used: LinearMap.proj, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
inst : Ring k
ι : Type u_10
V : ι → Type u_11
P : ι → Type u_12
inst_1 : (i : ι) → AddCommGroup (V i)
inst_2 : (i : ι) → Module.{u_1, u_11} k (V i)
inst_3 : (i : ι) → AddTorsor.{u_11, u_12} (V i) (P i)
f g : (i : ι) → P i
c : k
i : ι
⊢ Eq.{u_12 + 1} (α := P i) ((lineMap f g : (a : k) → (i : ι) → P i) c i : P i)
    ((lineMap (f i) (g i) : (a : k) → P i) c : P i)

Tactic:
(proj i : (∀ i, P i) →ᵃ[k] P i).apply_lineMap f g c

Premises used: AffineMap.apply_lineMap, AffineMap.proj
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
⊢ ∀ (x y : V1 →ᵃ[k] V2),
    ((x + y : (a : V1) → V2) 0, (x + y).linear) =
      HAdd.hAdd (α := V2 × (V1 →ₗ[k] V2)) (β := V2 × (V1 →ₗ[k] V2))
        (((x : (a : V1) → V2) 0, x.linear) : V2 × (V1 →ₗ[k] V2))
        (((y : (a : V1) → V2) 0, y.linear) : V2 × (V1 →ₗ[k] V2))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
⊢ ∀ (m : R) (x : V1 →ᵃ[k] V2),
    ((m • x : (a : V1) → V2) 0, (m • x).linear) =
      HSMul.hSMul (α := R) (β := V2 × (V1 →ₗ[k] V2)) ((RingHom.id R : (a : R) → R) m : R)
        (((x : (a : V1) → V2) 0, x.linear) : V2 × (V1 →ₗ[k] V2))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
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)
⊢ (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

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
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
⊢ 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:
rw [f.decomp]

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

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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))).1 =
    (v, f).1

Tactic:
simp [const_linear]

Premises used: AffineMap.const_linear
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
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:
simp [const_linear]

Premises used: AffineMap.const_linear
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V2 : Type u_5
P2 : Type u_6
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : AddCommGroup V2
inst_4 : AffineSpace V2 P2
inst_5 : Module k V1
inst_6 : Module k V2
inst_7 : SMulCommClass k k V2
f g : P1 →ᵃ[k] P2
c : k
p : P1
⊢ Eq.{u_6 + 1} (α := P2) ((((lineMap f g : (a : k) → P1 →ᵃ[k] P2) c : P1 →ᵃ[k] P2) : (a : P1) → P2) p : P2)
    (((lineMap ((f : (a : P1) → P2) p) ((g : (a : P1) → P2) p) : k →ᵃ[k] P2) : (a : k) → P2) c : P2)

Tactic:
simp [AffineMap.lineMap_apply]

Premises used: AffineMap.lineMap_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
φp : ι → Type u_11
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_6 : (i : ι) → AddTorsor.{u_10, u_11} (φv i) (φp i)
fp : (i : ι) → AffineMap.{u_2, u_3, u_4, u_10, u_11} k P1 (φp i)
c : P1
i : ι
⊢ Eq.{u_11 + 1} (α := φp i) ((pi (φv := φv) (φp := φp) fp : (a : P1) → (i : ι) → φp i) c i : φp i)
    ((fp i : (a : P1) → φp i) c : φp i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
V3 : Type u_7
P3 : Type u_8
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : AddCommGroup V3
inst_4 : AffineSpace V3 P3
inst_5 : Module k V1
inst_6 : Module k V3
ι : Type u_9
φv : ι → Type u_10
φp : ι → Type u_11
inst_7 : (i : ι) → AddCommGroup (φv i)
inst_8 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_9 : (i : ι) → AddTorsor.{u_10, u_11} (φv i) (φp i)
fp : (i : ι) → AffineMap.{u_2, u_3, u_4, u_10, u_11} k P1 (φp i)
g : P3 →ᵃ[k] P1
⊢ (pi (φv := φv) (φp := φp) fp).comp g = pi (φv := φv) (φp := φp) fun (i : ι) ↦ (fp i).comp g

Tactic:
rfl

Premises used: AffineMap.pi, LinearMap.pi, AffineMap.comp, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
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)
⊢ pi (φv := φv) (φp := φv) fv = 0 ↔ ∀ (i : ι), fv i = 0

Tactic:
simp only [AffineMap.ext_iff, funext_iff, pi_apply]

Premises used: AffineMap.pi_apply, funext_iff, AffineMap.ext_iff
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
⊢ (∀ (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:
forall_comm

Premises used: forall_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
⊢ (∀ (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:
exact forall_comm

Premises used: forall_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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)
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)
⊢ Eq (α := P1 →ᵃ[k] (i : ι) → φv i) (pi (φv := φv) (φp := φv) fun (x : ι) ↦ 0) 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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)
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:
rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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
φp : ι → Type u_11
inst_4 : (i : ι) → AddCommGroup (φv i)
inst_5 : (i : ι) → Module.{u_2, u_10} k (φv i)
inst_6 : (i : ι) → AddTorsor.{u_10, u_11} (φv i) (φp i)
fp : (i : ι) → AffineMap.{u_2, u_3, u_4, u_10, u_11} k P1 (φp i)
i : ι
⊢ comp (proj (V := φv) (P := φp) i) (pi (φv := φv) (φp := φp) fp) = fp i

Tactic:
ext fun _ => rfl

Premises used: AffineMap.ext, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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)
p : (i : ι) → φv i
⊢ f = g

Tactic:
apply ext_linear

Premises used: AffineMap.ext_linear
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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₁ :
  ∀ (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)
⊢ f.linear = g.linear

Tactic:
apply LinearMap.pi_ext

Premises used: LinearMap.pi_ext
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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_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
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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)
⊢ (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)
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
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)
⊢ (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)