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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
⊢ a ^ (n + 1 + 1) = a * a ^ (n + 1)

Tactic:
pow_succ _ n,

Goal state after:
M : Type u_2
inst✝ : Monoid M
a : M
n : ℕ
⊢ a ^ (n + 1 + 1) = a * (a ^ n * a)
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
a b : α
⊢ (a = b) = (b = a)

Tactic:
rw [@eq_comm _ a b]

Goal state after:
Module: Mathlib.Logic.Relation

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

Tactic:
simp_rw [reflTransGen_iff_eq_or_transGen, reflGen_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
ga ga' : α → α
gb gb' : β → β
h : Semiconj f ga gb
h' : Semiconj f ga' gb'
x : α
⊢ f ((ga ∘ ga') x) = (gb ∘ gb') (f x)

Tactic:
simp only [comp_apply, h.eq, h'.eq]

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

Goal state before:
pp: case zero
α : Type u
f : α → α
g : ℕ → α → α
H : ∀ (n : ℕ), Semiconj f (g n) (g (n + 1))
k : ℕ
⊢ Semiconj f^[0] (g k) (g (0 + k))

Tactic:
rw [Nat.zero_add]
    exact id_left

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

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
⊢ f^[m - n] a = a

Tactic:
by
  obtain h | h := Nat.le_total m n
  { simp [Nat.sub_eq_zero_of_le h] }
  { exact iterate_cancel_of_add hf (by rwa [Nat.sub_add_cancel h]) }

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
x : Option α
a : α
h : ∀ (a : α), a ∈ x → p a
ha : a ∈ x
⊢ f a ⋯ ∈ pmap f x h

Tactic:
by
  rw [mem_def] at ha ⊢
  subst ha
  rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ min a b ≤ a

Tactic:
rw [min_def]
  split_ifs with h <;> simp [h, le_of_not_ge]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : LE α
inst✝² : Top α
inst✝¹ : LE β
inst✝ : OrderTop β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_top : f ⊤ = ⊤
a : α
⊢ f a ≤ f ⊤

Tactic:
rw [map_top]

Goal state after:
α : Type u
β : Type v
inst✝³ : LE α
inst✝² : Top α
inst✝¹ : LE β
inst✝ : OrderTop β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_top : f ⊤ = ⊤
a : α
⊢ f a ≤ ⊤
Module: Mathlib.Data.Nat.Basic

Goal state before:
pp: x a : ℕ
hx : x ≠ 0
ha : a ≠ 0
⊢ x ^ (a - 1) = x ^ a / x

Tactic:
rw [← Nat.pow_div (one_le_iff_ne_zero.mpr ha) (Nat.pos_iff_ne_zero.mpr hx), Nat.pow_one]

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

Goal state before:
pp: case inr
k : ℕ
hk : k > 0
hk0 : 0 < 2 * k ^ 2
⊢ 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)

Tactic:
calc 2 * k ^ 2
      _ < 2 * k ^ 2 + 2 * k ^ 2 := Nat.lt_add_of_pos_left hk0
      _ = (2 * k) ^ 2 := by rw [Nat.mul_pow, ← Nat.add_mul]
      _ ≤ (2 ^ k) ^ 2 := Nat.pow_le_pow_left (Nat.mul_le_pow (by decide : 2 ≠ 1) _) 2
      _ = 2 ^ (2 * k) := (Nat.pow_mul' _ _ _).symm

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab : b < a
⊢ o.Compares a b

Tactic:
have hab : Compares Ordering.gt a b := hab

Goal state after:
case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
ho : o.Compares a' b'
hab✝ : b < a
hab : gt.Compares a b
⊢ o.Compares a b
Module: Mathlib.Data.Set.Disjoint

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

Tactic:
by rw [disjoint_comm, disjoint_left]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ b ⊔ c = a ⊔ c ⊔ b

Tactic:
rw [sup_assoc, sup_assoc, sup_comm b]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
b : α
⊢ b ⊔ b ⊓ (b ⊔ b) = b

Tactic:
by rw [sup_inf_self]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type u_1
inst✝¹ : Max α
inst✝ : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
b : α
⊢ b ⊓ b = b ⊓ (b ⊔ b ⊓ b)

Tactic:
by rw [sup_inf_self]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : Lattice α
a b : α
⊢ a ⊔ b = b ↔ a ⊓ b = a

Tactic:
sup_eq_right,

Goal state after:
α : Type u
inst✝ : Lattice α
a b : α
⊢ a ≤ b ↔ a ⊓ b = a
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : DistribLattice α
a b c : α
⊢ a ⊓ (a ⊓ b ⊔ c) = (a ⊔ a ⊓ b) ⊓ (a ⊓ b ⊔ c)

Tactic:
by rw [sup_inf_self]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
⊢ Lattice α

Tactic:
apply e.injective.lattice <;> intros

Goal state after:
case le
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
x✝ y✝ : α
⊢ e x✝ ≤ e y✝ ↔ x✝ ≤ y✝

case lt
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
x✝ y✝ : α
⊢ e x✝ < e y✝ ↔ x✝ < y✝

case map_sup
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
a✝ b✝ : α
⊢ e (a✝ ⊔ b✝) = e a✝ ⊔ e b✝

case map_inf
α : Type u
β : Type v
e : α ≃ β
inst✝ : Lattice β
semilatticeSup : SemilatticeSup α := e.semilatticeSup
semilatticeInf : SemilatticeInf α := e.semilatticeInf
a✝ b✝ : α
⊢ e (a✝ ⊓ b✝) = e a✝ ⊓ e b✝
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
⊢ ⊥ᶜ = ⊤

Tactic:
by rw [← himp_bot, himp_self]

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

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

Tactic:
by rw [sup_inf_self]

Goal state after:
Module: Mathlib.Order.SymmDiff

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

Tactic:
rw [symmDiff_def, sup_sdiff, sdiff_idem, sdiff_sdiff_self, bot_sup_eq]

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

Goal state before:
pp: α : Sort u_1
β : Sort u_4
W : α → Sort w
Z : β → Sort z
h₁ : α ≃ β
h₂ : (a : α) → W a ≃ Z (h₁ a)
f : (a : α) → W a
a : α
⊢ (h₁.piCongr h₂) f (h₁ a) = (h₂ a) (f a)

Tactic:
rw [piCongr, trans_apply, piCongrLeft_apply_apply, piCongrRight_apply, Pi.map_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
t : Set β
a : β
⊢ {a} ⊆ t ↔ a ∈ t

Tactic:
singleton_subset_iff

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
t : Set β
a : β
⊢ a ∈ t ↔ a ∈ t
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case inr.refine_1
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : Prod.fst '' s ×ˢ t ⊆ Prod.fst '' s₁ ×ˢ t₁
⊢ s ⊆ s₁

Tactic:
fst_image_prod _ st.2,

Goal state after:
case inr.refine_1
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
st : s.Nonempty ∧ t.Nonempty
H : s ×ˢ t ⊆ s₁ ×ˢ t₁
this : s ⊆ Prod.fst '' s₁ ×ˢ t₁
⊢ s ⊆ s₁
Module: Mathlib.Data.Set.Piecewise

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : (i : α) → Decidable (i ∈ sᶜ)
x : α
hx : x ∈ s
⊢ sᶜ.piecewise f g x = s.piecewise g f x

Tactic:
simp [hx]

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

Goal state before:
pp: α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝¹ : (j : α) → Decidable (j ∈ s)
inst✝ : (i : α) → Decidable (i ∈ sᶜ)
x : α
hx : ¬x ∈ s
⊢ sᶜ.piecewise f g x = s.piecewise g f x

Tactic:
simp [hx]

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

Goal state before:
pp: case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
h : (i : α) → δ i → δ' i
x : α
hx : x ∈ s
⊢ h x (s.piecewise f g x) = s.piecewise (fun x ↦ h x (f x)) (fun x ↦ h x (g x)) x

Tactic:
simp [hx]

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

Goal state before:
pp: case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
h : (i : α) → δ i → δ' i
x : α
hx : ¬x ∈ s
⊢ h x (s.piecewise f g x) = s.piecewise (fun x ↦ h x (f x)) (fun x ↦ h x (g x)) x

Tactic:
simp [hx]

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

Goal state before:
pp: case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
δ'' : α → Sort u_9
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
hx : x ∈ s
⊢ h x (s.piecewise f g x) (s.piecewise f' g' x) = s.piecewise (fun x ↦ h x (f x) (f' x)) (fun x ↦ h x (g x) (g' x)) x

Tactic:
simp [hx]

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

Goal state before:
pp: case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f g : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
δ' : α → Sort u_8
δ'' : α → Sort u_9
f' g' : (i : α) → δ' i
h : (i : α) → δ i → δ' i → δ'' i
x : α
hx : ¬x ∈ s
⊢ h x (s.piecewise f g x) (s.piecewise f' g' x) = s.piecewise (fun x ↦ h x (f x) (f' x)) (fun x ↦ h x (g x) (g' x)) x

Tactic:
simp [hx]

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

Goal state before:
pp: case pos
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
x : α
hx : x ∈ s
⊢ s.piecewise f f x = f x

Tactic:
simp [hx]

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

Goal state before:
pp: case neg
α : Type u_1
δ : α → Sort u_7
s : Set α
f : (i : α) → δ i
inst✝ : (j : α) → Decidable (j ∈ s)
x : α
hx : ¬x ∈ s
⊢ s.piecewise f f x = f x

Tactic:
simp [hx]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
b : β
⊢ (fun o ↦ o.elim b f) '' range some = range f

Tactic:
← range_comp'

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
b : β
⊢ (range fun x ↦ (some x).elim b f) = range f
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
x✝¹ x✝ : ↑s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h' : imageFactorization f s ⟨x, hx⟩ = imageFactorization f s ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
by simpa [imageFactorization, h.eq_iff hx hy] using h'

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
a : α
b : β
⊢ BijOn f {a} {b} ↔ f a = b

Tactic:
simp [BijOn, eq_comm]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ x ∈ insert a s

Tactic:
simp [hx]

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

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOne M
inst✝¹ : MulOne N
inst✝ : MulOne P
g : N →* P
f₁ f₂ : M →* N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ g (f₁ x) = g (f₂ x)

Tactic:
rw [← MonoidHom.comp_apply, h, MonoidHom.comp_apply]

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

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOne M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : N →* P
⊢ f.comp 1 = 1

Tactic:
ext
  simp only [map_one, coe_comp, Function.comp_apply, one_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ x ∈ s₁

Tactic:
rwa [← hf h]

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

Goal state before:
pp: F : Type u_7
G : Type u_8
H : Type u_9
inst✝³ : Group G
inst✝² : MulOneClass H
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : ∀ (a : G), f a = 1 → a = 1
x y : G
hxy : f x = f y
⊢ f x * f y⁻¹ = 1

Tactic:
hxy,

Goal state after:
F : Type u_7
G : Type u_8
H : Type u_9
inst✝³ : Group G
inst✝² : MulOneClass H
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
h : ∀ (a : G), f a = 1 → a = 1
x y : G
hxy : f x = f y
⊢ f y * f y⁻¹ = 1
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 * 1⁻¹ * y⁻¹))⁻¹ = f x * f y

Tactic:
simp only [map_div]

Goal state after:
α : 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
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: M : Type u_4
inst✝ : Monoid M
n : ℕ
a : M
⊢ (fun x ↦ x * a)^[n] 1 = a ^ n

Tactic:
simp [mul_right_iterate]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a⁻¹ * b = 1
⊢ a = b

Tactic:
by simpa using eq_inv_of_mul_eq_one_left h

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : a * b⁻¹ = 1
⊢ a = b

Tactic:
by simpa using eq_inv_of_mul_eq_one_left h

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

Goal state before:
pp: α : Type u_4
inst✝ : DecidableEq α
f : Perm α
x y : α
⊢ swap (f x) (f y) = f * swap x y * f⁻¹

Tactic:
rw [mul_swap_eq_swap_mul, mul_inv_cancel_right]

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

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑1 = 1

Tactic:
cast_succ,

Goal state after:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑0 + 1 = 1
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
m n : ℕ
ih : ↑(m + n) = ↑m + ↑n
⊢ ↑(m + n).succ = ↑m + ↑(n + 1)

Tactic:
cast_succ,

Goal state after:
case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
m n : ℕ
ih : ↑(m + n) = ↑m + ↑n
⊢ ↑(m + n) + 1 = ↑m + ↑(n + 1)
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
m n : ℕ
ih : ↑(m + n) = ↑m + ↑n
⊢ ↑m + ↑n + 1 = ↑m + ↑(n + 1)

Tactic:
cast_succ,

Goal state after:
case succ
R : Type u_1
inst✝ : AddMonoidWithOne R
m n : ℕ
ih : ↑(m + n) = ↑m + ↑n
⊢ ↑m + ↑n + 1 = ↑m + (↑n + 1)
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
⊢ a * a * a⁻¹ = a

Tactic:
by
  by_cases h : a = 0
  · rw [h, inv_zero, mul_zero]
  · rw [mul_assoc, mul_inv_cancel₀ h, mul_one]

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

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

Tactic:
simp [Int.pow_succ]

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

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.Data.Int.Cast.Basic

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

Tactic:
cast_succ,

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
n : ℕ
x✝ : 0 < n + 1
⊢ ↑(n + 1 - 1) = ↑n + 1 - 1
Module: Mathlib.Algebra.Ring.Int.Defs

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

Tactic:
simp [Int.pow_succ]

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

Tactic:
exact ⟨_, _, ‹_›⟩

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

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

Tactic:
exact ⟨_, _, ‹_›⟩

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

Tactic:
simp [hx]

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

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

Tactic:
simp [hx]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
f : R → S
hf : Surjective f
inst✝¹² : Add S
inst✝¹¹ : Mul S
inst✝¹⁰ : Zero S
inst✝⁹ : One S
inst✝⁸ : Neg S
inst✝⁷ : Sub S
inst✝⁶ : SMul ℕ S
inst✝⁵ : SMul ℤ S
inst✝⁴ : Pow S ℕ
inst✝³ : NatCast S
inst✝² : IntCast S
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
neg : ∀ (a : R), f (-a) = -f a
mul : ∀ (a b : R), f (a * b) = f a * f b
x y : R
⊢ f x * -f y = -(f x * f y)

Tactic:
rw [← neg, ← mul, mul_neg, neg, mul]

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

Goal state before:
pp: case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)
⊢ r (b * a * a⁻¹) c

Tactic:
← mul_inv_cancel_right c a

Goal state after:
case refine_1
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Covariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)
⊢ r (b * a * a⁻¹) (c * a * a⁻¹)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (b * a * a⁻¹) c
⊢ r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)

