mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Action.Opposite

Goal state before:
pp: M✝ : Type u_1
N✝ : Type u_2
α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
inst✝² : Mul N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
y : Nᵐᵒᵖ
z : N
⊢ x • y • z = y • x • z

Tactic:
induction y using MulOpposite.rec'

Goal state after:
case h
M✝ : Type u_1
N✝ : Type u_2
α : Type u_3
β : Type u_4
M : Type u_5
N : Type u_6
inst✝² : Mul N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
z X✝ : N
⊢ x • op X✝ • z = op X✝ • x • z
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_7
σ : Perm α
m n : ℤ
x : α
⊢ (σ ^ m) ((σ ^ n) x) = (σ ^ n) ((σ ^ m) x)

Tactic:
by
  rw [← Equiv.Perm.mul_apply, ← Equiv.Perm.mul_apply, zpow_mul_comm]

Goal state after:
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
p : α → Prop
f : Perm α
hf : ∀ (x : α), p (f x) ↔ p x
n : ℕ
⊢ ∀ (x : α), p ((f ^ Int.negSucc n) x) ↔ p x

Tactic:
by
    rw [zpow_negSucc]
    exact pow_aux (inv_aux.1 hf)

Goal state after:
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ σ * (swap i j * swap i j) = σ

Tactic:
swap_mul_self,

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
i j : α
σ : Perm α
⊢ σ * 1 = σ
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
e : MulAut M
m : M
⊢ e⁻¹ m = (MulEquiv.symm e) m

Tactic:
by
  rw [inv_def]

Goal state after:
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
x✝ : 0 < n + 1
⊢ ↑(n + 1 - 1) = ↑(n + 1) - 1

Tactic:
rw [cast_succ, add_sub_cancel_right, Nat.add_sub_cancel_right]

Goal state after:
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
a : α
⊢ IsSquare a⁻¹ → IsSquare a

Tactic:
intro h

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
a : α
h : IsSquare a⁻¹
⊢ IsSquare a
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : DivisionMonoid α
a : α
⊢ IsSquare a → IsSquare a⁻¹

Tactic:
intro h

Goal state after:
case mpr
α : Type u_2
inst✝ : DivisionMonoid α
a : α
h : IsSquare a
⊢ IsSquare a⁻¹
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: m n : ℕ
⊢ ¬Even 25394535

Tactic:
by decide

Goal state after:
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: m n : ℤ
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
by
  rcases emod_two_eq_zero_or_one m with h₁ | h₁ <;>
  rcases emod_two_eq_zero_or_one n with h₂ | h₂ <;>
  simp [even_iff, h₁, h₂, Int.mul_emod]

Goal state after:
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: m n : ℤ
⊢ ¬Even 25394535

Tactic:
by decide

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: case head.tail
a b : Prop
l : List Prop
h : b ∈ l
ab : a ↔ b
H : l.TFAE
q : Prop
hq : Mem q l
⊢ a ↔ q

Tactic:
exact ab.trans (H _ h _ hq)

Goal state after:
Module: Mathlib.Algebra.Field.Defs

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
⊢ q • 1 = ↑q

Tactic:
by rw [NNRat.smul_def, mul_one]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
⊢ (Covariant M N μ fun x1 x2 ↦ x1 < x2) → Covariant M N μ fun x1 x2 ↦ x1 ≤ x2

Tactic:
intro h

Goal state after:
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 ↦ x1 < x2
⊢ Covariant M N μ fun x1 x2 ↦ x1 ≤ x2
Module: Mathlib.Algebra.Order.ZeroLEOne

Goal state before:
pp: α : Type u_1
⊢ 0 ≤ 1

Tactic:
by decide

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

Goal state before:
pp: N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Covariant N N (flip mu) r ↔ Covariant N N mu r

Tactic:
by unfold flip; simp_rw [h.comm]

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

Goal state before:
pp: N : Type u_2
r : N → N → Prop
mu : N → N → N
h : Std.Commutative mu
⊢ Contravariant N N (flip mu) r ↔ Contravariant N N mu r

Tactic:
by unfold flip; simp_rw [h.comm]

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: n : ℕ
⊢ ∃ k, Xor (n = 2 * k) (n = 2 * k + 1)

Tactic:
obtain ⟨k, rfl⟩ | ⟨k, rfl⟩ := even_or_odd n

Goal state after:
case inl
k : ℕ
⊢ ∃ k_1, Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)

