mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : AddMonoidWithOne R
P : Prop
inst✝ : Decidable P
m n : ℕ
h✝ : P
⊢ ↑m = ↑m

pp: case neg
R : Type u_1
inst✝¹ : AddMonoidWithOne R
P : Prop
inst✝ : Decidable P
m n : ℕ
h✝ : ¬P
⊢ ↑n = ↑n

Tactic:
<;>

Goal state after:
case pos
R : Type u_1
inst✝¹ : AddMonoidWithOne R
P : Prop
inst✝ : Decidable P
m n : ℕ
h✝ : P
⊢ ↑m = ↑m

case neg
R : Type u_1
inst✝¹ : AddMonoidWithOne R
P : Prop
inst✝ : Decidable P
m n : ℕ
h✝ : ¬P
⊢ ↑n = ↑n
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: case pos
M : Type u_1
A : Type u_7
inst✝² : Zero A
inst✝¹ : SMulZeroClass M A
p : Prop
inst✝ : Decidable p
a : M
b : A
h✝ : p
⊢ a • b = a • b

pp: case neg
M : Type u_1
A : Type u_7
inst✝² : Zero A
inst✝¹ : SMulZeroClass M A
p : Prop
inst✝ : Decidable p
a : M
b : A
h✝ : ¬p
⊢ a • 0 = 0

Tactic:
<;>

Goal state after:
case pos
M : Type u_1
A : Type u_7
inst✝² : Zero A
inst✝¹ : SMulZeroClass M A
p : Prop
inst✝ : Decidable p
a : M
b : A
h✝ : p
⊢ a • b = a • b

case neg
M : Type u_1
A : Type u_7
inst✝² : Zero A
inst✝¹ : SMulZeroClass M A
p : Prop
inst✝ : Decidable p
a : M
b : A
h✝ : ¬p
⊢ a • 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: case inl
M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
⊢ 1 0 = 0 ↔ 0 = 0

pp: case inr
M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
x : M₀
hx : x ≠ 0
⊢ 1 x = 0 ↔ x = 0

Tactic:
<;>

Goal state after:
case inl
M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
⊢ 1 0 = 0 ↔ 0 = 0

case inr
M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
x : M₀
hx : x ≠ 0
⊢ 1 x = 0 ↔ x = 0
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: case inl
M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
⊢ 1 0 = 0 ↔ 0 = 0

Tactic:
simp_all [one_apply_of_ne_zero]

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

Goal state before:
pp: case inr
M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
x : M₀
hx : x ≠ 0
⊢ 1 x = 0 ↔ x = 0

Tactic:
simp_all [one_apply_of_ne_zero]

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

Goal state before:
pp: case inl
M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
⊢ 1 0 = 1 ↔ 0 ≠ 0

pp: case inr
M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
x : M₀
hx : x ≠ 0
⊢ 1 x = 1 ↔ x ≠ 0

Tactic:
<;>

Goal state after:
case inl
M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
⊢ 1 0 = 1 ↔ 0 ≠ 0

case inr
M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
x : M₀
hx : x ≠ 0
⊢ 1 x = 1 ↔ x ≠ 0
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: case inl
M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
⊢ 1 0 = 1 ↔ 0 ≠ 0

Tactic:
simp_all [one_apply_of_ne_zero]

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

Goal state before:
pp: case inr
M₀ : Type u_7
N₀ : Type u_8
inst✝⁵ : MulZeroOneClass M₀
inst✝⁴ : MulZeroOneClass N₀
inst✝³ : DecidablePred fun x ↦ x = 0
inst✝² : Nontrivial M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial N₀
x : M₀
hx : x ≠ 0
⊢ 1 x = 1 ↔ x ≠ 0

Tactic:
simp_all [one_apply_of_ne_zero]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : 1 / 0 ≠ 0
ha : a = 0
⊢ False

