awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ (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₃

Premises used: vadd_eq_add, add_zero
-- 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)
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)
⊢ (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₃

Premises used: vadd_eq_add, add_zero
-- 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) (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_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
-- 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)
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_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₂

Premises used: Pi.single_zero
-- 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)
⊢ Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)

Tactic:
h₂
-- 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)
⊢ Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)

Tactic:
exact h₂
-- 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
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)
apply : Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)
⊢ f = g

Tactic:
apply pi_ext_zero h

Premises used: AffineMap.pi_ext_zero
-- 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
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)
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)
⊢ Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)

Tactic:
inhabit ι
-- 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
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)
inhabited_h : Inhabited ι
rw :
  Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) default 0) : P2)
    ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) default 0) : P2)
⊢ Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) 0 : P2) ((g : (a : (i : ι) → φv i) → P2) 0 : P2)

Tactic:
rw [← Pi.single_zero default]

Premises used: Inhabited.default, Pi.single_zero
-- 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
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)
inhabited_h : Inhabited ι
⊢ Eq.{u_6 + 1} (α := P2) ((f : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) default 0) : P2)
    ((g : (a : (i : ι) → φv i) → P2) (Pi.single (M := φv) default 0) : P2)

Tactic:
apply h
-- 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
inst_8 : Nonempty ι
h :
  ∀ (i : ι),
    Eq (α := φv i →ᵃ[k] P2) (f.comp (LinearMap.toAffineMap (LinearMap.single k φv i)))
      (g.comp (LinearMap.toAffineMap (LinearMap.single k φv i)))
⊢ f = g

Tactic:
pi_ext_nonempty fun i x => ?_

Premises used: AffineMap.pi_ext_nonempty
-- 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
inst_8 : Nonempty ι
h :
  ∀ (i : ι),
    Eq (α := φv i →ᵃ[k] P2) (f.comp (LinearMap.toAffineMap (LinearMap.single k φv i)))
      (g.comp (LinearMap.toAffineMap (LinearMap.single k φv i)))
refine :
  ∀ (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

Tactic:
refine pi_ext_nonempty fun i x => ?_

Premises used: AffineMap.pi_ext_nonempty
-- 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
inst_8 : Nonempty ι
h :
  ∀ (i : ι),
    Eq (α := φv i →ᵃ[k] P2) (f.comp (LinearMap.toAffineMap (LinearMap.single k φv i)))
      (g.comp (LinearMap.toAffineMap (LinearMap.single k φv i)))
i : ι
x : φv i
⊢ Eq.{u_6 + 1} (α := P2) ((f.comp (LinearMap.toAffineMap (LinearMap.single k φv i)) : (a : φv i) → P2) x : P2)
    ((g.comp (LinearMap.toAffineMap (LinearMap.single k φv i)) : (a : φv i) → P2) x : P2)

Tactic:
AffineMap.congr_fun (h i) x

Premises used: AffineMap.congr_fun
-- 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
inst_8 : Nonempty ι
h :
  ∀ (i : ι),
    Eq (α := φv i →ᵃ[k] P2) (f.comp (LinearMap.toAffineMap (LinearMap.single k φv i)))
      (g.comp (LinearMap.toAffineMap (LinearMap.single k φv i)))
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:
convert! AffineMap.congr_fun (h i) x

Premises used: AffineMap.congr_fun
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c : P1
r : k
⊢ homothety c r =
    HVAdd.hVAdd (β := P1 →ᵃ[k] P1) (r • VSub.vsub (P := P1 →ᵃ[k] P1) (id k P1) (const k P1 c)) (const k P1 c)

Tactic:
rfl

Premises used: AffineMap.homothety, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c : P1
r : k
⊢ Eq.{u_4 + 1} (α := (a : P1) → P1) (⇑(homothety c r) : (a : P1) → P1) fun (p : P1) ↦ r • (p -ᵥ c) +ᵥ c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c : P1
r : k
p : P1
⊢ (homothety c r : (a : P1) → P1) p = r • (p -ᵥ c) +ᵥ c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c : P1
r : k
⊢ linear (homothety c r) = HSMul.hSMul (β := V1 →ₗ[k] V1) r LinearMap.id

Tactic:
simp [homothety]

Premises used: AffineMap.homothety
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c : P1
r : k
p : P1
⊢ Eq (α := P1) ((homothety c r : (a : P1) → P1) p : P1) ((lineMap c p : (a : k) → P1) r : P1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c : P1
h : ∀ (p : P1), Eq (α := P1) ((homothety c 1 : (a : P1) → P1) p : P1) ((id k P1 : (a : P1) → P1) p : P1)
⊢ Eq (α := P1 →ᵃ[k] P1) (homothety c 1) (id k P1)

Tactic:
ext p
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c p : P1
⊢ Eq (α := P1) ((homothety c 1 : (a : P1) → P1) p : P1) ((id k P1 : (a : P1) → P1) p : P1)

Tactic:
simp [homothety_apply]

Premises used: AffineMap.homothety_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c : P1
r : k
⊢ (homothety c r : (a : P1) → P1) c = c

Tactic:
lineMap_same_apply c r

Premises used: AffineMap.lineMap_same_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c : P1
r₁ r₂ : k
p : P1
⊢ Eq (α := P1) ((homothety c (r₁ * r₂) : (a : P1) → P1) p : P1)
    ((homothety c r₁ : (a : P1) → P1) ((homothety c r₂ : (a : P1) → P1) p : P1) : P1)

Tactic:
simp only [homothety_apply, mul_smul, vadd_vsub]

Premises used: AffineMap.homothety_apply, vadd_vsub, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c : P1
r₁ r₂ : k
⊢ Eq (α := P1 →ᵃ[k] P1) (homothety c (r₁ * r₂)) (comp (homothety c r₁) (homothety c r₂))

Tactic:
ext <| homothety_mul_apply c r₁ r₂

Premises used: AffineMap.ext, AffineMap.homothety_mul_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c : P1
h : ∀ (p : P1), Eq (α := P1) ((homothety c 0 : (a : P1) → P1) p : P1) ((const k P1 c : (a : P1) → P1) p : P1)
⊢ Eq (α := P1 →ᵃ[k] P1) (homothety c 0) (const k P1 c)

Tactic:
ext p
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c p : P1
⊢ Eq (α := P1) ((homothety c 0 : (a : P1) → P1) p : P1) ((const k P1 c : (a : P1) → P1) p : P1)

Tactic:
simp [homothety_apply]

Premises used: AffineMap.homothety_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c : P1
r₁ r₂ : k
⊢ homothety c (r₁ + r₂) =
    HVAdd.hVAdd (β := P1 →ᵃ[k] P1) (r₁ • VSub.vsub (P := P1 →ᵃ[k] P1) (id k P1) (const k P1 c)) (homothety c r₂)

Tactic:
simp only [homothety_def, add_smul, vadd_vadd]

Premises used: vadd_vadd, add_smul, AffineMap.homothety_def
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c p q : P1
r₁ r₂ : k
h : r₁ * r₂ = 1
⊢ r₂ * r₁ = 1

Tactic:
mul_eq_one_comm.mp h

Premises used: Iff.mp, mul_eq_one_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c p q : P1
r₁ r₂ : k
h : r₁ * r₂ = 1
⊢ r₂ * r₁ = 1

Tactic:
obtain h' : r₂ * r₁ = 1 := mul_eq_one_comm.mp h

Premises used: Iff.mp, mul_eq_one_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c p q : P1
r₁ r₂ : k
h : r₁ * r₂ = 1
h' : r₂ * r₁ = 1
⊢ (homothety c r₁ : (a : P1) → P1) p = q ↔ (homothety c r₂ : (a : P1) → P1) q = p

Tactic:
⟨fun h1 ↦ ?_, fun h1 ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c p q : P1
r₁ r₂ : k
h : r₁ * r₂ = 1
h' : r₂ * r₁ = 1
refine_1 : ∀ (h1 : (homothety c r₁ : (a : P1) → P1) p = q), (homothety c r₂ : (a : P1) → P1) q = p
refine_2 : ∀ (h1 : (homothety c r₂ : (a : P1) → P1) q = p), (homothety c r₁ : (a : P1) → P1) p = q
⊢ (homothety c r₁ : (a : P1) → P1) p = q ↔ (homothety c r₂ : (a : P1) → P1) q = p

Tactic:
refine ⟨fun h1 ↦ ?_, fun h1 ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c p q : P1
r₁ r₂ : k
h : r₁ * r₂ = 1
h' : r₂ * r₁ = 1
h1 : (homothety c r₁ : (a : P1) → P1) p = q
refine_1 : (homothety c (r₂ * r₁) : (a : P1) → P1) p = p
⊢ (homothety c r₂ : (a : P1) → P1) q = p

Tactic:
rw [← h1, ← homothety_mul_apply]

Premises used: AffineMap.homothety_mul_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c p q : P1
r₁ r₂ : k
h : r₁ * r₂ = 1
h' : r₂ * r₁ = 1
h1 : (homothety c r₁ : (a : P1) → P1) p = q
⊢ (homothety c (r₂ * r₁) : (a : P1) → P1) p = p

Tactic:
simp [h, h']
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c p q : P1
r₁ r₂ : k
h : r₁ * r₂ = 1
h' : r₂ * r₁ = 1
h1 : (homothety c r₂ : (a : P1) → P1) q = p
refine_2 : (homothety c (r₁ * r₂) : (a : P1) → P1) q = q
⊢ (homothety c r₁ : (a : P1) → P1) p = q

Tactic:
rw [← h1, ← homothety_mul_apply]

Premises used: AffineMap.homothety_mul_apply
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
c p q : P1
r₁ r₂ : k
h : r₁ * r₂ = 1
h' : r₂ * r₁ = 1
h1 : (homothety c r₂ : (a : P1) → P1) q = p
⊢ (homothety c (r₁ * r₂) : (a : P1) → P1) q = q

Tactic:
simp [h, h']
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
inst_4 : IsTorsionFree k V1
inst_5 : IsCancelMulZero k
c : P1
r : k
hr : r ≠ 0
x x_1 : P1
h : Eq (α := P1) ((homothety c r : (a : P1) → P1) x : P1) ((homothety c r : (a : P1) → P1) x_1 : P1)
⊢ x = x_1

Tactic:
simpa [homothety_def, hr] using h

Premises used: AffineMap.homothety_def
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_2
V1 : Type u_3
P1 : Type u_4
inst : CommRing k
inst_1 : AddCommGroup V1
inst_2 : AffineSpace V1 P1
inst_3 : Module k V1
inst_4 : IsTorsionFree k V1
inst_5 : IsCancelMulZero k
c : P1
r : k
hr : r ≠ 0
p q : P1
⊢ Eq (α := P1) ((homothety c r : (a : P1) → P1) p : P1) ((homothety c r : (a : P1) → P1) q : P1) ↔ p = q

Tactic:
(homothety_injective c hr).eq_iff

Premises used: Function.Injective.eq_iff, AffineMap.homothety_injective