awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module k E
inst_6 : IsStrictOrderedModule k E
inst_7 : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
rw : f (r • (b -ᵥ a) +ᵥ a) ≤ (lineMap (f a) (f b) : (a : k) → E) r ↔ slope f a (r • (b -ᵥ a) +ᵥ a) ≤ slope f a b
rw₁ : f (r • (b -ᵥ a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔ slope f a (r • (b -ᵥ a) +ᵥ a) ≤ slope f a b
rw₂ :
  f (r • (b -ᵥ a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔
    ((r • (b -ᵥ a) +ᵥ a) - a)⁻¹ • (f (r • (b -ᵥ a) +ᵥ a) -ᵥ f a) ≤ slope f a b
rw₃ :
  f (r • (b -ᵥ a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔
    ((r • (b -ᵥ a) +ᵥ a) - a)⁻¹ • (f (r • (b -ᵥ a) +ᵥ a) -ᵥ f a) ≤ (b - a)⁻¹ • (f b -ᵥ f a)
rw₄ :
  f (r • (b - a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔
    ((r • (b - a) +ᵥ a) - a)⁻¹ • (f (r • (b - a) +ᵥ a) -ᵥ f a) ≤ (b - a)⁻¹ • (f b -ᵥ f a)
rw₅ :
  f (r • (b - a) +ᵥ a) ≤ r • (f b - f a) +ᵥ f a ↔
    ((r • (b - a) +ᵥ a) - a)⁻¹ • (f (r • (b - a) +ᵥ a) -ᵥ f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₆ :
  f (r • (b - a) +ᵥ a) ≤ r • (f b - f a) +ᵥ f a ↔
    ((r • (b - a) +ᵥ a) - a)⁻¹ • (f (r • (b - a) +ᵥ a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₇ :
  f (r • (b - a) + a) ≤ r • (f b - f a) +ᵥ f a ↔
    (r • (b - a) + a - a)⁻¹ • (f (r • (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₈ :
  f (r • (b - a) + a) ≤ r • (f b - f a) + f a ↔
    (r • (b - a) + a - a)⁻¹ • (f (r • (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₉ :
  f (r * (b - a) + a) ≤ r • (f b - f a) + f a ↔
    (r * (b - a) + a - a)⁻¹ • (f (r * (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₁₀ :
  f (r * (b - a) + a) ≤ r • (f b - f a) + f a ↔ (r * (b - a))⁻¹ • (f (r * (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₁₁ :
  f (r * (b - a) + a) ≤ r • f b - r • f a + f a ↔
    (r * (b - a))⁻¹ • (f (r * (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₁₂ :
  f (r * (b - a) + a) ≤ r • f b - r • f a + f a ↔
    (r * (b - a))⁻¹ • f (r * (b - a) + a) - (r * (b - a))⁻¹ • f a ≤ (b - a)⁻¹ • (f b - f a)
⊢ f ((lineMap a b : (a : k) → k) r) ≤ (lineMap (f a) (f b) : (a : k) → E) r ↔
    slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f a b
have rw₁₃ : f (r * (b - a) + a) ≤ r • f b - r • f a + f a ↔
  (r * (b - a))⁻¹ • f (r * (b - a) + a) - (r * (b - a))⁻¹ • f a ≤ (b - a)⁻¹ • f b - (b - a)⁻¹ • f a
Tactic: rw [lineMap_apply, lineMap_apply, slope, slope, vsub_eq_sub, vsub_eq_sub, vsub_eq_sub,
    vadd_eq_add, vadd_eq_add, smul_eq_mul, add_sub_cancel_right, smul_sub, smul_sub, smul_sub,
    sub_le_iff_le_add, mul_inv_rev, mul_smul, mul_smul, ← smul_sub, ← smul_sub, ← smul_add,
    smul_smul, ← mul_inv_rev, inv_smul_le_iff_of_pos h, smul_smul,
    mul_inv_cancel_right₀ (right_ne_zero_of_mul h.ne'), smul_add,
    smul_inv_smul₀ (left_ne_zero_of_mul h.ne')]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module k E
inst_6 : IsStrictOrderedModule k E
inst_7 : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
rw : f (r • (b -ᵥ a) +ᵥ a) ≤ (lineMap (f a) (f b) : (a : k) → E) r ↔ slope f a (r • (b -ᵥ a) +ᵥ a) ≤ slope f a b
rw₁ : f (r • (b -ᵥ a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔ slope f a (r • (b -ᵥ a) +ᵥ a) ≤ slope f a b
rw₂ :
  f (r • (b -ᵥ a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔
    ((r • (b -ᵥ a) +ᵥ a) - a)⁻¹ • (f (r • (b -ᵥ a) +ᵥ a) -ᵥ f a) ≤ slope f a b
rw₃ :
  f (r • (b -ᵥ a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔
    ((r • (b -ᵥ a) +ᵥ a) - a)⁻¹ • (f (r • (b -ᵥ a) +ᵥ a) -ᵥ f a) ≤ (b - a)⁻¹ • (f b -ᵥ f a)
rw₄ :
  f (r • (b - a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔
    ((r • (b - a) +ᵥ a) - a)⁻¹ • (f (r • (b - a) +ᵥ a) -ᵥ f a) ≤ (b - a)⁻¹ • (f b -ᵥ f a)
rw₅ :
  f (r • (b - a) +ᵥ a) ≤ r • (f b - f a) +ᵥ f a ↔
    ((r • (b - a) +ᵥ a) - a)⁻¹ • (f (r • (b - a) +ᵥ a) -ᵥ f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₆ :
  f (r • (b - a) +ᵥ a) ≤ r • (f b - f a) +ᵥ f a ↔
    ((r • (b - a) +ᵥ a) - a)⁻¹ • (f (r • (b - a) +ᵥ a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₇ :
  f (r • (b - a) + a) ≤ r • (f b - f a) +ᵥ f a ↔
    (r • (b - a) + a - a)⁻¹ • (f (r • (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₈ :
  f (r • (b - a) + a) ≤ r • (f b - f a) + f a ↔
    (r • (b - a) + a - a)⁻¹ • (f (r • (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₉ :
  f (r * (b - a) + a) ≤ r • (f b - f a) + f a ↔
    (r * (b - a) + a - a)⁻¹ • (f (r * (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₁₀ :
  f (r * (b - a) + a) ≤ r • (f b - f a) + f a ↔ (r * (b - a))⁻¹ • (f (r * (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₁₁ :
  f (r * (b - a) + a) ≤ r • f b - r • f a + f a ↔
    (r * (b - a))⁻¹ • (f (r * (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₁₂ :
  f (r * (b - a) + a) ≤ r • f b - r • f a + f a ↔
    (r * (b - a))⁻¹ • f (r * (b - a) + a) - (r * (b - a))⁻¹ • f a ≤ (b - a)⁻¹ • (f b - f a)
rw₁₃ :
  f (r * (b - a) + a) ≤ r • f b - r • f a + f a ↔
    (r * (b - a))⁻¹ • f (r * (b - a) + a) - (r * (b - a))⁻¹ • f a ≤ (b - a)⁻¹ • f b - (b - a)⁻¹ • f a
⊢ f ((lineMap a b : (a : k) → k) r) ≤ (lineMap (f a) (f b) : (a : k) → E) r ↔
    slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f a b
have rw₁₄ : f (r * (b - a) + a) ≤ r • f b - r • f a + f a ↔
  (r * (b - a))⁻¹ • f (r * (b - a) + a) ≤ (b - a)⁻¹ • f b - (b - a)⁻¹ • f a + (r * (b - a))⁻¹ • f a
Tactic: rw [lineMap_apply, lineMap_apply, slope, slope, vsub_eq_sub, vsub_eq_sub, vsub_eq_sub,
    vadd_eq_add, vadd_eq_add, smul_eq_mul, add_sub_cancel_right, smul_sub, smul_sub, smul_sub,
    sub_le_iff_le_add, mul_inv_rev, mul_smul, mul_smul, ← smul_sub, ← smul_sub, ← smul_add,
    smul_smul, ← mul_inv_rev, inv_smul_le_iff_of_pos h, smul_smul,
    mul_inv_cancel_right₀ (right_ne_zero_of_mul h.ne'), smul_add,
    smul_inv_smul₀ (left_ne_zero_of_mul h.ne')]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module k E
inst_6 : IsStrictOrderedModule k E
inst_7 : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < r * (b - a)
rw : f (r • (b -ᵥ a) +ᵥ a) ≤ (lineMap (f a) (f b) : (a : k) → E) r ↔ slope f a (r • (b -ᵥ a) +ᵥ a) ≤ slope f a b
rw₁ : f (r • (b -ᵥ a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔ slope f a (r • (b -ᵥ a) +ᵥ a) ≤ slope f a b
rw₂ :
  f (r • (b -ᵥ a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔
    ((r • (b -ᵥ a) +ᵥ a) - a)⁻¹ • (f (r • (b -ᵥ a) +ᵥ a) -ᵥ f a) ≤ slope f a b
rw₃ :
  f (r • (b -ᵥ a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔
    ((r • (b -ᵥ a) +ᵥ a) - a)⁻¹ • (f (r • (b -ᵥ a) +ᵥ a) -ᵥ f a) ≤ (b - a)⁻¹ • (f b -ᵥ f a)
rw₄ :
  f (r • (b - a) +ᵥ a) ≤ r • (f b -ᵥ f a) +ᵥ f a ↔
    ((r • (b - a) +ᵥ a) - a)⁻¹ • (f (r • (b - a) +ᵥ a) -ᵥ f a) ≤ (b - a)⁻¹ • (f b -ᵥ f a)
rw₅ :
  f (r • (b - a) +ᵥ a) ≤ r • (f b - f a) +ᵥ f a ↔
    ((r • (b - a) +ᵥ a) - a)⁻¹ • (f (r • (b - a) +ᵥ a) -ᵥ f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₆ :
  f (r • (b - a) +ᵥ a) ≤ r • (f b - f a) +ᵥ f a ↔
    ((r • (b - a) +ᵥ a) - a)⁻¹ • (f (r • (b - a) +ᵥ a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₇ :
  f (r • (b - a) + a) ≤ r • (f b - f a) +ᵥ f a ↔
    (r • (b - a) + a - a)⁻¹ • (f (r • (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₈ :
  f (r • (b - a) + a) ≤ r • (f b - f a) + f a ↔
    (r • (b - a) + a - a)⁻¹ • (f (r • (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₉ :
  f (r * (b - a) + a) ≤ r • (f b - f a) + f a ↔
    (r * (b - a) + a - a)⁻¹ • (f (r * (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₁₀ :
  f (r * (b - a) + a) ≤ r • (f b - f a) + f a ↔ (r * (b - a))⁻¹ • (f (r * (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₁₁ :
  f (r * (b - a) + a) ≤ r • f b - r • f a + f a ↔
    (r * (b - a))⁻¹ • (f (r * (b - a) + a) - f a) ≤ (b - a)⁻¹ • (f b - f a)
rw₁₂ :
  f (r * (b - a) + a) ≤ r • f b - r • f a + f a ↔
    (r * (b - a))⁻¹ • f (r * (b - a) + a) - (r * (b - a))⁻¹ • f a ≤ (b - a)⁻¹ • (f b - f a)
rw₁₃ :
  f (r * (b - a) + a) ≤ r • f b - r • f a + f a ↔
    (r * (b - a))⁻¹ • f (r * (b - a) + a) - (r * (b - a))⁻¹ • f a ≤ (b - a)⁻¹ • f b - (b - a)⁻¹ • f a
rw₁₄ :
  f (r * (b - a) + a) ≤ r • f b - r • f a + f a ↔
    (r * (b - a))⁻¹ • f (r * (b - a) + a) ≤ (b - a)⁻¹ • f b - (b - a)⁻¹ • f a + (r * (b - a))⁻¹ • f a
⊢ f ((lineMap a b : (a : k) → k) r) ≤ (lineMap (f a) (f b) : (a : k) → E) r ↔
    slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f a b
have rw₁₅ : f (r * (b - a) + a) ≤ r • f b - r • f a + f a ↔
  ((b - a)⁻¹ * r⁻¹) • f (r * (b - a) + a) ≤ (b - a)⁻¹ • f b - (b - a)⁻¹ • f a + ((b - a)⁻¹ * r⁻¹) • f a
Tactic: rw [lineMap_apply, lineMap_apply, slope, slope, vsub_eq_sub, vsub_eq_sub, vsub_eq_sub,
    vadd_eq_add, vadd_eq_add, smul_eq_mul, add_sub_cancel_right, smul_sub, smul_sub, smul_sub,
    sub_le_iff_le_add, mul_inv_rev, mul_smul, mul_smul, ← smul_sub, ← smul_sub, ← smul_add,
    smul_smul, ← mul_inv_rev, inv_smul_le_iff_of_pos h, smul_smul,
    mul_inv_cancel_right₀ (right_ne_zero_of_mul h.ne'), smul_add,
    smul_inv_smul₀ (left_ne_zero_of_mul h.ne')]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module k E
inst_6 : IsStrictOrderedModule k E
inst_7 : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < (1 - r) * (b - a)
⊢ f ((lineMap a b : (a : k) → k) r) ≤ (lineMap (f a) (f b) : (a : k) → E) r ↔
    slope f a b ≤ slope f ((lineMap a b : (a : k) → k) r) b
have rw : f ((lineMap b a : (a : k) → k) (1 - r)) ≤ (lineMap (f b) (f a) : (a : k) → E) (1 - r) ↔
  slope f a b ≤ slope f ((lineMap b a : (a : k) → k) (1 - r)) b
Tactic: rw [← lineMap_apply_one_sub, ← lineMap_apply_one_sub _ _ r]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module k E
inst_6 : IsStrictOrderedModule k E
inst_7 : PosSMulReflectLE k E
f : k → E
a b r : k
h : 0 < (1 - r) * (b - a)
⊢ f ((lineMap b a : (a : k) → k) (1 - r)) ≤ (lineMap (f b) (f a) : (a : k) → E) (1 - r) ↔
    slope f a b ≤ slope f ((lineMap b a : (a : k) → k) (1 - r)) b
have revert : ∀ (h : 0 < (1 - r) * (b - a)),
  f ((lineMap b a : (a : k) → k) (1 - r)) ≤ (lineMap (f b) (f a) : (a : k) → E) (1 - r) ↔
    slope f a b ≤ slope f ((lineMap b a : (a : k) → k) (1 - r)) b
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module k E
inst_6 : IsStrictOrderedModule k E
inst_7 : PosSMulReflectLE k E
f : k → E
a b r : k
⊢ ∀ (h : 0 < (1 - r) * (b - a)),
    f ((lineMap b a : (a : k) → k) (1 - r)) ≤ (lineMap (f b) (f a) : (a : k) → E) (1 - r) ↔
      slope f a b ≤ slope f ((lineMap b a : (a : k) → k) (1 - r)) b
have generalize : ∀ (r' : k) (h : 0 < r' * (b - a)),
  f ((lineMap b a : (a : k) → k) r') ≤ (lineMap (f b) (f a) : (a : k) → E) r' ↔
    slope f a b ≤ slope f ((lineMap b a : (a : k) → k) r') b
Tactic: generalize 1 - r = r'
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module k E
inst_6 : IsStrictOrderedModule k E
inst_7 : PosSMulReflectLE k E
f : k → E
a b r' : k
h : 0 < r' * (b - a)
⊢ f ((lineMap b a : (a : k) → k) r') ≤ (lineMap (f b) (f a) : (a : k) → E) r' ↔
    slope f a b ≤ slope f ((lineMap b a : (a : k) → k) r') b
have simp_rw : f (r' * (a - b) + b) ≤ r' • (f a - f b) + f b ↔
  (b - a)⁻¹ • (f b - f a) ≤ (b - (r' * (a - b) + b))⁻¹ • (f b - f (r' * (a - b) + b))
Tactic: simp_rw [lineMap_apply, slope, vsub_eq_sub, vadd_eq_add, smul_eq_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module k E
inst_6 : IsStrictOrderedModule k E
inst_7 : PosSMulReflectLE k E
f : k → E
a b r' : k
h : 0 < r' * (b - a)
⊢ f (r' * (a - b) + b) ≤ r' • (f a - f b) + f b ↔
    (b - a)⁻¹ • (f b - f a) ≤ (b - (r' * (a - b) + b))⁻¹ • (f b - f (r' * (a - b) + b))
have h₁ : b - a ≠ 0
Tactic: rw [sub_add_eq_sub_sub_swap, sub_self, zero_sub, neg_mul_eq_mul_neg, neg_sub,
    le_inv_smul_iff_of_pos h, smul_smul, mul_inv_cancel_right₀, le_sub_comm, ← neg_sub (f b),
    smul_neg, neg_add_eq_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
inst_8 : PosSMulReflectLE k E
f : k → E
a b r : k
hab : a < b
h₀ : 0 < r
h₁ : r < 1
⊢ f ((lineMap a b : (a : k) → k) r) ≤ (lineMap (f a) (f b) : (a : k) → E) r ↔
    slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f ((lineMap a b : (a : k) → k) r) b
have rw : slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f a b ↔
  slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f ((lineMap a b : (a : k) → k) r) b
Tactic: rw [map_le_lineMap_iff_slope_le_slope_left (mul_pos h₀ (sub_pos.2 hab)), ←
    lineMap_slope_lineMap_slope_lineMap f a b r, right_le_lineMap_iff_le h₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
inst_8 : PosSMulReflectLE k E
f : k → E
a b r : k
hab : a < b
h₀ : 0 < r
h₁ : r < 1
rw :
  slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f a b ↔
    slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f ((lineMap a b : (a : k) → k) r) b
⊢ f ((lineMap a b : (a : k) → k) r) ≤ (lineMap (f a) (f b) : (a : k) → E) r ↔
    slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f ((lineMap a b : (a : k) → k) r) b
have rw₁ : slope f a ((lineMap a b : (a : k) → k) r) ≤
    (lineMap (slope f ((lineMap a b : (a : k) → k) r) b) (slope f a ((lineMap a b : (a : k) → k) r)) : (a : k) → E) r ↔
  slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f ((lineMap a b : (a : k) → k) r) b
Tactic: rw [map_le_lineMap_iff_slope_le_slope_left (mul_pos h₀ (sub_pos.2 hab)), ←
    lineMap_slope_lineMap_slope_lineMap f a b r, right_le_lineMap_iff_le h₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
inst_3 : AddCommGroup E
inst_4 : PartialOrder E
inst_5 : IsOrderedAddMonoid E
inst_6 : Module k E
inst_7 : IsStrictOrderedModule k E
inst_8 : PosSMulReflectLE k E
f : k → E
a b r : k
hab : a < b
h₀ : 0 < r
h₁ : r < 1
rw :
  slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f a b ↔
    slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f ((lineMap a b : (a : k) → k) r) b
rw₁ :
  slope f a ((lineMap a b : (a : k) → k) r) ≤
      (lineMap (slope f ((lineMap a b : (a : k) → k) r) b) (slope f a ((lineMap a b : (a : k) → k) r)) : (a : k) → E)
        r ↔
    slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f ((lineMap a b : (a : k) → k) r) b
⊢ f ((lineMap a b : (a : k) → k) r) ≤ (lineMap (f a) (f b) : (a : k) → E) r ↔
    slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f ((lineMap a b : (a : k) → k) r) b
have rw₂ : slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f ((lineMap a b : (a : k) → k) r) b ↔
  slope f a ((lineMap a b : (a : k) → k) r) ≤ slope f ((lineMap a b : (a : k) → k) r) b
Tactic: rw [map_le_lineMap_iff_slope_le_slope_left (mul_pos h₀ (sub_pos.2 hab)), ←
    lineMap_slope_lineMap_slope_lineMap f a b r, right_le_lineMap_iff_le h₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
f : 𝕜 → 𝕜
x₀ b : 𝕜
hb : b < x₀
⊢ 0 < slope f x₀ b ↔ f b < f x₀
have rw : 0 < slope f b x₀ ↔ f b < f x₀
Tactic: rw [slope_comm, slope_pos_iff hb]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Ordered (goal)
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
f : 𝕜 → 𝕜
x₀ b : 𝕜
hb : b < x₀
rw : 0 < slope f b x₀ ↔ f b < f x₀
⊢ 0 < slope f x₀ b ↔ f b < f x₀
have rw₁ : f b < f x₀ ↔ f b < f x₀
Tactic: rw [slope_comm, slope_pos_iff hb]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Pointwise (goal)
Goal:
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
v : V
⊢ HVAdd.hVAdd (β := AffineSubspace k P) v ⊥ = ⊥
have h : ∀ (x : P), x ∈ HVAdd.hVAdd (β := AffineSubspace k P) v ⊥ ↔ Membership.mem (γ := AffineSubspace k P) ⊥ x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Pointwise (goal)
Goal:
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
v : V
⊢ HVAdd.hVAdd (β := AffineSubspace k P) v ⊤ = ⊤
have h : ∀ (x : P), x ∈ HVAdd.hVAdd (β := AffineSubspace k P) v ⊤ ↔ Membership.mem (γ := AffineSubspace k P) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Pointwise (goal)
Goal:
k : Type u_2
V : Type u_3
P : Type u_4
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : AffineSpace V P
v : V
s : AffineSubspace k P
⊢ (v +ᵥ s).direction = s.direction
have rw : Submodule.map (AffineMap.linear (↑(AffineEquiv.constVAdd k P v) : P →ᵃ[k] P)) s.direction = s.direction
Tactic: rw [pointwise_vadd_eq_map, map_direction]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Pointwise (goal)
Goal:
k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
⊢ map f (v +ᵥ s) = HVAdd.hVAdd.{u_7, u_8, u_8} (α := V₂) ((f.linear : (a : V₁) → V₂) v : V₂) (map f s)
have rw : map (f.comp (↑(AffineEquiv.constVAdd k P₁ v) : P₁ →ᵃ[k] P₁)) s =
  map (AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ ((f.linear : (a : V₁) → V₂) v)) : P₂ →ᵃ[k] P₂) f) s
Tactic: rw [pointwise_vadd_eq_map, pointwise_vadd_eq_map, map_map, map_map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Pointwise (goal)
Goal:
k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
⊢ map (f.comp (↑(AffineEquiv.constVAdd k P₁ v) : P₁ →ᵃ[k] P₁)) s =
    map (AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ ((f.linear : (a : V₁) → V₂) v)) : P₂ →ᵃ[k] P₂) f) s
have e_f : f.comp (↑(AffineEquiv.constVAdd k P₁ v) : P₁ →ᵃ[k] P₁) =
  AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ ((f.linear : (a : V₁) → V₂) v)) : P₂ →ᵃ[k] P₂) f
Tactic: congr 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Pointwise (goal)
Goal:
k : Type u_2
V₁ : Type u_5
P₁ : Type u_6
V₂ : Type u_7
P₂ : Type u_8
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : Module k V₁
inst_3 : AffineSpace V₁ P₁
inst_4 : AddCommGroup V₂
inst_5 : Module k V₂
inst_6 : AffineSpace V₂ P₂
f : P₁ →ᵃ[k] P₂
v : V₁
s : AffineSubspace k P₁
⊢ f.comp (↑(AffineEquiv.constVAdd k P₁ v) : P₁ →ᵃ[k] P₁) =
    AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ ((f.linear : (a : V₁) → V₂) v)) : P₂ →ᵃ[k] P₂) f
have e_f : ∀ (p : P₁),
  Eq.{u_8 + 1} (α := P₂) ((f.comp (↑(AffineEquiv.constVAdd k P₁ v) : P₁ →ᵃ[k] P₁) : (a : P₁) → P₂) p : P₂)
    ((AffineMap.comp (↑(AffineEquiv.constVAdd k P₂ ((f.linear : (a : V₁) → V₂) v)) : P₂ →ᵃ[k] P₂) f : (a : P₁) → P₂) p :
      P₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Pointwise (goal)
Goal:
M : Type u_1
k : Type u_2
V : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : DistribSMul M V
inst_4 : SMulCommClass M k V
a : M
⊢ HSMul.hSMul (β := AffineSubspace k V) a ⊥ = ⊥
have h : ∀ (x : V), x ∈ HSMul.hSMul (β := AffineSubspace k V) a ⊥ ↔ Membership.mem (γ := AffineSubspace k V) ⊥ x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Pointwise (goal)
Goal:
M : Type u_1
k : Type u_2
V : Type u_3
inst : Ring k
inst_1 : AddCommGroup V
inst_2 : Module k V
inst_3 : Monoid M
inst_4 : DistribMulAction M V
inst_5 : SMulCommClass M k V
a : M
ha : IsUnit a
⊢ HSMul.hSMul (β := AffineSubspace k V) a ⊤ = ⊤
have h : ∀ (x : V), x ∈ HSMul.hSMul (β := AffineSubspace k V) a ⊤ ↔ Membership.mem (γ := AffineSubspace k V) ⊤ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Pointwise (goal)
Goal:
k : Type u_2
V : Type u_3
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
a : k
ha : a ≠ 0
s : AffineSubspace k V
⊢ DistribSMul.toLinearMap k V a = HSMul.hSMul (β := V →ₗ[k] V) a LinearMap.id
have h : ∀ (x : V),
  Eq (α := V) ((DistribSMul.toLinearMap k V a : (a : V) → V) x : V)
    ((HSMul.hSMul (β := V →ₗ[k] V) a LinearMap.id : (a : V) → V) x : V)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Pointwise (hypothesis)
Goal:
k : Type u_2
V : Type u_3
inst : Field k
inst_1 : AddCommGroup V
inst_2 : Module k V
a : k
ha : a ≠ 0
s : AffineSubspace k V
⊢ (a • s).direction = s.direction
have this : DistribSMul.toLinearMap k V a = HSMul.hSMul (β := V →ₗ[k] V) a LinearMap.id
Tactic: have : DistribSMul.toLinearMap k V a = a • LinearMap.id := by
    ext; simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Restrict (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
E : AffineSubspace k P₁
Ene : Nonempty.{u_3 + 1} ↥E
φ : P₁ →ᵃ[k] P₂
⊢ Nonempty.{u_5 + 1} ↥(map φ E)
have obtain : ∀ (x : P₁) (hx : x ∈ E), Nonempty.{u_5 + 1} ↥(map φ E)
Tactic: obtain ⟨x, hx⟩ := id Ene
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Restrict (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
hEF : AffineSubspace.map φ E ≤ F
⊢ AffineMap.{u_1, u_2, u_3, u_4, u_5} k ↥E ↥F
have refine_1 : ↥E → ↥F
Tactic: refine ⟨?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Restrict (goal)
Goal:
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst : Ring k
inst_1 : AddCommGroup V₁
inst_2 : AddCommGroup V₂
inst_3 : Module k V₁
inst_4 : Module k V₂
inst_5 : AddTorsor V₁ P₁
inst_6 : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst_7 : Nonempty.{u_3 + 1} ↥E
inst_8 : Nonempty.{u_5 + 1} ↥F
hEF : AffineSubspace.map φ E ≤ F
refine_1 : ↥E → ↥F
⊢ AffineMap.{u_1, u_2, u_3, u_4, u_5} k ↥E ↥F
have refine_2 : LinearMap.{u_1, u_1, u_2, u_4} (RingHom.id k) ↥E.direction ↥F.direction
Tactic: refine ⟨?_, ?_, ?_⟩