Tactic:
div_zero

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
h : 0 ≠ 0
ha : a = 0
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M₀ : Type u_2
A : Type u_7
inst✝³ : MonoidWithZero M₀
inst✝² : Zero A
inst✝¹ : MulActionWithZero M₀ A
inst✝ : Subsingleton M₀
x y : A
⊢ x = y

Tactic:
rw [← one_smul M₀ x, ← one_smul M₀ y, Subsingleton.elim (1 : M₀) 0, zero_smul, zero_smul]

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

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

Tactic:
rw [← Nat.cast_one, Nat.cast_ne_zero]
    trivial

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

Goal state before:
pp: case ofNat
R : Type u_1
inst✝ : AddGroupWithOne R
a✝ : ℕ
⊢ Int.ofNat a✝ • 1 = ↑(Int.ofNat a✝)

pp: case negSucc
R : Type u_1
inst✝ : AddGroupWithOne R
a✝ : ℕ
⊢ Int.negSucc a✝ • 1 = ↑(Int.negSucc a✝)

Tactic:
<;>

Goal state after:
case ofNat
R : Type u_1
inst✝ : AddGroupWithOne R
a✝ : ℕ
⊢ Int.ofNat a✝ • 1 = ↑(Int.ofNat a✝)

case negSucc
R : Type u_1
inst✝ : AddGroupWithOne R
a✝ : ℕ
⊢ Int.negSucc a✝ • 1 = ↑(Int.negSucc a✝)
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
x : M
⊢ -r • x + r • x = 0

Tactic:
rw [← add_smul, neg_add_cancel, zero_smul]

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Ring R
n : ℤ
⊢ ↑(n ^ 0) = ↑n ^ 0

pp: case succ
R : Type u_1
inst✝ : Ring R
n : ℤ
n✝ : ℕ
a✝ : ↑(n ^ n✝) = ↑n ^ n✝
⊢ ↑(n ^ (n✝ + 1)) = ↑n ^ (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝ : Ring R
n : ℤ
⊢ ↑(n ^ 0) = ↑n ^ 0

case succ
R : Type u_1
inst✝ : Ring R
n : ℤ
n✝ : ℕ
a✝ : ↑(n ^ n✝) = ↑n ^ n✝
⊢ ↑(n ^ (n✝ + 1)) = ↑n ^ (n✝ + 1)
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: case inl
n : ℤ
m : ℕ
hn : n = ↑n.natAbs
⊢ ↑m ∣ n ↔ m ∣ n.natAbs

pp: case inr
n : ℤ
m : ℕ
hn : n = -↑n.natAbs
⊢ ↑m ∣ n ↔ m ∣ n.natAbs

Tactic:
<;>

Goal state after:
case inl
n : ℤ
m : ℕ
hn : n = ↑n.natAbs
⊢ ↑m ∣ n ↔ m ∣ n.natAbs

case inr
n : ℤ
m : ℕ
hn : n = -↑n.natAbs
⊢ ↑m ∣ n ↔ m ∣ n.natAbs
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: case inl
n : ℤ
m : ℕ
hn : n = ↑n.natAbs
⊢ ↑m ∣ ↑n.natAbs ↔ m ∣ (↑n.natAbs).natAbs

pp: case inr
n : ℤ
m : ℕ
hn : n = -↑n.natAbs
⊢ ↑m ∣ -↑n.natAbs ↔ m ∣ (-↑n.natAbs).natAbs

Tactic:
<;>

Goal state after:
case inl
n : ℤ
m : ℕ
hn : n = ↑n.natAbs
⊢ ↑m ∣ ↑n.natAbs ↔ m ∣ (↑n.natAbs).natAbs

case inr
n : ℤ
m : ℕ
hn : n = -↑n.natAbs
⊢ ↑m ∣ -↑n.natAbs ↔ m ∣ (-↑n.natAbs).natAbs
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: case inl
m : ℤ
n : ℕ
hn : m = ↑m.natAbs
⊢ m ∣ ↑n ↔ m.natAbs ∣ n

pp: case inr
m : ℤ
n : ℕ
hn : m = -↑m.natAbs
⊢ m ∣ ↑n ↔ m.natAbs ∣ n

Tactic:
<;>

Goal state after:
case inl
m : ℤ
n : ℕ
hn : m = ↑m.natAbs
⊢ m ∣ ↑n ↔ m.natAbs ∣ n

case inr
m : ℤ
n : ℕ
hn : m = -↑m.natAbs
⊢ m ∣ ↑n ↔ m.natAbs ∣ n
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: case inl
m : ℤ
n : ℕ
hn : m = ↑m.natAbs
⊢ ↑m.natAbs ∣ ↑n ↔ (↑m.natAbs).natAbs ∣ n

pp: case inr
m : ℤ
n : ℕ
hn : m = -↑m.natAbs
⊢ -↑m.natAbs ∣ ↑n ↔ (-↑m.natAbs).natAbs ∣ n

Tactic:
<;>

Goal state after:
case inl
m : ℤ
n : ℕ
hn : m = ↑m.natAbs
⊢ ↑m.natAbs ∣ ↑n ↔ (↑m.natAbs).natAbs ∣ n

case inr
m : ℤ
n : ℕ
hn : m = -↑m.natAbs
⊢ -↑m.natAbs ∣ ↑n ↔ (-↑m.natAbs).natAbs ∣ n
Module: Mathlib.Algebra.Group.Even

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

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

Tactic:
<;>

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

case mpr
α : Type u_2
inst✝ : DivisionMonoid α
a : α
⊢ IsSquare a → IsSquare a⁻¹
Module: Mathlib.Algebra.Group.Even

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

pp: case mpr
α : Type u_2
inst✝ : DivisionMonoid α
a : α
h : IsSquare a
⊢ IsSquare a⁻¹

Tactic:
<;>

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
a : α
h : IsSquare a⁻¹
⊢ IsSquare a

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

Goal state before:
pp: case inl
m n : ℕ
h₁ : m % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

pp: case inr
m n : ℕ
h₁ : m % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
<;>

Goal state after:
case inl
m n : ℕ
h₁ : m % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

case inr
m n : ℕ
h₁ : m % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
Module: Mathlib.Algebra.Group.Nat.Even

Goal state before:
pp: case inl.inl
m n : ℕ
h₁ : m % 2 = 0
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

pp: case inl.inr
m n : ℕ
h₁ : m % 2 = 0
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n

pp: case inr.inl
m n : ℕ
h₁ : m % 2 = 1
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

pp: case inr.inr
m n : ℕ
h₁ : m % 2 = 1
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
<;>

Goal state after:
case inl.inl
m n : ℕ
h₁ : m % 2 = 0
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

case inl.inr
m n : ℕ
h₁ : m % 2 = 0
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n

case inr.inl
m n : ℕ
h₁ : m % 2 = 1
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

case inr.inr
m n : ℕ
h₁ : m % 2 = 1
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: case inl
m n : ℤ
h₁ : m % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

pp: case inr
m n : ℤ
h₁ : m % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
<;>

Goal state after:
case inl
m n : ℤ
h₁ : m % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

case inr
m n : ℤ
h₁ : m % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: case inl.inl
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

pp: case inl.inr
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n

pp: case inr.inl
m n : ℤ
h₁ : m % 2 = 1
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

pp: case inr.inr
m n : ℤ
h₁ : m % 2 = 1
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n

Tactic:
<;>

Goal state after:
case inl.inl
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

case inl.inr
m n : ℤ
h₁ : m % 2 = 0
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n

case inr.inl
m n : ℤ
h₁ : m % 2 = 1
h₂ : n % 2 = 0
⊢ Even (m * n) ↔ Even m ∨ Even n

case inr.inr
m n : ℤ
h₁ : m % 2 = 1
h₂ : n % 2 = 1
⊢ Even (m * n) ↔ Even m ∨ Even n
Module: Mathlib.Algebra.Group.Nat.Hom

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : M
n : Multiplicative ℕ
⊢ ((powersHom M).toFun (a * b)) n = ((powersHom M).toFun a * (powersHom M).toFun b) n

Tactic:
by simp [mul_pow]

Goal state after:
Module: Mathlib.Algebra.Group.Hom.Instances

Goal state before:
pp: M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝¹ : MulOneClass M
inst✝ : CommMonoid N
f : M →* N
n : ℕ
x y : M
⊢ (⇑f ^ n) (x * y) = (⇑f ^ n) x * (⇑f ^ n) y

Tactic:
by simp [mul_pow]

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

Goal state before:
pp: case zero
α : Type u_1
inst✝ : NonAssocSemiring α
m : ℕ
⊢ ↑(m * 0) = ↑m * ↑0

pp: case succ
α : Type u_1
inst✝ : NonAssocSemiring α
m n✝ : ℕ
a✝ : ↑(m * n✝) = ↑m * ↑n✝
⊢ ↑(m * (n✝ + 1)) = ↑m * ↑(n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
α : Type u_1
inst✝ : NonAssocSemiring α
m : ℕ
⊢ ↑(m * 0) = ↑m * ↑0

case succ
α : Type u_1
inst✝ : NonAssocSemiring α
m n✝ : ℕ
a✝ : ↑(m * n✝) = ↑m * ↑n✝
⊢ ↑(m * (n✝ + 1)) = ↑m * ↑(n✝ + 1)
Module: Mathlib.Logic.Nontrivial.Basic

Goal state before:
pp: case inl
α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h✝ : x < y
⊢ ∃ x y, x < y

pp: case inr
α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h✝ : y < x
⊢ ∃ x y, x < y

Tactic:
<;>

Goal state after:
case inl
α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h✝ : x < y
⊢ ∃ x y, x < y

case inr
α : Type u_3
inst✝¹ : Nontrivial α
inst✝ : LinearOrder α
x y : α
hxy : x ≠ y
h✝ : y < x
⊢ ∃ x y, x < y
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
f : α →+* α
⊢ (⇑f)^[0] = ⇑(npowRec 0 f)

pp: case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
f : α →+* α
n✝ : ℕ
a✝ : (⇑f)^[n✝] = ⇑(npowRec n✝ f)
⊢ (⇑f)^[n✝ + 1] = ⇑(npowRec (n✝ + 1) f)

Tactic:
<;>

Goal state after:
case zero
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
f : α →+* α
⊢ (⇑f)^[0] = ⇑(npowRec 0 f)

case succ
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
x✝² : NonAssocSemiring α
x✝¹ : NonAssocSemiring β
x✝ : NonAssocSemiring γ
f : α →+* α
n✝ : ℕ
a✝ : (⇑f)^[n✝] = ⇑(npowRec n✝ f)
⊢ (⇑f)^[n✝ + 1] = ⇑(npowRec (n✝ + 1) f)
Module: Mathlib.Algebra.Group.Commute.Units

Goal state before:
pp: case zero
M : Type u_1
inst✝ : Monoid M
a : M
hx : ¬IsUnit a
⊢ IsUnit (a ^ 0) ↔ 0 = 0

pp: case succ
M : Type u_1
inst✝ : Monoid M
a : M
hx : ¬IsUnit a
n : ℕ
⊢ IsUnit (a ^ (n + 1)) ↔ n + 1 = 0

Tactic:
<;>

Goal state after:
case zero
M : Type u_1
inst✝ : Monoid M
a : M
hx : ¬IsUnit a
⊢ IsUnit (a ^ 0) ↔ 0 = 0

case succ
M : Type u_1
inst✝ : Monoid M
a : M
hx : ¬IsUnit a
n : ℕ
⊢ IsUnit (a ^ (n + 1)) ↔ n + 1 = 0
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : 0 = 0 → a = 0
⊢ a / 0 * 0 = a

pp: case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
hb : b ≠ 0
⊢ a / b * b = a

Tactic:
<;>

Goal state after:
case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : 0 = 0 → a = 0
⊢ a / 0 * 0 = a

case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
hb : b ≠ 0
⊢ a / b * b = a
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : 0 = 0 → a = 0
⊢ a * 0 / 0 = a

pp: case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
hb : b ≠ 0
⊢ a * b / b = a

Tactic:
<;>

Goal state after:
case inl
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
h : 0 = 0 → a = 0
⊢ a * 0 / 0 = a

case inr
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
h : b = 0 → a = 0
hb : b ≠ 0
⊢ a * b / b = a
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
m n : ℕ
a : G₀
ha : a ≠ 0
h : n ≤ m
⊢ a ^ (m - n) = a ^ m * (a ^ n)⁻¹

Tactic:
by
  have h1 : m - n + n = m := Nat.sub_add_cancel h
  have h2 : a ^ (m - n) * a ^ n = a ^ m := by rw [← pow_add, h1]
  simpa only [div_eq_mul_inv] using eq_div_of_mul_eq (pow_ne_zero _ ha) h2

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

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hc : c ≠ 0
hd : d ≠ 0
h : a / 0 = c / d
hb : b = 0
⊢ False

Tactic:
div_zero

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hc : c ≠ 0
hd : d ≠ 0
h : 0 = c / d
hb : b = 0
⊢ False
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: case inl
R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : (-1) ^ n = 1
⊢ (-1) ^ n * a = 0 ↔ a = 0

pp: case inr
R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : (-1) ^ n = -1
⊢ (-1) ^ n * a = 0 ↔ a = 0

Tactic:
<;>

Goal state after:
case inl
R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : (-1) ^ n = 1
⊢ (-1) ^ n * a = 0 ↔ a = 0

case inr
R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : (-1) ^ n = -1
⊢ (-1) ^ n * a = 0 ↔ a = 0
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: case inl
R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : (-1) ^ n = 1
⊢ a * (-1) ^ n = 0 ↔ a = 0

pp: case inr
R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : (-1) ^ n = -1
⊢ a * (-1) ^ n = 0 ↔ a = 0

Tactic:
<;>

Goal state after:
case inl
R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : (-1) ^ n = 1
⊢ a * (-1) ^ n = 0 ↔ a = 0

case inr
R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : (-1) ^ n = -1
⊢ a * (-1) ^ n = 0 ↔ a = 0
Module: Mathlib.Algebra.Module.NatInt

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : M
⊢ -1 • a + 1 • a = 0

Tactic:
rw [← add_smul, neg_add_cancel, zero_smul]

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

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

pp: case inr
k : ℕ
⊢ ∃ k_1, Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)

Tactic:
<;>

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.Order.MinMax

Goal state before:
pp: case inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
h : a ≤ b
⊢ f (max a b) = max (f a) (f b)

pp: case inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
h : b ≤ a
⊢ f (max a b) = max (f a) (f b)

Tactic:
<;>

Goal state after:
case inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
h : a ≤ b
⊢ f (max a b) = max (f a) (f b)

case inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
s : Set α
a b : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
h : b ≤ a
⊢ f (max a b) = max (f a) (f b)
Module: Mathlib.Order.MinMax

Goal state before:
pp: case inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hf : Monotone f
h : a ≤ b
⊢ f (max a b) = max (f a) (f b)

pp: case inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hf : Monotone f
h : b ≤ a
⊢ f (max a b) = max (f a) (f b)

Tactic:
<;>

Goal state after:
case inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hf : Monotone f
h : a ≤ b
⊢ f (max a b) = max (f a) (f b)

case inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hf : Monotone f
h : b ≤ a
⊢ f (max a b) = max (f a) (f b)
Module: Mathlib.Order.MinMax

Goal state before:
pp: case inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hf : Antitone f
h : a ≤ b
⊢ f (max a b) = min (f a) (f b)

pp: case inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hf : Antitone f
h : b ≤ a
⊢ f (max a b) = min (f a) (f b)

Tactic:
<;>

Goal state after:
case inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hf : Antitone f
h : a ≤ b
⊢ f (max a b) = min (f a) (f b)

case inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hf : Antitone f
h : b ≤ a
⊢ f (max a b) = min (f a) (f b)
Module: Mathlib.Order.MinMax

Goal state before:
pp: case inl
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : a ≤ b
⊢ min a b = a ∨ min a b = b

pp: case inr
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : b ≤ a
⊢ min a b = a ∨ min a b = b

Tactic:
<;>

Goal state after:
case inl
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : a ≤ b
⊢ min a b = a ∨ min a b = b

case inr
α : Type u
inst✝ : LinearOrder α
a b : α
h✝ : b ≤ a
⊢ min a b = a ∨ min a b = b
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a = c + b
⊢ c ≤ a - b

Tactic:
by
    rw [h]
    exact hb.le_add_tsub

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

Goal state before:
pp: α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c : α
⊢ b⁻¹ * a ≤ c ↔ a ≤ b * c

Tactic:
rw [← mul_le_mul_iff_left b, mul_inv_cancel_left]

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 1 + 1

Tactic:
exact add_nonneg zero_le_one zero_le_one

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

Goal state before:
pp: α : Type u
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : MulLeftMono α
a b : α
inst✝ : MulRightMono α
⊢ a / b ≤ a⁻¹ * b ↔ a ≤ b

Tactic:
rw [div_eq_mul_inv, mul_inv_le_inv_mul_iff]
  exact
    ⟨fun h => not_lt.mp fun k => not_lt.mpr h (mul_lt_mul_of_lt_of_lt k k), fun h =>
      mul_le_mul' h h⟩

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

Goal state before:
pp: case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
⊢ a * a ≤ a

Tactic:
have : a * a < a * 1 := mul_lt_mul_right h a

Goal state after:
case h
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LinearOrder α
inst✝ : MulLeftStrictMono α
a : α
h : a < 1
this : a * a < a * 1
⊢ a * a ≤ a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: α : 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)
⊢ (fun x1 x2 ↦ x1 < x2) b c

Tactic:
obtain ha | ha := a.prop.eq_or_lt
        · simp [← ha] at h
        · exact @ContravariantClass.elim α>0 α (fun x y => x * y) (· < ·) _ ⟨_, ha⟩ _ _ h

Goal state after:
Module: Mathlib.Data.Prod.PProd

Goal state before:
pp: α✝ : Sort u_1
β✝ : Sort u_2
γ : Sort u_3
δ : Sort u_4
α : Type u_5
β : Type u_6
x₁ : α
y₁ : β
x₂ : α
y₂ : β
⊢ (x₁, y₁) = (x₂, y₂) → ⦃P : Sort u_7⦄ → (x₁ = x₂ → y₁ = y₂ → P) → P

Tactic:
intros h P w
  cases h
  exact w rfl rfl

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

Goal state before:
pp: case inl
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : a < 0
⊢ a * b ≠ 0

pp: case inr
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : 0 < a
⊢ a * b ≠ 0

Tactic:
<;>

Goal state after:
case inl
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : a < 0
⊢ a * b ≠ 0

case inr
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
ha : 0 < a
⊢ a * b ≠ 0
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
b : G₀
hb : 0 ≤ b
⊢ 0 * (0⁻¹ * b) ≤ b

pp: case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : 0 ≤ b
ha : a ≠ 0
⊢ a * (a⁻¹ * b) ≤ b

Tactic:
<;>

Goal state after:
case inl
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
b : G₀
hb : 0 ≤ b
⊢ 0 * (0⁻¹ * b) ≤ b

case inr
G₀ : Type u_3
inst✝¹ : GroupWithZero G₀
inst✝ : Preorder G₀
a b : G₀
hb : 0 ≤ b
ha : a ≠ 0
⊢ a * (a⁻¹ * b) ≤ b