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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
m : ℕ
⊢ a ^ (m * 0) = (a ^ m) ^ 0

Tactic:
Nat.mul_zero,

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
m : ℕ
⊢ a ^ 0 = (a ^ m) ^ 0
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
I : Injective (f ∘ g)
hg : Surjective g
y : α
x : γ
h : f (g x) = f y
⊢ g x = y

Tactic:
obtain ⟨y, rfl⟩ := hg y

Goal state after:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : γ → α
I : Injective (f ∘ g)
hg : Surjective g
x y : γ
h : f (g x) = f (g y)
⊢ g x = g y
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refine_1
α : Sort u_1
β : Sort u_2
r : α → β → Prop
h : ∀ (a : α), ∃! b, r a b
⊢ ∃ f, ∀ {a : α} {b : β}, r a b ↔ f a = b

Tactic:
refine ⟨fun a ↦ (h a).choose, fun hr ↦ ?_, fun h' ↦ h' ▸ ?_⟩
    exacts [((h _).choose_spec.2 _ hr).symm, (h _).choose_spec.1]

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → β → Prop
p : β → γ → Prop
q : γ → δ → Prop
⊢ (r ∘r p) ∘r q = r ∘r p ∘r q

Tactic:
by
  funext a d
  apply propext
  constructor
  · exact fun ⟨c, ⟨b, hab, hbc⟩, hcd⟩ ↦ ⟨b, hab, c, hbc, hcd⟩
  · exact fun ⟨b, hab, c, hbc, hcd⟩ ↦ ⟨c, ⟨b, hab, hbc⟩, hcd⟩

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_1
α : Type u_1
r : α → α → Prop
x y : α
h : TransGen (ReflGen r) x y
⊢ ReflTransGen r x y

Tactic:
simpa [reflTransGen_eq_self] using h.mono reflGen_le_reflTransGen x y |>.to_reflTransGen

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

Goal state before:
pp: case refine_1
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
x✝ : FaithfulSMul R A
r₁ r₂ : R
hr : r₁ • 1 = r₂ • 1
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
⊢ r₁ • (1 * a) = r₂ • (1 * a)

Tactic:
← smul_mul_assoc,

Goal state after:
case refine_1
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
x✝ : FaithfulSMul R A
r₁ r₂ : R
hr : r₁ • 1 = r₂ • 1
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
⊢ r₁ • 1 * a = r₂ • (1 * a)
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: case refine_1
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
x✝ : FaithfulSMul R A
r₁ r₂ : R
hr : r₁ • 1 = r₂ • 1
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
⊢ r₁ • 1 * a = r₂ • (1 * a)

Tactic:
← smul_mul_assoc,

Goal state after:
case refine_1
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
x✝ : FaithfulSMul R A
r₁ r₂ : R
hr : r₁ • 1 = r₂ • 1
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
⊢ r₁ • 1 * a = r₂ • 1 * a
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✝
R : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
r : R
s x : M
⊢ r • 1 • s • x = s • r • x

Tactic:
← smul_assoc,

Goal state after:
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✝
R : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
r : R
s x : M
⊢ (r • 1) • s • x = s • r • x
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: A : Type u_9
B : Type u_10
G : Type u_11
inst✝⁴ : CommMonoid G
inst✝³ : SMul A G
inst✝² : SMul B G
inst✝¹ : IsScalarTower A G G
inst✝ : IsScalarTower B G G
r : A
s : B
x : G
⊢ r • 1 • s • x = s • r • x

Tactic:
← smul_assoc,

Goal state after:
A : Type u_9
B : Type u_10
G : Type u_11
inst✝⁴ : CommMonoid G
inst✝³ : SMul A G
inst✝² : SMul B G
inst✝¹ : IsScalarTower A G G
inst✝ : IsScalarTower B G G
r : A
s : B
x : G
⊢ (r • 1) • s • x = s • r • x
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Irrefl r
inst✝ : Std.Irrefl s
⊢ ∀ (a : α × β), ¬Prod.Lex r s a a

Tactic:
by rintro ⟨i, a⟩ (⟨_, _, h⟩ | ⟨_, h⟩) <;> exact irrefl _ h

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
motive : α → Prop
ha : a ≤ b → motive a
hb : b ≤ a → motive b
⊢ motive (min a b)

Tactic:
by
  rw [min_def]; split_ifs with h
  exacts [ha h, hb (le_of_not_ge h)]

Goal state after:
Module: Mathlib.Tactic.CongrExclamation

Goal state before:
pp: α : Sort u_1
x y : α
p : x ≍ y → Prop
h : ∀ (he : x = y), p ⋯
he : x ≍ y
⊢ p he

Tactic:
cases he

Goal state after:
case refl
α : Sort u_1
x : α
p : x ≍ x → Prop
h : ∀ (he : x = x), p ⋯
⊢ p ⋯
Module: Mathlib.Tactic.CongrExclamation

Goal state before:
pp: x y : Prop
p : x = y → Prop
h : ∀ (he : x ↔ y), p ⋯
he : x = y
⊢ p he

Tactic:
cases he

Goal state after:
case refl
x : Prop
p : x = x → Prop
h : ∀ (he : x ↔ x), p ⋯
⊢ p ⋯
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
b : β
x : α × β
⊢ x.swap < (b, a) ↔ x < (a, b)

Tactic:
by rw [← swap_lt_swap]; simp

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

Goal state before:
pp: case false
b₁ : Bool
h : false ≤ b₁
⊢ false.toNat ≤ b₁.toNat

Tactic:
cases b₁

Goal state after:
case false.false
h : false ≤ false
⊢ false.toNat ≤ false.toNat

case false.true
h : false ≤ true
⊢ false.toNat ≤ true.toNat
Module: Mathlib.Data.Bool.Basic

Goal state before:
pp: case true
b₁ : Bool
h : true ≤ b₁
⊢ true.toNat ≤ b₁.toNat

Tactic:
cases b₁

Goal state after:
case true.false
h : true ≤ false
⊢ true.toNat ≤ false.toNat

case true.true
h : true ≤ true
⊢ true.toNat ≤ true.toNat
Module: Mathlib.Order.RelClasses

Goal state before:
pp: case ind.ind.inr
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
a : α
iha : ∀ (y : α), y < a → ∀ (a' : α), a' ≤ y → ∀ (b : β), Acc (fun x1 x2 ↦ x1 < x2) (a', b)
b : β
ihb : ∀ (y : β), y < b → ∀ (a' : α), a' ≤ a → Acc (fun x1 x2 ↦ x1 < x2) (a', y)
a' : α
ha : a' ≤ a
x : α × β
hx : x < (a', b)
ha' : x.fst ≤ (a', b).fst
hb : x.snd < (a', b).snd
⊢ Acc (fun x1 x2 ↦ x1 < x2) x

Tactic:
· exact ihb x.2 hb x.1 (ha'.trans ha)

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
simp_rw [not_monotone_not_antitone_iff_exists_le_le, ← and_assoc]

Goal state after:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ (∃ a b c, (a ≤ b ∧ b ≤ c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) ↔
    ∃ a b c, (a < b ∧ b < c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: case refine_1
α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
h : Monotone fun n ↦ f (n + k)
x : ℕ
hx : x ∈ {x | k ≤ x}
y : ℕ
hy : y ∈ {x | k ≤ x}
hle : x - k ≤ y - k
⊢ f (x - k + k) ≤ f (y - k + k)

Tactic:
exact h hle

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

Goal state before:
pp: α : Type u
s t : Set α
⊢ s ⊆ t ↔ ∀ ⦃a : α⦄, ¬a ∈ t → ¬a ∈ s

Tactic:
by
  simp only [subset_def, not_imp_not]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : DistribLattice α
x y z : α
h₁ : x ⊓ z ≤ y ⊓ z
h₂ : x ⊔ z ≤ y ⊔ z
⊢ (y ⊔ x) ⊓ (y ⊔ z) = y ⊔ x ⊓ z

Tactic:
← sup_inf_left

Goal state after:
α : Type u
inst✝ : DistribLattice α
x y z : α
h₁ : x ⊓ z ≤ y ⊓ z
h₂ : x ⊔ z ≤ y ⊔ z
⊢ y ⊔ x ⊓ z = y ⊔ x ⊓ z
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊔ b ⇨ a = b ⇨ a

Tactic:
sup_himp_distrib,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ (a ⇨ a) ⊓ (b ⇨ a) = b ⇨ a
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ⊔ b ⇨ b = a ⇨ b

Tactic:
sup_himp_distrib,

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ (a ⇨ b) ⊓ (b ⇨ b) = a ⇨ b
Module: Mathlib.Logic.Equiv.Option

Goal state before:
pp: case none.some
α : Type u_1
β : Type u_2
e : Option α ≃ Option β
x : α
h1 : e.symm (some (e.removeNoneAux x)) = none
val✝ : β
h2 : e (some x) = some val✝
⊢ some (e.symm.removeNoneAux (e.removeNoneAux x)) = some x

Tactic:
rw [removeNoneAux_some _ ⟨_, h2⟩] at h1
        simp at h1

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

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

Tactic:
inter_right_comm

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

Goal state before:
pp: case none
α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.12
p : Option α → Type v
h : ∀ (a : p none), False
n : p none
⊢ False

Tactic:
exact h n

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
rw [symmDiff, sdiff_idem]
  exact
    le_antisymm (sup_le_sup sdiff_le sdiff_le)
      (sup_le le_sdiff_sup <| le_sdiff_sup.trans <| sup_le le_sup_right le_sdiff_sup)

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

Goal state before:
pp: α : Sort u_11
α' : Sort u_12
β : Sort u_13
β' : Sort u_14
ε₁ : α ≃ α'
ε₂ : β' ≃ β
f : α → β
f' : α' → β'
⊢ ⇑ε₂.symm ∘ f ∘ ⇑ε₁.symm = f' ↔ f = ⇑ε₂ ∘ f' ∘ ⇑ε₁

Tactic:
by
  rw [Equiv.symm_comp_eq, Equiv.comp_symm_eq, Function.comp_assoc]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
compl_symmDiff,

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
⊢ a ⊓ b ⇔ c ⊔ b ∆ c ⊓ aᶜ = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
Module: Mathlib.Data.Set.Image

Goal state before:
pp: case succ
α : Type u_1
f : α → α
n : ℕ
ih : preimage f^[n] = (preimage f)^[n]
⊢ preimage f ∘ preimage f^[n] = preimage f ∘ (preimage f)^[n]

Tactic:
ih

Goal state after:
case succ
α : Type u_1
f : α → α
n : ℕ
ih : preimage f^[n] = (preimage f)^[n]
⊢ preimage f ∘ (preimage f)^[n] = preimage f ∘ (preimage f)^[n]
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
⊢ s.piecewise f₁ f₂ ≤ s.piecewise g₁ g₂

Tactic:
apply piecewise_le

Goal state after:
case h₁
α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
⊢ ∀ (i : α), i ∈ s → f₁ i ≤ s.piecewise g₁ g₂ i

case h₂
α : Type u_1
δ : α → Type u_8
inst✝¹ : (i : α) → Preorder (δ i)
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f₁ f₂ g₁ g₂ : (i : α) → δ i
h₁ : ∀ (i : α), i ∈ s → f₁ i ≤ g₁ i
h₂ : ∀ (i : α), ¬i ∈ s → f₂ i ≤ g₂ i
⊢ ∀ (i : α), ¬i ∈ s → f₂ i ≤ s.piecewise g₁ g₂ i
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ ∨ s₁ = ∅ ∨ t₁ = ∅ ↔ s₁ = ∅ ∨ t₁ = ∅

Tactic:
or_iff_right_iff_imp

Goal state after:
case inl
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ → s₁ = ∅ ∨ t₁ = ∅
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
⊢ range Sum.inl ⊓ range Sum.inr ⊆ ⊥

Tactic:
rintro y ⟨⟨x₁, rfl⟩, ⟨x₂, h⟩⟩

Goal state after:
α : Type u_1
β : Type u_2
x₁ : α
x₂ : β
h : Sum.inr x₂ = Sum.inl x₁
⊢ Sum.inl x₁ ∈ ⊥
Module: Mathlib.Data.Set.Image

Goal state before:
pp: α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ x = x'

Tactic:
rw [← singleton_eq_singleton_iff]

Goal state after:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ {x} = {x'}
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
inst✝ : DecidableEq ι
a : (i : ι) → α i
i : ι
b : α i
ha : a ∈ s.pi t
⊢ a ∈ (s \ {i}).pi t ∧ (i ∈ s → b ∈ t i) ↔ i ∈ s → b ∈ t i

Tactic:
and_iff_right

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
inst✝ : DecidableEq ι
a : (i : ι) → α i
i : ι
b : α i
ha : a ∈ s.pi t
⊢ i ∈ s → b ∈ t i ↔ i ∈ s → b ∈ t i

ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
inst✝ : DecidableEq ι
a : (i : ι) → α i
i : ι
b : α i
ha : a ∈ s.pi t
⊢ a ∈ (s \ {i}).pi t
Module: Mathlib.Data.Int.Init

Goal state before:
pp: case refine_1
a b c d m n✝ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
_n : ℤ
a✝ : m ≤ _n
⊢ ((k : ℤ) → k < _n → motive k) → (k : ℤ) → k < _n + 1 → motive k

Tactic:
ih

Goal state after:
case refine_1
a b c d m n✝ : ℤ
motive : ℤ → Sort u_1
lt : (n : ℤ) → n < m → motive n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → motive k) → motive n
n : ℤ
hnm : ¬n < m
_n : ℤ
a✝ : m ≤ _n
ih : (k : ℤ) → k < _n → motive k
⊢ (k : ℤ) → k < _n + 1 → motive k
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
a b : M
n : ℕ
h : a * b = 1
⊢ a ^ n.succ * b ^ n.succ = a ^ n * a * (b * b ^ n)

Tactic:
rw [pow_succ, pow_succ']

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

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
inst✝³ : Mul M₁
inst✝² : One M₁
inst✝¹ : Pow M₁ ℕ
inst✝ : Monoid M₂
f : M₁ → M₂
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : M₁), f (x * y) = f x * f y
npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n
x : M₁
⊢ f (x ^ 0) = f 1

Tactic:
by rw [npow, one, pow_zero]

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

Goal state before:
pp: α : Type u_1
inst✝ : MulOne α
⊢ IsDedekindFiniteMonoid αᵐᵒᵖ ↔ IsDedekindFiniteMonoid α

Tactic:
simp_rw [isDedekindFiniteMonoid_iff, ← opEquiv.forall_congr_right]
  simpa [← op_one, ← op_mul] using forall_comm

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℤ
⊢ (a ^ m) ^ n = (a ^ n) ^ m

Tactic:
← zpow_mul,

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a : α
m n : ℤ
⊢ a ^ (m * n) = (a ^ n) ^ m
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ ↑u₁ * u₁.inv = 1

Tactic:
val_inv

Goal state after:
α : Type u
inst✝ : Monoid α
u₁ u₂ : αˣ
⊢ 1 = 1
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
u : αˣ
⊢ (↑u)⁻¹ * ↑u = 1

Tactic:
rw [← Units.val_inv_eq_inv_val, Units.inv_mul]

Goal state after:
Module: Mathlib.Control.Basic

Goal state before:
pp: m : Type u → Type v
h : Applicative m
inst✝ : CommApplicative m
α β γ : Type u
a : m α
b : m β
f : α → β → γ
⊢ f <$> a <*> b = (fun p ↦ f p.fst p.snd) <$> (Prod.mk <$> a <*> b)

Tactic:
simp only [map_seq, map_map, Function.comp_def]

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
f : G₀' → G₀
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀'), f (x * y) = f x * f y
inv : ∀ (x : G₀'), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀'), f (x / y) = f x / f y
npow : ∀ (x : G₀') (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀') (n : ℤ), f (x ^ n) = f x ^ n
⊢ f 0⁻¹ = f 0

Tactic:
rw [inv, zero, inv_zero]

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

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

Tactic:
by
  rw [mul_eq_left, swap_eq_one_iff]

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

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a / (a / a) = a

Tactic:
rw [div_div_eq_mul_div]
  exact mul_self_div_self a

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

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✝
⊢ ?succ.succ.n + 1 = n✝ + 1

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

case succ.succ.h
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 = ↑?succ.succ.n
Module: Mathlib.Data.Int.Cast.Basic

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

Tactic:
Int.neg_negSucc,

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
m n : ℕ
⊢ ↑(-[m+1] + -[n+1]) = ↑-[m+1] + ↑-[n+1]

Tactic:
Int.negSucc_add_negSucc,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑-[(m + n).succ+1] = ↑-[m+1] + ↑-[n+1]
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
⊢ Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) (k + 1) 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 ⋯) l hl =
    Int.strongRec lt ge l

pp: case refine_3
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 : ℤ
hkm : k ≤ m
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
x✝ : ∀ (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
⊢ Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) (k - 1) 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 ⋯) l hl =
    Int.strongRec lt ge l

Tactic:
· rw [inductionOn'_add_one hmk]; split_ifs with hlm
    · rw [strongRec_of_lt hlm]
    · rw [ih' fun l hl ↦ ih l (Int.lt_trans hl k.lt_succ), ih _ hl]

Goal state after:
case refine_3
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 : ℤ
hkm : k ≤ m
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
x✝ : ∀ (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
⊢ Int.inductionOn' (motive := fun x ↦ (k : ℤ) → k < x → P k) (k - 1) 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 ⋯) l hl =
    Int.strongRec lt ge l
Module: Mathlib.Data.Int.Basic

Goal state before:
pp: a : ℤ
h : 1 < a.natAbs
⊢ Function.Injective fun x ↦ a ^ x

Tactic:
refine (?_ : (natAbs ∘ (a ^ · : ℕ → ℤ)).Injective).of_comp
  convert! Nat.pow_right_injective h using 2
  rw [Function.comp_apply, natAbs_pow]

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

Goal state before:
pp: case succ
α : Type u
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = ↑n * a
⊢ (n + 1) • a = ↑(n + 1) * a

Tactic:
succ_nsmul,

Goal state after:
case succ
α : Type u
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = ↑n * a
⊢ n • a + a = ↑(n + 1) * a
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: m n : ℕ
hl : m * m < n
hr : n < (m + 1) * (m + 1)
⊢ ¬∃ t, t * t = n

Tactic:
rintro ⟨t, rfl⟩

Goal state after:
m t : ℕ
hl : m * m < t * t
hr : t * t < (m + 1) * (m + 1)
⊢ False
Module: Mathlib.Algebra.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b : α
m n : ℕ
hab : a ∣ b
hmn : m ≤ n
⊢ a ^ m ∣ b ^ n

Tactic:
by
  trans (a ^ n) <;> [gcongr; apply_rules [pow_dvd_pow_of_dvd]]

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
inst✝ : CommMonoid P
⊢ { toFun := comp 1, map_one' := ⋯, map_mul' := ⋯ } = 1

Tactic:
ext1 f
    exact one_comp f

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

Goal state before:
pp: α : Type u_3
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ (b - x) * (b - x) - (b * (b - x) - x * (b - x)) = 0

Tactic:
← sub_mul,

Goal state after:
α : Type u_3
inst✝ : NonUnitalCommRing α
b c x : α
h : x * x - b * x + c = 0
this : c = x * (b - x)
⊢ (b - x) * (b - x) - (b - x) * (b - x) = 0
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: case succ
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = a * ↑n
⊢ (n + 1) • a = a * ↑(n + 1)

Tactic:
succ_nsmul,

Goal state after:
case succ
α : Type u_1
inst✝ : NonAssocSemiring α
a : α
n : ℕ
ih : n • a = a * ↑n
⊢ n • a + a = a * ↑(n + 1)
Module: Mathlib.Algebra.GroupWithZero.Commute

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
r : M₀
⊢ r⁻¹ʳ ^ 0 = (r ^ 0)⁻¹ʳ

Tactic:
by rw [pow_zero, pow_zero, Ring.inverse_one]

Goal state after:
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:
exact inv_ne_zero (pow_ne_zero _ ha)

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
a : α
⊢ f (2 * a + 1) = 2 * f a + 1

Tactic:
simp [two_mul]

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

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

Tactic:
· use 1
    rwa [mul_one]

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

Tactic:
· rwa [le_inv_mul_iff₀ hc] at h

Goal state after: