awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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₂
⊢ 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₂
have rw₅ : c₁ - c₂ = 0 ∨ p₁ -ᵥ p₀ = 0 ↔ 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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₂
⊢ 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₂
have rw₆ : c₁ = c₂ ∨ p₁ -ᵥ p₀ = 0 ↔ 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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₂
⊢ 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₂
have rw₇ : c₁ = c₂ ∨ p₁ = p₀ ↔ 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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₂
⊢ 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₂
have rw₈ : p₁ = p₀ ∨ c₁ = c₂ ↔ 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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₂
⊢ 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₂
have rw₉ : p₀ = p₁ ∨ c₁ = c₂ ↔ 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ (lineMap p₀ p₁ : (a : k) → P1) c = p₀ ↔ p₀ = p₁ ∨ c = 0
have 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)
Tactic: rw [← @lineMap_eq_lineMap_iff k V1, lineMap_apply_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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)
⊢ (lineMap p₀ p₁ : (a : k) → P1) c = p₀ ↔ p₀ = p₁ ∨ c = 0
have rw₁ : (lineMap p₀ p₁ : (a : k) → P1) c = p₀ ↔ (lineMap p₀ p₁ : (a : k) → P1) c = p₀
Tactic: rw [← @lineMap_eq_lineMap_iff k V1, lineMap_apply_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ (lineMap p₀ p₁ : (a : k) → P1) c = p₁ ↔ p₀ = p₁ ∨ c = 1
have 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)
Tactic: rw [← @lineMap_eq_lineMap_iff k V1, lineMap_apply_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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)
⊢ (lineMap p₀ p₁ : (a : k) → P1) c = p₁ ↔ p₀ = p₁ ∨ c = 1
have rw₁ : (lineMap p₀ p₁ : (a : k) → P1) c = p₁ ↔ (lineMap p₀ p₁ : (a : k) → P1) c = p₁
Tactic: rw [← @lineMap_eq_lineMap_iff k V1, lineMap_apply_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ Eq.{u_3 + 1} (α := P1) ((lineMap p₀ p₁ : (a : k) → P1) (1 - c) : P1) ((lineMap p₁ p₀ : (a : k) → P1) c : P1)
have 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)
Tactic: rw [lineMap_symm p₀, comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ 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)
have h : (lineMap 1 0 : (a : k) → k) (1 - c) = c
Tactic: congr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ p₀ -ᵥ (lineMap p₀ p₁ : (a : k) → P1) c = c • (p₀ -ᵥ p₁)
have rw : -((lineMap p₀ p₁ : (a : k) → P1) c -ᵥ p₀) = c • (p₀ -ᵥ p₁)
Tactic: rw [← neg_vsub_eq_vsub_rev, lineMap_vsub_left, ← smul_neg, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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₁)
⊢ p₀ -ᵥ (lineMap p₀ p₁ : (a : k) → P1) c = c • (p₀ -ᵥ p₁)
have rw₁ : -(c • (p₁ -ᵥ p₀)) = c • (p₀ -ᵥ p₁)
Tactic: rw [← neg_vsub_eq_vsub_rev, lineMap_vsub_left, ← smul_neg, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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₁)
⊢ p₀ -ᵥ (lineMap p₀ p₁ : (a : k) → P1) c = c • (p₀ -ᵥ p₁)
have rw₂ : c • -(p₁ -ᵥ p₀) = c • (p₀ -ᵥ p₁)
Tactic: rw [← neg_vsub_eq_vsub_rev, lineMap_vsub_left, ← smul_neg, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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₁)
⊢ p₀ -ᵥ (lineMap p₀ p₁ : (a : k) → P1) c = c • (p₀ -ᵥ p₁)
have rw₃ : c • (p₀ -ᵥ p₁) = c • (p₀ -ᵥ p₁)
Tactic: rw [← neg_vsub_eq_vsub_rev, lineMap_vsub_left, ← smul_neg, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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₁ = (1 - c) • (p₀ -ᵥ p₁)
have rw : (lineMap p₁ p₀ : (a : k) → P1) (1 - c) -ᵥ p₁ = (1 - c) • (p₀ -ᵥ p₁)
Tactic: rw [← lineMap_apply_one_sub, lineMap_vsub_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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₁)
⊢ (lineMap p₀ p₁ : (a : k) → P1) c -ᵥ p₁ = (1 - c) • (p₀ -ᵥ p₁)
have rw₁ : (1 - c) • (p₀ -ᵥ p₁) = (1 - c) • (p₀ -ᵥ p₁)
Tactic: rw [← lineMap_apply_one_sub, lineMap_vsub_left]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ p₁ -ᵥ (lineMap p₀ p₁ : (a : k) → P1) c = (1 - c) • (p₁ -ᵥ p₀)
have rw : p₁ -ᵥ (lineMap p₁ p₀ : (a : k) → P1) (1 - c) = (1 - c) • (p₁ -ᵥ p₀)
Tactic: rw [← lineMap_apply_one_sub, left_vsub_lineMap]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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₀)
⊢ p₁ -ᵥ (lineMap p₀ p₁ : (a : k) → P1) c = (1 - c) • (p₁ -ᵥ p₀)
have rw₁ : (1 - c) • (p₁ -ᵥ p₀) = (1 - c) • (p₁ -ᵥ p₀)
Tactic: rw [← lineMap_apply_one_sub, left_vsub_lineMap]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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 ((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)
have 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)
Tactic: simp_rw [lineMap_apply_one_sub, ← lineMap_apply_one_sub p₁, lineMap_lineMap_right]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [lineMap_apply_one_sub, ← lineMap_apply_one_sub p₁, lineMap_lineMap_right]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ LE.le.{u_2} (α := V1) ((lineMap p₀ p₁ : (a : k) → V1) x : V1) ((lineMap p₀ p₁ : (a : k) → V1) y : V1)
have suffices : x • (p₁ - p₀) ≤ y • (p₁ - p₀)
Tactic: suffices x • (p₁ - p₀) ≤ y • (p₁ - p₀) by simpa [lineMap]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ x • (p₁ - p₀) ≤ y • (p₁ - p₀)
have hb : 0 ≤ p₁ - p₀
Tactic: gcongr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ LE.le.{u_2} (α := V1) ((lineMap p₀ p₁ : (a : k) → V1) y : V1) ((lineMap p₀ p₁ : (a : k) → V1) x : V1)
have suffices : y • (p₁ - p₀) ≤ x • (p₁ - p₀)
Tactic: suffices y • (p₁ - p₀) ≤ x • (p₁ - p₀) by simpa [lineMap]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ y • (p₁ - p₀) ≤ x • (p₁ - p₀)
have rw : x • -(p₁ - p₀) ≤ y • -(p₁ - p₀)
Tactic: rw [← neg_le_neg_iff, ← smul_neg, ← smul_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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
⊢ x • -(p₁ - p₀) ≤ y • -(p₁ - p₀)
have hb : 0 ≤ -(p₁ - p₀)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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 : (a : V1) → V2) = HAdd.hAdd (α := (a : V1) → V2) (⇑f.linear : (a : V1) → V2) fun (x : V1) ↦ (f : (a : V1) → V2) 0
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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 : (a : V1) → V2) x =
    HVAdd.hVAdd (α := V2) (β := V2) ((f.linear : (a : V1) → V2) x : V2) ((f : (a : V1) → V2) 0 : V2)
have rw : Eq.{u_4 + 1} (α := V2) ((f : (a : V1) → V2) x : V2) ((f : (a : V1) → V2) (HVAdd.hVAdd (β := V1) x 0) : V2)
Tactic: rw [← f.map_vadd, vadd_eq_add, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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)
⊢ (f : (a : V1) → V2) x =
    HVAdd.hVAdd (α := V2) (β := V2) ((f.linear : (a : V1) → V2) x : V2) ((f : (a : V1) → V2) 0 : V2)
have rw₁ : Eq.{u_4 + 1} (α := V2) ((f : (a : V1) → V2) x : V2) ((f : (a : V1) → V2) (x + 0) : V2)
Tactic: rw [← f.map_vadd, vadd_eq_add, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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)
⊢ (f : (a : V1) → V2) x =
    HVAdd.hVAdd (α := V2) (β := V2) ((f.linear : (a : V1) → V2) x : V2) ((f : (a : V1) → V2) 0 : V2)
have rw₂ : Eq.{u_4 + 1} (α := V2) ((f : (a : V1) → V2) x : V2) ((f : (a : V1) → V2) x : V2)
Tactic: rw [← f.map_vadd, vadd_eq_add, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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 : (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
have f₁ : (f : (a : V1) → V2) x = HVAdd.hVAdd (α := V2) (β := V2) ((f.linear : (a : V1) → V2) x : V2) ((f : (a : V1) → V2) 0 : V2)
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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) = HSub.hSub (α := (a : V1) → V2) (⇑f : (a : V1) → V2) fun (x : V1) ↦ (f : (a : V1) → V2) 0
have 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
Tactic: rw [decomp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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))
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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)
    (((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)
have 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)
Tactic: change f x = x • (f 1 -ᵥ f 0) +ᵥ f 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
Goal:
k : Type u_10
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
f : k →ᵃ[k] k
a b x : 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)
have 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)
Tactic: rw [← f.linearMap_vsub, ← f.linear.map_smul, ← f.map_vadd]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (hypothesis)
Goal:
k : Type u_10
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
f : k →ᵃ[k] k
a b : k
⊢ 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)
have 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))
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.AffineMap (goal)
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) ((⇑f : (a : k) → k) '' Set.uIcc a b : Set k)
    (Set.uIcc ((f : (a : k) → k) a) ((f : (a : k) → k) b) : Set k)
have 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))
Tactic: rw [this, Set.image_comp]