awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
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 ℕ)
⊢ Eq (α := ℤ) (∑ n ∈ range #s, (c + (↑n : ℤ))) (∑ x ∈ Ico c (c + (↑(#s) : ℤ)), x)
have h₂ : Set.SurjOn (fun (x : ℕ) ↦ c + (↑x : ℤ)) (↑(range #s) : Set ℕ) (↑(Ico c (c + (↑(#s) : ℤ))) : Set ℤ)
Tactic: refine sum_nbij (c + ·) ?_ ?_ ?_ (fun _ _ ↦ rfl)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ range #s
⊢ (fun (x : ℕ) ↦ c + (↑x : ℤ)) x ∈ Ico c (c + (↑(#s) : ℤ))
have h : c ≤ (fun (x : ℕ) ↦ c + (↑x : ℤ)) x ∧ (fun (x : ℕ) ↦ c + (↑x : ℤ)) x < c + (↑(#s) : ℤ)
Tactic: rw [mem_Ico]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (hypothesis)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℕ
mx : x ∈ range #s
⊢ c ≤ c + (↑x : ℤ) ∧ c + (↑x : ℤ) < c + (↑(#s) : ℤ)
have mx₁ : x < #s
Tactic: rw [mem_range] at mx
Cleared hypotheses: mx
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : x ∈ (↑(Ico c (c + (↑(#s) : ℤ))) : Set ℤ)
⊢ Membership.mem (γ := Set ℤ) ((fun (x : ℕ) ↦ c + (↑x : ℤ)) '' (↑(range #s) : Set ℕ)) x
have h : ∃ x_1 < #s, c + (↑x_1 : ℤ) = x
Tactic: simp_rw [coe_range, Set.mem_image, Set.mem_Iio]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (hypothesis)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : x ∈ (↑(Ico c (c + (↑(#s) : ℤ))) : Set ℤ)
⊢ ∃ x_1 < #s, c + (↑x_1 : ℤ) = x
have mx₁ : c ≤ x ∧ x < c + (↑(#s) : ℤ)
Tactic: rw [mem_coe, mem_Ico] at mx
Cleared hypotheses: mx
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Int.Sum (goal)
Goal:
s : Finset ℤ
c : ℤ
hs : ∀ x ∈ s, c ≤ x
x : ℤ
mx : c ≤ x ∧ x < c + (↑(#s) : ℤ)
⊢ ∃ x_1 < #s, c + (↑x_1 : ℤ) = x
have h : (x - c).toNat < #s ∧ c + (↑(x - c).toNat : ℤ) = x
Tactic: use (x - c).toNat
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
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
⊢ 1 ≤ a
have rwa : a ⊓ 1 = 1
Tactic: rwa [← inf_eq_right, ← mul_eq_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
ha : 1 ≤ HPow.hPow (β := ℕ) a 2
⊢ 1 ≤ a
have suffices : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
Tactic: suffices this : (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1 by
    rwa [← inf_eq_right, ← mul_eq_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a : α
ha : 1 ≤ HPow.hPow (β := ℕ) a 2
⊢ (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
have rw : (a ⊓ 1) * a ⊓ (a ⊓ 1) * 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
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
⊢ (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
have rw₁ : a * a ⊓ 1 * a ⊓ (a ⊓ 1) * 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
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
⊢ (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
have rw₂ : HPow.hPow (β := ℕ) a 2 ⊓ 1 * a ⊓ (a ⊓ 1) * 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
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
⊢ (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
have rw₃ : HPow.hPow (β := ℕ) a 2 ⊓ 1 * a ⊓ (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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
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
⊢ (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
have rw₄ : HPow.hPow (β := ℕ) a 2 ⊓ a ⊓ (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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
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
⊢ (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
have rw₅ : HPow.hPow (β := ℕ) a 2 ⊓ (a ⊓ (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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
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
⊢ (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
have rw₆ : HPow.hPow (β := ℕ) a 2 ⊓ (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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
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
⊢ (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
have rw₇ : a ⊓ 1 ⊓ HPow.hPow (β := ℕ) a 2 = 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
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
⊢ (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
have rw₈ : a ⊓ (1 ⊓ HPow.hPow (β := ℕ) a 2) = 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
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
⊢ (a ⊓ 1) * (a ⊓ 1) = a ⊓ 1
have rw₉ : 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹))
have rw : (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a * b * b⁻¹ ⊔ a * b * a⁻¹)
Tactic: rw [mul_sup b⁻¹ a⁻¹ (a * b), mul_inv_cancel_right, mul_inv_cancel_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
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⁻¹)
⊢ (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹))
have rw₁ : (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a ⊔ a * b * a⁻¹)
Tactic: rw [mul_sup b⁻¹ a⁻¹ (a * b), mul_inv_cancel_right, mul_inv_cancel_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
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⁻¹)
⊢ (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹))
have rw₂ : (a ⊓ b) * (a ⊔ b) = (a ⊓ b) * (a ⊔ b)
Tactic: rw [mul_sup b⁻¹ a⁻¹ (a * b), mul_inv_cancel_right, mul_inv_cancel_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹)) = (a ⊓ b) * (a * b * (a ⊓ b)⁻¹)
have rw : (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹)) = (a ⊓ b) * (a * b * (a⁻¹ ⊔ b⁻¹))
Tactic: rw [inv_inf, sup_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
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⁻¹))
⊢ (a ⊓ b) * (a * b * (b⁻¹ ⊔ a⁻¹)) = (a ⊓ b) * (a * b * (a ⊓ b)⁻¹)
have rw₁ : (a ⊓ b) * (a * b * (a⁻¹ ⊔ b⁻¹)) = (a ⊓ b) * (a * b * (a⁻¹ ⊔ b⁻¹))
Tactic: rw [inv_inf, sup_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
⊢ (a ⊓ b) * (a * b * (a ⊓ b)⁻¹) = a * b
have rw : a * b * (a ⊓ b)⁻¹ * (a ⊓ b) = a * b
Tactic: rw [mul_comm, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : CommGroup α
inst_2 : MulLeftMono α
a b : α
rw : a * b * (a ⊓ b)⁻¹ * (a ⊓ b) = a * b
⊢ (a ⊓ b) * (a * b * (a ⊓ b)⁻¹) = a * b
have rw₁ : a * b = a * b
Tactic: rw [mul_comm, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
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) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
have rw : x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y ∧ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
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⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y ∧ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z
have left : x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
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
⊢ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y ∧ x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z
have right : x⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
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⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ y
have left : (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ (x ⊓ y) * (x ⊔ y)
Tactic: rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x y]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Lattice (goal)
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⁻¹ * ((x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z))) ≤ z
have right : (x ⊓ (y ⊓ z)) * ((x ⊔ y) ⊓ (x ⊔ z)) ≤ (x ⊓ z) * (x ⊔ z)
Tactic: rw [inv_mul_le_iff_le_mul, ← inf_mul_sup x z]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.MinMax (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
⊢ max a 1 / max a⁻¹ 1 = a
have inl : ∀ (h : a ≤ 1), max a 1 / max a⁻¹ 1 = a
Tactic: rcases le_total a 1 with (h | h)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.MinMax (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
inl : ∀ (h : a ≤ 1), max a 1 / max a⁻¹ 1 = a
⊢ max a 1 / max a⁻¹ 1 = a
have inr : ∀ (h : 1 ≤ a), max a 1 / max a⁻¹ 1 = a
Tactic: rcases le_total a 1 with (h | h)
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.MinMax (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
⊢ max a⁻¹ 1 = a⁻¹ * max a 1
have rw : a * max a⁻¹ 1 = max a 1
Tactic: rw [eq_inv_mul_iff_mul_eq, ← eq_div_iff_mul_eq', max_one_div_max_inv_one_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.MinMax (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
rw : a * max a⁻¹ 1 = max a 1
⊢ max a⁻¹ 1 = a⁻¹ * max a 1
have rw₁ : a = max a 1 / max a⁻¹ 1
Tactic: rw [eq_inv_mul_iff_mul_eq, ← eq_div_iff_mul_eq', max_one_div_max_inv_one_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.MinMax (goal)
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
⊢ max a⁻¹ 1 = a⁻¹ * max a 1
have rw₂ : a = a
Tactic: rw [eq_inv_mul_iff_mul_eq, ← eq_div_iff_mul_eq', max_one_div_max_inv_one_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.MinMax (goal)
Goal:
G₀ : Type u_1
inst : Inv G₀
inst_1 : LinearOrder G₀
x y : G₀
⊢ min x⁻¹ y⁻¹ ≤ (max x y)⁻¹
have inl : x ≤ y → min x⁻¹ y⁻¹ ≤ (max x y)⁻¹
Tactic: cases le_total x y
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.MinMax (goal)
Goal:
G₀ : Type u_1
inst : Inv G₀
inst_1 : LinearOrder G₀
x y : G₀
inl : x ≤ y → min x⁻¹ y⁻¹ ≤ (max x y)⁻¹
⊢ min x⁻¹ y⁻¹ ≤ (max x y)⁻¹
have inr : y ≤ x → min x⁻¹ y⁻¹ ≤ (max x y)⁻¹
Tactic: cases le_total x y
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.MinMax (goal)
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|
have refine_1 : max a b - max c d ≤ max |a - c| |b - d|
Tactic: refine abs_sub_le_iff.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.MinMax (goal)
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|
⊢ |max a b - max c d| ≤ max |a - c| |b - d|
have refine_2 : max c d - max a b ≤ max |a - c| |b - d|
Tactic: refine abs_sub_le_iff.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.MinMax (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
a b c d : α
⊢ max c d - max a b ≤ max |a - c| |b - d|
have refine_2 : max c d - max a b ≤ max |c - a| |d - b|
Tactic: rw [abs_sub_comm a c, abs_sub_comm b d]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (hypothesis)
Goal:
α : Type u_1
a : α
s : Multiset α
h : a ∈ HSMul.hSMul (α := ℕ) 0 s
⊢ a ∈ s
have h₁ : Membership.mem (γ := Multiset α) 0 a
Tactic: rw [zero_nsmul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (hypothesis)
Goal:
α : Type u_1
a : α
s : Multiset α
n : ℕ
ih : ∀ (h : a ∈ n • s), a ∈ s
h : a ∈ (n + 1) • s
⊢ a ∈ s
have h₁ : a ∈ n • s ∨ a ∈ s
Tactic: rw [succ_nsmul, mem_add] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : a ∈ n • s
⊢ a ∈ s
have zero : ∀ (h : a ∈ HSMul.hSMul (α := ℕ) 0 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
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : a ∈ n • s
zero : ∀ (h : a ∈ HSMul.hSMul (α := ℕ) 0 s), a ∈ s
⊢ a ∈ s
have succ : ∀ (n : ℕ) (ih : ∀ (h : a ∈ n • s), a ∈ s) (h : a ∈ (n + 1) • 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
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
a : α
s : Multiset α
n : ℕ
⊢ a ∈ n • s ↔ n ≠ 0 ∧ a ∈ s
have refine_1 : ∀ (ha : a ∈ n • s), n ≠ 0
Tactic: refine ⟨fun ha ↦ ⟨?_, mem_of_mem_nsmul ha⟩, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
a : α
s : Multiset α
n : ℕ
refine_1 : ∀ (ha : a ∈ n • s), n ≠ 0
⊢ a ∈ n • s ↔ n ≠ 0 ∧ a ∈ s
have refine_2 : ∀ (h : n ≠ 0 ∧ a ∈ s), a ∈ n • s
Tactic: refine ⟨fun ha ↦ ⟨?_, mem_of_mem_nsmul ha⟩, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n ≠ 0 ∧ a ∈ s
⊢ a ∈ n • s
have refine_2 : ∀ (n : ℕ) (h : n.succ ≠ 0 ∧ a ∈ s), a ∈ n.succ • s
Tactic: obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero h.1
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
a : α
s : Multiset α
n : ℕ
h : n.succ ≠ 0 ∧ a ∈ s
⊢ a ∈ n.succ • s
have refine_2 : a ∈ n • s ∨ a ∈ s
Tactic: rw [succ_nsmul, mem_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
s : Multiset α
n : ℕ
a : α
⊢ n • (a ::ₘ s) = HSMul.hSMul (β := Multiset α) n {a} + n • s
have rw : n • ({a} + s) = HSMul.hSMul (β := Multiset α) n {a} + n • s
Tactic: rw [← singleton_add, nsmul_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
s : Multiset α
n : ℕ
a : α
rw : n • ({a} + s) = HSMul.hSMul (β := Multiset α) n {a} + n • s
⊢ n • (a ::ₘ s) = HSMul.hSMul (β := Multiset α) n {a} + n • s
have rw₁ : HSMul.hSMul (β := Multiset α) n {a} + n • s = HSMul.hSMul (β := Multiset α) n {a} + n • s
Tactic: rw [← singleton_add, nsmul_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
a : α
n : ℕ
⊢ HSMul.hSMul (β := Multiset α) n {a} = replicate n a
have rw : n • replicate 1 a = replicate n a
Tactic: rw [← replicate_one, nsmul_replicate, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
a : α
n : ℕ
rw : n • replicate 1 a = replicate n a
⊢ HSMul.hSMul (β := Multiset α) n {a} = replicate n a
have rw₁ : replicate (n * 1) a = replicate n a
Tactic: rw [← replicate_one, nsmul_replicate, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
a : α
n : ℕ
rw : n • replicate 1 a = replicate n a
rw₁ : replicate (n * 1) a = replicate n a
⊢ HSMul.hSMul (β := Multiset α) n {a} = replicate n a
have rw₂ : replicate n a = replicate n a
Tactic: rw [← replicate_one, nsmul_replicate, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
⊢ filter p (n • s) = n • filter p s
have refine_1 : filter p (HSMul.hSMul (β := Multiset α) n 0) = n • filter p 0
Tactic: refine s.induction_on ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
refine_1 : filter p (HSMul.hSMul (β := Multiset α) n 0) = n • filter p 0
⊢ filter p (n • s) = n • filter p s
have refine_2 : ∀ (a : α) (s : Multiset α), filter p (n • s) = n • filter p s → filter p (n • (a ::ₘ s)) = n • filter p (a ::ₘ s)
Tactic: refine s.induction_on ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (n • (a ::ₘ ha)) = n • filter p (a ::ₘ ha)
have refine_2 : filter p (HSMul.hSMul (β := Multiset α) n {a}) + n • filter p ha =
  HSMul.hSMul (β := Multiset α) n (if p a then {a} else 0) + n • filter p ha
Tactic: rw [nsmul_cons, filter_add, ih, filter_cons, nsmul_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (HSMul.hSMul (β := Multiset α) n {a}) + n • filter p ha =
    HSMul.hSMul (β := Multiset α) n (if p a then {a} else 0) + n • filter p ha
have refine_2 : filter p (HSMul.hSMul (β := Multiset α) n {a}) = HSMul.hSMul (β := Multiset α) n (if p a then {a} else 0)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
⊢ filter p (HSMul.hSMul (β := Multiset α) n {a}) = HSMul.hSMul (β := Multiset α) n (if p a then {a} else 0)
have pos : ∀ (hp : p a), filter p (HSMul.hSMul (β := Multiset α) n {a}) = HSMul.hSMul (β := Multiset α) n {a}
Tactic: split_ifs with hp
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
pos : ∀ (hp : p a), filter p (HSMul.hSMul (β := Multiset α) n {a}) = HSMul.hSMul (β := Multiset α) n {a}
⊢ filter p (HSMul.hSMul (β := Multiset α) n {a}) = HSMul.hSMul (β := Multiset α) n (if p a then {a} else 0)
have neg : ∀ (hp : ¬p a), filter p (HSMul.hSMul (β := Multiset α) n {a}) = HSMul.hSMul (β := Multiset α) n 0
Tactic: split_ifs with hp
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : p a
⊢ filter p (HSMul.hSMul (β := Multiset α) n {a}) = HSMul.hSMul (β := Multiset α) n {a}
have pos : ∀ (a_1 : α), a_1 ∈ HSMul.hSMul (β := Multiset α) n {a} → p a_1
Tactic: simp only [filter_eq_self, nsmul_zero, filter_eq_nil]
-- Lean 4 proof step from Mathlib.Algebra.Order.Group.Multiset (goal)
Goal:
α : Type u_1
p : α → Prop
inst : DecidablePred p
s : Multiset α
n : ℕ
a : α
ha : Multiset α
ih : filter p (n • ha) = n • filter p ha
hp : ¬p a
⊢ filter p (HSMul.hSMul (β := Multiset α) n {a}) = HSMul.hSMul (β := Multiset α) n 0
have neg : ∀ (a_1 : α), a_1 ∈ HSMul.hSMul (β := Multiset α) n {a} → ¬p a_1
Tactic: simp only [filter_eq_self, nsmul_zero, filter_eq_nil]