mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulZeroOneClass β
f : α →* β
hf : Surjective ⇑f
⊢ Surjective ⇑(lift' f)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a : R
n : ℕ
n0 : 0 < n
⊢ IsRightRegular (a ^ n) → IsRightRegular a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: β : Type u_2
inst✝ : MulOneClass β
⊢ ↑(map' (MonoidHom.id β)) = MonoidHom.id (WithZero β)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsLeftRegular a
h : a * b = a
⊢ b = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsLeftRegular a
h : b = 1
⊢ a * b = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
f : α →* β
g : β →* γ
x : WithZero α
⊢ (map' g) ((map' f) x) = (map' (g.comp f)) x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsRightRegular a
h : b * a = a
⊢ b = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsRightRegular a
h : b = 1
⊢ b * a = a

Tactic:
rw [h, one_mul]

Goal state after:
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
a b : R
ha : IsRightRegular a
h : b = 1
⊢ b * a = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
⊢ Injective ⇑(map' f) ↔ Injective ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
h : ∀ (x y : R), x * y = 1 → IsLeftRegular x
a✝ b✝ : R
eq : a✝ * b✝ = 1
⊢ (fun x ↦ a✝ * x) (b✝ * a✝) = (fun x ↦ a✝ * x) 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : ∀ (b : β), ∃ a, f a = b
⊢ (map' f) 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Regular.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Monoid R
h : ∀ (x y : R), x * y = 1 → IsRightRegular y
a✝ b✝ : R
eq : a✝ * b✝ = 1
⊢ (fun x ↦ x * b✝) (b✝ * a✝) = (fun x ↦ x * b✝) 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommMonoidWithTop α
a : α
ha : a ≠ ⊤
⊢ IsAddRegular a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ -a + a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
b : α
⊢ a + (-a + b) = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
b : α
⊢ -a + (a + b) = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
hb : b ≠ ⊤
a : α
⊢ a + b + -b = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
hb : b ≠ ⊤
a : α
⊢ a + -b + b = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
⊢ ⊤ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ IsAddUnit a → a ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
⊢ Surjective ⇑(map' f) ↔ Surjective ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
ha : a ≠ ⊤
⊢ a + -a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Monoid α
n : ℕ
⊢ 0 ^ (n + 1) = 0 ^ n * 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DivInvMonoid α
n : ℕ
⊢ none ^ ↑n.succ = none ^ ↑n * none

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : InvolutiveInv α
a : WithZero α
⊢ Option.map ((fun x ↦ x⁻¹) ∘ fun x ↦ x⁻¹) a = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
h : -a = ⊤
⊢ a = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Group α
a : WithZero α
ha : a ≠ 0
⊢ a * a⁻¹ = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
h : a = ⊤
⊢ -a = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Group α
x✝ : (WithZero α)ˣ
⊢ ↑((fun a ↦ Units.mk0 ↑a ⋯) ((fun a ↦ unzero ⋯) x✝)) = ↑x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a - ⊤ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Group α
x✝¹ x✝ : (WithZero α)ˣ
⊢ ↑(unzero ⋯) = ↑(unzero ⋯ * unzero ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
inst✝ : Group α
γ : (WithZero α)ˣ
⊢ ↑(unitsWithZeroEquiv γ) = ↑γ

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x✝ : WithZero Gˣ
⊢ (fun a ↦ if h : a = 0 then 0 else ↑(Units.mk0 a h)) ((fun n ↦ recZeroCoe 0 Units.val n) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x✝ : G
⊢ (fun n ↦ recZeroCoe 0 Units.val n) ((fun a ↦ if h : a = 0 then 0 else ↑(Units.mk0 a h)) x✝) = x✝

Tactic:
simp only

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x✝ : G
⊢ recZeroCoe 0 Units.val (if h : x✝ = 0 then 0 else ↑(Units.mk0 x✝ h)) = x✝
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b c a : α
⊢ - -a = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x✝ : G
⊢ (fun n ↦ recZeroCoe 0 Units.val n) ((fun a ↦ if h : a = 0 then 0 else ↑(Units.mk0 a h)) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ -(a + b) + (a + b) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a + b + (-b + -a) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Group α
G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
x1✝ x2✝ : WithZero Gˣ
⊢ recZeroCoe 0 Units.val (x1✝ * x2✝) = recZeroCoe 0 Units.val x1✝ * recZeroCoe 0 Units.val x2✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: G : Type u_4
inst✝¹ : GroupWithZero G
inst✝ : DecidablePred fun a ↦ a = 0
a : Gˣ
⊢ withZeroUnitsEquiv.symm ↑a = ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
⊢ -(a + b) = -b + -a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
x✝ : WithZero α
⊢ (map' ↑e.symm) ((map' ↑e) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
h : a + b = 0
⊢ a ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
x✝ : WithZero β
⊢ (map' ↑e) ((map' ↑e.symm) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
h : a + b = 0
ha : a ≠ ⊤
⊢ -a + a = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
h : a + b = 0
⊢ -a = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ -b ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ Function.Injective fun x ↦ x - b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ Function.Injective fun x ↦ b - x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : α ≃* β
x1✝ x2✝ : WithZero α
⊢ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun (x1✝ * x2✝) =
    { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun x1✝ *
      { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯ }.toFun x2✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
b : α
h : b ≠ ⊤
⊢ StrictMono fun x ↦ x - b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
x : α
⊢ e ↑x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
x : β
⊢ e.symm ↑x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a + -a = 0 → a ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
⊢ LeftInverse (fun x ↦ unzero ⋯) fun x ↦ unzero ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
⊢ RightInverse (fun x ↦ unzero ⋯) fun x ↦ unzero ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ a - a = 0 ↔ a ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
e : WithZero α ≃* WithZero β
⊢ ∀ (x y : α),
    { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun (x * y) =
      { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun x *
        { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯ }.toFun y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
x✝ : α ≃* β
⊢ (fun e ↦ { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
      ((fun e ↦ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }) x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
⊢ 0 < a - b ↔ b < a ∨ b = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ 0 < -a ↔ a < 0 ∨ a = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
x✝ : WithZero α ≃* WithZero β
⊢ (fun e ↦ { toFun := ⇑(map' ↑e), invFun := ⇑(map' ↑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
      ((fun e ↦ { toFun := fun x ↦ unzero ⋯, invFun := fun x ↦ unzero ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ })
        x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ (if n + 1 = 0 then 0 else ↑↑(n + 1)) = (if n = 0 then 0 else ↑↑n) + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: M : Type u_4
a : M
⊢ exp a ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
x : WithZero (Multiplicative M)
hx : x ≠ 0
⊢ exp x.log = x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
x : M
⊢ exp x = 1 ↔ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
x y : WithZero (Multiplicative M)
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).log = x.log + y.log

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
⊢ (0 ^ 0).log = 0 • log 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
⊢ 0 ≤ a - a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
n : ℕ
⊢ (0 ^ (n + 1)).log = (n + 1) • log 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a b : α
ha : a ≠ ⊤
⊢ b - a = 0 ↔ b = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
x : WithZero (Multiplicative M)
hx : x ≠ 0
⊢ Multiplicative.toAdd (unzero hx) = x.log

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
x : WithTop G
⊢ ⊤ - x = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: G : Type u_5
inst✝ : AddGroup G
x y : WithZero (Multiplicative G)
hx : x ≠ 0
hy : y ≠ 0
⊢ (x / y).log = x.log - y.log

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: G : Type u_5
inst✝ : AddGroup G
⊢ 0⁻¹.log = -log 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
x : WithTop G
⊢ x - ⊤ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: G : Type u_5
inst✝ : AddGroup G
x : WithZero (Multiplicative G)
n : ℤ
⊢ (x ^ n).log = n • x.log

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀
⊢ x = 0 → f x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
x y : WithTop G
⊢ x - y = ⊤ ↔ x = ⊤ ∨ y = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: G₀ : Type u_1
M₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : MulZeroOneClass M₀
inst✝ : Nontrivial M₀
f : G₀ →*₀ M₀
x : G₀
⊢ f x = 0 ↔ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.WithZero

Goal state before:
pp: M₀ : Type u_1
N₀ : Type u_2
G₀ : Type u_3
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : Nontrivial M₀
inst✝³ : NoZeroDivisors M₀
inst✝² : MulZeroOneClass N₀
inst✝¹ : MulZeroOneClass G₀
inst✝ : DecidablePred fun x ↦ x = 0
f : N₀ →*₀ G₀
x : M₀
⊢ f (1 x) = 1 x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : AddCommGroup G
x y : WithTop G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedAddMonoid G
a b : WithTop G
⊢ a - b = a + -b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Units

Goal state before:
pp: α : Type u_1
inst✝¹ : Monoid α
inst✝ : LinearOrder α
a b : αˣ
⊢ ↑(a ⊔ b) = max ↑a ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Units

Goal state before:
pp: α : Type u_1
inst✝¹ : Monoid α
inst✝ : LinearOrder α
a b : αˣ
⊢ ↑(a ⊓ b) = min ↑a ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : One α
a : α
inst✝¹ : LE α
inst✝ : IsBotOneClass α
x : WithTop α
⊢ 1 ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
x : WithTop α
⊢ x + ⊤ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
x y : WithTop α
⊢ x + y = ⊤ ↔ x = ⊤ ∨ y = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
x y : WithTop α
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝¹ : Add α
x y : WithTop α
inst✝ : LT α
⊢ x + y < ⊤ ↔ x < ⊤ ∧ y < ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
b : WithTop α
c : α
⊢ ⊤ + b = ↑c ↔ ∃ a' b', ↑a' = ⊤ ∧ ↑b' = b ∧ a' + b' = c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Nat

Goal state before:
pp: ⊢ IsCompl {n | Even n} {n | Odd n}

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
a c : α
⊢ ↑a + ⊤ = ↑c ↔ ∃ a' b', ↑a' = ↑a ∧ ↑b' = ⊤ ∧ a' + b' = c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
a b c : α
⊢ ↑a + ↑b = ↑c ↔ ∃ a' b', ↑a' = ↑a ∧ ↑b' = ↑b ∧ a' + b' = c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
x : WithTop α
b : α
⊢ x + ↑b = ⊤ ↔ x = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
y : WithTop α
a : α
⊢ ↑a + y = ⊤ ↔ y = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
a : α
ha : IsAddLeftRegular a
⊢ IsAddLeftRegular ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝ : Add α
a : α
ha : IsAddRightRegular a
⊢ IsAddRightRegular ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝¹ : Add α
a : α
inst✝ : LE α
ha : AddLECancellable a
⊢ AddLECancellable ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝¹ : Add α
x y z : WithTop α
inst✝ : IsRightCancelAdd α
hz : z ≠ ⊤
⊢ x + z = y + z ↔ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
inst✝¹ : Add α
x y z : WithTop α
inst✝ : IsLeftCancelAdd α
hx : x ≠ ⊤
⊢ x + y = x + z ↔ y = z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
a✝² a✝¹ a✝ : α
x✝ : a✝¹ ≤ a✝
⊢ a✝² + a✝¹ ≤ a✝² + a✝

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
x y z : WithTop α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) x y) ((fun x1 x2 ↦ x1 + x2) x z)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x y z : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
a✝² a✝¹ a✝ : α
x✝ : a✝¹ ≤ a✝
⊢ a✝¹ + a✝² ≤ a✝ + a✝²

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddRightMono α
x y z : WithTop α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) (swap (fun x1 x2 ↦ x1 + x2) x y) (swap (fun x1 x2 ↦ x1 + x2) x z)

Tactic:
by

Goal state after: