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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a

Tactic:
rw [inv_le_iff_one_le_mul₀' ha, le_mul_inv_iff₀ hb, one_mul]

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α ↪ β
map_rel_iff'✝¹ : ∀ {a b : α}, s (f a) (f b) ↔ r a b
g : α ↪ β
map_rel_iff'✝ : ∀ {a b : α}, s (g a) (g b) ↔ r a b
⊢ { toEmbedding := f, map_rel_iff' := map_rel_iff'✝¹ }.toEmbedding =
      { toEmbedding := g, map_rel_iff' := map_rel_iff'✝ }.toEmbedding →
    { toEmbedding := f, map_rel_iff' := map_rel_iff'✝¹ } = { toEmbedding := g, map_rel_iff' := map_rel_iff'✝ }

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hb : 0 < b
hc : 0 < c
⊢ a < c * b ↔ a / c < b

Tactic:
div_lt_iff₀' hc

Goal state after:
G₀ : Type u_3
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hb : 0 < b
hc : 0 < c
⊢ a < c * b ↔ a < c * b
Module: Mathlib.Order.Lex

Goal state before:
pp: α : Type u_1
a b : α
⊢ toLex a = toLex b ↔ a = b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Lex

Goal state before:
pp: α : Type u_1
a b : Lex α
⊢ ofLex a = ofLex b ↔ a = b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Lex

Goal state before:
pp: α : Type u_1
a b : α
⊢ toColex a = toColex b ↔ a = b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Lex

Goal state before:
pp: α : Type u_1
a b : Colex α
⊢ ofColex a = ofColex b ↔ a = b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ ∀ (x : β), (e.symm.trans e) x = (RelIso.refl s) x

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
⊢ ∀ (x : α), (e.trans e.symm) x = (RelIso.refl r) x

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ →r s₁
x✝ : α₁
⊢ ((fun f₂ ↦ e₂.symm.toRelEmbedding.toRelHom.comp (f₂.comp e₁.toRelEmbedding.toRelHom))
        ((fun f₁ ↦ e₂.toRelEmbedding.toRelHom.comp (f₁.comp e₁.symm.toRelEmbedding.toRelHom)) f₁))
      x✝ =
    f₁ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ →r s₂
x✝ : α₂
⊢ ((fun f₁ ↦ e₂.toRelEmbedding.toRelHom.comp (f₁.comp e₁.symm.toRelEmbedding.toRelHom))
        ((fun f₂ ↦ e₂.symm.toRelEmbedding.toRelHom.comp (f₂.comp e₁.toRelEmbedding.toRelHom)) f₂))
      x✝ =
    f₂ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ ↪r s₁
x✝ : α₁
⊢ ((fun f₂ ↦ (e₁.toRelEmbedding.trans f₂).trans e₂.symm.toRelEmbedding)
        ((fun f₁ ↦ (e₁.symm.toRelEmbedding.trans f₁).trans e₂.toRelEmbedding) f₁))
      x✝ =
    f₁ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ ↪r s₂
x✝ : α₂
⊢ ((fun f₁ ↦ (e₁.symm.toRelEmbedding.trans f₁).trans e₂.toRelEmbedding)
        ((fun f₂ ↦ (e₁.toRelEmbedding.trans f₂).trans e₂.symm.toRelEmbedding) f₂))
      x✝ =
    f₂ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ ≃r s₁
x✝ : α₁
⊢ ((fun f₂ ↦ (e₁.trans f₂).trans e₂.symm) ((fun f₁ ↦ (e₁.symm.trans f₁).trans e₂) f₁)) x✝ = f₁ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ ≃r s₂
x✝ : α₂
⊢ ((fun f₁ ↦ (e₁.symm.trans f₁).trans e₂) ((fun f₂ ↦ (e₁.trans f₂).trans e₂.symm) f₂)) x✝ = f₂ x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝ : IsEmpty β
⊢ ∀ {a b : α ⊕ β}, r ((Equiv.sumEmpty α β) a) ((Equiv.sumEmpty α β) b) ↔ Sum.Lex r s a b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
r : α → α → Prop
s : β → β → Prop
inst✝ : IsEmpty α
⊢ ∀ {a b : α ⊕ β}, s ((Equiv.emptySum α β) a) ((Equiv.emptySum α β) b) ↔ Sum.Lex r s a b

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a b : β
⊢ EquivLike.inv f b ≤ EquivLike.inv f a ↔ b ≤ a

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a b : β
⊢ EquivLike.inv f b < EquivLike.inv f a ↔ b < a

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : α ≃o β
x✝ : α
⊢ (ofRelIsoLT e.toRelIsoLT) x✝ = e x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
e : (fun x1 x2 ↦ x1 < x2) ≃r fun x1 x2 ↦ x1 < x2
x✝ : α
⊢ (ofRelIsoLT e).toRelIsoLT x✝ = e x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁵ : Preorder α✝
inst✝⁴ : Preorder β✝
α : Type u_6
β : Type u_7
inst✝³ : Unique α
inst✝² : Unique β
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ ∀ {a b : α}, (Equiv.ofUnique α β) a ≤ (Equiv.ofUnique α β) b ↔ a ≤ b

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Defs

Goal state before:
pp: R : Type u_1
inst✝³ : CommGroup R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedMonoid R
inst✝ : MulArchimedean R
a : R
ha : a < 1
b : R
⊢ ∀ (a_1 : ℕ), b⁻¹ < a⁻¹ ^ a_1 → a ^ a_1 < b

Tactic:
simp

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

Goal state before:
pp: M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : MulLeftMono M
a : M
ha : 1 ≤ a
⊢ 1 ≤ a ^ 0

Tactic:
simp

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

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
x✝ : 1 ≠ 0
⊢ a ^ 1 ≤ b ^ (1 - 1) * a

Tactic:
simp

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

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
a b : M
hab : a ^ 2 ≤ b * a
n : ℕ
x✝ : n + 2 ≠ 0
⊢ b ^ (n + 1 - 1) * a * a ≤ b ^ n * a * a

Tactic:
simp

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

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
a b : M
hab : a ≤ b
⊢ a ^ 0 ≤ b ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1

Tactic:
cases le_or_gt 1 a

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
h✝ : 1 ≤ a
⊢ |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1

case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
h✝ : a < 1
⊢ |a|ₘ = a ∧ 1 ≤ a ∨ |a|ₘ = a⁻¹ ∧ a < 1
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
⊢ 1 < |1|ₘ ↔ 1 ≠ 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: case e'_3
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 1 = ↑1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: case e'_4
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ ↑n + 1 = ↑(n + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Cast.Order.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 1 ≤ n + 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: r : ℕ
s t : ℤ
r' : ℕ
s' t' : ℤ
h : 0 < r
⊢ r.xgcdAux s t r' s' t' = (r' % r).xgcdAux (s' - ↑r' / ↑r * s) (t' - ↑r' / ↑r * t) r s t

Tactic:
obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h.ne'
  rw [xgcdAux, Nat.strongRec_eq]
  rfl

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: x y : ℕ
⊢ ∀ (n : ℕ) (s t s' t' : ℤ), (xgcdAux 0 s t n s' t').1 = gcd 0 n

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case H0
x y n✝ : ℕ
⊢ ∀ {s t s' t' : ℤ}, x.P y (0, s, t) → x.P y (n✝, s', t') → x.P y (xgcdAux 0 s t n✝ s' t')

Tactic:
simp

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

Goal state before:
pp: case zero
m k : ℕ
⊢ m - 0 ≤ k ↔ m ≤ k + 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case ofNat.ofNat
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.ofNat m).gcd (Int.ofNat n) = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ Int.ofNat n = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case ofNat.negSucc
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.ofNat m).gcd (Int.negSucc n) = 1 ↔ a ^ Int.ofNat m = 1 ∧ a ^ Int.negSucc n = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case negSucc.ofNat
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.negSucc m).gcd (Int.ofNat n) = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ Int.ofNat n = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case negSucc.negSucc
M : Type u_1
inst✝ : Group M
a : M
m n : ℕ
⊢ a ^ (Int.negSucc m).gcd (Int.negSucc n) = 1 ↔ a ^ Int.negSucc m = 1 ∧ a ^ Int.negSucc n = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Defs

Goal state before:
pp: α : Type u
inst✝ : Semigroup α
b c : WithOne α
⊢ 1 * b * c = 1 * (b * c)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Defs

Goal state before:
pp: α : Type u
inst✝ : Semigroup α
a : α
c : WithOne α
⊢ ↑a * 1 * c = ↑a * (1 * c)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Defs

Goal state before:
pp: α : Type u
inst✝ : Semigroup α
a b : α
⊢ ↑a * ↑b * 1 = ↑a * (↑b * 1)

Tactic:
simp

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : EquivLike F α β
inst✝² : MulZeroClass α
inst✝¹ : MulZeroClass β
inst✝ : MulEquivClass F α β
f : F
⊢ f 0 * f (EquivLike.inv f 0) = 0

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
la : IsLeftRegular 0
x y : R
xy : x ≠ y
⊢ (fun x ↦ 0 * x) x = (fun x ↦ 0 * x) y

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : MulZeroClass R
inst✝ : Nontrivial R
ra : IsRightRegular 0
x y : R
xy : x ≠ y
⊢ (fun x ↦ x * 0) x = (fun x ↦ x * 0) y

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
| b * a = 0

Tactic:
rw [← mul_zero b]

Goal state after:
R : Type u_1
inst✝ : MulZeroClass R
a b : R
hb : IsLeftRegular b
| b * a = b * 0
Module: Mathlib.Algebra.Order.Monoid.WithTop

Goal state before:
pp: case coe.bot
α : Type u
inst✝² : Add α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝ : α
hx : ↑a✝ ≠ ⊥
⊢ ⊥ ≤ ⊥ + ↑a✝

Tactic:
simp

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

Goal state before:
pp: case coe.bot
α : Type u
inst✝² : AddCommMagma α
inst✝¹ : LE α
inst✝ : CanonicallyOrderedAdd α
a✝ : α
hx : ↑a✝ ≠ ⊥
⊢ ⊥ ≤ ↑a✝ + ⊥

Tactic:
simp

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

Goal state before:
pp: case bot
α : Type u_1
inst✝² : AddMonoid α
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedAdd α
⊢ ⊥ < 0 ↔ ⊥ = ⊥

Tactic:
simp

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

Goal state before:
pp: case coe
α : Type u_1
inst✝² : AddMonoid α
inst✝¹ : Preorder α
inst✝ : CanonicallyOrderedAdd α
a✝ : α
⊢ ↑a✝ < 0 ↔ ↑a✝ = ⊥

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : MulOneClass α
inst✝ : MulZeroOneClass β
f : α →* β
⊢ recZeroCoe 0 (⇑f) 1 = 1

Tactic:
simp

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

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

Tactic:
simp

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:
simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : InvOneClass α
⊢ ↑1⁻¹ = 1

Tactic:
simp

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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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:
simp

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✝ : α
⊢ (fun x ↦ unzero ⋯) ((fun x ↦ unzero ⋯) x✝) = x✝

Tactic:
simp

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✝ : β
⊢ (fun x ↦ unzero ⋯) ((fun x ↦ unzero ⋯) x✝) = x✝

Tactic:
simp

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

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

Tactic:
simp

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✝¹ : α ≃* β
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✝ =
    x✝¹ x✝

Tactic:
simp

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

Goal state before:
pp: case zero
α : 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✝))
      0 =
    x✝ 0

Tactic:
simp

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

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Group α
inst✝ : Group β
x✝ : WithZero α ≃* WithZero β
a✝ : α
⊢ ((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✝))
      ↑a✝ =
    x✝ ↑a✝

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case inl
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
⊢ 0 ≤ ⊤ - ⊤

Tactic:
simp

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:
simp

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:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case inl
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₀
⊢ f (1 0) = 1 0

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
h : a ≤ b
⊢ b - a + a = b

Tactic:
by
  rw [add_comm]
  exact add_tsub_cancel_of_le h

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

Goal state before:
pp: case top
α : Type u
inst✝³ : Add α
x y z : WithTop α
inst✝² : Preorder α
inst✝¹ : AddLeftStrictMono α
inst✝ : AddRightStrictMono α
xz : x < z
yw : y < ⊤
⊢ x + ⊤ ≤ z + ⊤

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝³ : Add α
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : AddLeftReflectLE α
h : AddLECancellable ⊤
⊢ ⊤ + ⊤ ≤ ⊤ + ↑(Classical.arbitrary α)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Basic

Goal state before:
pp: α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ b - a + a = max a b

Tactic:
max_comm,

Goal state after:
α : Type u_1
inst✝⁴ : AddCommMonoid α
inst✝³ : LinearOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ b - a + a = max b a
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : LE α
inst✝¹ : Add α
inst✝ : ExistsAddOfLE α
a b : WithTop α
⊢ ⊤ ≤ ⊤ → ∃ c, ⊤ = ⊤ + c

Tactic:
simp

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

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

Tactic:
simp

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:
simp

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

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

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
n : ℕ
x✝ : 0 ≤ ↑n
⊢ 0 ≤ ↑↑n

Tactic:
simp

Goal state after: