awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
inst : Ring k
a b c : k
⊢ (lineMap a b : (a : k) → k) c = c * (b - a) + a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
inst : Ring k
a b c : k
⊢ (lineMap a b : (a : k) → k) c = (1 - c) * a + c * b

Tactic:
lineMap_apply_module a b c

Premises used: AffineMap.lineMap_apply_module
-- 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
v : V1
c : k
rw : c • ((v +ᵥ p) -ᵥ p) +ᵥ p = c • v +ᵥ p
rw₁ rw₂ : c • v +ᵥ p = c • v +ᵥ p
⊢ (lineMap p (v +ᵥ p) : (a : k) → P1) c = c • v +ᵥ p

Tactic:
rw [lineMap_apply, vadd_vsub]

Premises used: AffineMap.lineMap_apply, vadd_vsub
-- 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 (α := k →ₗ[k] V1) (linear (lineMap p₀ p₁)) (LinearMap.smulRight LinearMap.id (p₁ -ᵥ p₀))

Tactic:
add_zero _

Premises used: LinearMap.smulRight, add_zero
-- 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
c : k
⊢ (lineMap p p : (a : k) → P1) c = p

Tactic:
simp [lineMap_apply]

Premises used: AffineMap.lineMap_apply
-- 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
⊢ Eq (α := k →ᵃ[k] P1) (lineMap p p) (const k k p)

Tactic:
ext <| lineMap_same_apply p

Premises used: AffineMap.ext, AffineMap.lineMap_same_apply
-- 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
⊢ (lineMap p₀ p₁ : (a : k) → P1) 0 = p₀

Tactic:
simp [lineMap_apply]

Premises used: AffineMap.lineMap_apply
-- 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
⊢ (lineMap p₀ p₁ : (a : k) → P1) 1 = p₁

Tactic:
simp [lineMap_apply]

Premises used: AffineMap.lineMap_apply
-- 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
inst_4 : IsDomain k
inst_5 : IsTorsionFree k V1
p₀ p₁ : P1
c₁ c₂ : k
rw : c₁ • (p₁ -ᵥ p₀) +ᵥ p₀ = (lineMap p₀ p₁ : (a : k) → P1) c₂ ↔ p₀ = p₁ ∨ c₁ = c₂
rw₁ : c₁ • (p₁ -ᵥ p₀) +ᵥ p₀ = c₂ • (p₁ -ᵥ p₀) +ᵥ p₀ ↔ p₀ = p₁ ∨ c₁ = c₂
rw₂ : (c₁ • (p₁ -ᵥ p₀) +ᵥ p₀) -ᵥ (c₂ • (p₁ -ᵥ p₀) +ᵥ p₀) = 0 ↔ p₀ = p₁ ∨ c₁ = c₂
rw₃ : c₁ • (p₁ -ᵥ p₀) - c₂ • (p₁ -ᵥ p₀) = 0 ↔ p₀ = p₁ ∨ c₁ = c₂
rw₄ : (c₁ - c₂) • (p₁ -ᵥ p₀) = 0 ↔ p₀ = p₁ ∨ c₁ = c₂
rw₅ : c₁ - c₂ = 0 ∨ p₁ -ᵥ p₀ = 0 ↔ p₀ = p₁ ∨ c₁ = c₂
rw₆ : c₁ = c₂ ∨ p₁ -ᵥ p₀ = 0 ↔ p₀ = p₁ ∨ c₁ = c₂
rw₇ : c₁ = c₂ ∨ p₁ = p₀ ↔ p₀ = p₁ ∨ c₁ = c₂
rw₈ : p₁ = p₀ ∨ c₁ = c₂ ↔ p₀ = p₁ ∨ c₁ = c₂
rw₉ rw₁₀ : p₀ = p₁ ∨ c₁ = c₂ ↔ p₀ = p₁ ∨ c₁ = c₂
⊢ Eq.{u_3 + 1} (α := P1) ((lineMap p₀ p₁ : (a : k) → P1) c₁ : P1) ((lineMap p₀ p₁ : (a : k) → P1) c₂ : P1) ↔
    p₀ = p₁ ∨ c₁ = c₂

Tactic:
rw [lineMap_apply, lineMap_apply, ← @vsub_eq_zero_iff_eq V1, vadd_vsub_vadd_cancel_right, ←
    sub_smul, smul_eq_zero, sub_eq_zero, vsub_eq_zero_iff_eq, or_comm, eq_comm]

Premises used: sub_eq_zero, vsub_eq_zero_iff_eq, sub_smul, vadd_vsub_vadd_cancel_right, eq_comm, AffineMap.lineMap_apply, or_comm, smul_eq_zero
-- 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
inst_4 : IsDomain k
inst_5 : IsTorsionFree k V1
p₀ p₁ : P1
c : k
rw :
  (lineMap p₀ p₁ : (a : k) → P1) c = p₀ ↔
    Eq.{u_3 + 1} (α := P1) ((lineMap p₀ p₁ : (a : k) → P1) c : P1) ((lineMap p₀ p₁ : (a : k) → P1) 0 : P1)
rw₁ rw₂ : (lineMap p₀ p₁ : (a : k) → P1) c = p₀ ↔ (lineMap p₀ p₁ : (a : k) → P1) c = p₀
⊢ (lineMap p₀ p₁ : (a : k) → P1) c = p₀ ↔ p₀ = p₁ ∨ c = 0

Tactic:
rw [← @lineMap_eq_lineMap_iff k V1, lineMap_apply_zero]

Premises used: AffineMap.lineMap_eq_lineMap_iff, AffineMap.lineMap_apply_zero
-- 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
inst_4 : IsDomain k
inst_5 : IsTorsionFree k V1
p₀ p₁ : P1
c : k
rw :
  (lineMap p₀ p₁ : (a : k) → P1) c = p₁ ↔
    Eq.{u_3 + 1} (α := P1) ((lineMap p₀ p₁ : (a : k) → P1) c : P1) ((lineMap p₀ p₁ : (a : k) → P1) 1 : P1)
rw₁ rw₂ : (lineMap p₀ p₁ : (a : k) → P1) c = p₁ ↔ (lineMap p₀ p₁ : (a : k) → P1) c = p₁
⊢ (lineMap p₀ p₁ : (a : k) → P1) c = p₁ ↔ p₀ = p₁ ∨ c = 1

Tactic:
rw [← @lineMap_eq_lineMap_iff k V1, lineMap_apply_one]

Premises used: AffineMap.lineMap_eq_lineMap_iff, AffineMap.lineMap_apply_one
-- 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
inst_4 : IsDomain k
inst_5 : IsTorsionFree k V1
p₀ p₁ : P1
h : p₀ ≠ p₁
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (α := k) (β := P1) (⇑(lineMap p₀ p₁) : (a : k) → P1)

Tactic:
fun _c₁ _c₂ hc =>
  (lineMap_eq_lineMap_iff.mp hc).resolve_left h

Premises used: Or.resolve_left, AffineMap.lineMap_eq_lineMap_iff, Iff.mp, Function.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
p₀ p₁ : P1
c : k
⊢ Eq.{u_5 + 1} (α := P2) ((f : (a : P1) → P2) ((lineMap p₀ p₁ : (a : k) → P1) c : P1) : P2)
    (((lineMap ((f : (a : P1) → P2) p₀) ((f : (a : P1) → P2) p₁) : k →ᵃ[k] P2) : (a : k) → P2) c : P2)

Tactic:
simp [lineMap_apply]

Premises used: AffineMap.lineMap_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
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₀ p₁ : P1
⊢ f.comp (lineMap p₀ p₁) = lineMap ((f : (a : P1) → P2) p₀) ((f : (a : P1) → P2) p₁)

Tactic:
ext <| f.apply_lineMap p₀ p₁

