awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
a : α
⊢ map (⇑f : (a : α) → β) ((↑a : WithBot α) + ⊥) =
    HAdd.hAdd (α := WithBot β) (map (⇑f : (a : α) → β) (↑a : WithBot α)) (map.{u, v} (α := α) (⇑f : (a : α) → β) ⊥)

Tactic:
exact (add_bot _).symm

Premises used: WithBot.add_bot, Eq.symm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
a a_1 : α
coe :
  Eq.{v + 1} (α := WithBot β) (map (⇑f : (a : α) → β) (↑(a + a_1) : WithBot α) : WithBot β)
    ((↑((f : (a : α) → β) (a + a_1)) : WithBot β) : WithBot β)
⊢ map (⇑f : (a : α) → β) ((↑a : WithBot α) + (↑a_1 : WithBot α)) =
    HAdd.hAdd (α := WithBot β) (map (⇑f : (a : α) → β) (↑a : WithBot α)) (map (⇑f : (a : α) → β) (↑a_1 : WithBot α))

Tactic:
rw [map_coe, map_coe, ← coe_add, ← coe_add, ← map_add]

Premises used: map_add, WithBot.map_coe, WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
F : Type u_1
inst_1 : Add β
inst_2 : FunLike F α β
inst_3 : AddHomClass F α β
f : F
a a_1 : α
⊢ Eq.{v + 1} (α := WithBot β) (map (⇑f : (a : α) → β) (↑(a + a_1) : WithBot α) : WithBot β)
    ((↑((f : (a : α) → β) (a + a_1)) : WithBot β) : WithBot β)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoid α
⊢ Eq.{u + 1} (α := (a : α) → WithBot α) (⇑addHom : (a : α) → WithBot α) some

Tactic:
rfl

Premises used: WithBot.some, WithTop.some, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoid α
a : α
n : ℕ
⊢ (↑(n • a) : WithBot α) = n • (↑a : WithBot α)

Tactic:
(addHom : α →+ WithBot α).map_nsmul _ _

