awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : LowerSet α
rw : ⋃ (a : α), ⋃ (_ : Membership.mem (γ := Set α) (Set.Iic 1) a), a • (↑s : Set α) ⊆ (↑s : Set α)
⊢ Set.Iic 1 * (↑s : Set α) ⊆ (↑s : Set α)

Tactic:
rw [← smul_eq_mul, ← Set.iUnion_smul_set]

Premises used: Set.iUnion_smul_set, smul_eq_mul
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : LowerSet α
⊢ ⋃ (a : α), ⋃ (_ : Membership.mem (γ := Set α) (Set.Iic 1) a), a • (↑s : Set α) ⊆ (↑s : Set α)

Tactic:
Set.iUnion₂_subset fun _ ↦ s.lower.smul_subset

Premises used: Set.iUnion₂_subset, IsLowerSet.smul_subset, LowerSet.lower
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : LowerSet α
⊢ ⋃ (a : α), ⋃ (_ : Membership.mem (γ := Set α) (Set.Iic 1) a), a • (↑s : Set α) ⊆ (↑s : Set α)

Tactic:
exact Set.iUnion₂_subset fun _ ↦ s.lower.smul_subset

Premises used: Set.iUnion₂_subset, IsLowerSet.smul_subset, LowerSet.lower
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s_1 t : Set α
a : α
s : LowerSet α
rw : 1 * s = s
⊢ s * 1 = s

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s_1 t : Set α
a : α
s : LowerSet α
⊢ 1 * s = s

Tactic:
one_mul _

Premises used: _private.0.LowerSet.one_mul
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s_1 t : Set α
a : α
s : LowerSet α
⊢ 1 * s = s

Tactic:
exact one_mul _

Premises used: _private.0.LowerSet.one_mul
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
⊢ Eq.{u_1 + 1} (α := UpperSet α) (upperClosure 1) 1

Tactic:
upperClosure_singleton _

Premises used: upperClosure_singleton
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
⊢ Eq.{u_1 + 1} (α := LowerSet α) (lowerClosure 1) 1

Tactic:
lowerClosure_singleton _

Premises used: lowerClosure_singleton
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
a : α
⊢ upperClosure (a • s) = HSMul.hSMul (β := UpperSet α) a (upperClosure s)

Tactic:
upperClosure_image <| OrderIso.mulLeft a

Premises used: upperClosure_image, OrderIso.mulLeft
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s : Set α
a : α
⊢ lowerClosure (a • s) = HSMul.hSMul (β := LowerSet α) a (lowerClosure s)

Tactic:
lowerClosure_image <| OrderIso.mulLeft a

Premises used: lowerClosure_image, OrderIso.mulLeft
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
simp_rw :
  Eq.{u_1 + 1} (α := Set α) (⋃ a ∈ s, a • (↑(upperClosure t) : Set α))
    (⋃ i ∈ s, (↑(HSMul.hSMul (β := UpperSet α) i (upperClosure t)) : Set α))
⊢ s * (↑(upperClosure t) : Set α) = (↑(upperClosure (s * t)) : Set α)

Tactic:
simp_rw [← smul_eq_mul, ← Set.iUnion_smul_set, upperClosure_iUnion, upperClosure_smul,
    UpperSet.coe_iInf₂]

Premises used: UpperSet.coe_iInf₂, Set.iUnion_smul_set, smul_eq_mul, upperClosure_iUnion, upperClosure_smul
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ a ∈ s, a • (↑(upperClosure t) : Set α))
    (⋃ i ∈ s, (↑(HSMul.hSMul (β := UpperSet α) i (upperClosure t)) : Set α))

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
simp_rw :
  Eq.{u_1 + 1} (α := Set α) (⋃ a ∈ s, a • (↑(lowerClosure t) : Set α))
    (⋃ i ∈ s, (↑(HSMul.hSMul (β := LowerSet α) i (lowerClosure t)) : Set α))
⊢ s * (↑(lowerClosure t) : Set α) = (↑(lowerClosure (s * t)) : Set α)

Tactic:
simp_rw [← smul_eq_mul, ← Set.iUnion_smul_set, lowerClosure_iUnion, lowerClosure_smul,
    LowerSet.coe_iSup₂]

