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

Goal state before:
pp: b : Bool
x n : Nat
⊢ bit b x < 2 ^ (n + 1) ↔ x < 2 ^ n

Tactic:
by
  cases b <;> simp <;> lia

Goal state after:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
⊢ bitCasesOn (bit b n) h = h b n

Tactic:
change congrArg motive (bit b n).bit_testBit_zero_shiftRight_one ▸ h _ _ = h b n
  generalize congrArg motive (bit b n).bit_testBit_zero_shiftRight_one = e; revert e
  rw [testBit_bit_zero, bit_shiftRight_one]
  intros; rfl

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

Goal state before:
pp: case zero
M : Type u_2
inst✝ : Monoid M
a x y : M
h : SemiconjBy a x y
⊢ SemiconjBy a (x ^ 0) (y ^ 0)

Tactic:
rw [pow_zero, pow_zero]
    exact SemiconjBy.one_right _

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
h : Commute a b
⊢ a * (b * a⁻¹) = b

Tactic:
rw [← mul_assoc, h.mul_inv_cancel]

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

Goal state before:
pp: M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k✝ : ℕ
m : M
k : ℕ
⊢ npowRec (k + 1) m = 1 * npowRec' (k + 1) m

Tactic:
npowRec_eq

Goal state after:
M : Type u_2
x✝¹ : Semigroup M
x✝ : One M
k✝ : ℕ
m : M
k : ℕ
⊢ 1 * npowRec' (k + 1) m = 1 * npowRec' (k + 1) m
Module: Mathlib.Logic.Basic

Goal state before:
pp: ι₁ : Sort u_3
ι₂ : Sort u_4
κ₁ : ι₁ → Sort u_5
κ₂ : ι₂ → Sort u_6
p : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → Prop
⊢ (∃ i₁ j₁ i₂ j₂, p i₁ j₁ i₂ j₂) ↔ ∃ i₂ j₂ i₁ j₁, p i₁ j₁ i₂ j₂

Tactic:
by
  simp only [@exists_comm (κ₁ _), @exists_comm ι₁]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
simp [hp, hq]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : ¬Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
simp [hp, hq]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
simp [hp, hq]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : ¬Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
simp [hp, hq]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
simp [hp, hq]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : ¬Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
simp [hp, hq]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
simp [hp, hq]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : ¬Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
simp [hp, hq]

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
a₂' : α'
⊢ curry (update f (a₂, a₂') b) a a' =
    update (curry f) (a₂, a₂').fst (update (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'

Tactic:
obtain rfl | ha := eq_or_ne a a₂

Goal state after:
case inl
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' a₂' : α'
⊢ curry (update f (a, a₂') b) a a' = update (curry f) (a, a₂').fst (update (curry f (a, a₂').fst) (a, a₂').snd b) a a'

case inr
α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
a : α
a' : α'
a₂ : α
a₂' : α'
ha : a ≠ a₂
⊢ curry (update f (a₂, a₂') b) a a' =
    update (curry f) (a₂, a₂').fst (update (curry f (a₂, a₂').fst) (a₂, a₂').snd b) a a'
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
inst✝¹ : DecidableEq α
inst✝ : DecidableEq α'
f : α × α' → β
aa' : α × α'
b : β
⊢ curry (update f aa' b) = update (curry f) aa'.fst (update (curry f aa'.fst) aa'.snd b)

Tactic:
ext a a'
  let ⟨a₂, a₂'⟩ := aa'
  obtain rfl | ha := eq_or_ne a a₂ <;> obtain rfl | ha' := eq_or_ne a' a₂' <;> simp [*]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝² : Monoid M
inst✝¹ : MulAction M α
a : M
inst✝ : SMul M β
f : α → β
hf : Surjective f
smul : ∀ (c : M) (x : α), f (c • x) = c • f x
⊢ ∀ (b : β), 1 • b = b

Tactic:
simp [hf.forall, ← smul]

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

Goal state before:
pp: M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul P Q
inst✝⁵ : Monoid N
inst✝⁴ : MulAction N P
inst✝³ : MulAction N Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M N Q
inst✝ : IsScalarTower M P Q
h : Surjective fun m ↦ m • 1
p : P
q : Q
m : M
⊢ ((fun m ↦ m • 1) m • p) • q = (fun m ↦ m • 1) m • p • q

Tactic:
simp_rw [smul_one_smul, smul_assoc]

Goal state after:
Module: Mathlib.Logic.IsEmpty.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
⊢ IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β

Tactic:
rw [isEmpty_pi, ← exists_true_iff_nonempty, ← exists_and_right, true_and]

Goal state after:
Module: Mathlib.Data.Bool.Basic

Goal state before:
pp: case isTrue
n m : Nat
h : n ≤ m
hn : n = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)

Tactic:
| isTrue hn =>

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: m n : ℕ
⊢ ¬2 * n % 2 = (2 * m + 1) % 2

Tactic:
rw [Nat.add_comm, add_mul_mod_self_left, mul_mod_right, mod_eq_of_lt] <;> simp

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

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : p y
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

Tactic:
have hx : p x := hp h hy

Goal state after:
case pos
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : p y
hx : p x
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
hab : a < a + ↑n.succ
⊢ r (f a) (f (a + ↑n.succ))

Tactic:
clear hab

Goal state after:
β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a : ℤ
n : ℕ
⊢ r (f a) (f (a + ↑n.succ))
Module: Mathlib.Data.Set.Basic

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s ≠ univ ↔ ∃ a, ¬a ∈ s

Tactic:
rw [← not_forall, ← eq_univ_iff_forall]

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

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : BoundedOrder α
a b c : α
h : ¬b ≤ c
⊢ a ≤ c ↔ min a b ≤ c

Tactic:
· rw [inf_le_iff, or_iff_left h]

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ s \ t = tᶜ ∩ s

Tactic:
sdiff_eq,

Goal state after:
α : Type u_1
s t : Set α
⊢ s ∩ tᶜ = tᶜ ∩ s
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t u : Set α
⊢ (s ∩ t) \ u = s \ u ∩ t

Tactic:
sdiff_eq,

Goal state after:
α : Type u_1
s t u : Set α
⊢ s ∩ t ∩ uᶜ = s \ u ∩ t
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t u : Set α
⊢ s ∩ t ∩ uᶜ = s \ u ∩ t

Tactic:
sdiff_eq,

Goal state after:
α : Type u_1
s t u : Set α
⊢ s ∩ t ∩ uᶜ = s ∩ uᶜ ∩ t
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊔ x \ y) ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)

Tactic:
sup_sdiff_left,

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x \ y)) = x ⊓ (y \ z ⊔ (x ⊓ z ⊔ x ⊓ y) ⊔ x \ y)
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ b ⊔ a \ b = a

Tactic:
sdiff_eq,

Goal state after:
α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ b ⊔ a ⊓ bᶜ = a
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ b ⊓ a \ b = ⊥

Tactic:
sdiff_eq,

Goal state after:
α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ b ⊓ (a ⊓ bᶜ) = ⊥
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a : α
⊢ ⊤ \ a = aᶜ

Tactic:
sdiff_eq,

Goal state after:
α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a : α
⊢ ⊤ ⊓ aᶜ = aᶜ
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
h : x = yᶜ
⊢ IsCompl yᶜ y

Tactic:
exact isCompl_compl.symm

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

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x \ yᶜ = x ⊓ y

Tactic:
sdiff_eq,

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ x ⊓ yᶜᶜ = x ⊓ y
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ (x \ y)ᶜ = x ⇨ y

Tactic:
sdiff_eq,

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ (x ⊓ yᶜ)ᶜ = x ⇨ y
Module: Mathlib.Order.BooleanAlgebra.Basic

Goal state before:
pp: α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ xᶜ ⊓ y = y \ x

Tactic:
sdiff_eq,

Goal state after:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ xᶜ ⊓ y = y ⊓ xᶜ
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ (a ⊔ b) \ (a ⊓ b) = (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ)

Tactic:
sdiff_eq,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ (a ⊔ b) ⊓ (a ⊓ b)ᶜ = (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ)
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a \ b ⊔ b \ a = a ∆ b

Tactic:
sdiff_eq,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⊓ bᶜ ⊔ b ⊓ aᶜ = a ∆ b
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
x✝ : α × β
⊢ x✝ ∈ s ×ˢ ∅ ↔ x✝ ∈ ∅

Tactic:
exact iff_of_eq (and_false _)

Goal state after:
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' (s \ f ⁻¹' t) = f '' s \ t

Tactic:
sdiff_eq,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' (s ∩ (f ⁻¹' t)ᶜ) = f '' s ∩ tᶜ
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
x : α
⊢ MapsTo f (Insert.insert x s) (Insert.insert (f x) t)

Tactic:
simpa [← singleton_union] using h.mono_right subset_union_right

Goal state after:
Module: Mathlib.Data.Set.Function

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
h3 : SurjOn f s t
⊢ MapsTo g (p₁ '' s) (p₂ '' t)

Tactic:
rintro _ ⟨a, ha, rfl⟩
    exact ⟨f a, h1 ha, by rw [comm a]⟩

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

Goal state before:
pp: m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
⊢ Int.leInduction base succ m ⋯ = base

Tactic:
rw [Int.leInduction, inductionOn'_self]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H : Type u_6
F : Type u_7
inst✝¹ : Mul M
inst✝ : CommSemigroup N
f g : M →ₙ* N
x y : M
⊢ f (x * y) * g (x * y) = f x * g x * (f y * g y)

Tactic:
show f (x * y) * g (x * y) = f x * g x * (f y * g y)
        rw [f.map_mul, g.map_mul, ← mul_assoc, ← mul_assoc, mul_right_comm (f x)]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
G : Type u_5
H✝ : Type u_6
F : Type u_7
inst✝¹ : Group G
H : Type u_8
inst✝ : Group H
f : G → H
map_div : ∀ (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
x y : G
⊢ f x * (f 1 * (f 1)⁻¹ * (f y)⁻¹)⁻¹ = f x * f y

Tactic:
simp only [mul_inv_cancel, one_mul, inv_inv]

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a b : G
⊢ a * b * a⁻¹ = 1 ↔ b = 1

Tactic:
by
  rw [mul_inv_eq_one, mul_eq_left]

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

Goal state before:
pp: α : Type u
M : Type u_1
hM : Monoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ ↑⋯.unit⁻¹ * a = 1

Tactic:
rw [Units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one]

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

Goal state before:
pp: α : Type u
M : Type u_1
hM : CommMonoid M
h : ∀ (a : M), IsUnit a
a : M
⊢ ↑⋯.unit⁻¹ * a = 1

Tactic:
rw [Units.inv_mul_eq_iff_eq_mul, (h a).unit_spec, mul_one]

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

Goal state before:
pp: case zero
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
y : M₀
⊢ f (x ^ 0 * y) = f x ^ 0 * f y

Tactic:
rw [pow_zero, pow_zero, one_mul, one_mul]

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

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
a : Subtype p
h : ↑(x a) = ↑(y a)
⊢ x a = y a

Tactic:
SetCoe.ext_iff

Goal state after:
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
x y : Perm (Subtype p)
a : Subtype p
h : x a = y a
⊢ x a = y a
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b x a : G₀
⊢ a⁻¹⁻¹ = a

Tactic:
by
    by_cases h : a = 0
    · simp [h]
    · exact left_inv_eq_right_inv (inv_mul_cancel₀ <| inv_ne_zero h) (inv_mul_cancel₀ h)

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✝³ : Zero A
inst✝² : SMulZeroClass M A
inst✝¹ : Zero B
inst✝ : SMul M B
f : ZeroHom A B
smul : ∀ (c : M) (x : A), f (c • x) = c • f x
c : M
⊢ c • 0 = 0

Tactic:
by rw [← map_zero f, ← smul, smul_zero]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
⊢ 0 ^ n = if n = 0 then 1 else 0

Tactic:
by
  split_ifs with h
  · rw [h, zpow_zero]
  · rw [zero_zpow _ h]

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

Goal state before:
pp: x✝¹ : ℕ
x✝ : ℤ
⊢ x✝ ^ (x✝¹ + 1) = x✝ ^ x✝¹ * x✝

Tactic:
by simp [Int.pow_succ]

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

Goal state before:
pp: x✝¹ : ℕ
x✝ : ℤ
⊢ x✝ ^ (x✝¹ + 1) = x✝ ^ x✝¹ * x✝

Tactic:
by simp [Int.pow_succ]

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

Goal state before:
pp: case inl.succ
α : Type u_1
inst✝ : NonAssocRing α
m : ℕ
ih : ∀ (n : ℤ), ↑(↑m * n) = ↑↑m * ↑n
⊢ ∀ (n : ℤ), ↑(↑(m + 1) * n) = ↑↑(m + 1) * ↑n

Tactic:
simp_all [add_mul]

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

Goal state before:
pp: case inr.succ
α : Type u_1
inst✝ : NonAssocRing α
m : ℕ
ih : ∀ (n : ℤ), ↑(-↑m * n) = ↑(-↑m) * ↑n
⊢ ∀ (n : ℤ), ↑(-↑(m + 1) * n) = ↑(-↑(m + 1)) * ↑n

Tactic:
simp_all [add_mul]

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

Tactic:
simp [even_iff, h₁, h₂, Nat.mul_mod]

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

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

Tactic:
simp [even_iff, h₁, h₂, Nat.mul_mod]

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

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

Tactic:
simp [even_iff, h₁, h₂, Nat.mul_mod]

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

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

Tactic:
simp [even_iff, h₁, h₂, Nat.mul_mod]

Goal state after:
Module: Mathlib.Algebra.Group.Commute.Units

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
n : ℕ
a✝ b✝ : M
u✝ u₁ u₂ u : Mˣ
a b : M
hu : a * b = ↑u
hc : Commute a b
⊢ a * (b * ↑u⁻¹) = 1

Tactic:
rw [← mul_assoc, hu, u.mul_inv]

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
a b : R
⊢ (a - b) ^ 2 = (b - a) ^ 2

Tactic:
rw [sub_sq', mul_right_comm, add_comm, sub_sq']

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

Goal state before:
pp: R : Type u_1
S : Type u_2
f : S → R
hf : Injective f
inst✝⁴ : Add S
inst✝³ : Mul S
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : LeftDistribClass R
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
x y z : S
⊢ f (x * (y + z)) = f (x * y + x * z)

Tactic:
by simp only [*, left_distrib]

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

Goal state before:
pp: R : Type u_4
inst✝ : AddMonoidWithOne R
n : ℕ
h : 2 = 0
⊢ (Even n → ↑n = 0) ∧ (Odd n → ↑n = 1)

Tactic:
induction n using Nat.twoStepInduction with
  | zero => simp
  | one => simp
  | more n _ _ => simpa [add_assoc, Nat.even_add_one, Nat.odd_add_one, h]

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ a + b ≤ a - c + (b + c)

Tactic:
rw [add_comm a, add_comm (a - c)]

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c : α
inst✝ : AddLeftMono α
⊢ b + a ≤ b + c + (a - c)
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ a + (b - d) - c ≤ a - c + (b - d)

Tactic:
rw [add_comm a, add_comm (a - c)]

Goal state after:
α : Type u_1
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : AddLeftMono α
⊢ b - d + a - c ≤ b - d + (a - c)
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝³ : MulZeroClass α
b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < 0 * b
⊢ 0 < 0 ∧ 0 < b ∨ 0 < 0 ∧ b < 0

pp: case inr.inr
α : Type u_1
inst✝³ : MulZeroClass α
a b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
· rw [zero_mul] at hab
    exact hab.false.elim

Goal state after:
case inr.inr
α : Type u_1
inst✝³ : MulZeroClass α
a b : α
inst✝² : LinearOrder α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
hab : 0 < a * b
ha : 0 < a
⊢ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u
β : Sort v
x✝¹ x✝ : α ≃ β
h : x✝¹.toEmbedding = x✝.toEmbedding
⊢ x✝¹ = x✝

Tactic:
DFunLike.ext'_iff

Goal state after:
α : Sort u
β : Sort v
x✝¹ x✝ : α ≃ β
h : ⇑x✝¹.toEmbedding = ⇑x✝.toEmbedding
⊢ ⇑x✝¹ = ⇑x✝
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁵ : Semiring R
inst✝⁴ : PartialOrder R
inst✝³ : ExistsAddOfLE R
inst✝² : MulPosStrictMono R
inst✝¹ : AddRightStrictMono R
inst✝ : AddRightReflectLT R
a b : R
ha : a < 0
hb : b < 0
⊢ 0 < a * b

Tactic:
simpa only [zero_mul] using mul_lt_mul_of_neg_right ha hb

Goal state after:
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: one : Type u_1
α : Type u_2
inst✝ : Unique one
f : one ↪ α
⊢ (fun a ↦ { toFun := fun x ↦ a, inj' := ⋯ }) ((fun f ↦ f default) f) = f

Tactic:
ext; simp [Unique.uniq]

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₀
hc : 0 < c
⊢ a ≤ b * c⁻¹ ↔ c * a ≤ b

Tactic:
by
  rw [le_mul_inv_iff₀ hc, mul_comm]

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

Goal state before:
pp: case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc r a → Acc (Quotient.lift₂ r H) ⟦a⟧

Tactic:
intro ac
    induction ac with | intro _ _ IH => ?_
    refine ⟨_, fun q h => ?_⟩
    obtain ⟨a', rfl⟩ := q.exists_rep
    exact IH a' h

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

Goal state before:
pp: case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ab : b ≤ a
⊢ |a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1

Tactic:
· simpa only [mul_comm, and_comm] using mabs_mul_eq_mul_mabs_le ab

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

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

Tactic:
simpa using LinearOrderedAddCommMonoidWithTop.isAddLeftRegular_of_ne_top ha

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

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

Tactic:
cases n <;> simp [log_pow, log_inv]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : IsOrderedRing α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : AddLeftReflectLE α
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n

Tactic:
· rcases le_iff_exists_add'.mp h with ⟨m, rfl⟩
    rw [add_tsub_cancel_right, cast_add, add_tsub_cancel_right]

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

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℤ
h : a < 0
⊢ ↑a ≤ -1

Tactic:
by
  rw [← Int.cast_one, ← Int.cast_neg, cast_le]
  exact Int.le_sub_one_of_lt h

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : WithBot α
⊢ x = ⊥ ↔ ∀ (b : α), x < ↑b

Tactic:
by
  cases x <;> simp; simpa using ⟨_, lt_irrefl _⟩

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

Goal state before:
pp: α : Type u_2
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
z : ℤ
a : α
⊢ z ≤ ⌈a⌉ ↔ ↑z - 1 < a

Tactic:
rw [← sub_one_lt_iff, lt_ceil]; norm_cast

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
a : R
inst✝ : IsStrictOrderedRing R
⊢ 0 < ⌊a⌋₊ ↔ 1 ≤ a

Tactic:
rw [Nat.lt_iff_add_one_le, zero_add, le_floor_iff' Nat.one_ne_zero, cast_one]

Goal state after: