awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
h : r = (a - ((1 - r) * a + r * b)) / (a - b)
h₁ : r * (a - b) = a - ((1 - r) * a + r * b)
⊢ r = HSub.hSub (β := k) a ((lineMap a b : (a : k) → k) r : k) / (a - b)
have h₂ : r * (a - b) = a - (1 * a - r * a + r * b)
Tactic: rw [lineMap_apply_ring, eq_div_iff (sub_ne_zero.2 hab), sub_mul, one_mul, mul_sub, ← sub_sub,
    sub_sub_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
h : r = (a - ((1 - r) * a + r * b)) / (a - b)
h₁ : r * (a - b) = a - ((1 - r) * a + r * b)
h₂ : r * (a - b) = a - (1 * a - r * a + r * b)
⊢ r = HSub.hSub (β := k) a ((lineMap a b : (a : k) → k) r : k) / (a - b)
have h₃ : r * (a - b) = a - (a - r * a + r * b)
Tactic: rw [lineMap_apply_ring, eq_div_iff (sub_ne_zero.2 hab), sub_mul, one_mul, mul_sub, ← sub_sub,
    sub_sub_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
h : r = (a - ((1 - r) * a + r * b)) / (a - b)
h₁ : r * (a - b) = a - ((1 - r) * a + r * b)
h₂ : r * (a - b) = a - (1 * a - r * a + r * b)
h₃ : r * (a - b) = a - (a - r * a + r * b)
⊢ r = HSub.hSub (β := k) a ((lineMap a b : (a : k) → k) r : k) / (a - b)
have h₄ : r * a - r * b = a - (a - r * a + r * b)
Tactic: rw [lineMap_apply_ring, eq_div_iff (sub_ne_zero.2 hab), sub_mul, one_mul, mul_sub, ← sub_sub,
    sub_sub_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
h : r = (a - ((1 - r) * a + r * b)) / (a - b)
h₁ : r * (a - b) = a - ((1 - r) * a + r * b)
h₂ : r * (a - b) = a - (1 * a - r * a + r * b)
h₃ : r * (a - b) = a - (a - r * a + r * b)
h₄ : r * a - r * b = a - (a - r * a + r * b)
⊢ r = HSub.hSub (β := k) a ((lineMap a b : (a : k) → k) r : k) / (a - b)
have h₅ : r * a - r * b = a - (a - r * a) - r * b
Tactic: rw [lineMap_apply_ring, eq_div_iff (sub_ne_zero.2 hab), sub_mul, one_mul, mul_sub, ← sub_sub,
    sub_sub_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
PE : Type u_3
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : AddTorsor E PE
f : k → PE
a b r : k
hab : a ≠ b
h : r = (a - ((1 - r) * a + r * b)) / (a - b)
h₁ : r * (a - b) = a - ((1 - r) * a + r * b)
h₂ : r * (a - b) = a - (1 * a - r * a + r * b)
h₃ : r * (a - b) = a - (a - r * a + r * b)
h₄ : r * a - r * b = a - (a - r * a + r * b)
h₅ : r * a - r * b = a - (a - r * a) - r * b
⊢ r = HSub.hSub (β := k) a ((lineMap a b : (a : k) → k) r : k) / (a - b)
have h₆ : r * a - r * b = r * a - r * b
Tactic: rw [lineMap_apply_ring, eq_div_iff (sub_ne_zero.2 hab), sub_mul, one_mul, mul_sub, ← sub_sub,
    sub_sub_cancel]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
⊢ 0 ≤ slope f x y ↔ f x ≤ f y
have pos : ∀ (hxeqy : x = y), 0 ≤ slope f x y ↔ f x ≤ f y
Tactic: by_cases hxeqy : x = y
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
pos : ∀ (hxeqy : x = y), 0 ≤ slope f x y ↔ f x ≤ f y
⊢ 0 ≤ slope f x y ↔ f x ≤ f y
have neg : ∀ (hxeqy : ¬x = y), 0 ≤ slope f x y ↔ f x ≤ f y
Tactic: by_cases hxeqy : x = y
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
hxeqy : ¬x = y
⊢ 0 ≤ slope f x y ↔ f x ≤ f y
have neg : ∀ (h : 0 ≤ slope f x y), f x ≤ f y
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ smul_nonneg (inv_nonneg.2 (sub_nonneg.2 hxy)) ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
hxeqy : ¬x = y
neg : ∀ (h : 0 ≤ slope f x y), f x ≤ f y
⊢ 0 ≤ slope f x y ↔ f x ≤ f y
have neg₁ : ∀ (h : f x ≤ f y), 0 ≤ f y -ᵥ f x
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ smul_nonneg (inv_nonneg.2 (sub_nonneg.2 hxy)) ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (hypothesis)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
hxeqy : ¬x = y
h : 0 ≤ slope f x y
⊢ f x ≤ f y
have this : 0 ≤ (y - x) • slope f x y
Tactic: have := smul_nonneg (sub_nonneg.2 hxy) h
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
hxeqy : ¬x = y
h : 0 ≤ slope f x y
this : 0 ≤ (y - x) • slope f x y
⊢ f x ≤ f y
have neg : ∀ (this : 0 ≤ (y - x) • (y - x)⁻¹ • (f y -ᵥ f x)), f x ≤ f y
Tactic: rwa [slope, ← mul_smul, mul_inv_cancel₀ (mt sub_eq_zero.1 (Ne.symm hxeqy)), one_smul,
      vsub_eq_sub, sub_nonneg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
hxeqy : ¬x = y
h : 0 ≤ slope f x y
this : 0 ≤ (y - x) • slope f x y
neg : ∀ (this : 0 ≤ (y - x) • (y - x)⁻¹ • (f y -ᵥ f x)), f x ≤ f y
⊢ f x ≤ f y
have neg₁ : ∀ (this : 0 ≤ ((y - x) * (y - x)⁻¹) • (f y -ᵥ f x)), f x ≤ f y
Tactic: rwa [slope, ← mul_smul, mul_inv_cancel₀ (mt sub_eq_zero.1 (Ne.symm hxeqy)), one_smul,
      vsub_eq_sub, sub_nonneg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
hxeqy : ¬x = y
h : 0 ≤ slope f x y
this : 0 ≤ (y - x) • slope f x y
neg : ∀ (this : 0 ≤ (y - x) • (y - x)⁻¹ • (f y -ᵥ f x)), f x ≤ f y
neg₁ : ∀ (this : 0 ≤ ((y - x) * (y - x)⁻¹) • (f y -ᵥ f x)), f x ≤ f y
⊢ f x ≤ f y
have neg₂ : ∀ (this : 0 ≤ HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (f y -ᵥ f x)), f x ≤ f y
Tactic: rwa [slope, ← mul_smul, mul_inv_cancel₀ (mt sub_eq_zero.1 (Ne.symm hxeqy)), one_smul,
      vsub_eq_sub, sub_nonneg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
hxeqy : ¬x = y
h : 0 ≤ slope f x y
this : 0 ≤ (y - x) • slope f x y
neg : ∀ (this : 0 ≤ (y - x) • (y - x)⁻¹ • (f y -ᵥ f x)), f x ≤ f y
neg₁ : ∀ (this : 0 ≤ ((y - x) * (y - x)⁻¹) • (f y -ᵥ f x)), f x ≤ f y
neg₂ : ∀ (this : 0 ≤ HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (f y -ᵥ f x)), f x ≤ f y
⊢ f x ≤ f y
have neg₃ : ∀ (this : 0 ≤ f y -ᵥ f x), f x ≤ f y
Tactic: rwa [slope, ← mul_smul, mul_inv_cancel₀ (mt sub_eq_zero.1 (Ne.symm hxeqy)), one_smul,
      vsub_eq_sub, sub_nonneg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
hxeqy : ¬x = y
h : 0 ≤ slope f x y
this : 0 ≤ (y - x) • slope f x y
neg : ∀ (this : 0 ≤ (y - x) • (y - x)⁻¹ • (f y -ᵥ f x)), f x ≤ f y
neg₁ : ∀ (this : 0 ≤ ((y - x) * (y - x)⁻¹) • (f y -ᵥ f x)), f x ≤ f y
neg₂ : ∀ (this : 0 ≤ HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (f y -ᵥ f x)), f x ≤ f y
neg₃ : ∀ (this : 0 ≤ f y -ᵥ f x), f x ≤ f y
⊢ f x ≤ f y
have neg₄ : ∀ (this : 0 ≤ f y - f x), f x ≤ f y
Tactic: rwa [slope, ← mul_smul, mul_inv_cancel₀ (mt sub_eq_zero.1 (Ne.symm hxeqy)), one_smul,
      vsub_eq_sub, sub_nonneg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
hxeqy : ¬x = y
h : 0 ≤ slope f x y
this : 0 ≤ (y - x) • slope f x y
neg : ∀ (this : 0 ≤ (y - x) • (y - x)⁻¹ • (f y -ᵥ f x)), f x ≤ f y
neg₁ : ∀ (this : 0 ≤ ((y - x) * (y - x)⁻¹) • (f y -ᵥ f x)), f x ≤ f y
neg₂ : ∀ (this : 0 ≤ HSMul.hSMul.{u_1, u_2, u_2} (α := k) 1 (f y -ᵥ f x)), f x ≤ f y
neg₃ : ∀ (this : 0 ≤ f y -ᵥ f x), f x ≤ f y
neg₄ : ∀ (this : 0 ≤ f y - f x), f x ≤ f y
⊢ f x ≤ f y
have neg₅ : ∀ (this : f x ≤ f y), f x ≤ f y
Tactic: rwa [slope, ← mul_smul, mul_inv_cancel₀ (mt sub_eq_zero.1 (Ne.symm hxeqy)), one_smul,
      vsub_eq_sub, sub_nonneg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
hxeqy : ¬x = y
h : f x ≤ f y
⊢ 0 ≤ f y -ᵥ f x
have neg : 0 ≤ f y - f x
Tactic: rwa [vsub_eq_sub, sub_nonneg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
s : Set k
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
⊢ 0 ≤ slope f x y
have inl : ∀ (hxy : x ≤ y), 0 ≤ slope f x y
Tactic: rcases le_total x y with hxy | hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
s : Set k
hf : MonotoneOn f s
hx : x ∈ s
hy : y ∈ s
inl : ∀ (hxy : x ≤ y), 0 ≤ slope f x y
⊢ 0 ≤ slope f x y
have inr : ∀ (hxy : y ≤ x), 0 ≤ slope f x y
Tactic: rcases le_total x y with hxy | hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
⊢ 0 < slope f x y ↔ f x < f y
have simp_rw : 0 ≤ slope f x y ∧ 0 ≠ slope f x y ↔ f x ≤ f y ∧ f x ≠ f y
Tactic: simp_rw [lt_iff_le_and_ne, slope_nonneg_iff_of_le hxy, Ne, eq_comm, slope_eq_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
simp_rw : 0 ≤ slope f x y ∧ 0 ≠ slope f x y ↔ f x ≤ f y ∧ f x ≠ f y
⊢ 0 < slope f x y ↔ f x < f y
have simp_rw₁ : f x ≤ f y ∧ 0 ≠ slope f x y ↔ f x ≤ f y ∧ f x ≠ f y
Tactic: simp_rw [lt_iff_le_and_ne, slope_nonneg_iff_of_le hxy, Ne, eq_comm, slope_eq_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
simp_rw : 0 ≤ slope f x y ∧ 0 ≠ slope f x y ↔ f x ≤ f y ∧ f x ≠ f y
simp_rw₁ : f x ≤ f y ∧ 0 ≠ slope f x y ↔ f x ≤ f y ∧ f x ≠ f y
⊢ 0 < slope f x y ↔ f x < f y
have simp_rw₂ : f x ≤ f y ∧ ¬0 = slope f x y ↔ f x ≤ f y ∧ ¬f x = f y
Tactic: simp_rw [lt_iff_le_and_ne, slope_nonneg_iff_of_le hxy, Ne, eq_comm, slope_eq_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
hxy : x ≤ y
simp_rw : 0 ≤ slope f x y ∧ 0 ≠ slope f x y ↔ f x ≤ f y ∧ f x ≠ f y
simp_rw₁ : f x ≤ f y ∧ 0 ≠ slope f x y ↔ f x ≤ f y ∧ f x ≠ f y
simp_rw₂ : f x ≤ f y ∧ ¬0 = slope f x y ↔ f x ≤ f y ∧ ¬f x = f y
⊢ 0 < slope f x y ↔ f x < f y
have simp_rw₃ : f x ≤ f y ∧ ¬slope f x y = 0 ↔ f x ≤ f y ∧ ¬f x = f y
Tactic: simp_rw [lt_iff_le_and_ne, slope_nonneg_iff_of_le hxy, Ne, eq_comm, slope_eq_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
s : Set k
hf : StrictMonoOn f s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
⊢ 0 < slope f x y
have inl : ∀ (hxy : x < y), 0 < slope f x y
Tactic: rcases lt_or_gt_of_ne hxy with hxy | hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Slope (goal)
Goal:
k : Type u_1
E : Type u_2
inst : Field k
inst_1 : AddCommGroup E
inst_2 : Module k E
inst_3 : LinearOrder k
inst_4 : IsStrictOrderedRing k
inst_5 : PartialOrder E
inst_6 : IsOrderedAddMonoid E
inst_7 : PosSMulMono k E
f : k → E
x y : k
s : Set k
hf : StrictMonoOn f s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
inl : ∀ (hxy : x < y), 0 < slope f x y
⊢ 0 < slope f x y
have inr : ∀ (hxy : y < x), 0 < slope f x y
Tactic: rcases lt_or_gt_of_ne hxy with hxy | hxy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
P : Type u_4
inst_5 : AddCommMonoid P
inst_6 : Module R P
M' : Type u_5
inst_7 : AddCommGroup M'
inst_8 : Module R M'
N' : Type u_6
inst_9 : AddCommGroup N'
inst_10 : Module R N'
ι : Type u_7
ι' : Type u_8
ι'' : Type u_9
f_1 f' : M [⋀^ι]→ₗ[R] N
g_1 g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
f g : M [⋀^ι]→ₗ[R] N
h :
  Eq (α := (a : ι → M) → N) ((fun (f : M [⋀^ι]→ₗ[R] N) ↦ f.toFun (M₁ := fun (x : ι) ↦ M)) f)
    ((fun (f : M [⋀^ι]→ₗ[R] N) ↦ f.toFun (M₁ := fun (x : ι) ↦ M)) g)
⊢ f = g
have rcases : ∀ (toFun : ((i : ι) → M) → N)
  (map_update_add' :
    ∀ [inst : DecidableEq ι] (m : (i : ι) → M) (i : ι) (x y : M),
      toFun (update (β := fun (x : ι) ↦ M) m i (x + y)) =
        toFun (update (β := fun (x : ι) ↦ M) m i x) + toFun (update (β := fun (x : ι) ↦ M) m i y))
  (map_update_smul' :
    ∀ [inst_11 : DecidableEq ι] (m : (i : ι) → M) (i : ι) (c : R) (x : M),
      toFun (update (β := fun (x : ι) ↦ M) m i (c • x)) = c • toFun (update (β := fun (x : ι) ↦ M) m i x))
  (map_eq_zero_of_eq' :
    ∀ (v : ι → M) (i j : ι),
      v i = v j →
        i ≠ j →
          (MultilinearMap.mk (M₁ := fun (x : ι) ↦ M) toFun map_update_add' map_update_smul').toFun (M₁ := fun (x : ι) ↦
              M) v =
            0)
  (h :
    Eq (α := (a : ι → M) → N)
      ((fun (f : M [⋀^ι]→ₗ[R] N) ↦ f.toFun (M₁ := fun (x : ι) ↦ M))
        { toFun := toFun, map_update_add' := map_update_add', map_update_smul' := map_update_smul',
          map_eq_zero_of_eq' := map_eq_zero_of_eq' })
      ((fun (f : M [⋀^ι]→ₗ[R] N) ↦ f.toFun (M₁ := fun (x : ι) ↦ M)) g)),
  { toFun := toFun, map_update_add' := map_update_add', map_update_smul' := map_update_smul',
      map_eq_zero_of_eq' := map_eq_zero_of_eq' : M [⋀^ι]→ₗ[R] N } =
    g
Tactic: rcases f with ⟨⟨_, _, _⟩, _⟩
Cleared hypotheses: f, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
hv : ¬Injective v
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)
have hv₁ : ¬∀ ⦃a₁ a₂ : ι⦄, v a₁ = v a₂ → a₁ = a₂
Tactic: rw [Function.Injective] at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
hv : ¬∀ ⦃a₁ a₂ : ι⦄, v a₁ = v a₂ → a₁ = a₂
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)
have hv₁ : ∃ (a₁ : ι) (a₂ : ι), v a₁ = v a₂ ∧ a₁ ≠ a₂
Tactic: push Not at hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
hv : ∃ (a₁ : ι) (a₂ : ι), v a₁ = v a₂ ∧ a₁ ≠ a₂
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)
have rcases : ∀ (i₁ i₂ : ι) (heq : v i₁ = v i₂) (hne : i₁ ≠ i₂), Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) v : N) (0 : N)
Tactic: rcases hv with ⟨i₁, i₂, heq, hne⟩
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
g : M₂ →ₗ[R] M
⊢ Eq (α := M₂ [⋀^ι]→ₗ[R] N) (compLinearMap 0 g) 0
have H : ∀ (x : ι → M₂), Eq.{u_3 + 1} (α := N) ((compLinearMap 0 g : (a : ι → M₂) → N) x : N) ((0 : (a : ι → M₂) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
f₁ f₂ : M [⋀^ι]→ₗ[R] N
g : M₂ →ₗ[R] M
⊢ (f₁ + f₂).compLinearMap g = f₁.compLinearMap g + f₂.compLinearMap g
have H : ∀ (x : ι → M₂),
  Eq.{u_3 + 1} (α := N) (((f₁ + f₂).compLinearMap g : (a : ι → M₂) → N) x : N)
    ((f₁.compLinearMap g + f₂.compLinearMap g : (a : ι → M₂) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : M [⋀^ι]→ₗ[R] N
⊢ Eq (α := M₂ [⋀^ι]→ₗ[R] N) (f.compLinearMap 0) 0
have H : ∀ (x : ι → M₂), Eq.{u_3 + 1} (α := N) ((f.compLinearMap 0 : (a : ι → M₂) → N) x : N) ((0 : (a : ι → M₂) → N) x : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : M [⋀^ι]→ₗ[R] N
x : ι → M₂
⊢ Eq.{u_3 + 1} (α := N) ((f.compLinearMap 0 : (a : ι → M₂) → N) x : N) ((0 : (a : ι → M₂) → N) x : N)
have H : Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) fun (i : ι) ↦ (0 : (a : M₂) → M) (x i) : N) ((0 : (a : ι → M₂) → N) x : N)
Tactic: simp_rw [compLinearMap_apply, LinearMap.zero_apply, ← Pi.zero_def, map_zero, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : M [⋀^ι]→ₗ[R] N
x : ι → M₂
H :
  Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) fun (i : ι) ↦ (0 : (a : M₂) → M) (x i) : N)
    ((0 : (a : ι → M₂) → N) x : N)
⊢ Eq.{u_3 + 1} (α := N) ((f.compLinearMap 0 : (a : ι → M₂) → N) x : N) ((0 : (a : ι → M₂) → N) x : N)
have H₁ : Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) fun (i : ι) ↦ 0 : N) ((0 : (a : ι → M₂) → N) x : N)
Tactic: simp_rw [compLinearMap_apply, LinearMap.zero_apply, ← Pi.zero_def, map_zero, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : M [⋀^ι]→ₗ[R] N
x : ι → M₂
H :
  Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) fun (i : ι) ↦ (0 : (a : M₂) → M) (x i) : N)
    ((0 : (a : ι → M₂) → N) x : N)
H₁ : Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) fun (i : ι) ↦ 0 : N) ((0 : (a : ι → M₂) → N) x : N)
⊢ Eq.{u_3 + 1} (α := N) ((f.compLinearMap 0 : (a : ι → M₂) → N) x : N) ((0 : (a : ι → M₂) → N) x : N)
have H₂ : Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) 0 : N) ((0 : (a : ι → M₂) → N) x : N)
Tactic: simp_rw [compLinearMap_apply, LinearMap.zero_apply, ← Pi.zero_def, map_zero, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
M₂ : Type u_10
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
inst_7 : Nonempty ι
f : M [⋀^ι]→ₗ[R] N
x : ι → M₂
H :
  Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) fun (i : ι) ↦ (0 : (a : M₂) → M) (x i) : N)
    ((0 : (a : ι → M₂) → N) x : N)
H₁ : Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) fun (i : ι) ↦ 0 : N) ((0 : (a : ι → M₂) → N) x : N)
H₂ : Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) 0 : N) ((0 : (a : ι → M₂) → N) x : N)
⊢ Eq.{u_3 + 1} (α := N) ((f.compLinearMap 0 : (a : ι → M₂) → N) x : N) ((0 : (a : ι → M₂) → N) x : N)
have H₃ : Eq.{u_3 + 1} (α := N) (0 : N) ((0 : (a : ι → M₂) → N) x : N)
Tactic: simp_rw [compLinearMap_apply, LinearMap.zero_apply, ← Pi.zero_def, map_zero, zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Alternating.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_7
f : M [⋀^ι]→ₗ[R] N
v : ι → M
inst_5 : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ update (β := fun (a : ι) ↦ M) v i (v j) i = update (β := fun (a : ι) ↦ M) v i (v j) j
have rw : v j = update (β := fun (a : ι) ↦ M) v i (v j) j
Tactic: rw [Function.update_self, Function.update_of_ne hij.symm]