Premises used: AffineMap.ext, AffineMap.apply_lineMap
-- 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
p₀ p₁ : P1 × P2
c : k
⊢ Eq.{u_3 + 1} (α := P1) (((lineMap p₀ p₁ : (a : k) → P1 × P2) c).1 : P1) ((lineMap p₀.1 p₁.1 : (a : k) → P1) c : P1)

Tactic:
fst.apply_lineMap p₀ p₁ c

Premises used: AffineMap.fst, AffineMap.apply_lineMap
-- 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
p₀ p₁ : P1 × P2
c : k
⊢ Eq.{u_5 + 1} (α := P2) (((lineMap p₀ p₁ : (a : k) → P1 × P2) c).2 : P2) ((lineMap p₀.2 p₁.2 : (a : k) → P2) c : P2)

Tactic:
snd.apply_lineMap p₀ p₁ c

Premises used: AffineMap.apply_lineMap, AffineMap.snd
-- 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 (α := k →ᵃ[k] P1) (lineMap p₀ p₁) (comp (lineMap p₁ p₀) (lineMap 1 0))

Tactic:
simp
-- 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
rw :
  Eq.{u_3 + 1} (α := P1) ((lineMap p₁ p₀ : (a : k) → P1) ((lineMap 1 0 : (a : k) → k) (1 - c) : k) : P1)
    ((lineMap p₁ p₀ : (a : k) → P1) c : P1)
⊢ Eq.{u_3 + 1} (α := P1) ((lineMap p₀ p₁ : (a : k) → P1) (1 - c) : P1) ((lineMap p₁ p₀ : (a : k) → P1) c : P1)

Tactic:
rw [lineMap_symm p₀, comp_apply]

Premises used: AffineMap.comp_apply, AffineMap.lineMap_symm
-- 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
h : (lineMap 1 0 : (a : k) → k) (1 - c) = c
⊢ Eq.{u_3 + 1} (α := P1) ((lineMap p₁ p₀ : (a : k) → P1) ((lineMap 1 0 : (a : k) → k) (1 - c) : k) : P1)
    ((lineMap p₁ p₀ : (a : k) → P1) c : P1)

Tactic:
congr
-- 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 1 0 : (a : k) → k) (1 - c) = c

Tactic:
simp [lineMap_apply]

Premises used: AffineMap.lineMap_apply
-- 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 -ᵥ p₀ = c • (p₁ -ᵥ p₀)

Tactic:
vadd_vsub _ _

Premises used: vadd_vsub
-- 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
rw : -((lineMap p₀ p₁ : (a : k) → P1) c -ᵥ p₀) = c • (p₀ -ᵥ p₁)
rw₁ : -(c • (p₁ -ᵥ p₀)) = c • (p₀ -ᵥ p₁)
rw₂ : c • -(p₁ -ᵥ p₀) = c • (p₀ -ᵥ p₁)
rw₃ rw₄ : c • (p₀ -ᵥ p₁) = c • (p₀ -ᵥ p₁)
⊢ p₀ -ᵥ (lineMap p₀ p₁ : (a : k) → P1) c = c • (p₀ -ᵥ p₁)

Tactic:
rw [← neg_vsub_eq_vsub_rev, lineMap_vsub_left, ← smul_neg, neg_vsub_eq_vsub_rev]

Premises used: AffineMap.lineMap_vsub_left, smul_neg, neg_vsub_eq_vsub_rev
-- 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
rw : (lineMap p₁ p₀ : (a : k) → P1) (1 - c) -ᵥ p₁ = (1 - c) • (p₀ -ᵥ p₁)
rw₁ rw₂ : (1 - c) • (p₀ -ᵥ p₁) = (1 - c) • (p₀ -ᵥ p₁)
⊢ (lineMap p₀ p₁ : (a : k) → P1) c -ᵥ p₁ = (1 - c) • (p₀ -ᵥ p₁)

Tactic:
rw [← lineMap_apply_one_sub, lineMap_vsub_left]

Premises used: AffineMap.lineMap_vsub_left, AffineMap.lineMap_apply_one_sub
-- 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
rw : p₁ -ᵥ (lineMap p₁ p₀ : (a : k) → P1) (1 - c) = (1 - c) • (p₁ -ᵥ p₀)
rw₁ rw₂ : (1 - c) • (p₁ -ᵥ p₀) = (1 - c) • (p₁ -ᵥ p₀)
⊢ p₁ -ᵥ (lineMap p₀ p₁ : (a : k) → P1) c = (1 - c) • (p₁ -ᵥ p₀)

Tactic:
rw [← lineMap_apply_one_sub, left_vsub_lineMap]

Premises used: AffineMap.left_vsub_lineMap, AffineMap.lineMap_apply_one_sub
-- 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
v₁ v₂ : V1
p₁ p₂ : P1
c : k
⊢ HVAdd.hVAdd.{u_2, u_3, u_3} (α := V1) (β := P1) ((lineMap v₁ v₂ : (a : k) → V1) c : V1)
      ((lineMap p₁ p₂ : (a : k) → P1) c : P1) =
    (lineMap (v₁ +ᵥ p₁) (v₂ +ᵥ p₂) : (a : k) → P1) c

Tactic:
((fst : V1 × P1 →ᵃ[k] V1) +ᵥ (snd : V1 × P1 →ᵃ[k] P1)).apply_lineMap (v₁, p₁) (v₂, p₂) c

Premises used: AffineMap.fst, AffineMap.apply_lineMap, Prod.mk, HVAdd.hVAdd, AffineMap.snd
-- 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₂ p₃ p₄ : P1
c : k
⊢ VSub.vsub.{u_2, u_3} (P := P1) ((lineMap p₁ p₂ : (a : k) → P1) c : P1) ((lineMap p₃ p₄ : (a : k) → P1) c : P1) =
    (lineMap (p₁ -ᵥ p₃) (p₂ -ᵥ p₄) : (a : k) → V1) c

Tactic:
((fst : P1 × P1 →ᵃ[k] P1) -ᵥ (snd : P1 × P1 →ᵃ[k] P1)).apply_lineMap (_, _) (_, _) c

Premises used: AffineMap.fst, AffineMap.apply_lineMap, Prod.mk, VSub.vsub, AffineMap.snd
-- 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 d : k
⊢ Eq.{u_3 + 1} (α := P1) ((lineMap p₀ ((lineMap p₀ p₁ : (a : k) → P1) c) : (a : k) → P1) d : P1)
    ((lineMap p₀ p₁ : (a : k) → P1) (d * c) : P1)

Tactic:
simp [lineMap_apply, mul_smul]

Premises used: AffineMap.lineMap_apply, SemigroupAction.mul_smul
-- 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 d : k
simp_rw :
  Eq.{u_3 + 1} (α := P1) (((lineMap ((lineMap p₀ p₁ : (a : k) → P1) c) p₁ : k →ᵃ[k] P1) : (a : k) → P1) d : P1)
    ((lineMap p₁ p₀ : (a : k) → P1) ((1 - d) * (1 - c)) : P1)
simp_rw₁ :
  Eq.{u_3 + 1} (α := P1) ((lineMap p₁ ((lineMap p₁ p₀ : (a : k) → P1) (1 - c)) : (a : k) → P1) (1 - d) : P1)
    ((lineMap p₁ p₀ : (a : k) → P1) ((1 - d) * (1 - c)) : P1)
⊢ Eq.{u_3 + 1} (α := P1) (((lineMap ((lineMap p₀ p₁ : (a : k) → P1) c) p₁ : k →ᵃ[k] P1) : (a : k) → P1) d : P1)
    ((lineMap p₀ p₁ : (a : k) → P1) (1 - (1 - d) * (1 - c)) : P1)

Tactic:
simp_rw [lineMap_apply_one_sub, ← lineMap_apply_one_sub p₁, lineMap_lineMap_right]

Premises used: AffineMap.lineMap_lineMap_right, AffineMap.lineMap_apply_one_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
inst_3 : LinearOrder k
inst_4 : Preorder V1
inst_5 : AddRightMono V1
inst_6 : SMulPosMono k V1
p₀ p₁ : V1
h : p₀ ≤ p₁
x y : k
hxy : x ≤ y
this : x • (p₁ - p₀) ≤ y • (p₁ - p₀)
⊢ LE.le.{u_2} (α := V1) ((lineMap p₀ p₁ : (a : k) → V1) x : V1) ((lineMap p₀ p₁ : (a : k) → V1) y : V1)

Tactic:
simpa [lineMap]

Premises used: AffineMap.lineMap
-- 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
inst_3 : LinearOrder k
inst_4 : Preorder V1
inst_5 : AddRightMono V1
inst_6 : SMulPosMono k V1
p₀ p₁ : V1
h : p₀ ≤ p₁
x y : k
hxy : x ≤ y
suffices : x • (p₁ - p₀) ≤ y • (p₁ - p₀)
⊢ LE.le.{u_2} (α := V1) ((lineMap p₀ p₁ : (a : k) → V1) x : V1) ((lineMap p₀ p₁ : (a : k) → V1) y : V1)

Tactic:
suffices x • (p₁ - p₀) ≤ y • (p₁ - p₀) by simpa [lineMap]
-- 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
inst_3 : LinearOrder k
inst_4 : Preorder V1
inst_5 : AddRightMono V1
inst_6 : SMulPosMono k V1
p₀ p₁ : V1
h : p₀ ≤ p₁
x y : k
hxy : x ≤ y
hb : 0 ≤ p₁ - p₀
⊢ x • (p₁ - p₀) ≤ y • (p₁ - p₀)

Tactic:
gcongr
-- 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
inst_3 : LinearOrder k
inst_4 : Preorder V1
inst_5 : AddRightMono V1
inst_6 : SMulPosMono k V1
p₀ p₁ : V1
h : p₀ ≤ p₁
x y : k
hxy : x ≤ y
⊢ 0 ≤ p₁ - p₀

Tactic:
simpa
-- 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
inst_3 : LinearOrder k
inst_4 : Preorder V1
inst_5 : AddLeftMono V1
inst_6 : SMulPosMono k V1
p₀ p₁ : V1
h : p₁ ≤ p₀
x y : k
hxy : x ≤ y
this : y • (p₁ - p₀) ≤ x • (p₁ - p₀)
⊢ LE.le.{u_2} (α := V1) ((lineMap p₀ p₁ : (a : k) → V1) y : V1) ((lineMap p₀ p₁ : (a : k) → V1) x : V1)

Tactic:
simpa [lineMap]

Premises used: AffineMap.lineMap
-- 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
inst_3 : LinearOrder k
inst_4 : Preorder V1
inst_5 : AddLeftMono V1
inst_6 : SMulPosMono k V1
p₀ p₁ : V1
h : p₁ ≤ p₀
x y : k
hxy : x ≤ y
suffices : y • (p₁ - p₀) ≤ x • (p₁ - p₀)
⊢ LE.le.{u_2} (α := V1) ((lineMap p₀ p₁ : (a : k) → V1) y : V1) ((lineMap p₀ p₁ : (a : k) → V1) x : V1)

Tactic:
suffices y • (p₁ - p₀) ≤ x • (p₁ - p₀) by simpa [lineMap]
-- 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
inst_3 : LinearOrder k
inst_4 : Preorder V1
inst_5 : AddLeftMono V1
inst_6 : SMulPosMono k V1
p₀ p₁ : V1
h : p₁ ≤ p₀
x y : k
hxy : x ≤ y
rw : x • -(p₁ - p₀) ≤ y • -(p₁ - p₀)
⊢ y • (p₁ - p₀) ≤ x • (p₁ - p₀)

Tactic:
rw [← neg_le_neg_iff, ← smul_neg, ← smul_neg]

Premises used: smul_neg, neg_le_neg_iff
-- 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
inst_3 : LinearOrder k
inst_4 : Preorder V1
inst_5 : AddLeftMono V1
inst_6 : SMulPosMono k V1
p₀ p₁ : V1
h : p₁ ≤ p₀
x y : k
hxy : x ≤ y
hb : 0 ≤ -(p₁ - p₀)
⊢ x • -(p₁ - p₀) ≤ y • -(p₁ - p₀)

Tactic:
gcongr
-- 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
inst_3 : LinearOrder k
inst_4 : Preorder V1
inst_5 : AddLeftMono V1
inst_6 : SMulPosMono k V1
p₀ p₁ : V1
h : p₁ ≤ p₀
x y : k
hxy : x ≤ y
⊢ 0 ≤ -(p₁ - p₀)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AddCommGroup V2
inst_4 : Module k V2
f : V1 →ᵃ[k] V2
h :
  ∀ (x : V1),
    (f : (a : V1) → V2) x =
      HAdd.hAdd (α := (a : V1) → V2) (β := V1 → V2) (⇑f.linear : (a : V1) → V2) (fun (x : V1) ↦ (f : (a : V1) → V2) 0) x
⊢ (⇑f : (a : V1) → V2) = HAdd.hAdd (α := (a : V1) → V2) (⇑f.linear : (a : V1) → V2) fun (x : V1) ↦ (f : (a : V1) → V2) 0

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AddCommGroup V2
inst_4 : Module k V2
f : V1 →ᵃ[k] V2
x : V1
rw : Eq.{u_4 + 1} (α := V2) ((f : (a : V1) → V2) x : V2) ((f : (a : V1) → V2) (HVAdd.hVAdd (β := V1) x 0) : V2)
rw₁ : Eq.{u_4 + 1} (α := V2) ((f : (a : V1) → V2) x : V2) ((f : (a : V1) → V2) (x + 0) : V2)
rw₂ rw₃ : Eq.{u_4 + 1} (α := V2) ((f : (a : V1) → V2) x : V2) ((f : (a : V1) → V2) x : V2)
⊢ (f : (a : V1) → V2) x =
    HVAdd.hVAdd (α := V2) (β := V2) ((f.linear : (a : V1) → V2) x : V2) ((f : (a : V1) → V2) 0 : V2)

Tactic:
rw [← f.map_vadd, vadd_eq_add, add_zero]

Premises used: AffineMap.map_vadd, vadd_eq_add, add_zero
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AddCommGroup V2
inst_4 : Module k V2
f : V1 →ᵃ[k] V2
x : V1
⊢ HVAdd.hVAdd (α := V2) (β := V2) ((f.linear : (a : V1) → V2) x : V2) ((f : (a : V1) → V2) 0 : V2) =
    HAdd.hAdd (α := (a : V1) → V2) (β := V1 → V2) (⇑f.linear : (a : V1) → V2) (fun (x : V1) ↦ (f : (a : V1) → V2) 0) x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AddCommGroup V2
inst_4 : Module k V2
f : V1 →ᵃ[k] V2
x : V1
f₁ :
  (f : (a : V1) → V2) x =
    HVAdd.hVAdd (α := V2) (β := V2) ((f.linear : (a : V1) → V2) x : V2) ((f : (a : V1) → V2) 0 : V2)
⊢ (f : (a : V1) → V2) x =
    HAdd.hAdd (α := (a : V1) → V2) (β := V1 → V2) (⇑f.linear : (a : V1) → V2) (fun (x : V1) ↦ (f : (a : V1) → V2) 0) x

Tactic:
calc
    f x = f.linear x +ᵥ f 0 := by rw [← f.map_vadd, vadd_eq_add, add_zero]
    _ = (f.linear + fun _ : V1 => f 0) x := rfl

Premises used: HAdd.hAdd, AffineMap.linear, OfNat.ofNat, DFunLike.coe, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AddCommGroup V2
inst_4 : Module k V2
f : V1 →ᵃ[k] V2
rw :
  (⇑f.linear : (a : V1) → V2) =
    (HAdd.hAdd (α := (a : V1) → V2) (⇑f.linear : (a : V1) → V2) fun (x : V1) ↦ (f : (a : V1) → V2) 0) - fun (x : V1) ↦
      HAdd.hAdd (α := (a : V1) → V2) (β := V1 → V2) (⇑f.linear : (a : V1) → V2) (fun (x : V1) ↦ (f : (a : V1) → V2) 0) 0
⊢ (⇑f.linear : (a : V1) → V2) = HSub.hSub (α := (a : V1) → V2) (⇑f : (a : V1) → V2) fun (x : V1) ↦ (f : (a : V1) → V2) 0

Tactic:
rw [decomp]

Premises used: AffineMap.decomp
-- Module: Mathlib.LinearAlgebra.AffineSpace.AffineMap
Goal:
k : Type u_1
V1 : Type u_2
V2 : Type u_4
inst : Ring k
inst_1 : AddCommGroup V1
inst_2 : Module k V1
inst_3 : AddCommGroup V2
inst_4 : Module k V2
f : V1 →ᵃ[k] V2
⊢ (⇑f.linear : (a : V1) → V2) =
    (HAdd.hAdd (α := (a : V1) → V2) (⇑f.linear : (a : V1) → V2) fun (x : V1) ↦ (f : (a : V1) → V2) 0) - fun (x : V1) ↦
      HAdd.hAdd (α := (a : V1) → V2) (β := V1 → V2) (⇑f.linear : (a : V1) → V2) (fun (x : V1) ↦ (f : (a : V1) → V2) 0) 0

Tactic:
simp only [map_zero, Pi.add_apply, add_sub_cancel_right, zero_add]

Premises used: map_zero, zero_add, Pi.add_apply, add_sub_cancel_right
-- 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
h :
  ∀ (x : k),
    Eq (α := k) ((f : (a : k) → k) x : 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))
          x :
        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:
ext x
-- 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 x : k
h :
  (f : (a : k) → k) x =
    HVAdd.hVAdd (β := k) (x • VSub.vsub (P := k) ((f : (a : k) → k) 1 : k) ((f : (a : k) → k) 0 : k))
      ((f : (a : k) → k) 0 : k)
⊢ Eq (α := k) ((f : (a : k) → k) x : 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))
        x :
      k)

Tactic:
change f x = x • (f 1 -ᵥ f 0) +ᵥ f 0

Premises used: VSub.vsub, OfNat.ofNat, DFunLike.coe
-- 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 x : k
h : Eq (α := k) ((f : (a : k) → k) x : k) ((f : (a : k) → k) (HVAdd.hVAdd (β := k) (x • VSub.vsub (P := k) 1 0) 0) : k)
⊢ (f : (a : k) → k) x =
    HVAdd.hVAdd (β := k) (x • VSub.vsub (P := k) ((f : (a : k) → k) 1 : k) ((f : (a : k) → k) 0 : k))
      ((f : (a : k) → k) 0 : k)

Tactic:
rw [← f.linearMap_vsub, ← f.linear.map_smul, ← f.map_vadd]

Premises used: AffineMap.linearMap_vsub, AffineMap.map_vadd, LinearMap.map_smul, AffineMap.linear
-- 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 x : k
⊢ Eq (α := k) ((f : (a : k) → k) x : k) ((f : (a : k) → k) (HVAdd.hVAdd (β := k) (x • VSub.vsub (P := k) 1 0) 0) : k)

Tactic:
simp only [vsub_eq_sub, add_zero, mul_one, vadd_eq_add, sub_zero, smul_eq_mul]

Premises used: sub_zero, vadd_eq_add, smul_eq_mul, mul_one, add_zero, vsub_eq_sub