Tactic:
← mul_inv_cancel_right c a

Goal state after:
case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r (b * a * a⁻¹) (c * a * a⁻¹)
⊢ r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: case refine_2
N : Type u_2
r : N → N → Prop
inst✝ : Group N
h : Contravariant N N (swap fun x1 x2 ↦ x1 * x2) r
a b c : N
bc : r b c
⊢ r (swap (fun x1 x2 ↦ x1 * x2) a b) (swap (fun x1 x2 ↦ x1 * x2) a c)

Tactic:
rw [← mul_inv_cancel_right b a, ← mul_inv_cancel_right c a] at bc
    exact h a⁻¹ bc

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

Goal state before:
pp: case zero
α : Type u_2
inst✝ : Semiring α
a : α
ha : Odd a
⊢ Odd (a ^ 0)

Tactic:
simp [pow_zero]

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 d : α
inst✝ : AddLeftMono α
⊢ a + b ≤ d + (c + (a - c + (b - d)))

Tactic:
← tsub_le_iff_left,

Goal state after:
α : 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))
Module: Mathlib.Algebra.Order.Sub.Defs

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

Tactic:
← tsub_le_iff_left,

Goal state after:
case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - a ≤ c + (b - a - c)
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

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

Tactic:
inv_le_div_iff_le_mul,

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c : α
⊢ c ≤ b * a ↔ c ≤ a * b
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a

Tactic:
rw [mul_nonneg_iff]

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ 0 ≤ b * c ∨ 0 ≤ c * a
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 < a
n : ℕ
⊢ 0 < (a ^ ↑(n + 1))⁻¹

Tactic:
inv_pos,

Goal state after:
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : ZeroLEOneClass G₀
ha : 0 < a
n : ℕ
⊢ 0 < a ^ ↑(n + 1)
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ 0 ≤ b * c ∨ 0 ≤ c * a

Tactic:
rw [mul_nonneg_iff]

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c * a
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c * a

Tactic:
rw [mul_nonneg_iff]

Goal state after:
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : MulPosStrictMono R
inst✝² : PosMulStrictMono R
inst✝¹ : AddLeftMono R
inst✝ : AddLeftReflectLE R
a b c : R
⊢ (0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0) ∨ (0 ≤ b ∧ 0 ≤ c ∨ b ≤ 0 ∧ c ≤ 0) ∨ 0 ≤ c ∧ 0 ≤ a ∨ c ≤ 0 ∧ a ≤ 0
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
⊢ b * c⁻¹ < a ↔ b < c * a

Tactic:
by
  rw [mul_inv_lt_iff₀ hc, mul_comm]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
f : α ≃o β
x y : α
⊢ f (x ⊓ y) = f x ⊓ f y

Tactic:
refine (f.toOrderEmbedding.map_inf_le x y).antisymm ?_

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeInf α
inst✝ : SemilatticeInf β
f : α ≃o β
x y : α
⊢ f.toOrderEmbedding x ⊓ f.toOrderEmbedding y ≤ f.toOrderEmbedding (x ⊓ y)
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
a b : M
hab : a ≤ b
k : ℕ
⊢ a ^ k * a ≤ b ^ k * b

Tactic:
exact mul_le_mul' (pow_le_pow_left' hab k) hab

Goal state after: