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

Goal state before:
pp: case succ
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
y : M₀
⊢ f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y

Tactic:
;

Goal state after:
case succ
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
M : Type u_2
inst✝ : Monoid M
f : M₀ → M
x : M₀
hx : ∀ (y : M₀), f (x * y) = f x * f y
n : ℕ
hn : ∀ (y : M₀), f (x ^ n * y) = f x ^ n * f y
y : M₀
⊢ f (x ^ (n + 1) * y) = f x ^ (n + 1) * f y
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
⊢ (if f z = x then y else if f z = y then x else f z) = f (if z = f⁻¹ x then f⁻¹ y else if z = f⁻¹ y then f⁻¹ x else z)

Tactic:
;

Goal state after:
α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y z : α
⊢ (if f z = x then y else if f z = y then x else f z) = f (if z = f⁻¹ x then f⁻¹ y else if z = f⁻¹ y then f⁻¹ x else z)
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
hn : n ≠ 0
ha : 0 ^ n ≠ 0
⊢ False

Tactic:
;

Goal state after:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
n : ℕ
hn : n ≠ 0
ha : 0 ^ n ≠ 0
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroHomClass F α β
a : α
f : F
neZero : NeZero (f a)
h : a = 0
⊢ f 0 = 0

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroHomClass F α β
a : α
f : F
neZero : NeZero (f a)
h : a = 0
⊢ f 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
h : 0 ^ 0 = 0
⊢ False

Tactic:
;

Goal state after:
M₀ : Type u_1
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
h : 0 ^ 0 = 0
⊢ False
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
inst✝ : Group α
a : α
n : ℕ
x✝ : α
⊢ (Equiv.mulLeft a ^ n) x✝ = (Equiv.mulLeft (a ^ n)) x✝

Tactic:
;

Goal state after:
α : Type u_4
inst✝ : Group α
a : α
n : ℕ
x✝ : α
⊢ (Equiv.mulLeft a ^ n) x✝ = (Equiv.mulLeft (a ^ n)) x✝
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
inst✝ : Group α
a : α
n : ℕ
x✝ : α
⊢ (Equiv.mulRight a ^ n) x✝ = (Equiv.mulRight (a ^ n)) x✝

Tactic:
;

Goal state after:
α : Type u_4
inst✝ : Group α
a : α
n : ℕ
x✝ : α
⊢ (Equiv.mulRight a ^ n) x✝ = (Equiv.mulRight (a ^ n)) x✝
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: case succ
M₀ : Type u_1
G₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
a✝ : M₀
n✝ : ℕ
inst✝ : NoZeroDivisors M₀
a : M₀
x✝ : IsNilpotent a
n : ℕ
ih : a ^ n = 0 → a = 0
ha : a ^ n = 0 ∨ a = 0
⊢ a = 0

Tactic:
;

Goal state after:
case succ
M₀ : Type u_1
G₀ : Type u_2
inst✝¹ : MonoidWithZero M₀
a✝ : M₀
n✝ : ℕ
inst✝ : NoZeroDivisors M₀
a : M₀
x✝ : IsNilpotent a
n : ℕ
ih : a ^ n = 0 → a = 0
ha : a ^ n = 0 ∨ a = 0
⊢ a = 0
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : FunLike F α β
inst✝¹ : ZeroHomClass F α β
a : α
f : F
hf : Injective ⇑f
inst✝ : NeZero a
⊢ f a ≠ f 0

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : FunLike F α β
inst✝¹ : ZeroHomClass F α β
a : α
f : F
hf : Injective ⇑f
inst✝ : NeZero a
⊢ f a ≠ f 0
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝¹ : Mul M
inst✝ : Group G
x✝ : G
⊢ { toFun := fun h ↦ 1 * h * 1⁻¹, invFun := fun h ↦ 1⁻¹ * h * 1, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ } x✝ =
    1 x✝

Tactic:
;

Goal state after:
A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝¹ : Mul M
inst✝ : Group G
x✝ : G
⊢ { toFun := fun h ↦ 1 * h * 1⁻¹, invFun := fun h ↦ 1⁻¹ * h * 1, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ } x✝ =
    1 x✝
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝¹ : Mul M
inst✝ : Group G
x✝² x✝¹ x✝ : G
⊢ { toFun := fun h ↦ x✝² * x✝¹ * h * (x✝² * x✝¹)⁻¹, invFun := fun h ↦ (x✝² * x✝¹)⁻¹ * h * (x✝² * x✝¹), left_inv := ⋯,
        right_inv := ⋯, map_mul' := ⋯ }
      x✝ =
    ({ toFun := fun h ↦ x✝² * h * x✝²⁻¹, invFun := fun h ↦ x✝²⁻¹ * h * x✝², left_inv := ⋯, right_inv := ⋯,
          map_mul' := ⋯ } *
        { toFun := fun h ↦ x✝¹ * h * x✝¹⁻¹, invFun := fun h ↦ x✝¹⁻¹ * h * x✝¹, left_inv := ⋯, right_inv := ⋯,
          map_mul' := ⋯ })
      x✝

Tactic:
;

Goal state after:
A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝¹ : Mul M
inst✝ : Group G
x✝² x✝¹ x✝ : G
⊢ { toFun := fun h ↦ x✝² * x✝¹ * h * (x✝² * x✝¹)⁻¹, invFun := fun h ↦ (x✝² * x✝¹)⁻¹ * h * (x✝² * x✝¹), left_inv := ⋯,
        right_inv := ⋯, map_mul' := ⋯ }
      x✝ =
    ({ toFun := fun h ↦ x✝² * h * x✝²⁻¹, invFun := fun h ↦ x✝²⁻¹ * h * x✝², left_inv := ⋯, right_inv := ⋯,
          map_mul' := ⋯ } *
        { toFun := fun h ↦ x✝¹ * h * x✝¹⁻¹, invFun := fun h ↦ x✝¹⁻¹ * h * x✝¹, left_inv := ⋯, right_inv := ⋯,
          map_mul' := ⋯ })
      x✝
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
g : α →*₀ β
toFun✝ : α → β
map_zero'✝ : toFun✝ 0 = 0
map_one'✝ : { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun x * { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun y
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } = g

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
g : α →*₀ β
toFun✝ : α → β
map_zero'✝ : toFun✝ 0 = 0
map_one'✝ : { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun x * { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun y
h :
  (fun f ↦ f.toFun) { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } = g
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
toFun✝¹ : α → β
map_zero'✝¹ : toFun✝¹ 0 = 0
map_one'✝¹ : { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }.toFun 1 = 1
map_mul'✝¹ :
  ∀ (x y : α),
    { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }.toFun (x * y) =
      { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }.toFun x * { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }.toFun y
toFun✝ : α → β
map_zero'✝ : toFun✝ 0 = 0
map_one'✝ : { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun x * { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun y
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, map_zero' := map_zero'✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ { toFun := toFun✝¹, map_zero' := map_zero'✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝³ : MulZeroOneClass α
inst✝² : MulZeroOneClass β
inst✝¹ : MulZeroOneClass γ
inst✝ : MulZeroOneClass δ
toFun✝¹ : α → β
map_zero'✝¹ : toFun✝¹ 0 = 0
map_one'✝¹ : { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }.toFun 1 = 1
map_mul'✝¹ :
  ∀ (x y : α),
    { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }.toFun (x * y) =
      { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }.toFun x * { toFun := toFun✝¹, map_zero' := map_zero'✝¹ }.toFun y
toFun✝ : α → β
map_zero'✝ : toFun✝ 0 = 0
map_one'✝ : { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun 1 = 1
map_mul'✝ :
  ∀ (x y : α),
    { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun x * { toFun := toFun✝, map_zero' := map_zero'✝ }.toFun y
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, map_zero' := map_zero'✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ { toFun := toFun✝¹, map_zero' := map_zero'✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    { toFun := toFun✝, map_zero' := map_zero'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
| ↑(k + 1)

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : (k + 1) % 2 = 0
| ↑(k + 1)
Module: Mathlib.Algebra.GroupWithZero.Hom

Goal state before:
pp: F : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝⁵ : MulZeroOneClass α
inst✝⁴ : MulZeroOneClass β✝
inst✝³ : MulZeroOneClass γ
inst✝² : MulZeroOneClass δ
inst✝¹ : FunLike F α β✝
β : Type ?u.21
inst✝ : CommMonoidWithZero β
f g : α →*₀ β
⊢ f 0 * g 0 = 0

Tactic:
;

Goal state after:
F : Type u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
M₀ : Type u_6
inst✝⁵ : MulZeroOneClass α
inst✝⁴ : MulZeroOneClass β✝
inst✝³ : MulZeroOneClass γ
inst✝² : MulZeroOneClass δ
inst✝¹ : FunLike F α β✝
β : Type ?u.21
inst✝ : CommMonoidWithZero β
f g : α →*₀ β
⊢ f 0 * g 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b x✝ x : G₀
hx : x ≠ 0
y z : G₀
h : x * y = x * z
⊢ y = z

Tactic:
;

Goal state after:
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b x✝ x : G₀
hx : x ≠ 0
y z : G₀
h : x * y = x * z
⊢ y = z
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
| ↑(k + 1)

Tactic:
;

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
| ↑(k + 1)
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b x✝ x : G₀
hx : x ≠ 0
y z : G₀
h : y * x = z * x
⊢ y = z

Tactic:
;

Goal state after:
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b x✝ x : G₀
hx : x ≠ 0
y z : G₀
h : y * x = z * x
⊢ y = z
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁵ : Zero M₀
inst✝⁴ : Zero A
inst✝³ : SMulWithZero M₀ A
a : M₀
b : A
inst✝² : Zero M₀'
inst✝¹ : Zero A'
inst✝ : SMul M₀ A'
f : ZeroHom M₀' M₀
m : A
⊢ f 0 • m = 0

Tactic:
;

Goal state after:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁵ : Zero M₀
inst✝⁴ : Zero A
inst✝³ : SMulWithZero M₀ A
a : M₀
b : A
inst✝² : Zero M₀'
inst✝¹ : Zero A'
inst✝ : SMul M₀ A'
f : ZeroHom M₀' M₀
m : A
⊢ f 0 • m = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ n ≠ 0

Tactic:
;

Goal state after:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℕ
h : ↑n ≠ 0
⊢ n ≠ 0
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:
by
    rw [← one_smul M₀ x, ← one_smul M₀ y, Subsingleton.elim (1 : M₀) 0, zero_smul, zero_smul]

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

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁶ : MonoidWithZero M₀
inst✝⁵ : MonoidWithZero M₀'
inst✝⁴ : Zero A
inst✝³ : MulActionWithZero M₀ A
inst✝² : Zero A'
inst✝¹ : SMul M₀ A'
p : Prop
inst✝ : Decidable p
f : M₀' →*₀ M₀
r s : M₀'
m : A
⊢ f (r * s) • m = f r • f s • m

Tactic:
;

Goal state after:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁶ : MonoidWithZero M₀
inst✝⁵ : MonoidWithZero M₀'
inst✝⁴ : Zero A
inst✝³ : MulActionWithZero M₀ A
inst✝² : Zero A'
inst✝¹ : SMul M₀ A'
p : Prop
inst✝ : Decidable p
f : M₀' →*₀ M₀
r s : M₀'
m : A
⊢ f (r * s) • m = f r • f s • m
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁶ : MonoidWithZero M₀
inst✝⁵ : MonoidWithZero M₀'
inst✝⁴ : Zero A
inst✝³ : MulActionWithZero M₀ A
inst✝² : Zero A'
inst✝¹ : SMul M₀ A'
p : Prop
inst✝ : Decidable p
f : M₀' →*₀ M₀
m : A
⊢ f 1 • m = m

Tactic:
;

Goal state after:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝⁶ : MonoidWithZero M₀
inst✝⁵ : MonoidWithZero M₀'
inst✝⁴ : Zero A
inst✝³ : MulActionWithZero M₀ A
inst✝² : Zero A'
inst✝¹ : SMul M₀ A'
p : Prop
inst✝ : Decidable p
f : M₀' →*₀ M₀
m : A
⊢ f 1 • m = m
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: case zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
n : ℕ
h : ↑0 = ↑n
⊢ ↑n = 0

Tactic:
;

Goal state after:
case zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
n : ℕ
h : ↑0 = ↑n
⊢ ↑n = 0
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: case succ.zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
h : ↑(m + 1) = ↑0
⊢ ↑(m + 1) = 0

Tactic:
;

Goal state after:
case succ.zero
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
h : ↑(m + 1) = ↑0
⊢ ↑(m + 1) = 0
Module: Mathlib.Algebra.CharZero.Defs

Goal state before:
pp: case succ.succ
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
n✝ : ℕ
h : ↑m = ↑n✝
⊢ m + 1 = n✝ + 1

Tactic:
;

Goal state after:
case succ.succ
R : Type u_1
inst✝ : AddGroupWithOne R
H : ∀ (n : ℕ), ↑n = 0 → n = 0
m : ℕ
ih : ∀ (n : ℕ), ↑m = ↑n → m = n
n✝ : ℕ
h : ↑m = ↑n✝
⊢ m + 1 = n✝ + 1
Module: Mathlib.Data.Int.Cast.Basic

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

Tactic:
;

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑-[n+1] = -↑(n + 1)
Module: Mathlib.Data.Int.Cast.Basic

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

Tactic:
;

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
⊢ ↑(n + 1) = -↑-[n+1]
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
ih : ∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x ↦ Int.strongRec lt ge k_1
hn : m ≤ n
⊢ (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) n m lt
      (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
    fun k x ↦ Int.strongRec lt ge k

Tactic:
;

Goal state after:
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
ih : ∀ (k : ℤ), k < n → ∀ (hn : m ≤ k), Int.strongRec lt ge k = ge k hn fun k_1 x ↦ Int.strongRec lt ge k_1
hn : m ≤ n
⊢ (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) n m lt
      (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
    fun k x ↦ Int.strongRec lt ge k
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: case refine_2
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
⊢ (if hlm : l < m then lt l hlm
    else
      ge l ⋯ fun k_1 x ↦
        Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
          (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) (fun n x hn l x_1 ↦ hn l ⋯)
          k_1 ⋯) =
    Int.strongRec lt ge l

Tactic:
;

Goal state after:
case refine_2
m n✝ : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
x✝ : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  (∀ (k_1 : ℤ), k_1 < k → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k) →
    (Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
        (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) fun n x hn l x_1 ↦ hn l ⋯) =
      fun k_1 x ↦ Int.strongRec lt ge k_1
ih : ∀ (k_1 : ℤ), k_1 < k + 1 → ∀ (hn : m ≤ k_1), Int.strongRec lt ge k_1 = ge k_1 hn fun k x ↦ Int.strongRec lt ge k
l : ℤ
hl : l < k + 1
⊢ (if hlm : l < m then lt l hlm
    else
      ge l ⋯ fun k_1 x ↦
        Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) k m lt
          (fun _n a ih l a_1 ↦ if hlm : l < m then lt l hlm else ge l ⋯ fun k x ↦ ih k ⋯) (fun n x hn l x_1 ↦ hn l ⋯)
          k_1 ⋯) =
    Int.strongRec lt ge l
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n : ℕ
⊢ n ≤ n.sqrt.succ * n.sqrt + n.sqrt

Tactic:
;

Goal state after:
n : ℕ
⊢ n ≤ n.sqrt.succ * n.sqrt + n.sqrt
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: n : ℕ
h : 1 < n
this : n * 1 < n * n
⊢ n < n * n

Tactic:
;

Goal state after:
n : ℕ
h : 1 < n
this : n * 1 < n * n
⊢ n < n * n
Module: Mathlib.Algebra.Group.Int.Even

Goal state before:
pp: case succ
i✝ : ℕ
a✝ : IsSquare (↑i✝).sign ↔ 0 ≤ ↑i✝
⊢ IsSquare (↑(i✝ + 1)).sign ↔ 0 ≤ i✝ + 1

Tactic:
;

Goal state after:
case succ
i✝ : ℕ
a✝ : IsSquare (↑i✝).sign ↔ 0 ≤ ↑i✝
⊢ IsSquare (↑(i✝ + 1)).sign ↔ 0 ≤ i✝ + 1
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b : α
hab : a ∣ b
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a ∣ b * b ^ n

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
hab : a ∣ b
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a ∣ b * b ^ n
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a b c : α
h : a * c = b
⊢ a * c = b

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : CommSemigroup α
a b c : α
h : a * c = b
⊢ a * c = b
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a b : α
h : a ∣ b
c : α
⊢ a ∣ b * c

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : CommSemigroup α
a b : α
h : a ∣ b
c : α
⊢ a ∣ b * c
Module: Mathlib.Algebra.Group.Semiconj.Units

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
u : Mˣ
x : M
⊢ ↑u * x = ↑u * x * ↑u⁻¹ * ↑u

Tactic:
;

Goal state after:
M : Type u_1
inst✝ : Monoid M
u : Mˣ
x : M
⊢ ↑u * x = ↑u * x * ↑u⁻¹ * ↑u
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
x y : G₀
hxy : x * y ≠ 0
⊢ ↑(mk0 (x * y) hxy) = ↑(mk0 x ⋯ * mk0 y ⋯)

Tactic:
;

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
x y : G₀
hxy : x * y ≠ 0
⊢ ↑(mk0 (x * y) hxy) = ↑(mk0 x ⋯ * mk0 y ⋯)
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
⊢ a = 0 → a / a ≠ 1

Tactic:
;

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
⊢ a = 0 → a / a ≠ 1
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
ha : a ≠ 0
h : a = c * b⁻¹
⊢ b ≠ 0

Tactic:
;

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
ha : a ≠ 0
h : a = c * b⁻¹
⊢ b ≠ 0
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a c : G₀
ha : a ≠ 0
h : a = c * 0⁻¹
⊢ False

Tactic:
;

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a c : G₀
ha : a ≠ 0
h : a = c * 0⁻¹
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
h : b = a⁻¹ * c
⊢ a ≠ 0

Tactic:
;

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hb : b ≠ 0
h : b = a⁻¹ * c
⊢ a ≠ 0
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
b c : G₀
hb : b ≠ 0
h : b = 0⁻¹ * c
⊢ False

Tactic:
;

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
b c : G₀
hb : b ≠ 0
h : b = 0⁻¹ * c
⊢ False
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
a✝ : ℕ
⊢ a ≠ 0 → a ^ a✝ ≠ 0

Tactic:
;

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
a✝ : ℕ
⊢ a ≠ 0 → a ^ a✝ ≠ 0
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
n : ℕ
ha : a ≠ 0
⊢ (a ^ (n + 1))⁻¹ ≠ 0

Tactic:
;

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
n : ℕ
ha : a ≠ 0
⊢ (a ^ (n + 1))⁻¹ ≠ 0
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
ha : a ≠ 0
⊢ (a ^ n)⁻¹ * a ^ n = 1

Tactic:
;

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a : G₀
n : ℤ
ha : a ≠ 0
⊢ (a ^ n)⁻¹ * a ^ n = 1
Module: Mathlib.Data.Nat.Cast.Commute

Goal state before:
pp: case zero
α : Type u_1
inst✝ : NonAssocSemiring α
x : α
⊢ Commute 0 x

Tactic:
;

Goal state after:
case zero
α : Type u_1
inst✝ : NonAssocSemiring α
x : α
⊢ Commute 0 x
Module: Mathlib.Data.Nat.Cast.Commute

Goal state before:
pp: case succ
α : Type u_1
inst✝ : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n) x
⊢ Commute (↑n + 1) x

Tactic:
;

Goal state after:
case succ
α : Type u_1
inst✝ : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n) x
⊢ Commute (↑n + 1) x
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
⊢ (-1) ^ (n % 2) * ((-1) ^ 2) ^ (n / 2) = (-1) ^ ((n % 2 + 2 * (n / 2)) % 2)

Tactic:
;

Goal state after:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ (-1) ^ (n % 2) * ((-1) ^ 2) ^ (n / 2) = (-1) ^ ((n % 2 + 2 * (n / 2)) % 2)
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
⊢ 0 • a = 0

Tactic:
;

Goal state after:
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
⊢ 0 • a = 0