case inr
k : ℕ
⊢ ∃ k_1, Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
m n : ℕ
⊢ ¬Even 25394535

Tactic:
by decide

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : PosMulStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ 0 < f a

Tactic:
rwa [← zero, lt]

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

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : MulPosStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ 0 < f a

Tactic:
rwa [← zero, lt]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ a₂ * b₂ ≤ a₁ * b₁ ↔ a₁ = a₂ ∧ b₁ = b₂

Tactic:
have := mulLeftMono_of_mulLeftStrictMono α

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a₁ a₂ b₁ b₂ : α
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
this : MulLeftMono α
⊢ a₂ * b₂ ≤ a₁ * b₁ ↔ a₁ = a₂ ∧ b₁ = b₂
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
⊢ a * b = c * d ↔ a = c ∧ b = d

Tactic:
have := mulLeftMono_of_mulLeftStrictMono α

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this : MulLeftMono α
⊢ a * b = c * d ↔ a = c ∧ b = d
Module: Mathlib.Algebra.Ring.GrindInstances

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n : ℕ
⊢ OfNat.ofNat n = ↑n

Tactic:
match n with
  | 0 => simp
  | 1 => simp
  | n + 2 => rfl

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass α>0 α (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 < x2
a : { x // 0 ≤ x }
b c : α
h : (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ ↑x * y) a b) ((fun x y ↦ ↑x * y) a c)
ha : 0 < ↑a
⊢ b < c

Tactic:
exact @ContravariantClass.elim α>0 α (fun x y => x * y) (· < ·) _ ⟨_, ha⟩ _ _ h

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

Goal state before:
pp: M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a b : M₀
inst✝ : MulPosMono M₀
hb : 0 ≤ b
⊢ a * a < b * b → a < b

Tactic:
simp only [← sq]

Goal state after:
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : LinearOrder M₀
inst✝¹ : PosMulStrictMono M₀
a b : M₀
inst✝ : MulPosMono M₀
hb : 0 ≤ b
⊢ a ^ 2 < b ^ 2 → a < b
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

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

Tactic:
by simpa using inv_mul_le_one₀ ha (b := 1)

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

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
hb : 0 ≤ b
hc : 0 ≤ 0
h : a ≤ 0⁻¹ * b
⊢ 0 * a ≤ b

Tactic:
simpa using hb

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

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b c : G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ b * c
hb : 0 < b
⊢ b⁻¹ * a ≤ c

Tactic:
rwa [inv_mul_le_iff₀ hb]

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : ZeroLEOneClass G₀
h : a ≤ b
hb : 0 ≤ b
⊢ a ≤ b * 1

Tactic:
by rwa [mul_one]

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

Goal state before:
pp: case mpr
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
a : R
⊢ a ≠ 0 → 0 < a * a

Tactic:
intro h

Goal state after:
case mpr
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
a : R
h : a ≠ 0
⊢ 0 < a * a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
hb : 0 ≤ b
hc : 0 ≤ 0
h : a ≤ b * 0⁻¹
⊢ a * 0 ≤ b

Tactic:
simpa using hb

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

Goal state before:
pp: R : Type u
inst✝⁵ : CommSemiring R
inst✝⁴ : LinearOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftReflectLE R
inst✝ : AddLeftMono R
a b : R
⊢ 4 * a * b ≤ (a + b) ^ 2

Tactic:
by
  calc 4 * a * b
    _ = 2 * a * b + 2 * a * b := by rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]
    _ ≤ a ^ 2 + b ^ 2 + 2 * a * b := by gcongr; exact two_mul_le_add_sq _ _
    _ = a ^ 2 + 2 * a * b + b ^ 2 := by rw [add_right_comm]
    _ = (a + b) ^ 2 := (add_sq a b).symm

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r x y
⊢ x = y

pp: case inr.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : x = y
⊢ x = y

pp: case inr.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
⊢ x = y

Tactic:
· have := hf h
    rw [hxy] at this
    exfalso
    exact irrefl_of s (f y) this

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : x = y
⊢ x = y

case inr.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
⊢ x = y
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Irrefl s
f : α → β
hf : ∀ {x y : α}, r x y → s (f x) (f y)
x y : α
hxy : f x = f y
h : r y x
⊢ x = y

Tactic:
· have := hf h
    rw [hxy] at this
    exfalso
    exact irrefl_of s (f y) this

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
f : α ↪o β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
a₁ a₂ : α
⊢ Disjoint (f a₁) (f a₂) → Disjoint a₁ a₂