Premises used: WithBot.some, AddMonoidHom.map_nsmul, WithTop.some, WithBot.addHom
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Eq.{u + 1} (α := WithBot α) (↑(↑n : α) : WithBot α) (↑n : WithBot α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Ne.{u + 1} (α := WithBot α) (↑n : WithBot α) ⊥

Tactic:
coe_ne_bot

Premises used: WithBot.coe_ne_bot
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
⊢ Ne.{u + 1} (α := WithBot α) ⊥ (↑n : WithBot α)

Tactic:
bot_ne_coe

Premises used: WithBot.bot_ne_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Eq.{u + 1} (α := WithBot α) (↑(OfNat.ofNat n) : WithBot α) (OfNat.ofNat n)

Tactic:
rfl

Premises used: WithBot.some, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
inst_1 : n.AtLeastTwo
m : α
⊢ (↑m : WithBot α) = OfNat.ofNat n ↔ m = OfNat.ofNat n

Tactic:
coe_eq_coe

Premises used: WithBot.some, WithBot.coe_eq_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
inst_1 : n.AtLeastTwo
m : α
⊢ OfNat.ofNat n = (↑m : WithBot α) ↔ OfNat.ofNat n = m

Tactic:
coe_eq_coe

Premises used: WithBot.some, WithBot.coe_eq_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Ne.{u + 1} (α := WithBot α) (OfNat.ofNat n) ⊥

Tactic:
natCast_ne_bot n

Premises used: WithBot.natCast_ne_bot
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoidWithOne α
n : ℕ
inst_1 : n.AtLeastTwo
⊢ Ne.{u + 1} (α := WithBot α) ⊥ (OfNat.ofNat n)

Tactic:
bot_ne_natCast n

Premises used: WithBot.bot_ne_natCast
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoidWithOne α
f : α → β
n : ℕ
inst_1 : n.AtLeastTwo
⊢ map f (OfNat.ofNat n) = (↑(f (OfNat.ofNat n)) : WithBot β)

Tactic:
map_coe f n

Premises used: WithBot.some, Nat.cast, WithBot.map_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoidWithOne α
f : α → β
n : ℕ
⊢ map f (↑n : WithBot α) = (↑(f (↑n : α)) : WithBot β)

Tactic:
map_coe f n

Premises used: Nat.cast, WithBot.map_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoidWithOne α
f : β → α
n : ℕ
inst_1 : n.AtLeastTwo
a : WithBot β
⊢ map f a = OfNat.ofNat n ↔ ∃ (x : β), a = (↑x : WithBot β) ∧ f x = (↑n : α)

Tactic:
map_eq_some_iff

Premises used: WithBot.some, WithBot.map_eq_some_iff
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoidWithOne α
f : β → α
n : ℕ
inst_1 : n.AtLeastTwo
a : WithBot β
⊢ OfNat.ofNat n = map f a ↔ ∃ (x : β), a = (↑x : WithBot β) ∧ f x = (↑n : α)

Tactic:
some_eq_map_iff

Premises used: WithBot.some, WithBot.some_eq_map_iff
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoidWithOne α
f : β → α
n : ℕ
a : WithBot β
⊢ map f a = (↑n : WithBot α) ↔ ∃ (x : β), a = (↑x : WithBot β) ∧ f x = (↑n : α)

Tactic:
map_eq_some_iff

Premises used: WithBot.map_eq_some_iff
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoidWithOne α
f : β → α
n : ℕ
a : WithBot β
⊢ (↑n : WithBot α) = map f a ↔ ∃ (x : β), a = (↑x : WithBot β) ∧ f x = (↑n : α)

Tactic:
some_eq_map_iff

Premises used: WithBot.some_eq_map_iff
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : AddMonoidWithOne α
inst_1 : LT α
n : ℕ
⊢ LT.lt.{u} (α := WithBot α) ⊥ (↑n : WithBot α)

Tactic:
WithBot.bot_lt_coe _

Premises used: WithBot.bot_lt_coe
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : AddMonoidWithOne α
inst_1 : CharZero α
⊢ CharZero.{u} (WithBot α)

Tactic:
inferInstanceAs <| CharZero (WithTop α)

Premises used: _private.0.WithBot.charZero._proof_1
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
M : Type u_1
N : Type u_2
inst : One M
inst_1 : One N
f : OneHom M N
rw : Eq.{u_2 + 1} (α := WithBot N) ((↑((f : (a : M) → N) 1) : WithBot N) : WithBot N) (1 : WithBot N)
rw₁ : Eq.{u_2 + 1} (α := WithBot N) (↑1 : WithBot N) 1
rw₂ rw₃ : Eq.{u_2 + 1} (α := WithBot N) 1 1
⊢ Eq.{u_2 + 1} (α := WithBot N) (map.{u_1, u_2} (α := M) (⇑f : (a : M) → N) 1) 1

Tactic:
rw [WithBot.map_one, map_one, coe_one]

Premises used: WithBot.map_one, map_one, WithBot.coe_one
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
inst_1 : Add β
e : α ≃+ β
⊢ Eq (α := (a : WithBot α) → WithBot β) (⇑e.withBotCongr : (a : WithBot α) → WithBot β) (WithBot.map (⇑e : (a : α) → β))

Tactic:
rfl

Premises used: WithBot, WithBot.map, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
inst_1 : Add β
e : α ≃+ β
⊢ (↑e.withBotCongr : WithBot α ≃ WithBot β) = (↑e : α ≃ β).withBotCongr

Tactic:
rfl

Premises used: WithBot, Equiv.withBotCongr, WithBot.map, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
inst_1 : Add β
e : α ≃+ β
⊢ Eq (α := AddHom.{u, v} (WithBot α) (WithBot β)) (↑e.withBotCongr : WithBot α →ₙ+ WithBot β)
    (AddHom.withBotMap (↑e : α →ₙ+ β))

Tactic:
rfl

Premises used: WithBot, AddHom.withBotMap, AddHomClass.toAddHom, WithBot.map, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
inst : Add α
⊢ Eq (α := WithBot α ≃+ WithBot α) (withBotCongr (refl α)) (refl (WithBot α))

Tactic:
AddEquiv.ext <| congr_fun WithBot.map_id

Premises used: AddEquiv.ext, congr_fun, WithBot.map_id
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
inst : Add α
inst_1 : Add β
e : α ≃+ β
⊢ e.withBotCongr.symm = e.symm.withBotCongr

Tactic:
rfl

Premises used: WithBot, Equiv.withBotCongr, AddEquiv.withBotCongr, Equiv.symm, WithBot.map, rfl, AddEquiv.symm
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : Add α
inst_1 : Add β
inst_2 : Add γ
e₁ : α ≃+ β
e₂ : β ≃+ γ
h :
  ∀ (x : WithBot α),
    Eq.{u_1 + 1} (α := WithBot γ) (((e₁.trans e₂).withBotCongr : (a : WithBot α) → WithBot γ) x : WithBot γ)
      ((e₁.withBotCongr.trans e₂.withBotCongr : (a : WithBot α) → WithBot γ) x : WithBot γ)
⊢ (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr

Tactic:
ext x
-- Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : Add α
inst_1 : Add β
inst_2 : Add γ
e₁ : α ≃+ β
e₂ : β ≃+ γ
x : WithBot α
⊢ Eq.{u_1 + 1} (α := WithBot γ) (((e₁.trans e₂).withBotCongr : (a : WithBot α) → WithBot γ) x : WithBot γ)
    ((e₁.withBotCongr.trans e₂.withBotCongr : (a : WithBot α) → WithBot γ) x : WithBot γ)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Units
Goal:
α : Type u_1
inst : Monoid α
inst_1 : Preorder α
a b : αˣ
⊢ (↑a : α) ≤ (↑b : α) ↔ a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Monoid.Units
Goal:
α : Type u_1
inst : Monoid α
inst_1 : Preorder α
a b : αˣ
⊢ (↑a : α) < (↑b : α) ↔ a < b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Algebra.Order.Monoid.Units
Goal:
α : Type u_1
inst : Monoid α
inst_1 : LinearOrder α
a b : αˣ
simp_rw : (↑(a ⊔ b) : α) = (↑(if a ≤ b then b else a) : α)
⊢ (↑(a ⊔ b) : α) = max (↑a : α) (↑b : α)

Tactic:
simp_rw [max_def, val_le_val, ← apply_ite]

Premises used: apply_ite, Units.val_le_val, max_def
-- Module: Mathlib.Algebra.Order.Monoid.Units
Goal:
α : Type u_1
inst : Monoid α
inst_1 : LinearOrder α
a b : αˣ
⊢ (↑(a ⊔ b) : α) = (↑(if a ≤ b then b else a) : α)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Monoid.Units
Goal:
α : Type u_1
inst : Monoid α
inst_1 : LinearOrder α
a b : αˣ
simp_rw : (↑(a ⊓ b) : α) = (↑(if a ≤ b then a else b) : α)
⊢ (↑(a ⊓ b) : α) = min (↑a : α) (↑b : α)

Tactic:
simp_rw [min_def, val_le_val, ← apply_ite]

Premises used: apply_ite, Units.val_le_val, min_def
-- Module: Mathlib.Algebra.Order.Monoid.Units
Goal:
α : Type u_1
inst : Monoid α
inst_1 : LinearOrder α
a b : αˣ
⊢ (↑(a ⊓ b) : α) = (↑(if a ≤ b then a else b) : α)

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Monoid.Units
Goal:
α : Type u_1
inst : Monoid α
inst_1 : Ord α
a b : αˣ
⊢ compare (↑a : α) (↑b : α) = compare a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Monoid.WithTop
Goal:
α : Type u
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedAddMonoid α
⊢ IsOrderedAddMonoid.{u} (WithBot α)

Tactic:
{ add_le_add_left := fun _ _ h c => add_le_add_left h c }

Premises used: WithBot, add_le_add_left, IsOrderedAddMonoid._proof_1, IsOrderedAddMonoid.mk
-- Module: Mathlib.Algebra.Order.Monoid.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
x : WithBot α
hx : x ≠ ⊥
y : WithBot α
bot : ∀ (hx : Ne.{u + 1} (α := WithBot α) ⊥ ⊥), y ≤ y + ⊥
coe : ∀ (a : α) (hx : (↑a : WithBot α) ≠ ⊥), y ≤ y + (↑a : WithBot α)
⊢ y ≤ y + x

Tactic:
induction x
-- Module: Mathlib.Algebra.Order.Monoid.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
y : WithBot α
hx : Ne.{u + 1} (α := WithBot α) ⊥ ⊥
⊢ y ≤ y + ⊥

Tactic:
simp at hx
-- Module: Mathlib.Algebra.Order.Monoid.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
y : WithBot α
a : α
hx : (↑a : WithBot α) ≠ ⊥
coe : ⊥ ≤ ⊥ + (↑a : WithBot α)
coe₁ : ∀ (a_1 : α), (↑a_1 : WithBot α) ≤ (↑a_1 : WithBot α) + (↑a : WithBot α)
⊢ y ≤ y + (↑a : WithBot α)

Tactic:
induction y
-- Module: Mathlib.Algebra.Order.Monoid.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
a : α
hx : (↑a : WithBot α) ≠ ⊥
⊢ ⊥ ≤ ⊥ + (↑a : WithBot α)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
a : α
hx : (↑a : WithBot α) ≠ ⊥
a_1 : α
coe : a_1 ≤ a_1 + a
⊢ (↑a_1 : WithBot α) ≤ (↑a_1 : WithBot α) + (↑a : WithBot α)

Tactic:
rw [← WithBot.coe_add, WithBot.coe_le_coe]

Premises used: WithBot.coe_le_coe, WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
a : α
hx : (↑a : WithBot α) ≠ ⊥
a_1 : α
⊢ a_1 ≤ a_1 + a

Tactic:
le_self_add

Premises used: le_self_add
-- Module: Mathlib.Algebra.Order.Monoid.WithTop
Goal:
α : Type u
inst : Add α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
a : α
hx : (↑a : WithBot α) ≠ ⊥
a_1 : α
⊢ a_1 ≤ a_1 + a

Tactic:
exact le_self_add

Premises used: le_self_add
-- Module: Mathlib.Algebra.Order.Monoid.WithTop
Goal:
α : Type u
inst : AddCommMagma α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
x : WithBot α
hx : x ≠ ⊥
y : WithBot α
bot : ∀ (hx : Ne.{u + 1} (α := WithBot α) ⊥ ⊥), y ≤ ⊥ + y
coe : ∀ (a : α) (hx : (↑a : WithBot α) ≠ ⊥), y ≤ (↑a : WithBot α) + y
⊢ y ≤ x + y

Tactic:
induction x
-- Module: Mathlib.Algebra.Order.Monoid.WithTop
Goal:
α : Type u
inst : AddCommMagma α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
y : WithBot α
hx : Ne.{u + 1} (α := WithBot α) ⊥ ⊥
⊢ y ≤ ⊥ + y

Tactic:
simp at hx
-- Module: Mathlib.Algebra.Order.Monoid.WithTop
Goal:
α : Type u
inst : AddCommMagma α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
y : WithBot α
a : α
hx : (↑a : WithBot α) ≠ ⊥
coe : ⊥ ≤ (↑a : WithBot α) + ⊥
coe₁ : ∀ (a_1 : α), (↑a_1 : WithBot α) ≤ (↑a : WithBot α) + (↑a_1 : WithBot α)
⊢ y ≤ (↑a : WithBot α) + y

Tactic:
induction y
-- Module: Mathlib.Algebra.Order.Monoid.WithTop
Goal:
α : Type u
inst : AddCommMagma α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
a : α
hx : (↑a : WithBot α) ≠ ⊥
⊢ ⊥ ≤ (↑a : WithBot α) + ⊥

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.WithTop
Goal:
α : Type u
inst : AddCommMagma α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
a : α
hx : (↑a : WithBot α) ≠ ⊥
a_1 : α
coe : a_1 ≤ a + a_1
⊢ (↑a_1 : WithBot α) ≤ (↑a : WithBot α) + (↑a_1 : WithBot α)

Tactic:
rw [← WithBot.coe_add, WithBot.coe_le_coe]

Premises used: WithBot.coe_le_coe, WithBot.coe_add
-- Module: Mathlib.Algebra.Order.Monoid.WithTop
Goal:
α : Type u
inst : AddCommMagma α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
a : α
hx : (↑a : WithBot α) ≠ ⊥
a_1 : α
⊢ a_1 ≤ a + a_1

Tactic:
le_add_self

Premises used: le_add_self
-- Module: Mathlib.Algebra.Order.Monoid.WithTop
Goal:
α : Type u
inst : AddCommMagma α
inst_1 : LE α
inst_2 : CanonicallyOrderedAdd α
a : α
hx : (↑a : WithBot α) ≠ ⊥
a_1 : α
⊢ a_1 ≤ a + a_1

Tactic:
exact le_add_self

Premises used: le_add_self
-- Module: Mathlib.Algebra.Order.Monoid.WithTop
Goal:
α : Type u_1
inst : AddMonoid α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedAdd α
a : WithBot α
bot : LT.lt.{u_1} (α := WithBot α) ⊥ 0 ↔ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥
coe : ∀ (a : α), (↑a : WithBot α) < 0 ↔ (↑a : WithBot α) = ⊥
⊢ a < 0 ↔ a = ⊥

Tactic:
induction a
-- Module: Mathlib.Algebra.Order.Monoid.WithTop
Goal:
α : Type u_1
inst : AddMonoid α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedAdd α
⊢ LT.lt.{u_1} (α := WithBot α) ⊥ 0 ↔ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.WithTop
Goal:
α : Type u_1
inst : AddMonoid α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedAdd α
a : α
⊢ (↑a : WithBot α) < 0 ↔ (↑a : WithBot α) = ⊥

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : PartialOrder β
s : Set ι
f : ι → α
g : ι → β
⊢ MonovaryOn f⁻¹ g s ↔ AntivaryOn f g s

Tactic:
simp [MonovaryOn, AntivaryOn]

Premises used: MonovaryOn, AntivaryOn
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : PartialOrder β
s : Set ι
f : ι → α
g : ι → β
⊢ AntivaryOn f⁻¹ g s ↔ MonovaryOn f g s

Tactic:
simp [MonovaryOn, AntivaryOn]

Premises used: MonovaryOn, AntivaryOn
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : PartialOrder β
f : ι → α
g : ι → β
⊢ Monovary f⁻¹ g ↔ Antivary f g

Tactic:
simp [Monovary, Antivary]

Premises used: Monovary, Antivary
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : PartialOrder β
f : ι → α
g : ι → β
⊢ Antivary f⁻¹ g ↔ Monovary f g

Tactic:
simp [Monovary, Antivary]

Premises used: Monovary, Antivary
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : PartialOrder β
s : Set ι
f₁ f₂ : ι → α
g : ι → β
h₁ : MonovaryOn f₁ g s
h₂ : MonovaryOn f₂ g s
⊢ MonovaryOn (f₁ * f₂) g s

Tactic:
fun _i hi _j hj hij ↦ mul_le_mul' (h₁ hi hj hij) (h₂ hi hj hij)

Premises used: MonovaryOn, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : PartialOrder β
s : Set ι
f₁ f₂ : ι → α
g : ι → β
h₁ : AntivaryOn f₁ g s
h₂ : AntivaryOn f₂ g s
⊢ AntivaryOn (f₁ * f₂) g s

Tactic:
fun _i hi _j hj hij ↦ mul_le_mul' (h₁ hi hj hij) (h₂ hi hj hij)

Premises used: AntivaryOn, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : PartialOrder β
s : Set ι
f₁ f₂ : ι → α
g : ι → β
h₁ : MonovaryOn f₁ g s
h₂ : AntivaryOn f₂ g s
⊢ MonovaryOn (f₁ / f₂) g s

Tactic:
fun _i hi _j hj hij ↦ div_le_div'' (h₁ hi hj hij) (h₂ hi hj hij)

Premises used: div_le_div'', MonovaryOn
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : PartialOrder β
s : Set ι
f₁ f₂ : ι → α
g : ι → β
h₁ : AntivaryOn f₁ g s
h₂ : MonovaryOn f₂ g s
⊢ AntivaryOn (f₁ / f₂) g s

Tactic:
fun _i hi _j hj hij ↦ div_le_div'' (h₁ hi hj hij) (h₂ hi hj hij)

Premises used: div_le_div'', AntivaryOn
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : PartialOrder β
s : Set ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g s
n : ℕ
⊢ MonovaryOn (f ^ n) g s

Tactic:
fun _i hi _j hj hij ↦ pow_le_pow_left' (hfg hi hj hij) _

Premises used: MonovaryOn, pow_le_pow_left'
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : PartialOrder β
s : Set ι
f : ι → α
g : ι → β
hfg : AntivaryOn f g s
n : ℕ
⊢ AntivaryOn (f ^ n) g s

Tactic:
fun _i hi _j hj hij ↦ pow_le_pow_left' (hfg hi hj hij) _

Premises used: AntivaryOn, pow_le_pow_left'
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : PartialOrder β
f₁ f₂ : ι → α
g : ι → β
h₁ : Monovary f₁ g
h₂ : Monovary f₂ g
⊢ Monovary (f₁ * f₂) g

Tactic:
fun _i _j hij ↦ mul_le_mul' (h₁ hij) (h₂ hij)

Premises used: Monovary, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : PartialOrder β
f₁ f₂ : ι → α
g : ι → β
h₁ : Antivary f₁ g
h₂ : Antivary f₂ g
⊢ Antivary (f₁ * f₂) g

Tactic:
fun _i _j hij ↦ mul_le_mul' (h₁ hij) (h₂ hij)

Premises used: Antivary, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : PartialOrder β
f₁ f₂ : ι → α
g : ι → β
h₁ : Monovary f₁ g
h₂ : Antivary f₂ g
⊢ Monovary (f₁ / f₂) g

Tactic:
fun _i _j hij ↦ div_le_div'' (h₁ hij) (h₂ hij)

Premises used: Monovary, div_le_div''
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : PartialOrder β
f₁ f₂ : ι → α
g : ι → β
h₁ : Antivary f₁ g
h₂ : Monovary f₂ g
⊢ Antivary (f₁ / f₂) g

Tactic:
fun _i _j hij ↦ div_le_div'' (h₁ hij) (h₂ hij)

Premises used: Antivary, div_le_div''
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : PartialOrder β
f : ι → α
g : ι → β
hfg : Monovary f g
n : ℕ
⊢ Monovary (f ^ n) g

Tactic:
fun _i _j hij ↦ pow_le_pow_left' (hfg hij) _

Premises used: Monovary, pow_le_pow_left'
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : PartialOrder β
f : ι → α
g : ι → β
hfg : Antivary f g
n : ℕ
⊢ Antivary (f ^ n) g

Tactic:
fun _i _j hij ↦ pow_le_pow_left' (hfg hij) _

Premises used: Antivary, pow_le_pow_left'
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : CommGroup β
inst_2 : PartialOrder β
inst_3 : IsOrderedMonoid β
s : Set ι
f : ι → α
g : ι → β
⊢ MonovaryOn f g⁻¹ s ↔ AntivaryOn f g s

Tactic:
simpa [MonovaryOn, AntivaryOn] using forall₂_comm

Premises used: MonovaryOn, AntivaryOn, forall₂_comm
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : CommGroup β
inst_2 : PartialOrder β
inst_3 : IsOrderedMonoid β
s : Set ι
f : ι → α
g : ι → β
⊢ AntivaryOn f g⁻¹ s ↔ MonovaryOn f g s

Tactic:
simpa [MonovaryOn, AntivaryOn] using forall₂_comm

Premises used: MonovaryOn, AntivaryOn, forall₂_comm
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : CommGroup β
inst_2 : PartialOrder β
inst_3 : IsOrderedMonoid β
f : ι → α
g : ι → β
⊢ Monovary f g⁻¹ ↔ Antivary f g

Tactic:
simpa [Monovary, Antivary] using forall_comm

Premises used: Monovary, Antivary, forall_comm
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : CommGroup β
inst_2 : PartialOrder β
inst_3 : IsOrderedMonoid β
f : ι → α
g : ι → β
⊢ Antivary f g⁻¹ ↔ Monovary f g

Tactic:
simpa [Monovary, Antivary] using forall_comm

Premises used: Monovary, Antivary, forall_comm
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : CommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedMonoid β
s : Set ι
f : ι → α
g : ι → β
⊢ MonovaryOn f⁻¹ g⁻¹ s ↔ MonovaryOn f g s

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : CommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedMonoid β
s : Set ι
f : ι → α
g : ι → β
⊢ AntivaryOn f⁻¹ g⁻¹ s ↔ AntivaryOn f g s

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : CommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedMonoid β
f : ι → α
g : ι → β
⊢ Monovary f⁻¹ g⁻¹ ↔ Monovary f g

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : CommGroup α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : CommGroup β
inst_4 : PartialOrder β
inst_5 : IsOrderedMonoid β
f : ι → α
g : ι → β
⊢ Antivary f⁻¹ g⁻¹ ↔ Antivary f g

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monovary
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : CommGroup β
inst_2 : LinearOrder β
inst_3 : IsOrderedMonoid β
s : Set ι
f : ι → α
g₁ g₂ : ι → β
h₁ : MonovaryOn f g₁ s
h₂ : MonovaryOn f g₂ s
⊢ MonovaryOn f (g₁ * g₂) s

Tactic:
fun _i hi _j hj hij ↦ (lt_or_lt_of_mul_lt_mul hij).elim (h₁ hi hj) <| h₂ hi hj

Premises used: lt_or_lt_of_mul_lt_mul, MonovaryOn, Or.elim