awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
rw : (c + (↑(#s) : ℤ) - c).toNat = #s
rw₁ : Int.toNat (↑(#s) : ℤ) = #s
rw₂ rw₃ : #s = #s
⊢ #r = #s

Tactic:
rw [Int.card_Ico, add_sub_cancel_left, Int.toNat_natCast]

Premises used: Int.toNat_natCast, add_sub_cancel_left, Int.card_Ico
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
grw : ∀ (x : ℤ) (mx : x ∈ s \ r), c + (↑(#s) : ℤ) ≤ x
⊢ ∑ x ∈ s ∩ r, x + #(s \ r) • (c + (↑(#s) : ℤ)) ≤ ∑ x ∈ s, x

Tactic:
grw [← sum_inter_add_sum_diff s r, card_nsmul_le_sum _ _ _ fun x mx ↦ ?_]

Premises used: Finset.sum_inter_add_sum_diff, Finset.card_nsmul_le_sum
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
x : ℤ
mx : x ∈ s \ r
⊢ c + (↑(#s) : ℤ) ≤ x

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
r : Finset ℤ := Ico c (c + (↑(#s) : ℤ))
_ : ∑ x ∈ r, x ≤ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + (↑(#s) : ℤ))
_₁ : ∑ x ∈ r ∩ s, x + #(r \ s) • (c + (↑(#s) : ℤ)) = ∑ x ∈ s ∩ r, x + #(s \ r) • (c + (↑(#s) : ℤ))
_₂ : ∑ x ∈ s ∩ r, x + #(s \ r) • (c + (↑(#s) : ℤ)) ≤ ∑ x ∈ s, x
⊢ LE.le (α := ℤ) (∑ x ∈ r, x) (∑ x ∈ s, x)

Tactic:
calc
    _ ≤ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + #s) := by
      grw [← sum_inter_add_sum_diff r s, ← sum_le_card_nsmul _ _ _ fun x mx ↦ ?_]
      rw [mem_sdiff, mem_Ico] at mx; exact mx.1.2.le
    _ = ∑ x ∈ s ∩ r, x + #(s \ r) • (c + #s) := by
      rw [inter_comm, card_sdiff_comm]
      rw [Int.card_Ico, add_sub_cancel_left, Int.toNat_natCast]
    _ ≤ _ := by
      grw [← sum_inter_add_sum_diff s r, card_nsmul_le_sum _ _ _ fun x mx ↦ ?_]
      grind

Premises used: Nat.cast, SDiff.sdiff, HAdd.hAdd, Finset.card
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
⊢ LE.le (α := ℤ) (∑ x ∈ Ico c (c + (↑(#s) : ℤ)), x) (∑ x ∈ s, x)

Tactic:
sum_Ico_le_sum hs

Premises used: Finset.sum_Ico_le_sum
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
h : Eq (α := ℤ) (∑ n ∈ range #s, (c + (↑n : ℤ))) (∑ x ∈ Ico c (c + (↑(#s) : ℤ)), x)
⊢ LE.le (α := ℤ) (∑ n ∈ range #s, (c + (↑n : ℤ))) (∑ x ∈ s, x)

Tactic:
convert! sum_Ico_le_sum hs

Premises used: Finset.sum_Ico_le_sum
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
⊢ Eq (α := ℤ) (∑ n ∈ range #s, (c + (↑n : ℤ))) (∑ x ∈ Ico c (c + (↑(#s) : ℤ)), x)

Tactic:
sum_nbij (c + ·) ?_ ?_ ?_ (fun _ _ ↦ rfl)

Premises used: Finset.sum_nbij, Nat.cast, HAdd.hAdd, rfl
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
h : ∀ a ∈ range #s, (fun (x : ℕ) ↦ c + (↑x : ℤ)) a ∈ Ico c (c + (↑(#s) : ℤ))
h₁ : Set.InjOn (β := ℤ) (fun (x : ℕ) ↦ c + (↑x : ℤ)) (↑(range #s) : Set ℕ)
h₂ : Set.SurjOn (fun (x : ℕ) ↦ c + (↑x : ℤ)) (↑(range #s) : Set ℕ) (↑(Ico c (c + (↑(#s) : ℤ))) : Set ℤ)
⊢ Eq (α := ℤ) (∑ n ∈ range #s, (c + (↑n : ℤ))) (∑ x ∈ Ico c (c + (↑(#s) : ℤ)), x)

Tactic:
refine sum_nbij (c + ·) ?_ ?_ ?_ (fun _ _ ↦ rfl)

Premises used: Finset.sum_nbij, HAdd.hAdd, rfl
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ range #s
h : c ≤ (fun (x : ℕ) ↦ c + (↑x : ℤ)) x ∧ (fun (x : ℕ) ↦ c + (↑x : ℤ)) x < c + (↑(#s) : ℤ)
⊢ (fun (x : ℕ) ↦ c + (↑x : ℤ)) x ∈ Ico c (c + (↑(#s) : ℤ))

Tactic:
rw [mem_Ico]

Premises used: Finset.mem_Ico
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ range #s
⊢ x < #s

Tactic:
rw [mem_range] at mx

Premises used: Finset.mem_range
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x < #s
⊢ c ≤ c + (↑x : ℤ) ∧ c + (↑x : ℤ) < c + (↑(#s) : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ (↑(range #s) : Set ℕ)
y : ℕ
my : y ∈ (↑(range #s) : Set ℕ)
h : ∀ (h : c + (↑x : ℤ) = c + (↑y : ℤ)), x = y
⊢ Eq (α := ℤ) ((fun (x : ℕ) ↦ c + (↑x : ℤ)) x) ((fun (x : ℕ) ↦ c + (↑x : ℤ)) y) → x = y

Tactic:
(h : c + x = c + y)
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ (↑(range #s) : Set ℕ)
y : ℕ
my : y ∈ (↑(range #s) : Set ℕ)
h : c + (↑x : ℤ) = c + (↑y : ℤ)
⊢ x = y

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : x ∈ (↑(Ico c (c + (↑(#s) : ℤ))) : Set ℤ)
h : ∃ x_1 < #s, c + (↑x_1 : ℤ) = x
⊢ Membership.mem (γ := Set ℤ) ((fun (x : ℕ) ↦ c + (↑x : ℤ)) '' (↑(range #s) : Set ℕ)) x

Tactic:
simp_rw [coe_range, Set.mem_image, Set.mem_Iio]

Premises used: Set.mem_Iio, Finset.coe_range, Set.mem_image
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : x ∈ (↑(Ico c (c + (↑(#s) : ℤ))) : Set ℤ)
⊢ c ≤ x ∧ x < c + (↑(#s) : ℤ)

Tactic:
rw [mem_coe, mem_Ico] at mx

Premises used: Finset.mem_coe, Finset.mem_Ico
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : c ≤ x ∧ x < c + (↑(#s) : ℤ)
h : (x - c).toNat < #s ∧ c + (↑(x - c).toNat : ℤ) = x
⊢ ∃ x_1 < #s, c + (↑x_1 : ℤ) = x

Tactic:
use (x - c).toNat

Premises used: HSub.hSub, Int.toNat
-- Module: Mathlib.Algebra.Order.Group.Int.Sum
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : c ≤ x ∧ x < c + (↑(#s) : ℤ)
⊢ (x - c).toNat < #s ∧ c + (↑(x - c).toNat : ℤ) = x

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
a b c : α
⊢ c * (a ⊔ b) = c * a ⊔ c * b

Tactic:
(OrderIso.mulLeft _).map_sup _ _

Premises used: OrderIso.mulLeft, OrderIso.map_sup
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulRightMono α
a b c : α
⊢ (a ⊔ b) * c = a * c ⊔ b * c

Tactic:
(OrderIso.mulRight _).map_sup _ _

Premises used: OrderIso.map_sup, OrderIso.mulRight
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
a b c : α
⊢ c * (a ⊓ b) = c * a ⊓ c * b

Tactic:
(OrderIso.mulLeft _).map_inf _ _

Premises used: OrderIso.mulLeft, OrderIso.map_inf
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulRightMono α
a b c : α
⊢ (a ⊓ b) * c = a * c ⊓ b * c

Tactic:
(OrderIso.mulRight _).map_inf _ _

Premises used: OrderIso.map_inf, OrderIso.mulRight
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulRightMono α
a b c : α
⊢ (a ⊔ b) / c = a / c ⊔ b / c

Tactic:
(OrderIso.divRight _).map_sup _ _

Premises used: OrderIso.map_sup, OrderIso.divRight
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulRightMono α
a b c : α
⊢ (a ⊓ b) / c = a / c ⊓ b / c

Tactic:
(OrderIso.divRight _).map_inf _ _

Premises used: OrderIso.map_inf, OrderIso.divRight
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
⊢ (a ⊔ b)⁻¹ = a⁻¹ ⊓ b⁻¹

Tactic:
(OrderIso.inv α).map_sup _ _

Premises used: OrderIso.inv, OrderIso.map_sup, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
⊢ (a ⊓ b)⁻¹ = a⁻¹ ⊔ b⁻¹

Tactic:
(OrderIso.inv α).map_inf _ _

Premises used: OrderIso.map_inf, OrderIso.inv, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b c : α
⊢ c / (a ⊔ b) = c / a ⊓ c / b

Tactic:
(OrderIso.divLeft c).map_sup _ _

Premises used: OrderIso.divLeft, OrderIso.map_sup, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b c : α
⊢ c / (a ⊓ b) = c / a ⊔ c / b

Tactic:
(OrderIso.divLeft c).map_inf _ _

Premises used: OrderIso.map_inf, OrderIso.divLeft, OrderDual
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
ha : 1 ≤ HPow.hPow (β := ℕ) a 2
this : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
rwa : a ⊓ 1 = 1
rwa₁ : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
rwa₂ : α
rwa₃ : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
rwa₄ : α
rwa₅ : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
rwa₆ : α
rwa₇ : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
rwa₈ : α
⊢ 1 ≤ a

Tactic:
rwa [← inf_eq_right, ← mul_eq_left]

Premises used: mul_eq_left, inf_eq_right
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
ha : 1 ≤ HPow.hPow (β := ℕ) a 2
suffices : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
⊢ 1 ≤ a

Tactic:
suffices this : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1 by
    rwa [← inf_eq_right, ← mul_eq_left]
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
ha : 1 ≤ HPow.hPow (β := ℕ) a 2
rw : (a ⊓ 1) * a ⊓ (a ⊓ 1) * 1 = a ⊓ 1
rw₁ : a * a ⊓ 1 * a ⊓ (a ⊓ 1) * 1 = a ⊓ 1
rw₂ : HPow.hPow (β := ℕ) a 2 ⊓ 1 * a ⊓ (a ⊓ 1) * 1 = a ⊓ 1
rw₃ : HPow.hPow (β := ℕ) a 2 ⊓ 1 * a ⊓ (a ⊓ 1) = a ⊓ 1
rw₄ : HPow.hPow (β := ℕ) a 2 ⊓ a ⊓ (a ⊓ 1) = a ⊓ 1
rw₅ : HPow.hPow (β := ℕ) a 2 ⊓ (a ⊓ (a ⊓ 1)) = a ⊓ 1
rw₆ : HPow.hPow (β := ℕ) a 2 ⊓ (a ⊓ 1) = a ⊓ 1
rw₇ : a ⊓ 1 ⊓ HPow.hPow (β := ℕ) a 2 = a ⊓ 1
rw₈ : a ⊓ (1 ⊓ HPow.hPow (β := ℕ) a 2) = a ⊓ 1
rw₉ rw₁₀ : a ⊓ 1 = a ⊓ 1
⊢ (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1

Tactic:
rw [mul_inf, inf_mul, ← pow_two, mul_one, one_mul, inf_assoc, inf_left_idem, inf_comm,
    inf_assoc, inf_of_le_left ha]

Premises used: inf_mul, pow_two, inf_of_le_left, inf_left_idem, inf_comm, mul_inf, mul_one, inf_assoc, one_mul
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a * b * b⁻¹ ⊔ a * b * a⁻¹)
rw₁ : (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a ⊔ a * b * a⁻¹)
rw₂ rw₃ : (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a ⊔ b)
⊢ (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹))

Tactic:
rw [mul_sup b⁻¹ a⁻¹ (a * b), mul_inv_cancel_right, mul_inv_cancel_comm]

Premises used: mul_inv_cancel_right, HMul.hMul, mul_inv_cancel_comm, mul_sup, Inv.inv
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹)) = (a ⊓ b) * (a * b * (a⁻¹ ⊔ b⁻¹))
rw₁ rw₂ : (a ⊓ b) * (a * b * (a⁻¹ ⊔ b⁻¹)) = (a ⊓ b) * (a * b * (a⁻¹ ⊔ b⁻¹))
⊢ (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹)) = (a ⊓ b) * (a * b * (a ⊓ b)⁻¹)

Tactic:
rw [inv_inf, sup_comm]

Premises used: sup_comm, inv_inf
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : a * b * (a ⊓ b)⁻¹ * (a ⊓ b) = a * b
rw₁ rw₂ : a * b = a * b
⊢ (a ⊓ b) * (a * b * (a ⊓ b)⁻¹) = a * b

Tactic:
rw [mul_comm, inv_mul_cancel_right]

Premises used: mul_comm, inv_mul_cancel_right
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α_1 : Type u_1
inst : Lattice α_1
inst_1 : CommGroup α_1
α : Type u_2
inst_2 : Lattice α
inst_3 : CommGroup α
inst_4 : MulLeftMono α
x y z : α
rw : x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y ∧ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z

Tactic:
rw [← mul_le_mul_iff_left (x ⊓ (y ⊓ z)), inf_mul_sup x (y ⊓ z), ← inv_mul_le_iff_le_mul,
      le_inf_iff]

Premises used: mul_le_mul_iff_left, le_inf_iff, inv_mul_le_iff_le_mul, inf_mul_sup, Min.min
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α_1 : Type u_1
inst : Lattice α_1
inst_1 : CommGroup α_1
α : Type u_2
inst_2 : Lattice α
inst_3 : CommGroup α
inst_4 : MulLeftMono α
x y z : α
left : x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y
right : x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y ∧ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α_1 : Type u_1
inst : Lattice α_1
inst_1 : CommGroup α_1
α : Type u_2
inst_2 : Lattice α
inst_3 : CommGroup α
inst_4 : MulLeftMono α
x y z : α
left : (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ (x ⊓ y) * (x ⊔ y)
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y

Tactic:
rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x y]

Premises used: inv_mul_le_iff_le_mul, inf_mul_sup
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α_1 : Type u_1
inst : Lattice α_1
inst_1 : CommGroup α_1
α : Type u_2
inst_2 : Lattice α
inst_3 : CommGroup α
inst_4 : MulLeftMono α
x y z : α
⊢ (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ (x ⊓ y) * (x ⊔ y)

Tactic:
mul_le_mul' (inf_le_inf_left _ inf_le_left) inf_le_left

Premises used: inf_le_inf_left, inf_le_left, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α_1 : Type u_1
inst : Lattice α_1
inst_1 : CommGroup α_1
α : Type u_2
inst_2 : Lattice α
inst_3 : CommGroup α
inst_4 : MulLeftMono α
x y z : α
⊢ (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ (x ⊓ y) * (x ⊔ y)

Tactic:
exact mul_le_mul' (inf_le_inf_left _ inf_le_left) inf_le_left

Premises used: inf_le_inf_left, inf_le_left, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α_1 : Type u_1
inst : Lattice α_1
inst_1 : CommGroup α_1
α : Type u_2
inst_2 : Lattice α
inst_3 : CommGroup α
inst_4 : MulLeftMono α
x y z : α
right : (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ (x ⊓ z) * (x ⊔ z)
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z

Tactic:
rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x z]

Premises used: inv_mul_le_iff_le_mul, inf_mul_sup
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α_1 : Type u_1
inst : Lattice α_1
inst_1 : CommGroup α_1
α : Type u_2
inst_2 : Lattice α
inst_3 : CommGroup α
inst_4 : MulLeftMono α
x y z : α
⊢ (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ (x ⊓ z) * (x ⊔ z)

Tactic:
mul_le_mul' (inf_le_inf_left _ inf_le_right) inf_le_right

Premises used: inf_le_right, inf_le_inf_left, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Group.Lattice
Goal:
α_1 : Type u_1
inst : Lattice α_1
inst_1 : CommGroup α_1
α : Type u_2
inst_2 : Lattice α
inst_3 : CommGroup α
inst_4 : MulLeftMono α
x y z : α
⊢ (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ (x ⊓ z) * (x ⊔ z)

Tactic:
exact mul_le_mul' (inf_le_inf_left _ inf_le_right) inf_le_right

Premises used: inf_le_right, inf_le_inf_left, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
inl : ∀ (h : a ≤ 1), max a 1 / max a⁻¹ 1 = a
inr : ∀ (h : 1 ≤ a), max a 1 / max a⁻¹ 1 = a
⊢ max a 1 / max a⁻¹ 1 = a

Tactic:
rcases le_total a 1 with (h | h)

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
h : a ≤ 1
⊢ max a 1 / max a⁻¹ 1 = a

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
h : 1 ≤ a
⊢ max a 1 / max a⁻¹ 1 = a

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
rw : a * max a⁻¹ 1 = max a 1
rw₁ : a = max a 1 / max a⁻¹ 1
rw₂ rw₃ : a = a
⊢ max a⁻¹ 1 = a⁻¹ * max a 1

Tactic:
rw [eq_inv_mul_iff_mul_eq, ← eq_div_iff_mul_eq', max_one_div_max_inv_one_eq_self]

Premises used: max_one_div_max_inv_one_eq_self, eq_inv_mul_iff_mul_eq, eq_div_iff_mul_eq'
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
G₀ : Type u_1
inst : Inv G₀
inst_1 : LinearOrder G₀
x y : G₀
inl : x ≤ y → min x⁻¹ y⁻¹ ≤ (max x y)⁻¹
inr : y ≤ x → min x⁻¹ y⁻¹ ≤ (max x y)⁻¹
⊢ min x⁻¹ y⁻¹ ≤ (max x y)⁻¹

Tactic:
cases le_total x y

Premises used: le_total
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
G₀ : Type u_1
inst : Inv G₀
inst_1 : LinearOrder G₀
x y : G₀
h : x ≤ y
⊢ min x⁻¹ y⁻¹ ≤ (max x y)⁻¹

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
G₀ : Type u_1
inst : Inv G₀
inst_1 : LinearOrder G₀
x y : G₀
h : y ≤ x
⊢ min x⁻¹ y⁻¹ ≤ (max x y)⁻¹

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ min a⁻¹ b⁻¹ = (max a b)⁻¹

Tactic:
Eq.symm <| (@Monotone.map_max α αᵒᵈ _ _ Inv.inv a b) fun _ _ =>
    inv_le_inv_iff.mpr

Premises used: Iff.mpr, Monotone.map_max, inv_le_inv_iff, Eq.symm
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a b : α
⊢ max a⁻¹ b⁻¹ = (min a b)⁻¹

Tactic:
Eq.symm <| (@Monotone.map_min α αᵒᵈ _ _ Inv.inv a b) fun _ _ =>
    inv_le_inv_iff.mpr

Premises used: Iff.mpr, inv_le_inv_iff, Monotone.map_min, Eq.symm
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ min (a / c) (b / c) = min a b / c

Tactic:
simpa only [div_eq_mul_inv] using min_mul_mul_right a b c⁻¹

Premises used: div_eq_mul_inv, Inv.inv, min_mul_mul_right
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ max (a / c) (b / c) = max a b / c

Tactic:
simpa only [div_eq_mul_inv] using max_mul_mul_right a b c⁻¹

Premises used: max_mul_mul_right, div_eq_mul_inv, Inv.inv
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ min (a / b) (a / c) = a / max b c

Tactic:
simp only [div_eq_mul_inv, min_mul_mul_left, min_inv_inv']

Premises used: min_mul_mul_left, div_eq_mul_inv, min_inv_inv'
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a b c : α
⊢ max (a / b) (a / c) = a / min b c

Tactic:
simp only [div_eq_mul_inv, max_mul_mul_left, max_inv_inv']

Premises used: max_inv_inv', div_eq_mul_inv, max_mul_mul_left
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ max a b - max c d ≤ max (a - c) (b - d)

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ |max a b - max c d| ≤ max |a - c| |b - d|

Tactic:
abs_sub_le_iff.2 ⟨?_, ?_⟩

Premises used: Iff.mpr, abs_sub_le_iff, And.intro
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
refine_1 : max a b - max c d ≤ max |a - c| |b - d|
refine_2 : max c d - max a b ≤ max |a - c| |b - d|
⊢ |max a b - max c d| ≤ max |a - c| |b - d|

Tactic:
refine abs_sub_le_iff.2 ⟨?_, ?_⟩

Premises used: Iff.mpr, abs_sub_le_iff, And.intro
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ max a b - max c d ≤ max |a - c| |b - d|

Tactic:
(max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))

Premises used: le_abs_self, max_sub_max_le_max, max_le_max, LE.le.trans
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ max a b - max c d ≤ max |a - c| |b - d|

Tactic:
exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))

Premises used: le_abs_self, max_sub_max_le_max, max_le_max, LE.le.trans
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
refine_2 : max c d - max a b ≤ max |c - a| |d - b|
⊢ max c d - max a b ≤ max |a - c| |b - d|

Tactic:
rw [abs_sub_comm a c, abs_sub_comm b d]

Premises used: abs_sub_comm
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ max c d - max a b ≤ max |c - a| |d - b|

Tactic:
(max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))

Premises used: le_abs_self, max_sub_max_le_max, max_le_max, LE.le.trans
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ max c d - max a b ≤ max |c - a| |d - b|

Tactic:
exact (max_sub_max_le_max _ _ _ _).trans (max_le_max (le_abs_self _) (le_abs_self _))

Premises used: le_abs_self, max_sub_max_le_max, max_le_max, LE.le.trans
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ |min a b - min c d| ≤ max |a - c| |b - d|

Tactic:
simpa only [max_neg_neg, neg_sub_neg, abs_sub_comm] using
    abs_max_sub_max_le_max (-a) (-b) (-c) (-d)

Premises used: max_neg_neg, abs_max_sub_max_le_max, neg_sub_neg, abs_sub_comm, Neg.neg
-- Module: Mathlib.Algebra.Order.Group.MinMax
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c : α
⊢ |max a c - max b c| ≤ |a - b|

Tactic:
simpa only [sub_self, abs_zero, max_eq_left (abs_nonneg (a - b))]
    using abs_max_sub_max_le_max a c b c

Premises used: sub_self, HSub.hSub, abs_max_sub_max_le_max, max_eq_left, abs_zero, abs_nonneg
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
a : α
s : Multiset α
h : a ∈ HSMul.hSMul (α := ℕ) 0 s
⊢ Membership.mem (γ := Multiset α) 0 a

Tactic:
rw [zero_nsmul] at h

Premises used: zero_nsmul
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
a : α
s : Multiset α
h : Membership.mem (γ := Multiset α) 0 a
⊢ a ∈ s

Tactic:
absurd h (notMem_zero _)

Premises used: Multiset.notMem_zero, absurd
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
a : α
s : Multiset α
h : Membership.mem (γ := Multiset α) 0 a
⊢ a ∈ s

Tactic:
exact absurd h (notMem_zero _)

Premises used: Multiset.notMem_zero, absurd
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
a : α
s : Multiset α
n : ℕ
ih : ∀ (h : a ∈ n • s), a ∈ s
h : a ∈ (n + 1) • s
⊢ a ∈ n • s ∨ a ∈ s

Tactic:
rw [succ_nsmul, mem_add] at h

Premises used: Multiset.mem_add, succ_nsmul
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
a : α
s : Multiset α
n : ℕ
ih : ∀ (h : a ∈ n • s), a ∈ s
h : a ∈ n • s ∨ a ∈ s
⊢ a ∈ s

Tactic:
h.elim ih id

Premises used: id, Or.elim
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
a : α
s : Multiset α
n : ℕ
ih : ∀ (h : a ∈ n • s), a ∈ s
h : a ∈ n • s ∨ a ∈ s
⊢ a ∈ s

Tactic:
exact h.elim ih id

Premises used: id, Or.elim
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : a ∈ n • s
zero : ∀ (h : a ∈ HSMul.hSMul (α := ℕ) 0 s), a ∈ s
succ : ∀ (n : ℕ) (ih : ∀ (h : a ∈ n • s), a ∈ s) (h : a ∈ (n + 1) • s), a ∈ s
⊢ a ∈ s

Tactic:
induction n with
  | zero =>
    rw [zero_nsmul] at h
    exact absurd h (notMem_zero _)
  | succ n ih =>
    rw [succ_nsmul, mem_add] at h
    exact h.elim ih id

Premises used: Multiset.mem_add, absurd, zero_nsmul, Nat.zero, Nat.succ, succ_nsmul
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
a : α
s : Multiset α
n : ℕ
⊢ a ∈ n • s ↔ n ≠ 0 ∧ a ∈ s

Tactic:
⟨fun ha ↦ ⟨?_, mem_of_mem_nsmul ha⟩, fun h ↦ ?_⟩

Premises used: And.intro, Iff.intro, Multiset.mem_of_mem_nsmul
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
a : α
s : Multiset α
n : ℕ
refine_1 : ∀ (ha : a ∈ n • s), n ≠ 0
refine_2 : ∀ (h : n ≠ 0 ∧ a ∈ s), a ∈ n • s
⊢ a ∈ n • s ↔ n ≠ 0 ∧ a ∈ s

Tactic:
refine ⟨fun ha ↦ ⟨?_, mem_of_mem_nsmul ha⟩, fun h ↦ ?_⟩
-- Module: Mathlib.Algebra.Order.Group.Multiset
Goal:
α : Type u_1
a : α
s : Multiset α
ha : a ∈ HSMul.hSMul (α := ℕ) 0 s
⊢ False

Tactic:
simp [zero_nsmul] at ha

Premises used: zero_nsmul