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 n : ℕ
⊢ a ^ (m * n) = (a ^ n) ^ m

Tactic:
by rw [Nat.mul_comm, pow_mul]

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

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

Tactic:
by
  rw [mul_assoc, mul_inv_cancel, mul_one]

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

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a' : α
v v' : β a'
h : update f a' v = update f a' v'
this : v = update f a' v' a'
⊢ v = v'

Tactic:
update_self

Goal state after:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a' : α
v v' : β a'
h : update f a' v = update f a' v'
this : v = v'
⊢ v = v'
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (p a (update f a b a) ∧ ∀ (b_1 : α), b_1 ≠ a → p b_1 (update f a b b_1)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)

Tactic:
update_self

Goal state after:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (p a b ∧ ∀ (b_1 : α), b_1 ≠ a → p b_1 (update f a b b_1)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
n : ℕ
hn : 0 < n
⊢ f^[n.pred] ∘ f = f^[n]

Tactic:
rw [← iterate_succ, Nat.succ_pred_eq_of_pos hn]

Goal state after:
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.Trichotomous r
inst✝ : Std.Trichotomous s
⊢ ∀ {a b : α × β}, Prod.Lex r s a b ∨ a = b ∨ Prod.Lex r s b a

Tactic:
intro ⟨i, a⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Trichotomous s
i : α
a : β
⊢ ∀ {b : α × β}, Prod.Lex r s (i, a) b ∨ (i, a) = b ∨ Prod.Lex r s b (i, a)
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_1
inst✝ : LE α
⊢ (∀ (a : α), ∃ b, ¬a ≤ b) ↔ ∀ (x : α), ¬IsBot x

Tactic:
IsBot,

Goal state after:
α : Type u_1
inst✝ : LE α
⊢ (∀ (a : α), ∃ b, ¬a ≤ b) ↔ ∀ (x : α), ¬∀ (b : α), x ≤ b
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), le✝ a a
le_trans✝¹ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
A_iff : ∀ (a b : α), A_lt a b ↔ le✝ a b ∧ ¬le✝ b a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), le✝ a a
le_trans✝ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
B_iff : ∀ (a b : α), B_lt a b ↔ le✝ a b ∧ ¬le✝ b a
a b : α
⊢ A_lt a b = B_lt a b

Tactic:
A_iff,

Goal state after:
α : Type u_2
le✝ A_lt : α → α → Prop
le_refl✝¹ : ∀ (a : α), le✝ a a
le_trans✝¹ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
A_iff : ∀ (a b : α), A_lt a b ↔ le✝ a b ∧ ¬le✝ b a
B_lt : α → α → Prop
le_refl✝ : ∀ (a : α), le✝ a a
le_trans✝ : ∀ (a b c : α), le✝ a b → le✝ b c → le✝ a c
B_iff : ∀ (a b : α), B_lt a b ↔ le✝ a b ∧ ¬le✝ b a
a b : α
⊢ (le✝ a b ∧ ¬le✝ b a) = B_lt a b
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x < y ↔ x < y
⊢ A = B

Tactic:
by ext x y; rw [le_iff_lt_or_eq, @le_iff_lt_or_eq _ A, H]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb : c < b i
⊢ a i < update a i c i

Tactic:
update_self

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb : c < b i
⊢ a i < c
Module: Mathlib.Order.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb : c < b i
⊢ update a i c i < b i

Tactic:
update_self

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (π i)
inst✝ : ∀ (i : ι), DenselyOrdered (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
c : π i
ha : a i < c
hb : c < b i
⊢ c < b i
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : 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)

Tactic:
refine exists₃_congr (fun a b c ↦ and_congr_left <|
    fun h ↦ (Ne.le_iff_lt ?_).and <| Ne.le_iff_lt ?_)

Goal state after:
case refine_1
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
h : f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c
⊢ a ≠ b

case refine_2
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
h : f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c
⊢ b ≠ c
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: P : ℕ → Prop
h : ∀ (N : ℕ), ∃ n, n > N ∧ P n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
have : NoMaxOrder {n // P n} :=
    ⟨fun n ↦ Exists.intro ⟨(h n.1).choose, (h n.1).choose_spec.2⟩ (h n.1).choose_spec.1⟩
  obtain ⟨f, hf, _⟩ := Nat.exists_strictMono' (⟨(h 0).choose, (h 0).choose_spec.2⟩ : {n // P n})
  exact Exists.intro (fun n ↦ (f n).1) ⟨hf, fun n ↦ (f n).2⟩

Goal state after:
Module: Mathlib.Order.Lattice

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

Tactic:
rw [sup_comm]

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ ⊤ ⊓ a ≤ b ↔ a ≤ b

Tactic:
top_inf_eq

Goal state after:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ a ≤ b ↔ a ≤ b
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b : α
⊢ ⊤ ⊓ (b ⇨ a) = b ⇨ a

Tactic:
top_inf_eq

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d : α
a b c : αᵒᵈ
⊢ toDual (ofDual b ⇨ ofDual a) ≤ c ↔ a ≤ b ⊔ c

Tactic:
rw [sup_comm]

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d : α
a b c : αᵒᵈ
⊢ toDual (ofDual b ⇨ ofDual a) ≤ c ↔ a ≤ c ⊔ b
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ : α
a b c : αᵒᵈ
⊢ toDual (ofDual b ⇨ ofDual a) ≤ c ↔ a ≤ b ⊔ c

Tactic:
rw [sup_comm]

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : HeytingAlgebra α
a✝ b✝ : α
a b c : αᵒᵈ
⊢ toDual (ofDual b ⇨ ofDual a) ≤ c ↔ a ≤ c ⊔ b
Module: Mathlib.Order.BooleanAlgebra.Set

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

Tactic:
by
  rw [union_comm]
  exact sup_inf_sdiff _ _

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y \ x ≤ x ⊔ y \ x

Tactic:
rw [sup_sdiff_cancel_right hx]

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hz : z ≤ y
hx : x ≤ y
H : Disjoint z (y \ x)
⊢ z ⊔ y \ x ≤ y
Module: Mathlib.Order.BooleanAlgebra.Basic

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

Tactic:
top_inf_eq

Goal state after:
α : Type u
β : Type u_1
x y z : α
inst✝ : BooleanAlgebra α
a : α
⊢ aᶜ = aᶜ
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ (∀ ⦃a : α × β⦄, a ∈ s₁ ×ˢ t₁ → ¬a ∈ s₂ ×ˢ t₂) ↔ (∀ ⦃a : α⦄, a ∈ s₁ → ¬a ∈ s₂) ∨ ∀ ⦃a : β⦄, a ∈ t₁ → ¬a ∈ t₂

Tactic:
mem_prod,

Goal state after:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ (∀ ⦃a : α × β⦄, a.1 ∈ s₁ ∧ a.2 ∈ t₁ → ¬(a.1 ∈ s₂ ∧ a.2 ∈ t₂)) ↔
    (∀ ⦃a : α⦄, a ∈ s₁ → ¬a ∈ s₂) ∨ ∀ ⦃a : β⦄, a ∈ t₁ → ¬a ∈ t₂
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:
image_inter_preimage

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

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

Tactic:
simp only [not_nonempty_iff_eq_empty.symm, prod_nonempty_iff, not_and_or]

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
⊢ (∀ (x : α), x ∈ range f ↔ x ∈ {y}) ↔ ∀ (x : ι), f x = y

Tactic:
Set.mem_range,

Goal state after:
α : Type u_1
ι : Sort u_4
f : ι → α
inst✝ : Nonempty ι
y : α
⊢ (∀ (x : α), (∃ y, f y = x) ↔ x ∈ {y}) ↔ ∀ (x : ι), f x = y
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
inst✝ : ∀ (i : ι), Nonempty (α i)
⊢ Disjoint (s.pi t₁) (s.pi t₂) ↔ ∃ i, i ∈ s ∧ Disjoint (t₁ i) (t₂ i)

Tactic:
simp only [disjoint_iff_inter_eq_empty, ← pi_inter_distrib, pi_eq_empty_iff']

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
x✝ : a ∈ univ.pi t ∧ ∀ (x : (i : ι) → α i), x ∈ univ.pi t → x = a
i : ι
h₁ : a ∈ univ.pi t
h₂ : ∀ (x : (i : ι) → α i), x ∈ univ.pi t → x = a
x : α i
hx : x ∈ t i
⊢ x = update a i x i

Tactic:
update_self

Goal state after:
ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
a : (i : ι) → α i
x✝ : a ∈ univ.pi t ∧ ∀ (x : (i : ι) → α i), x ∈ univ.pi t → x = a
i : ι
h₁ : a ∈ univ.pi t
h₂ : ∀ (x : (i : ι) → α i), x ∈ univ.pi t → x = a
x : α i
hx : x ∈ t i
⊢ x = x
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul 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 [← MulHom.comp_apply, h, MulHom.comp_apply]

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 s t
⊢ BijOn f (insert a s) (insert (f a) t)

Tactic:
rw [insert_eq]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f s t
⊢ BijOn f ({a} ∪ s) (insert (f a) t)
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 s t
⊢ BijOn f ({a} ∪ s) (insert (f a) t)

Tactic:
rw [insert_eq]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f s t
⊢ BijOn f ({a} ∪ s) ({f a} ∪ t)
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 s t
⊢ BijOn f ({a} ∪ s) ({f a} ∪ t)

Tactic:
rw [insert_eq]

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f s t
⊢ BijOn f ({a} ∪ s) ({f a} ∪ t)
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 : x ∈ s
⊢ f' (f x) ∈ s₁

Tactic:
hf h

Goal state after:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h₁ : x ∈ s₁
h : x ∈ s
⊢ x ∈ s₁
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) ⋯
n : ℤ
hmn : m ≤ n
⊢ Int.inductionOn' (motive := fun x ↦ (hmn : m ≤ x) → motive x hmn) (n + 1) m (fun x ↦ base)
      (fun k hle ih x ↦ succ k hle (ih hle)) (fun x x_1 x_2 x_3 ↦ ⋯.elim) ⋯ =
    succ n hmn (Int.leInduction base succ n hmn)

Tactic:
inductionOn'_add_one hmn

Goal state after:
m : ℤ
motive : (n : ℤ) → m ≤ n → Sort u_1
base : motive m ⋯
succ : (n : ℤ) → (hmn : m ≤ n) → motive n hmn → motive (n + 1) ⋯
n : ℤ
hmn : m ≤ n
⊢ succ n hmn
      (Int.inductionOn' (motive := fun x ↦ (hmn : m ≤ x) → motive x hmn) n m (fun x ↦ base)
        (fun k hle ih x ↦ succ k hle (ih hle)) (fun x x_1 x_2 x_3 ↦ ⋯.elim) hmn) =
    succ n hmn (Int.leInduction base succ n hmn)
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r (f '' (s₁ ∩ f ⁻¹' t') \ t)
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'

Tactic:
image_inter_preimage

Goal state after:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ ∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
Module: Mathlib.Data.Set.Function

Goal state before:
pp: β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
⊢ t₁.Nonempty ∨ t₂ = ∅ → SurjOn Prod.snd (t₁ ×ˢ t₂) t₂

Tactic:
by simp +contextual [or_imp, prod_surjOn_snd]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ a * b * c = a * c * b

Tactic:
rw [mul_assoc, mul_comm b, mul_assoc]

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

Goal state before:
pp: case pred
G : Type u_3
inst✝ : Group G
a : G
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ (m + -↑n - 1)

Tactic:
Int.add_sub_assoc

Goal state after:
case pred
G : Type u_3
inst✝ : Group G
a : G
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ (m + (-↑n - 1))
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
⊢ f a c = f a b * f b c

Tactic:
← one_mul (f a c),

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab✝ : p a b✝
pbc✝ : p b✝ c✝
pac✝ : p a c✝
b c : α
rbc : r b c
pab : p a b
pbc : p b c
pac : p a c
rba : r b a
⊢ 1 * f a c = f a b * f b c
Module: Mathlib.Algebra.Group.Units.Defs

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : IsDedekindFiniteMonoid M
x y : M
hu : IsUnit (x * y)
z : M
hz : z * (x * y) = 1
⊢ z * x * y = 1

Tactic:
by rwa [mul_assoc]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a * (b / a) = b

Tactic:
by
  rw [mul_comm, h.div_mul_cancel]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoid R
inst✝ : One R
⊢ Nat.binCast 0 = 0

Tactic:
simp only [Nat.binCast]

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

Goal state before:
pp: case pred
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ (m + -↑n - 1)

Tactic:
Int.add_sub_assoc

Goal state after:
case pred
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
m : ℤ
n : ℕ
ihn : a ^ (m + -↑n) = a ^ m * a ^ (-↑n)
⊢ a ^ (m + (-↑n - 1)) = a ^ (m + (-↑n - 1))
Module: Mathlib.Data.Int.Basic

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

Tactic:
convert! Nat.pow_right_injective h using 2

Goal state after:
a : ℤ
h : 1 < a.natAbs
x✝ : ℕ
⊢ (natAbs ∘ fun x ↦ a ^ x) x✝ = a.natAbs ^ x✝
Module: Mathlib.Data.Nat.Sqrt

Goal state before:
pp: x : ℕ
⊢ (∃ n, n ^ 2 = x) ↔ x.sqrt ^ 2 = x

Tactic:
by
  simpa only [Nat.pow_two] using exists_mul_self x

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

Goal state before:
pp: A : Type u_2
F : Type u_4
inst✝² : FunLike F ℕ A
inst✝¹ : AddZeroClass A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : f 1 = g 1
⊢ ∀ (x : ℕ), f x = g x

Tactic:
intro n
    induction n with
    | zero => simp_rw [map_zero f, map_zero g]
    | succ n ihn =>
      simp [h, ihn]

Goal state after:
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: a b : Prop
l : List Prop
h : b ∈ l
⊢ (a ↔ b) ∧ l.TFAE → (a :: l).TFAE

Tactic:
rintro ⟨ab, H⟩ p (_ | ⟨_, hp⟩) q (_ | ⟨_, hq⟩)
        · rfl
        · exact ab.trans (H _ h _ hq)
        · exact (ab.trans (H _ h _ hp)).symm
        · exact H _ hp _ hq

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ -(b * (1 / a)) = -(b / a)

Tactic:
by rw [mul_one_div]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
x y : Mˣ
h : SemiconjBy a ↑x ↑y
⊢ ↑y⁻¹ * (↑y * a) * ↑x⁻¹ = ↑y⁻¹ * a

Tactic:
rw [← h.eq, mul_assoc, Units.mul_inv_cancel_right]

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
u : Mˣ
a : M
⊢ Commute (↑u) a ↔ ↑u⁻¹ * a * ↑u = a

Tactic:
rw [mul_assoc, Units.inv_mul_eq_iff_eq_mul, eq_comm, Commute, SemiconjBy]

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

Goal state before:
pp: α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ a /ₚ u - b = (a - b * ↑u) /ₚ u

Tactic:
simp only [divp, sub_mul, sub_right_inj]

Goal state after:
α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ b = b * ↑u * ↑u⁻¹
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = -1
⊢ -1 * -1 = 1

Tactic:
neg_one_mul,

Goal state after:
R : Type u
inst✝¹ : Monoid R
inst✝ : HasDistribNeg R
n : ℕ
h : (-1) ^ n = -1
⊢ - -1 = 1
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✝¹⁸ : 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✝
S : Type ?u.36
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Add S
inst✝⁶ : SMul ℕ S
inst✝⁵ : Neg S
inst✝⁴ : Sub S
inst✝³ : SMul ℤ S
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ ↑(Int.negSucc n) = -↑(n + 1)

Tactic:
Int.cast_negSucc

Goal state after:
R : Type u_1
S✝ : Type u_2
f✝ : S✝ → R
hf✝ : Injective 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✝
S : Type ?u.36
inst✝⁹ : Zero S
inst✝⁸ : One S
inst✝⁷ : Add S
inst✝⁶ : SMul ℕ S
inst✝⁵ : Neg S
inst✝⁴ : Sub S
inst✝³ : SMul ℤ S
inst✝² : NatCast S
inst✝¹ : IntCast S
inst✝ : AddGroupWithOne R
f : S → R
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
neg : ∀ (x : S), f (-x) = -f x
sub : ∀ (x y : S), f (x - y) = f x - f y
nsmul : ∀ (n : ℕ) (x : S), f (n • x) = n • f x
zsmul : ∀ (n : ℤ) (x : S), f (n • x) = n • f x
natCast : ∀ (n : ℕ), f ↑n = ↑n
intCast : ∀ (n : ℤ), f ↑n = ↑n
n : ℕ
⊢ -↑(n + 1) = -↑(n + 1)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case h
α : Type u_2
inst✝² : Add α
inst✝¹ : Mul α
inst✝ : LeftDistribClass α
b k : α
⊢ b * (k + k) = b * k + b * k

Tactic:
mul_add

Goal state after:
case h
α : Type u_2
inst✝² : Add α
inst✝¹ : Mul α
inst✝ : LeftDistribClass α
b k : α
⊢ b * k + b * k = b * k + b * k
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ ↑2 * (a * ↑2 * b + b + a) + 1 = ↑2 * (↑2 * a * b + b + a) + 1

Tactic:
← Nat.cast_comm

Goal state after:
α : Type u_2
inst✝ : Semiring α
a b : α
⊢ ↑2 * (↑2 * a * b + b + a) + 1 = ↑2 * (↑2 * a * b + b + a) + 1
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
n : ℤ
⊢ Even n → ∀ (a : α), (-a) ^ n = a ^ n

Tactic:
by
  rintro ⟨c, rfl⟩ a; simp_rw [← Int.two_mul, zpow_mul, zpow_two, neg_mul_neg]

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

Goal state before:
pp: α : Type u_1
inst✝³ : LE α
inst✝² : Mul α
inst✝¹ : IsMulCommutative α
inst✝ : MulLeftMono α
a b c : α
ha : MulLECancellable a
⊢ a * b ≤ c * a ↔ b ≤ c

Tactic:
mul_comm' c,

Goal state after:
α : Type u_1
inst✝³ : LE α
inst✝² : Mul α
inst✝¹ : IsMulCommutative α
inst✝ : MulLeftMono α
a b c : α
ha : MulLECancellable a
⊢ a * b ≤ a * c ↔ b ≤ c
Module: Mathlib.Algebra.Ring.GrindInstances

Goal state before:
pp: α : Type u_1
s : Semiring α
⊢ OfNat.ofNat (1 + 1) = OfNat.ofNat 1 + 1

Tactic:
change Nat.cast 2 = 1 + 1

Goal state after:
α : Type u_1
s : Semiring α
⊢ ↑2 = 1 + 1
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u
γ : Sort w
inst✝ : Inhabited γ
x✝¹ : α → γ
x✝ : α
⊢ (Embedding.refl α).arrowCongrLeft x✝¹ x✝ = (Embedding.refl (α → γ)) x✝¹ x✝

Tactic:
simp [coe_refl]

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

Goal state before:
pp: α₁ : Sort u
α₂ : Sort v
α₃ : Sort x
γ : Sort w
inst✝ : Inhabited γ
e₁₂ : α₁ ↪ α₂
e₂₃ : α₂ ↪ α₃
⊢ e₁₂.arrowCongrLeft.trans e₂₃.arrowCongrLeft = (e₁₂.trans e₂₃).arrowCongrLeft

Tactic:
by
  ext f a
  simp only [trans_apply, arrowCongrLeft_apply, Pi.default_def, coe_trans]
  rw [e₁₂.injective.extend_comp e₂₃.injective, Function.comp_def]

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
⊢ |a|ₘ = max a 1 * max a⁻¹ 1

Tactic:
rcases le_total 1 a with (ha | ha)

Goal state after:
case inl
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
ha : 1 ≤ a
⊢ |a|ₘ = max a 1 * max a⁻¹ 1

case inr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a : G
ha : a ≤ 1
⊢ |a|ₘ = max a 1 * max a⁻¹ 1
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: case ofNat
α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
a : α
k : ℕ
⊢ (-a) ^ (2 * Int.ofNat k + 1) = -a ^ (2 * Int.ofNat k + 1)

Tactic:
rw [Int.ofNat_eq_natCast]
    norm_cast
    simp [pow_add]

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

Goal state before:
pp: α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
⊢ a ≤ b ∧ a ≠ b ↔ ∃ c, c > 1 ∧ b = a * c

Tactic:
le_iff_exists_mul,

Goal state after:
α : Type u
inst✝³ : MulOneClass α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedMul α
a b : α
inst✝ : MulLeftStrictMono α
⊢ (∃ c, b = a * c) ∧ a ≠ b ↔ ∃ c, c > 1 ∧ b = a * c
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ -(a + b) + (a + b) = 0

Tactic:
simp [neg_add_cancel_of_ne_top, *]

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
h : a + b = 0
ha : a ≠ ⊤
⊢ -a + a = 0

Tactic:
simp [neg_add_cancel_of_ne_top, *]

Goal state after: