awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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 c : k
hab : ¬a = b
hbc : ¬b = c
neg :
  ((c - b) / (c - a)) • (c - b)⁻¹ • (f c -ᵥ f b) + ((b - a) / (c - a)) • (b - a)⁻¹ • (f b -ᵥ f a) =
    (c - a)⁻¹ • (f c -ᵥ f a)
neg₁ :
  ((c - a)⁻¹ * (c - b)) • (c - b)⁻¹ • (f c -ᵥ f b) + ((c - a)⁻¹ * (b - a)) • (b - a)⁻¹ • (f b -ᵥ f a) =
    (c - a)⁻¹ • (f c -ᵥ f a)
neg₂ :
  (c - a)⁻¹ • (c - b) • (c - b)⁻¹ • (f c -ᵥ f b) + (c - a)⁻¹ • (b - a) • (b - a)⁻¹ • (f b -ᵥ f a) =
    (c - a)⁻¹ • (f c -ᵥ f a)
neg₃ : (c - a)⁻¹ • ((c - b) • (c - b)⁻¹ • (f c -ᵥ f b) + (b - a) • (b - a)⁻¹ • (f b -ᵥ f a)) = (c - a)⁻¹ • (f c -ᵥ f a)
neg₄ : (c - a)⁻¹ • ((c - b) • (c - b)⁻¹ • (f c -ᵥ f b) + (f b -ᵥ f a)) = (c - a)⁻¹ • (f c -ᵥ f a)
neg₅ : (c - a)⁻¹ • (f c -ᵥ f b + (f b -ᵥ f a)) = (c - a)⁻¹ • (f c -ᵥ f a)
⊢ ((c - b) / (c - a)) • slope f b c + ((b - a) / (c - a)) • slope f a b = slope f a c

Tactic:
simp_rw [slope, div_eq_inv_mul, mul_smul, ← smul_add,
    smul_inv_smul₀ (sub_ne_zero.2 <| Ne.symm hab), smul_inv_smul₀ (sub_ne_zero.2 <| Ne.symm hbc),
    vsub_add_vsub_cancel]

Premises used: Iff.mpr, smul_inv_smul₀, sub_ne_zero, vsub_add_vsub_cancel, Ne.symm, slope, div_eq_inv_mul, SemigroupAction.mul_smul, smul_add
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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 c : k
h : a ≠ c
simp : (1 - (c - b) / (c - a)) • slope f a b = ((b - a) / (c - a)) • slope f a b
⊢ (lineMap (slope f a b) (slope f b c) : (a : k) → E) ((c - b) / (c - a)) = slope f a c

Tactic:
simp only [lineMap_apply_module, ← sub_div_sub_smul_slope_add_sub_div_sub_smul_slope f a b c,
    add_left_inj]

Premises used: AffineMap.lineMap_apply_module, add_left_inj, sub_div_sub_smul_slope_add_sub_div_sub_smul_slope
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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 c : k
h : a ≠ c
match_scalars : (1 - (c - b) / (c - a)) * 1 = (b - a) / (c - a) * 1
⊢ (1 - (c - b) / (c - a)) • slope f a b = ((b - a) / (c - a)) • slope f a b

Tactic:
match_scalars
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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 c : k
h : a ≠ c
⊢ (1 - (c - b) / (c - a)) * 1 = (b - a) / (c - a) * 1

Tactic:
field [sub_ne_zero.2 h.symm]

Premises used: Iff.mpr, sub_ne_zero, Ne.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
⊢ a = b ∨ a ≠ b

Tactic:
Classical.em _

Premises used: Classical.em
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
inl :
  (lineMap (slope f ((lineMap a a : (a : k) → k) r) a) (slope f a ((lineMap a a : (a : k) → k) r)) : (a : k) → E) r =
    slope f a a
inr :
  ∀ (hab : a ≠ b),
    (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 b
⊢ (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 b

Tactic:
obtain rfl | hab : a = b ∨ a ≠ b := Classical.em _

Premises used: Classical.em, rfl
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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 r : k
⊢ (lineMap (slope f ((lineMap a a : (a : k) → k) r) a) (slope f a ((lineMap a a : (a : k) → k) r)) : (a : k) → E) r =
    slope f a a

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
inr :
  (lineMap (slope f b ((lineMap a b : (a : k) → k) r)) (slope f ((lineMap a b : (a : k) → k) r) a) : (a : k) → E) r =
    slope f b a
⊢ (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 b

Tactic:
rw [slope_comm _ a, slope_comm _ a, slope_comm _ _ b]

Premises used: slope_comm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
⊢ (lineMap (slope f b ((lineMap a b : (a : k) → k) r)) (slope f ((lineMap a b : (a : k) → k) r) a) : (a : k) → E)
      (HSub.hSub (β := k) a ((lineMap a b : (a : k) → k) r : k) / (a - b)) =
    slope f b a

Tactic:
lineMap_slope_slope_sub_div_sub f b (lineMap a b r) a hab.symm

Premises used: AffineMap.lineMap, Ne.symm, DFunLike.coe, lineMap_slope_slope_sub_div_sub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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 = HSub.hSub (β := k) a ((lineMap a b : (a : k) → k) r : k) / (a - b)
⊢ (lineMap (slope f b ((lineMap a b : (a : k) → k) r)) (slope f ((lineMap a b : (a : k) → k) r) a) : (a : k) → E) r =
    slope f b a

Tactic:
convert! lineMap_slope_slope_sub_div_sub f b (lineMap a b r) a hab.symm using 2

Premises used: AffineMap.lineMap, Ne.symm, DFunLike.coe, lineMap_slope_slope_sub_div_sub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
h₆ h₇ : r * a - r * b = r * a - r * b
⊢ r = HSub.hSub (β := k) a ((lineMap a b : (a : k) → k) r : k) / (a - 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]

Premises used: Iff.mpr, mul_sub, sub_ne_zero, sub_mul, sub_sub, sub_sub_cancel, AffineMap.lineMap_apply_ring, eq_div_iff, one_mul
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
neg : ∀ (hxeqy : ¬x = y), 0 ≤ slope f x y ↔ f x ≤ f y
⊢ 0 ≤ slope f x y ↔ f x ≤ f y

Tactic:
by_cases hxeqy : x = y
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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

Tactic:
simp [hxeqy]
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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

Tactic:
⟨fun h ↦ ?_, fun h ↦ smul_nonneg (inv_nonneg.2 (sub_nonneg.2 hxy)) ?_⟩

Premises used: Iff.mpr, smul_nonneg, inv_nonneg, Iff.intro, sub_nonneg
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
neg₁ : ∀ (h : f x ≤ f y), 0 ≤ f y -ᵥ f x
⊢ 0 ≤ slope f x y ↔ f x ≤ f y

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ smul_nonneg (inv_nonneg.2 (sub_nonneg.2 hxy)) ?_⟩
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
⊢ 0 ≤ (y - x) • slope f x y

Tactic:
have := smul_nonneg (sub_nonneg.2 hxy) h
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
neg₅ neg₆ neg₇ neg₈ : ∀ (this : f x ≤ f y), 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

Premises used: mul_inv_cancel₀, mt, Ne.symm, slope, one_smul, sub_nonneg, vsub_eq_sub, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
neg : 0 ≤ f y - f x
neg₁ neg₂ neg₃ neg₄ : f x ≤ f y
⊢ 0 ≤ f y -ᵥ f x

Tactic:
rwa [vsub_eq_sub, sub_nonneg]

Premises used: sub_nonneg, vsub_eq_sub
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
inr : ∀ (hxy : y ≤ x), 0 ≤ slope f x y
⊢ 0 ≤ slope f x y

Tactic:
rcases le_total x y with hxy | hxy

Premises used: le_total
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
hxy : x ≤ y
⊢ 0 ≤ slope f x y

Tactic:
(slope_nonneg_iff_of_le hxy).mpr (hf hx hy hxy)

Premises used: Iff.mpr, slope_nonneg_iff_of_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
hxy : x ≤ y
⊢ 0 ≤ slope f x y

Tactic:
exact (slope_nonneg_iff_of_le hxy).mpr (hf hx hy hxy)

Premises used: Iff.mpr, slope_nonneg_iff_of_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
hxy : y ≤ x
⊢ 0 ≤ slope f x y

Tactic:
slope_comm f x y ▸ (slope_nonneg_iff_of_le hxy).mpr (hf hy hx hxy)

Premises used: Iff.mpr, Eq.rec, slope_comm, Eq.symm, slope_nonneg_iff_of_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
hxy : y ≤ x
⊢ 0 ≤ slope f x y

Tactic:
exact slope_comm f x y ▸ (slope_nonneg_iff_of_le hxy).mpr (hf hy hx hxy)
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
⊢ slope f x y ≤ 0 ↔ f y ≤ f x

Tactic:
simpa using slope_nonneg_iff_of_le (f := -f) hxy

Premises used: slope_nonneg_iff_of_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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 : AntitoneOn f s
hx : x ∈ s
hy : y ∈ s
⊢ slope f x y ≤ 0

Tactic:
simpa using hf.neg.slope_nonneg hx hy

Premises used: MonotoneOn.slope_nonneg, AntitoneOn.neg
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
simp_rw₃ : f x ≤ f y ∧ ¬slope f x y = 0 ↔ f x ≤ f y ∧ ¬f x = f y
⊢ 0 < slope f x 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]

Premises used: lt_iff_le_and_ne, slope_eq_zero_iff, Ne, eq_comm, slope_nonneg_iff_of_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
inr : ∀ (hxy : y < x), 0 < slope f x y
⊢ 0 < slope f x y

Tactic:
rcases lt_or_gt_of_ne hxy with hxy | hxy

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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_1 : x ≠ y
hxy : x < y
⊢ 0 < slope f x y

Tactic:
(slope_pos_iff_of_le hxy.le).mpr (hf hx hy hxy)

Premises used: Iff.mpr, slope_pos_iff_of_le, LT.lt.le
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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_1 : x ≠ y
hxy : x < y
⊢ 0 < slope f x y

Tactic:
exact (slope_pos_iff_of_le hxy.le).mpr (hf hx hy hxy)

Premises used: Iff.mpr, slope_pos_iff_of_le, LT.lt.le
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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_1 : x ≠ y
hxy : y < x
⊢ 0 < slope f x y

Tactic:
slope_comm f x y ▸ (slope_pos_iff_of_le hxy.le).mpr (hf hy hx hxy)

Premises used: Iff.mpr, slope_pos_iff_of_le, Eq.rec, LT.lt.le, slope_comm, Eq.symm
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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_1 : x ≠ y
hxy : y < x
⊢ 0 < slope f x y

Tactic:
exact slope_comm f x y ▸ (slope_pos_iff_of_le hxy.le).mpr (hf hy hx hxy)
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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
⊢ slope f x y < 0 ↔ f y < f x

Tactic:
simpa using slope_pos_iff_of_le (f := -f) hxy

Premises used: slope_pos_iff_of_le
-- Module: Mathlib.LinearAlgebra.AffineSpace.Slope
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 : StrictAntiOn f s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
⊢ slope f x y < 0

Tactic:
simpa using hf.neg.slope_pos hx hy hxy

Premises used: StrictAntiOn.neg, StrictMonoOn.slope_pos
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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)
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
⊢ f = g

Tactic:
rcases f with ⟨⟨_, _, _⟩, _⟩
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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 f' : M [⋀^ι]→ₗ[R] N
g g₂ : M [⋀^ι]→ₗ[R] N'
g' : M' [⋀^ι]→ₗ[R] N'
v : ι → M
v' : ι → M'
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
toFun_1 : ((i : ι) → M) → N
map_update_add'_1 :
  ∀ [inst : DecidableEq ι] (m : (i : ι) → M) (i : ι) (x y : M),
    toFun_1 (update (β := fun (x : ι) ↦ M) m i (x + y)) =
      toFun_1 (update (β := fun (x : ι) ↦ M) m i x) + toFun_1 (update (β := fun (x : ι) ↦ M) m i y)
map_update_smul'_1 :
  ∀ [inst_11 : DecidableEq ι] (m : (i : ι) → M) (i : ι) (c : R) (x : M),
    toFun_1 (update (β := fun (x : ι) ↦ M) m i (c • x)) = c • toFun_1 (update (β := fun (x : ι) ↦ M) m i x)
map_eq_zero_of_eq'_1 :
  ∀ (v : ι → M) (i j : ι),
    v i = v j →
      i ≠ j →
        (MultilinearMap.mk (M₁ := fun (x : ι) ↦ M) toFun_1 map_update_add'_1 map_update_smul'_1).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))
      { toFun := toFun_1, map_update_add' := map_update_add'_1, map_update_smul' := map_update_smul'_1,
        map_eq_zero_of_eq' := map_eq_zero_of_eq'_1 })
⊢ { 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 } =
    { toFun := toFun_1, map_update_add' := map_update_add'_1, map_update_smul' := map_update_smul'_1,
      map_eq_zero_of_eq' := map_eq_zero_of_eq'_1 }

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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
⊢ f.toFun (M₁ := fun (x : ι) ↦ M) = (⇑f : (a : ι → M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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 : MultilinearMap.{u_1, u_7, u_2, u_3} R (fun (x : ι) ↦ M) N
h : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → f.toFun (M₁ := fun (x : ι) ↦ M) v = 0
⊢ Eq (α := (a : ι → M) → N) (⇑{ toMultilinearMap := f, map_eq_zero_of_eq' := h : M [⋀^ι]→ₗ[R] N } : (a : ι → M) → N)
    (⇑f : (a : (i : ι) → M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Alternating.Basic
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 g : M [⋀^ι]→ₗ[R] N
h : f = g
x : ι → M
⊢ Eq.{u_3 + 1} (α := N) ((f : (a : ι → M) → N) x : N) ((g : (a : ι → M) → N) x : N)

Tactic:
congr_arg (fun h : M [⋀^ι]→ₗ[R] N => h x) h

Premises used: congr_arg, DFunLike.coe