Premises used: Set.iUnion_smul_set, lowerClosure_iUnion, LowerSet.coe_iSup₂, lowerClosure_smul, smul_eq_mul
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ a ∈ s, a • (↑(lowerClosure t) : Set α))
    (⋃ i ∈ s, (↑(HSMul.hSMul (β := LowerSet α) i (lowerClosure t)) : Set α))

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
simp_rw : t * (↑(upperClosure s) : Set α) = (↑(upperClosure (t * s)) : Set α)
⊢ (↑(upperClosure s) : Set α) * t = (↑(upperClosure (s * t)) : Set α)

Tactic:
simp_rw [mul_comm _ t]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
⊢ t * (↑(upperClosure s) : Set α) = (↑(upperClosure (t * s)) : Set α)

Tactic:
mul_upperClosure _ _

Premises used: mul_upperClosure
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
⊢ t * (↑(upperClosure s) : Set α) = (↑(upperClosure (t * s)) : Set α)

Tactic:
exact mul_upperClosure _ _

Premises used: mul_upperClosure
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
simp_rw : t * (↑(lowerClosure s) : Set α) = (↑(lowerClosure (t * s)) : Set α)
⊢ (↑(lowerClosure s) : Set α) * t = (↑(lowerClosure (s * t)) : Set α)

Tactic:
simp_rw [mul_comm _ t]

Premises used: mul_comm
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
⊢ t * (↑(lowerClosure s) : Set α) = (↑(lowerClosure (t * s)) : Set α)

Tactic:
mul_lowerClosure _ _

Premises used: mul_lowerClosure
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
⊢ t * (↑(lowerClosure s) : Set α) = (↑(lowerClosure (t * s)) : Set α)

Tactic:
exact mul_lowerClosure _ _

Premises used: mul_lowerClosure
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
rw : (↑(upperClosure (s * t)) : Set α) = (↑(upperClosure s) : Set α) * (↑(upperClosure t) : Set α)
rw₁ : (↑(upperClosure (s * t)) : Set α) = (↑(upperClosure ((↑(upperClosure s) : Set α) * t)) : Set α)
rw₂ : (↑(upperClosure (s * t)) : Set α) = (↑(upperClosure (↑(upperClosure (s * t)) : Set α)) : Set α)
rw₃ rw₄ : (↑(upperClosure (s * t)) : Set α) = (↑(upperClosure (s * t)) : Set α)
⊢ (↑(upperClosure (s * t)) : Set α) = (↑(HMul.hMul (α := UpperSet α) (upperClosure s) (upperClosure t)) : Set α)

Tactic:
rw [UpperSet.coe_mul, mul_upperClosure, upperClosure_mul, UpperSet.upperClosure]

Premises used: upperClosure_mul, UpperSet.coe_mul, UpperSet.upperClosure, mul_upperClosure
-- Module: Mathlib.Algebra.Order.UpperLower
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
s t : Set α
rw : (↑(lowerClosure (s * t)) : Set α) = (↑(lowerClosure s) : Set α) * (↑(lowerClosure t) : Set α)
rw₁ : (↑(lowerClosure (s * t)) : Set α) = (↑(lowerClosure ((↑(lowerClosure s) : Set α) * t)) : Set α)
rw₂ : (↑(lowerClosure (s * t)) : Set α) = (↑(lowerClosure (↑(lowerClosure (s * t)) : Set α)) : Set α)
rw₃ rw₄ : (↑(lowerClosure (s * t)) : Set α) = (↑(lowerClosure (s * t)) : Set α)
⊢ (↑(lowerClosure (s * t)) : Set α) = (↑(HMul.hMul (α := LowerSet α) (lowerClosure s) (lowerClosure t)) : Set α)

Tactic:
rw [LowerSet.coe_mul, mul_lowerClosure, lowerClosure_mul, LowerSet.lowerClosure]

Premises used: lowerClosure_mul, mul_lowerClosure, LowerSet.lowerClosure, LowerSet.coe_mul
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : Zero α
a : WithTop α
⊢ a.untop₀ = 0 ↔ a = 0 ∨ a = ⊤

Tactic:
simp [untop₀]

Premises used: WithTop.untop₀
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : Zero α
⊢ Eq.{u_1 + 1} (α := α) (untop₀ ⊤) 0

Tactic:
simp [untop₀]

Premises used: WithTop.untop₀
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : Zero α
⊢ Eq.{u_1 + 1} (α := α) (untop₀ 0) 0

Tactic:
simp [untop₀]

Premises used: WithTop.untop₀
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : Zero α
a : α
⊢ (↑a : WithTop α).untop₀ = a

Tactic:
rfl

Premises used: WithTop.untop₀, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : Zero α
a : WithTop α
ha : a ≠ ⊤
obtain : ∀ (b : α) (hb : (↑b : WithTop α) = a), (↑a.untop₀ : WithTop α) = a
⊢ (↑a.untop₀ : WithTop α) = a

Tactic:
obtain ⟨b, hb⟩ := WithTop.ne_top_iff_exists.1 ha

Premises used: WithTop.ne_top_iff_exists, Iff.mp
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : Zero α
a : WithTop α
ha : a ≠ ⊤
b : α
hb : (↑b : WithTop α) = a
⊢ (↑a.untop₀ : WithTop α) = a

Tactic:
simp [← hb]
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : Add α
a b : WithTop α
c : α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a ≠ ⊤

Tactic:
ha
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : Add α
a b : WithTop α
c : α
ha : a ≠ ⊤
hb : b ≠ ⊤
lift : ∀ (a : α), untopD c ((↑a : WithTop α) + b) = untopD c (↑a : WithTop α) + untopD c b
⊢ untopD c (a + b) = untopD c a + untopD c b

Tactic:
lift a to α using ha
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : Add α
b : WithTop α
c : α
hb : b ≠ ⊤
a : α
⊢ b ≠ ⊤

Tactic:
hb
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : Add α
b : WithTop α
c : α
hb : b ≠ ⊤
a : α
lift : ∀ (b : α), untopD c ((↑a : WithTop α) + (↑b : WithTop α)) = untopD c (↑a : WithTop α) + untopD c (↑b : WithTop α)
⊢ untopD c ((↑a : WithTop α) + b) = untopD c (↑a : WithTop α) + untopD c b

Tactic:
lift b to α using hb
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : Add α
c a b : α
⊢ untopD c ((↑a : WithTop α) + (↑b : WithTop α)) = untopD c (↑a : WithTop α) + untopD c (↑b : WithTop α)

Tactic:
simp [← coe_add]

Premises used: WithTop.coe_add
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddZeroClass α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ (a + b).untop₀ = a.untop₀ + b.untop₀

Tactic:
untopD_add ha hb

Premises used: WithTop.untop₀, WithTop.untopD_add
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (untop₀ (↑n : WithTop α)) (↑n : α)

Tactic:
rfl

Premises used: WithTop.untop₀, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddMonoidWithOne α
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u_1 + 1} (α := α) (untop₀ (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
rfl

Premises used: WithTop.untop₀, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
⊢ Eq.{u_1 + 1} (α := α) (untop₀ (-⊤)) (-untop₀ ⊤)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : MulZeroClass α
a b : WithTop α
⊢ (a * b).untop₀ = a.untop₀ * b.untop₀

Tactic:
untopD_zero_mul a b

Premises used: WithTop.untop₀, WithTop.untopD_zero_mul
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
top : LE.le.{u_1} (α := α) 0 (untop₀ ⊤) → LE.le.{u_1} (α := WithTop α) 0 ⊤
top₁ : LE.le.{u_1} (α := WithTop α) 0 ⊤ → LE.le.{u_1} (α := α) 0 (untop₀ ⊤)
top₂ top₃ top₄ : LE.le.{u_1} (α := α) 0 (untop₀ ⊤) → LE.le.{u_1} (α := WithTop α) 0 ⊤
top₅ top₆ top₇ : LE.le.{u_1} (α := WithTop α) 0 ⊤ → LE.le.{u_1} (α := α) 0 0
top₈ top₉ top₁₀ : LE.le.{u_1} (α := α) 0 (untop₀ ⊤) → LE.le.{u_1} (α := WithTop α) 0 ⊤
top₁₁ top₁₂ top₁₃ : LE.le.{u_1} (α := WithTop α) 0 ⊤ → LE.le.{u_1} (α := α) 0 0
top₁₄ top₁₅ : LE.le.{u_1} (α := α) 0 (untop₀ ⊤) → LE.le.{u_1} (α := WithTop α) 0 ⊤
top₁₆ : LE.le.{u_1} (α := WithTop α) 0 ⊤ → LE.le.{u_1} (α := α) 0 0
⊢ LE.le.{u_1} (α := α) 0 (untop₀ ⊤) ↔ LE.le.{u_1} (α := WithTop α) 0 ⊤

Tactic:
tauto
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a : α
⊢ 0 ≤ (↑a : WithTop α).untop₀ ↔ 0 ≤ (↑a : WithTop α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a : WithTop α
top : LE.le.{u_1} (α := α) 0 (untop₀ ⊤) ↔ LE.le.{u_1} (α := WithTop α) 0 ⊤
coe : ∀ (a : α), 0 ≤ (↑a : WithTop α).untop₀ ↔ 0 ≤ (↑a : WithTop α)
⊢ 0 ≤ a.untop₀ ↔ 0 ≤ a

Tactic:
cases a with
  | top => tauto
  | coe a => simp

Premises used: WithTop.top, WithTop.coe
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a b : WithTop α
ha : a ≠ ⊤
h : a.untop₀ ≤ b.untop₀
⊢ a ≠ ⊤

Tactic:
ha
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a b : WithTop α
ha : a ≠ ⊤
h : a.untop₀ ≤ b.untop₀
lift : ∀ (a : α) (h : (↑a : WithTop α).untop₀ ≤ b.untop₀), (↑a : WithTop α) ≤ b
⊢ a ≤ b

Tactic:
lift a to α using ha
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
b : WithTop α
a : α
h : (↑a : WithTop α).untop₀ ≤ b.untop₀
pos : ∀ (hb : b = ⊤), (↑a : WithTop α) ≤ b
neg : ∀ (hb : ¬b = ⊤), (↑a : WithTop α) ≤ b
⊢ (↑a : WithTop α) ≤ b

Tactic:
by_cases hb : b = ⊤
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
b : WithTop α
a : α
h : (↑a : WithTop α).untop₀ ≤ b.untop₀
hb : b = ⊤
⊢ (↑a : WithTop α) ≤ b

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
b : WithTop α
a : α
h : (↑a : WithTop α).untop₀ ≤ b.untop₀
hb : ¬b = ⊤
⊢ b ≠ ⊤

Tactic:
hb
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
b : WithTop α
a : α
h : (↑a : WithTop α).untop₀ ≤ b.untop₀
hb : ¬b = ⊤
neg : ∀ (b : α) (h : (↑a : WithTop α).untop₀ ≤ (↑b : WithTop α).untop₀), (↑a : WithTop α) ≤ (↑b : WithTop α)
⊢ (↑a : WithTop α) ≤ b

Tactic:
lift b to α using hb
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a b : α
h : (↑a : WithTop α).untop₀ ≤ (↑b : WithTop α).untop₀
⊢ (↑a : WithTop α) ≤ (↑b : WithTop α)

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a b : WithTop α
hb : b ≠ ⊤
h : a ≤ b
⊢ b ≠ ⊤

Tactic:
hb
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a b : WithTop α
hb : b ≠ ⊤
h : a ≤ b
lift : ∀ (b : α) (h : a ≤ (↑b : WithTop α)), a.untop₀ ≤ (↑b : WithTop α).untop₀
⊢ a.untop₀ ≤ b.untop₀

Tactic:
lift b to α using hb
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a : WithTop α
b : α
h : a ≤ (↑b : WithTop α)
pos : ∀ (ha : a = ⊤), a.untop₀ ≤ (↑b : WithTop α).untop₀
neg : ∀ (ha : ¬a = ⊤), a.untop₀ ≤ (↑b : WithTop α).untop₀
⊢ a.untop₀ ≤ (↑b : WithTop α).untop₀

Tactic:
by_cases ha : a = ⊤
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a : WithTop α
b : α
h : a ≤ (↑b : WithTop α)
ha : a = ⊤
⊢ a.untop₀ ≤ (↑b : WithTop α).untop₀

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a : WithTop α
b : α
h : a ≤ (↑b : WithTop α)
ha : ¬a = ⊤
⊢ a ≠ ⊤

Tactic:
ha
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a : WithTop α
b : α
h : a ≤ (↑b : WithTop α)
ha : ¬a = ⊤
neg : ∀ (a : α) (h : (↑a : WithTop α) ≤ (↑b : WithTop α)), (↑a : WithTop α).untop₀ ≤ (↑b : WithTop α).untop₀
⊢ a.untop₀ ≤ (↑b : WithTop α).untop₀

Tactic:
lift a to α using ha
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
b a : α
h : (↑a : WithTop α) ≤ (↑b : WithTop α)
⊢ (↑a : WithTop α).untop₀ ≤ (↑b : WithTop α).untop₀

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a ≠ ⊤

Tactic:
ha
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
lift : ∀ (a : α), (↑a : WithTop α).untop₀ ≤ b.untop₀ ↔ (↑a : WithTop α) ≤ b
⊢ a.untop₀ ≤ b.untop₀ ↔ a ≤ b

Tactic:
lift a to α using ha
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
b : WithTop α
hb : b ≠ ⊤
a : α
⊢ b ≠ ⊤

Tactic:
hb
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
b : WithTop α
hb : b ≠ ⊤
a : α
lift : ∀ (b : α), (↑a : WithTop α).untop₀ ≤ (↑b : WithTop α).untop₀ ↔ (↑a : WithTop α) ≤ (↑b : WithTop α)
⊢ (↑a : WithTop α).untop₀ ≤ b.untop₀ ↔ (↑a : WithTop α) ≤ b

Tactic:
lift b to α using hb
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : PartialOrder α
a b : α
⊢ (↑a : WithTop α).untop₀ ≤ (↑b : WithTop α).untop₀ ↔ (↑a : WithTop α) ≤ (↑b : WithTop α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a ≠ ⊤

Tactic:
ha
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
lift : ∀ (a : α), (max (↑a : WithTop α) b).untop₀ = max (↑a : WithTop α).untop₀ b.untop₀
⊢ (max a b).untop₀ = max a.untop₀ b.untop₀

Tactic:
lift a to α using ha
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
b : WithTop α
hb : b ≠ ⊤
a : α
⊢ b ≠ ⊤

Tactic:
hb
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
b : WithTop α
hb : b ≠ ⊤
a : α
lift : ∀ (b : α), (max (↑a : WithTop α) (↑b : WithTop α)).untop₀ = max (↑a : WithTop α).untop₀ (↑b : WithTop α).untop₀
⊢ (max (↑a : WithTop α) b).untop₀ = max (↑a : WithTop α).untop₀ b.untop₀

Tactic:
lift b to α using hb
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : α
simp : (max (↑a : WithTop α) (↑b : WithTop α)).untop₀ = max a b
⊢ (max (↑a : WithTop α) (↑b : WithTop α)).untop₀ = max (↑a : WithTop α).untop₀ (↑b : WithTop α).untop₀

Tactic:
simp only [untop₀_coe]

Premises used: WithTop.untop₀_coe
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : α
pos : ∀ (h : a ≤ b), (max (↑a : WithTop α) (↑b : WithTop α)).untop₀ = max a b
neg : ∀ (h : ¬a ≤ b), (max (↑a : WithTop α) (↑b : WithTop α)).untop₀ = max a b
⊢ (max (↑a : WithTop α) (↑b : WithTop α)).untop₀ = max a b

Tactic:
by_cases h : a ≤ b
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : α
h : a ≤ b
⊢ (max (↑a : WithTop α) (↑b : WithTop α)).untop₀ = max a b

Tactic:
simp [max_eq_right h, max_eq_right (coe_le_coe.mpr h)]

Premises used: Iff.mpr, max_eq_right, WithTop.coe_le_coe
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ b < a

Tactic:
rw [not_le] at h

Premises used: not_le
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : α
h : b < a
⊢ (max (↑a : WithTop α) (↑b : WithTop α)).untop₀ = max a b

Tactic:
simp [max_eq_left h.le, max_eq_left (coe_lt_coe.mpr h).le]

Premises used: Iff.mpr, LT.lt.le, max_eq_left, WithTop.coe_lt_coe
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : WithTop α
ha : a ≠ ⊤
hb : b ≠ ⊤
lift : ∀ (a : α), (min (↑a : WithTop α) b).untop₀ = min (↑a : WithTop α).untop₀ b.untop₀
⊢ (min a b).untop₀ = min a.untop₀ b.untop₀

Tactic:
lift a to α using ha
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
b : WithTop α
hb : b ≠ ⊤
a : α
lift : ∀ (b : α), (min (↑a : WithTop α) (↑b : WithTop α)).untop₀ = min (↑a : WithTop α).untop₀ (↑b : WithTop α).untop₀
⊢ (min (↑a : WithTop α) b).untop₀ = min (↑a : WithTop α).untop₀ b.untop₀

Tactic:
lift b to α using hb
-- Module: Mathlib.Algebra.Order.WithTop.Untop0
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
a b : α
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  (↑(min a b) : WithTop α).untop₀ = min (↑a : WithTop α).untop₀ (↑b : WithTop α).untop₀
⊢ (min (↑a : WithTop α) (↑b : WithTop α)).untop₀ = min (↑a : WithTop α).untop₀ (↑b : WithTop α).untop₀

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.ZeroLEOne
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : LE α
inst_3 : ZeroLEOneClass α
⊢ LE.le.{u_1} (α := α) 0 1

Tactic:
ZeroLEOneClass.zero_le_one

Premises used: ZeroLEOneClass.zero_le_one
-- Module: Mathlib.Algebra.Order.ZeroLEOne
Goal:
α : Type u_2
inst : Zero α
inst_1 : One α
inst_2 : LE α
inst_3 : ZeroLEOneClass α
⊢ LE.le.{u_2} (α := α) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Algebra.Order.ZeroLEOne
Goal:
α : Type u_1
R : Type u_2
S : Type u_3
inst : Zero R
inst_1 : One R
inst_2 : LE R
inst_3 : ZeroLEOneClass R
inst_4 : Zero S
inst_5 : One S
inst_6 : LE S
inst_7 : ZeroLEOneClass S
⊢ ZeroLEOneClass (R × S)

Tactic:
⟨⟨zero_le_one, zero_le_one⟩⟩

Premises used: ZeroLEOneClass.mk, zero_le_one, And.intro
-- Module: Mathlib.Algebra.Order.ZeroLEOne
Goal:
α : Type u_1
ι : Type u_2
R : ι → Type u_3
inst : (i : ι) → Zero (R i)
inst_1 : (i : ι) → One (R i)
inst_2 : (i : ι) → LE (R i)
inst_3 : ∀ (i : ι), ZeroLEOneClass.{u_3} (R i)
⊢ ZeroLEOneClass ((i : ι) → R i)

Tactic:
⟨fun _ ↦ zero_le_one⟩

Premises used: ZeroLEOneClass.mk, zero_le_one
-- Module: Mathlib.Algebra.Order.ZeroLEOne
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : PartialOrder α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
⊢ LT.lt.{u_1} (α := α) 0 1

Tactic:
zero_le_one.lt_of_ne (NeZero.ne' 1)

Premises used: NeZero.ne', zero_le_one, LE.le.lt_of_ne, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.ZeroLEOne
Goal:
α : Type u_1
inst : Zero α
inst_1 : One α
inst_2 : PartialOrder α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
⊢ LT.lt.{u_1} (α := α) 0 1

Tactic:
zero_lt_one

Premises used: zero_lt_one
-- Module: Mathlib.Algebra.Order.ZeroLEOne
Goal:
α : Type u_1
⊢ ZeroLEOneClass ℕ

Tactic:
⟨Nat.le_of_lt Nat.zero_lt_one⟩

Premises used: ZeroLEOneClass.mk, Nat.le_of_lt, Nat.zero_lt_one
-- Module: Mathlib.Algebra.Order.ZeroLEOne
Goal:
α : Type u_1
⊢ ZeroLEOneClass Int

Tactic:
⟨Int.le_of_lt Int.zero_lt_one⟩

Premises used: ZeroLEOneClass.mk, Int.zero_lt_one, Int.le_of_lt
-- Module: Mathlib.Algebra.Order.ZeroLEOne
Goal:
α : Type u_1
⊢ LE.le (α := Rat) 0 1

Tactic:
decide
-- Module: Mathlib.Algebra.PEmptyInstances
Goal:
x x_1 : PEmpty
⊢ PEmpty

Tactic:
cases x
-- Module: Mathlib.Algebra.PEmptyInstances
Goal:
x y z : PEmpty
⊢ x * y * z = x * (y * z)

Tactic:
cases x
-- Module: Mathlib.Algebra.Pointwise.Stabilizer
Goal:
G : Type u_1
α : Type u_3
inst : Group G
inst_1 : MulAction G α
⊢ Eq (α := Subgroup G) (stabilizer.{u_1, u_3} G (α := Set α) ∅) ⊤

Tactic:
Subgroup.coe_eq_univ.1 <| eq_univ_of_forall fun _a ↦ smul_set_empty

Premises used: Set.smul_set_empty, Set.eq_univ_of_forall, Subgroup.coe_eq_univ, Iff.mp