Tactic:
intro h

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
f : α ↪o β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
a₁ a₂ : α
h : Disjoint (f a₁) (f a₂)
⊢ Disjoint a₁ a₂
Module: Mathlib.Algebra.Order.Group.Abs

Goal state before:
pp: case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
n : ℕ
a : G
ha : a ≤ 1
⊢ 1 ≤ a⁻¹ ^ n

Tactic:
exact one_le_pow_of_one_le' (one_le_inv'.2 ha) n

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
⊢ a ^ (n + 1) * a ≤ b ^ n * a * a

Tactic:
grw [pow_le_pow_mul_of_sq_le_mul hab (by lia)]

Goal state after:
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
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ n.natAbs = 1 ↔ a ^ n = 1

Tactic:
pow_natAbs_eq_one

Goal state after:
G : Type u_1
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ n = 1 ↔ a ^ n = 1
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: p : ℕ
⊢ 0 < 2

Tactic:
by decide

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

Goal state before:
pp: α : Type u_1
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
⊢ 1 ≠ 0

Tactic:
by decide

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

Goal state before:
pp: m : ℤ
even : Even m
⊢ 0 < 2

Tactic:
by decide

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

Goal state before:
pp: case succ.succ
n p q : ℕ
dvd : (p + 1).gcd (q + 1) ∣ n
le : (p + 1).pred * (q + 1).pred ≤ n
⊢ ∃ a b, a * (p + 1) + b * (q + 1) = n

Tactic:
← Int.gcd_natCast_natCast,

Goal state after:
case succ.succ
n p q : ℕ
dvd : (↑(p + 1)).gcd ↑(q + 1) ∣ n
le : (p + 1).pred * (q + 1).pred ≤ n
⊢ ∃ a b, a * (p + 1) + b * (q + 1) = n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: case mp
a b : ℤ
n : ℕ
⊢ a.gcd b ∣ n → ∃ x y, ↑n = a * x + b * y

Tactic:
intro h

Goal state after:
case mp
a b : ℤ
n : ℕ
h : a.gcd b ∣ n
⊢ ∃ x y, ↑n = a * x + b * y
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: a b : ℤ
n : ℕ
⊢ a.gcd b ∣ n ↔ ∃ x y, ↑n = a * x + b * y

Tactic:
by
  constructor
  · intro h
    rw [← Nat.mul_div_cancel' h, Int.natCast_mul, gcd_eq_gcd_ab, Int.add_mul, mul_assoc, mul_assoc]
    exact ⟨_, _, rfl⟩
  · rintro ⟨x, y, h⟩
    rw [← Int.natCast_dvd_natCast, h]
    exact Int.dvd_add (dvd_mul_of_dvd_left (gcd_dvd_left ..))
      (dvd_mul_of_dvd_left (gcd_dvd_right ..))

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : MulZeroOneClass G
inst✝ : MulZeroOneClass H
f g : G ≃* H
⊢ f.toMonoidWithZeroHom = g.toMonoidWithZeroHom ↔ f = g

Tactic:
simp [MonoidWithZeroHom.ext_iff, MulEquiv.ext_iff]

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

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

Tactic:
intro h

Goal state after:
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
h : ⊤ = 0
⊢ False
Module: Mathlib.Algebra.Order.AddGroupWithTop

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

Tactic:
by simpa [h] using add_neg_cancel_of_ne_top (x := a)

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 β
x : 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 =
    x✝ x

Tactic:
cases x

Goal state after:
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

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✝
Module: Mathlib.Algebra.Order.AddGroupWithTop

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

Tactic:
cases x

Goal state after:
case top
G : Type u_1
inst✝ : AddCommGroup G
⊢ ⊤ - ⊤ = ⊤

case coe
G : Type u_1
inst✝ : AddCommGroup G
a✝ : G
⊢ ⊤ - ↑a✝ = ⊤
Module: Mathlib.Algebra.Order.AddGroupWithTop

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

Tactic:
cases x

Goal state after:
case top
G : Type u_1
inst✝ : AddCommGroup G
⊢ ⊤ - ⊤ = ⊤

case coe
G : Type u_1
inst✝ : AddCommGroup G
a✝ : G
⊢ ↑a✝ - ⊤ = ⊤
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:
cases x

Goal state after:
case top
G : Type u_1
inst✝ : AddCommGroup G
y : WithTop G
⊢ ⊤ - y = ⊤ ↔ ⊤ = ⊤ ∨ y = ⊤

case coe
G : Type u_1
inst✝ : AddCommGroup G
y : WithTop G
a✝ : G
⊢ ↑a✝ - y = ⊤ ↔ ↑a✝ = ⊤ ∨ y = ⊤
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:
cases x

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

case coe
α : Type u
β : Type v
inst✝² : One α
a : α
inst✝¹ : LE α
inst✝ : IsBotOneClass α
a✝ : α
⊢ 1 ≤ ↑a✝
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases x

Goal state after:
case top
α : Type u
inst✝ : Add α
⊢ ⊤ + ⊤ = ⊤

case coe
α : Type u
inst✝ : Add α
a✝ : α
⊢ ↑a✝ + ⊤ = ⊤
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
cases x

Goal state after:
case top
α : Type u
inst✝ : Add α
y : WithTop α
⊢ ⊤ + y = ⊤ ↔ ⊤ = ⊤ ∨ y = ⊤

case coe
α : Type u
inst✝ : Add α
y : WithTop α
a✝ : α
⊢ ↑a✝ + y = ⊤ ↔ ↑a✝ = ⊤ ∨ y = ⊤
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top.top
α : Type u
inst✝ : Add α
⊢ ⊤ + ⊤ = ⊤ ↔ ⊤ = ⊤ ∨ ⊤ = ⊤

Tactic:
simp [← coe_add]

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

Goal state before:
pp: case top.coe
α : Type u
inst✝ : Add α
a✝ : α
⊢ ⊤ + ↑a✝ = ⊤ ↔ ⊤ = ⊤ ∨ ↑a✝ = ⊤

Tactic:
simp [← coe_add]

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

Goal state before:
pp: case coe.top
α : Type u
inst✝ : Add α
a✝ : α
⊢ ↑a✝ + ⊤ = ⊤ ↔ ↑a✝ = ⊤ ∨ ⊤ = ⊤

Tactic:
simp [← coe_add]

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

Goal state before:
pp: case coe.coe
α : Type u
inst✝ : Add α
a✝¹ a✝ : α
⊢ ↑a✝¹ + ↑a✝ = ⊤ ↔ ↑a✝¹ = ⊤ ∨ ↑a✝ = ⊤

Tactic:
simp [← coe_add]

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:
cases x

Goal state after:
case top
α : Type u
inst✝ : Add α
y : WithTop α
⊢ ⊤ + y ≠ ⊤ ↔ ⊤ ≠ ⊤ ∧ y ≠ ⊤

case coe
α : Type u
inst✝ : Add α
y : WithTop α
a✝ : α
⊢ ↑a✝ + y ≠ ⊤ ↔ ↑a✝ ≠ ⊤ ∧ y ≠ ⊤
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: case top.top
α : Type u
inst✝ : Add α
⊢ ⊤ + ⊤ ≠ ⊤ ↔ ⊤ ≠ ⊤ ∧ ⊤ ≠ ⊤

Tactic:
simp [← coe_add]

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

Goal state before:
pp: case top.coe
α : Type u
inst✝ : Add α
a✝ : α
⊢ ⊤ + ↑a✝ ≠ ⊤ ↔ ⊤ ≠ ⊤ ∧ ↑a✝ ≠ ⊤

Tactic:
simp [← coe_add]

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

Goal state before:
pp: case coe.top
α : Type u
inst✝ : Add α
a✝ : α
⊢ ↑a✝ + ⊤ ≠ ⊤ ↔ ↑a✝ ≠ ⊤ ∧ ⊤ ≠ ⊤

Tactic:
simp [← coe_add]

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

Goal state before:
pp: case coe.coe
α : Type u
inst✝ : Add α
a✝¹ a✝ : α
⊢ ↑a✝¹ + ↑a✝ ≠ ⊤ ↔ ↑a✝¹ ≠ ⊤ ∧ ↑a✝ ≠ ⊤

Tactic:
simp [← coe_add]

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
  lift z to α using hz; exact (IsAddRightRegular.all _).withTop.eq_iff

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:
cases x

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

case coe
α : Type u
β : Type v
inst✝² : Add α
w x y✝ z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
y z : WithTop α
a✝ : α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) (↑a✝) y) ((fun x1 x2 ↦ x1 + x2) (↑a✝) z)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

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

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

Tactic:
simp [← coe_add]

Goal state after: