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

Goal state before:
pp: M : Type u
⊢ ∀ ⦃m₁ m₂ : MulOneClass M⦄, Mul.mul = Mul.mul → m₁ = m₂

Tactic:
rintro @⟨@⟨⟨one₁⟩, ⟨mul₁⟩⟩, one_mul₁, mul_one₁⟩ @⟨@⟨⟨one₂⟩, ⟨mul₂⟩⟩, one_mul₂, mul_one₂⟩ ⟨rfl⟩
  -- FIXME (See https://github.com/leanprover/lean4/issues/1711)
  -- congr
  suffices one₁ = one₂ by cases this; rfl
  exact (one_mul₂ one₁).symm.trans (mul_one₁ one₂)

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

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

Tactic:
pow_add,

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

Goal state before:
pp: a b : Prop
⊢ Xor a b ↔ (¬a ↔ b)

Tactic:
simp only [← @xor_not_left _ b, not_not]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
⊢ (∀ (x : α), p x) → b ↔ ∃ x, p x → b

Tactic:
classical
  let ⟨a⟩ := ha
  refine ⟨fun h ↦ not_forall_not.1 fun h' ↦ ?_, fun ⟨x, hx⟩ h ↦ hx (h x)⟩
  exact if hb : b then h' a fun _ ↦ hb else hb <| h fun x ↦ (Classical.not_imp.1 (h' x)).1

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ (g₁ ∘ f) ∘ g₂ = g₂

Tactic:
h₁.comp_eq_id,

Goal state after:
α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ id ∘ g₂ = g₂
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a b c : α
inst✝ : Std.Symm r
x y : α
h : TransGen r x y
⊢ TransGen r y x

Tactic:
induction h with
    | single i => exact .single <| symm i
    | tail _ h₁ h₂ => exact .head (symm h₁) h₂

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

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

Tactic:
by
  induction n generalizing k with
  | zero =>
    rw [Nat.zero_add]
    exact id_left
  | succ n ihn =>
    rw [Nat.add_right_comm, Nat.add_assoc]
    exact (H k).trans (ihn (k + 1))

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

Goal state before:
pp: α : Type u
f g : α → α
hg : LeftInverse g f
n✝ n : ℕ
ihn : LeftInverse g^[n] f^[n]
⊢ LeftInverse g^[n.succ] f^[n.succ]

Tactic:
by
    rw [iterate_succ', iterate_succ]
    exact ihn.comp hg

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
M : Type u_9
α : Type u_10
inst✝¹ : CommMonoid M
inst✝ : MulAction M α
a a' : M
b : α
⊢ a • a' • b = a' • a • b

Tactic:
by rw [← mul_smul, mul_comm, mul_smul]

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

Goal state before:
pp: α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (¬∀ (x : (ab : α ⊕ β) → γ ab), ¬p x) ↔ ∃ fa fb, p fun t ↦ rec fa fb t

Tactic:
forall_sum

Goal state after:
α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (¬∀ (fa : (val : α) → γ (inl val)) (fb : (val : β) → γ (inr val)), ¬p fun t ↦ rec fa fb t) ↔
    ∃ fa fb, p fun t ↦ rec fa fb t
Module: Mathlib.Algebra.Group.Pi.Basic

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → MulOneClass (f i)
⊢ ∀ (a : (i : I) → f i), a * 1 = a

Tactic:
by intros; ext; exact mul_one _

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

Goal state before:
pp: case left
α : 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
i : α
a : β
h : r i i
⊢ False

Tactic:
exact irrefl _ h

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

Goal state before:
pp: case right
α : 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
i : α
a : β
h : s a a
⊢ False

Tactic:
exact irrefl _ h

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⟩ ⟨j, b⟩

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 : β
j : α
b : β
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty β
inst✝ : Nonempty δ
f₁ : α → β
g₁ : γ → δ
f₂ : β → α
g₂ : δ → γ
h : LeftInverse (map f₁ g₁) (map f₂ g₂)
d : δ
⊢ g₁ (g₂ d) = d

Tactic:
inhabit β
      exact congr_arg Prod.snd (h (default, d))

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ max a b = if b ≤ a then a else b

Tactic:
simp [le_of_lt, not_le_of_gt, h, max_def]

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a = b
⊢ max a b = if b ≤ a then a else b

Tactic:
simp [le_of_lt, not_le_of_gt, h, max_def]

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

Goal state before:
pp: case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b < a
⊢ max a b = if b ≤ a then a else b

Tactic:
simp [le_of_lt, not_le_of_gt, h, max_def]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd → x < y

Tactic:
· rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)
    · exact ⟨⟨h₁.le, h₂⟩, fun h ↦ h₁.not_ge h.1⟩
    · exact ⟨⟨h₁, h₂.le⟩, fun h ↦ h₂.not_ge h.2⟩

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

Goal state before:
pp: case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Injective next
m✝ : ℕ
hnm : n.le m✝
ih : Injective (leRecOn hnm fun {k} ↦ next)
⊢ Injective (leRecOn ⋯ fun {k} ↦ next)

Tactic:
| step hnm ih =>

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

Goal state before:
pp: case step
C : ℕ → Sort u_1
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Surjective next
m✝ : ℕ
hnm : n.le m✝
ih : Surjective (leRecOn hnm fun {k} ↦ next)
⊢ Surjective (leRecOn ⋯ fun {k} ↦ next)

Tactic:
| step hnm ih =>

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

Goal state before:
pp: case inr.inr
n m : ℕ
h : m < n
hm : m ≠ 0
⊢ n ∣ n - m ↔ m = 0 ∨ n ≤ m

Tactic:
· simp only [hm, h.not_ge, or_self, iff_false]
      refine not_dvd_of_pos_of_lt ?_ ?_ <;>
      grind

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsStrictOrder α r
x y : α
h : r x x
e : y = x
⊢ False

Tactic:
exact irrefl _ h

Goal state after:
Module: Mathlib.Order.Lattice

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

Tactic:
inf_le_sup.lt_iff_ne,

Goal state after:
α : Type u
inst✝ : Lattice α
a b : α
⊢ a ⊓ b ≠ a ⊔ b ↔ a ≠ b
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
h : c ⊔ a ≤ c ⊔ b
⊢ a \ c ≤ b \ c

Tactic:
← sup_sdiff_left_self,

Goal state after:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
h : c ⊔ a ≤ c ⊔ b
⊢ (c ⊔ a) \ c ≤ b \ c
Module: Mathlib.Order.Heyting.Basic

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ a ≤ aᶜ ↔ a = ⊥

Tactic:
by
  rw [le_compl_iff_disjoint_left, disjoint_self]

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

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

Tactic:
rw [inf_assoc, sup_inf_right, sup_inf_sdiff, inf_sup_right, inf_sdiff_left]

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

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
e₁ : α ≃ β
e₂ : γ ≃ δ
⊢ LeftInverse (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm)) fun x ↦
    PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂)

Tactic:
rintro (x | x)

Goal state after:
case inl
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
e₁ : α ≃ β
e₂ : γ ≃ δ
x : α
⊢ (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm))
      ((fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂)) (PSum.inl x)) =
    PSum.inl x

case inr
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
e₁ : α ≃ β
e₂ : γ ≃ δ
x : γ
⊢ (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm))
      ((fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂)) (PSum.inr x)) =
    PSum.inr x
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
e₁ : α ≃ β
e₂ : γ ≃ δ
⊢ RightInverse (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm)) fun x ↦
    PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂)

Tactic:
rintro (x | x)

Goal state after:
case inl
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
e₁ : α ≃ β
e₂ : γ ≃ δ
x : β
⊢ (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂))
      ((fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm)) (PSum.inl x)) =
    PSum.inl x

case inr
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
e₁ : α ≃ β
e₂ : γ ≃ δ
x : δ
⊢ (fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁) (PSum.inr ∘ ⇑e₂))
      ((fun x ↦ PSum.casesOn x (PSum.inl ∘ ⇑e₁.symm) (PSum.inr ∘ ⇑e₂.symm)) (PSum.inr x)) =
    PSum.inr x
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
⊢ s ×ˢ insert b t = (fun a ↦ (a, b)) '' s ∪ s ×ˢ t

Tactic:
by
  simp only [insert_eq, prod_union, prod_singleton]

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

Goal state before:
pp: α : Type u_1
s t : Set α
h : t ⊆ s
x : α
⊢ (∃ x_1, x_1 ∈ {x | ↑x ∈ t} ∧ ↑x_1 = x) ↔ x ∈ t

Tactic:
exact ⟨fun ⟨_, hx', hx⟩ => hx ▸ hx', fun hx => ⟨⟨x, h hx⟩, hx, rfl⟩⟩

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
i : ι
s : Set (α i)
⊢ univ.pi (update (fun j ↦ univ) i s) = eval i ⁻¹' s

Tactic:
by
  rw [univ_pi_update i (fun j => (univ : Set (α j))) s fun j t => t, pi_univ, inter_univ, preimage]

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

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a : α
n : ℕ
⊢ a⁻¹ ^ (n + 1) = (a ^ (n + 1))⁻¹

Tactic:
by rw [pow_succ', pow_succ, inv_pow _ n, mul_inv_rev]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ a * b / (a / c) = b * c

Tactic:
rw [← div_mul, mul_div_cancel_left]

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

Goal state before:
pp: α : 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
⊢ p a b → p b c → p a c → f a c = f a b * f b c

Tactic:
pab

Goal state after:
α : 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
⊢ p b c → p a c → f a c = f a b * f b c
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case inl
α : 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
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
rbc : r b c
⊢ f a c = f a b * f b c

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
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
rcb : r c b
⊢ f a c = f a b * f b c

Tactic:
· exact hmul' rbc pab pbc pac

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
hmul' : ∀ {b c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c
rcb : r c b
⊢ f a c = f a b * f b c
Module: Mathlib.Algebra.Group.Units.Hom

Goal state before:
pp: M : Type u
N : Type v
P : Type w
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
f : M →* N
g : M → Nˣ
h : ∀ (x : M), ↑(g x) = f x
x y : M
⊢ ↑(g (x * y)) = ↑(g x * g y)

Tactic:
by simp only [h, val_mul, f.map_mul]

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) = 1 / b

Tactic:
h.div_mul_left

Goal state after:
α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ 1 / b = 1 / b
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: M : Type u_3
N : Type u_4
inst✝¹ : MulOneClass M
inst✝ : Mul N
b₁ b₂ : N
⊢ (1, b₁) * (1, b₂) = (1, b₁ * b₂)

Tactic:
mk_mul_mk,

Goal state after:
M : Type u_3
N : Type u_4
inst✝¹ : MulOneClass M
inst✝ : Mul N
b₁ b₂ : N
⊢ (1 * 1, b₁ * b₂) = (1, b₁ * b₂)
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: M : Type u_3
N : Type u_4
inst✝¹ : Mul M
inst✝ : MulOneClass N
a₁ a₂ : M
⊢ (a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)

Tactic:
mk_mul_mk,

Goal state after:
M : Type u_3
N : Type u_4
inst✝¹ : Mul M
inst✝ : MulOneClass N
a₁ a₂ : M
⊢ (a₁ * a₂, 1 * 1) = (a₁ * a₂, 1)
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivisionCommMonoid G
inst✝ : DivisionCommMonoid H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)

Tactic:
mk_mul_mk,

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : DivisionCommMonoid G
inst✝ : DivisionCommMonoid H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (g₁ * fst✝, h₁ * snd✝) = (fst✝, snd✝) * (g₁, h₁)
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
x✝¹ x✝ : M × N
m₁ : M
n₁ : N
fst✝ : M
snd✝ : N
⊢ (m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)

Tactic:
mk_mul_mk,

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
x✝¹ x✝ : M × N
m₁ : M
n₁ : N
fst✝ : M
snd✝ : N
⊢ (m₁ * fst✝, n₁ * snd✝) = (fst✝, snd✝) * (m₁, n₁)
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
x✝¹ x✝ : M × N
m₁ : M
n₁ : N
fst✝ : M
snd✝ : N
⊢ (m₁ * fst✝, n₁ * snd✝) = (fst✝, snd✝) * (m₁, n₁)

Tactic:
mk_mul_mk,

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
x✝¹ x✝ : M × N
m₁ : M
n₁ : N
fst✝ : M
snd✝ : N
⊢ (m₁ * fst✝, n₁ * snd✝) = (fst✝ * m₁, snd✝ * n₁)
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommGroup G
inst✝ : CommGroup H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)

Tactic:
mk_mul_mk,

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommGroup G
inst✝ : CommGroup H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (g₁ * fst✝, h₁ * snd✝) = (fst✝, snd✝) * (g₁, h₁)
Module: Mathlib.Algebra.Group.Prod

Goal state before:
pp: G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommGroup G
inst✝ : CommGroup H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (g₁ * fst✝, h₁ * snd✝) = (fst✝, snd✝) * (g₁, h₁)

Tactic:
mk_mul_mk,

Goal state after:
G : Type u_1
H : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹ : CommGroup G
inst✝ : CommGroup H
x✝¹ x✝ : G × H
g₁ : G
h₁ : H
fst✝ : G
snd✝ : H
⊢ (g₁ * fst✝, h₁ * snd✝) = (fst✝ * g₁, snd✝ * h₁)
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: n : ℕ
S : Type u_5
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
N : ℕ
hN : x ^ N = 0
⊢ x ^ (n * N + N) = 0

Tactic:
pow_add,

Goal state after:
n : ℕ
S : Type u_5
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
N : ℕ
hN : x ^ N = 0
⊢ x ^ (n * N) * x ^ N = 0
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
m n : ℕ
hmn : m ≤ n
h : a ^ m * b = 0
⊢ a ^ (n - m + m) * b = 0

Tactic:
pow_add,

Goal state after:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
m n : ℕ
hmn : m ≤ n
h : a ^ m * b = 0
⊢ a ^ (n - m) * a ^ m * b = 0
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 B A
hf : Injective ⇑f
smul : ∀ (c : M) (x : B), f (c • x) = c • f x
c : M
⊢ f (c • 0) = f 0

Tactic:
simp only [smul, map_zero, smul_zero]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
a b : R
h : a + b = 1
⊢ a • x + b • y = b • y - b • x + (a • x + b • x)

Tactic:
rw [sub_add_add_cancel, add_comm]

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

Goal state before:
pp: n : ℕ
⊢ n.sqrt ^ 2 ≤ n

Tactic:
simpa [Nat.pow_two] using sqrt_le n

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)
⊢ x * (b - x) = c

Tactic:
rw [this]

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

Goal state before:
pp: R : Type u_3
inst✝ : NonUnitalNonAssocRing R
tfae_1_iff_2 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0
⊢ [NoZeroDivisors R, ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0, ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0,
      ∀ {a : R}, a ≠ 0 → (∀ (x : R), a * x = 0 → x = 0) ∧ ∀ (x : R), x * a = 0 → x = 0].TFAE

Tactic:
tfae_have 1 ↔ 3 := noZeroDivisors_iff_left_eq_zero_of_mul

Goal state after:
R : Type u_3
inst✝ : NonUnitalNonAssocRing R
tfae_1_iff_2 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0
tfae_1_iff_3 : NoZeroDivisors R ↔ ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0
⊢ [NoZeroDivisors R, ∀ {a : R}, a ≠ 0 → ∀ (x : R), a * x = 0 → x = 0, ∀ {a : R}, a ≠ 0 → ∀ (x : R), x * a = 0 → x = 0,
      ∀ {a : R}, a ≠ 0 → (∀ (x : R), a * x = 0 → x = 0) ∧ ∀ (x : R), x * a = 0 → x = 0].TFAE
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
f : α →+* β
h : f 1 = 0
x : α
⊢ f x = 0

Tactic:
rw [← mul_one x, map_mul, h, mul_zero]

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

Goal state before:
pp: case pos
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀ˣ
h : Commute ↑a ↑b
hab : IsUnit (↑a * ↑b)
⊢ (↑a * ↑b)⁻¹ʳ = (↑b)⁻¹ʳ * (↑a)⁻¹ʳ

Tactic:
← Units.val_mul,

Goal state after:
case pos
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀ˣ
h : Commute ↑a ↑b
hab : IsUnit (↑a * ↑b)
⊢ (↑(a * b))⁻¹ʳ = (↑b)⁻¹ʳ * (↑a)⁻¹ʳ
Module: Mathlib.Algebra.GroupWithZero.Commute

Goal state before:
pp: case pos
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀ˣ
h : Commute ↑a ↑b
hab : IsUnit (↑a * ↑b)
⊢ ↑(a * b)⁻¹ = ↑b⁻¹ * ↑a⁻¹

Tactic:
← Units.val_mul,

Goal state after:
case pos
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀ˣ
h : Commute ↑a ↑b
hab : IsUnit (↑a * ↑b)
⊢ ↑(a * b)⁻¹ = ↑(b⁻¹ * a⁻¹)
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
⊢ a⁻¹ʳ⁻¹ʳ⁻¹ʳ = a⁻¹ʳ

Tactic:
by
  nontriviality M₀
  by_cases h : IsUnit a
  · rw [Ring.inverse_inverse h]
  · simp [Ring.not_isUnit_iff_inverse_eq_zero.mp h]

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

Goal state before:
pp: α : Type u_1
inst✝ : AddMonoidWithOne α
m n : ℕ
⊢ AddCommute ↑m ↑n

Tactic:
by
  rw [addCommute_iff_eq, ← Nat.cast_add, ← Nat.cast_add, m.add_comm]

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

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

Tactic:
pow_add,

Goal state after:
R : Type u
inst✝ : Ring R
n : ℕ
⊢ (-1) ^ (n % 2) * (-1) ^ (2 * (n / 2)) = (-1) ^ ((n % 2 + 2 * (n / 2)) % 2)
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : Rˣ
⊢ a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b

Tactic:
simp_rw [Units.ext_iff, val_pow_eq_pow_val, sq_eq_sq_iff_eq_or_eq_neg, Units.val_neg]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ (-a) ^ (2 * c + 1) = -a ^ (2 * c + 1)

Tactic:
pow_add,

Goal state after:
α : Type u_2
inst✝¹ : Monoid α
inst✝ : HasDistribNeg α
c : ℕ
a : α
⊢ (-a) ^ (2 * c) * (-a) ^ 1 = -(a ^ (2 * c) * a ^ 1)
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : LinearOrder α
inst✝ : MulLeftMono α
a b : α
⊢ a / b ≤ b / a ↔ a ≤ b

Tactic:
by
  rw [div_eq_mul_inv b, mul_comm]
  exact div_le_inv_mul_iff

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

Goal state before:
pp: case inl
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
m n : ℕ
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
a1 : 1 ≤ a
nm : n ≤ m
⊢ a ^ n ≤ a ^ m

pp: case inr
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
m n : ℕ
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
a0 : 0 ≤ a
a1 : a ≤ 1
mn : m ≤ n
⊢ a ^ n ≤ a ^ m

Tactic:
· exact pow_right_mono₀ a1 nm

Goal state after:
case inr
M₀ : Type u_2
inst✝³ : MonoidWithZero M₀
inst✝² : Preorder M₀
a : M₀
m n : ℕ
inst✝¹ : ZeroLEOneClass M₀
inst✝ : PosMulMono M₀
a0 : 0 ≤ a
a1 : a ≤ 1
mn : m ≤ n
⊢ a ^ n ≤ a ^ m
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
a b c : R
h : c + b * c ≤ a + b
⊢ 1 - a ≤ (1 + b) * (1 - c)

Tactic:
rw [mul_one_sub, one_add_mul, sub_le_sub_iff, add_assoc, add_comm b]
  gcongr

Goal state after: