mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
h : ∃ n, ∀ (m : ℕ), n ≤ m → a n = a m
⊢ a m ≤ monotonicSequenceLimit a

Tactic:
exact (Nat.sInf_mem (s := {n | ∀ m, n ≤ m → a n = a m}) h m hm.le).ge

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
f : ℕ → α × β
⊢ ∃ m n, m < n ∧ (fun a b ↦ r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)

Tactic:
obtain ⟨g, h₁⟩ := hr.exists_monotone_subseq (Prod.fst ∘ f)

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsPreorder α r
hr : WellQuasiOrdered r
hs : WellQuasiOrdered s
f : ℕ → α × β
g : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (g m)) ((Prod.fst ∘ f) (g n))
⊢ ∃ m n, m < n ∧ (fun a b ↦ r a.1 b.1 ∧ s a.2 b.2) (f m) (f n)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ a ∈ Icc a b ↔ a ≤ b

Tactic:
by simp only [mem_Icc, true_and, le_rfl]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ b ∈ Ioc a b ↔ a < b

Tactic:
by simp only [mem_Ioc, and_true, le_rfl]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
f' : β → ↑(range f) := fun c ↦ ⟨f c, ⋯⟩
h : WellFounded (r on f)
c : β
⊢ ∀ {a : β} {b : ↑(range f)}, Subrel r (fun x ↦ x ∈ range f) b (f' a) → ∃ c, f' c = b

Tactic:
rintro _ ⟨_, c', rfl⟩ -
    exact ⟨c', rfl⟩

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ insert a (Ioc a b) = Icc a b

Tactic:
by
  rw [← coe_inj, coe_insert, coe_Ioc, coe_Icc, Set.insert_eq, Set.union_comm, Set.Ioc_union_left h]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ r (f m) (f n)
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g : ℕ → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
m n : ℕ
hlt : m < n
hmn : r (g m) (g n)
⊢ ∃ m n, m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)

Tactic:
exact ⟨m, n, hlt, hf _ (hgs m) _ (hgs n) hmn⟩

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
H K : Submonoid M
⊢ H ⊔ closure ↑K ≤ H ⊔ K

Tactic:
closure_eq

Goal state after:
M : Type u_3
inst✝ : Monoid M
H K : Submonoid M
⊢ H ⊔ K ≤ H ⊔ K
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = insert a (Ioc a b)

Tactic:
Ioc_insert_left h

Goal state after:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = Icc a b
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ closure s⁻¹ ≤ (closure s)⁻¹

Tactic:
closure_le,

Goal state after:
case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ s⁻¹ ⊆ ↑(closure s)⁻¹
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ closure s ≤ (closure s⁻¹)⁻¹

Tactic:
closure_le,

Goal state after:
case a
G : Type u_2
inst✝ : Group G
s : Set G
⊢ s ⊆ ↑(closure s⁻¹)⁻¹
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
h : center G = ⊤
⊢ ∀ (a b : G), a * b = b * a

Tactic:
rw [eq_top_iff'] at h
      intro x y
      apply Subgroup.mem_center_iff.mp _ x
      exact h y

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case h.left
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
n : ℕ
hn : (ofLex f (g 0)).1 < (ofLex f (g n)).1
⊢ g 0 < g n

pp: case h.right
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
n : ℕ
hn : (ofLex f (g 0)).1 < (ofLex f (g n)).1
⊢ f (g 0) ≤ f (g n)

Tactic:
· by_contra hx
      simp_all

Goal state after:
case h.right
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
n : ℕ
hn : (ofLex f (g 0)).1 < (ofLex f (g n)).1
⊢ f (g 0) ≤ f (g n)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H K : Subgroup G
⊢ H ⊔ closure ↑K ≤ H ⊔ K

Tactic:
closure_eq

Goal state after:
G : Type u_2
inst✝ : Group G
H K : Subgroup G
⊢ H ⊔ K ≤ H ⊔ K
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case mpr
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x ∈ ↑A, ∃ y ∈ ↑B, x * y = x✝) ∧ x✝ ∈ ↑C → ∃ x ∈ ↑A, ∃ y, (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝

Tactic:
rintro ⟨⟨y, hy, z, hz, rfl⟩, hyz⟩

Goal state after:
case mpr
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ ↑A
z : G
hz : z ∈ ↑B
hyz : y * z ∈ ↑C
⊢ ∃ x ∈ ↑A, ∃ y_1, (y_1 ∈ ↑B ∧ y_1 ∈ ↑C) ∧ x * y_1 = y * z
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ (L1 ++ L2).length + 2 = (L1 ++ (x, b) :: (x, !b) :: L2).length

Tactic:
rw [List.length_append, List.length_append]

Goal state after:
α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ L1.length + L2.length + 2 = L1.length + ((x, b) :: (x, !b) :: L2).length
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁ ∪ s₂, f x = (∏ x ∈ s₁, f x) * ∏ x ∈ s₂, f x

Tactic:
rw [← prod_union_inter, disjoint_iff_inter_eq_empty.mp h]

Goal state after:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : Disjoint s₁ s₂
⊢ ∏ x ∈ s₁ ∪ s₂, f x = (∏ x ∈ s₁ ∪ s₂, f x) * ∏ x ∈ ∅, f x
Module: Mathlib.GroupTheory.Coset.Defs

Goal state before:
pp: α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
x : α
⊢ x ∈ mk ⁻¹' mk '' s ↔ x ∈ ⋃ x, (fun x_1 ↦ x_1 * ↑x) ⁻¹' s

Tactic:
simp only [QuotientGroup.eq, SetLike.exists, exists_prop, Set.mem_preimage, Set.mem_iUnion,
    Set.mem_image]

Goal state after:
α : Type u_1
inst✝ : Group α
N : Subgroup α
s : Set α
x : α
⊢ (∃ x_1 ∈ s, x_1⁻¹ * x ∈ N) ↔ ∃ x_1 ∈ N, x * x_1 ∈ s
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:

Tactic:
∏ x ∈ s, f x = ∏ x ∈ s with f x ≠ 1, f x := by rw [prod_filter_ne_one]
    _ = ∏ x ∈ t with g x ≠ 1, g x :=
      prod_bij (fun a ha => i a (mem_filter.mp ha).1 <| by simpa using (mem_filter.mp ha).2)
        ?_ ?_ ?_ ?_
    _ = ∏ x ∈ t, g x := prod_filter_ne_one _

Goal state after:
case calc_1
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∀ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), i a ⋯ ⋯ ∈ {x ∈ t | g x ≠ 1}

case calc_2
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∀ (a₁ : ι) (ha₁ : a₁ ∈ {x ∈ s | f x ≠ 1}) (a₂ : ι) (ha₂ : a₂ ∈ {x ∈ s | f x ≠ 1}), i a₁ ⋯ ⋯ = i a₂ ⋯ ⋯ → a₁ = a₂

case calc_3
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∀ b ∈ {x ∈ t | g x ≠ 1}, ∃ a, ∃ (ha : a ∈ {x ∈ s | f x ≠ 1}), i a ⋯ ⋯ = b

case calc_4
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
i : (a : ι) → a ∈ s → f a ≠ 1 → κ
hi : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ ∈ t
i_inj :
  ∀ (a₁ : ι) (h₁₁ : a₁ ∈ s) (h₁₂ : f a₁ ≠ 1) (a₂ : ι) (h₂₁ : a₂ ∈ s) (h₂₂ : f a₂ ≠ 1),
    i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂
i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a, ∃ (h₁ : a ∈ s) (h₂ : f a ≠ 1), i a h₁ h₂ = b
h : ∀ (a : ι) (h₁ : a ∈ s) (h₂ : f a ≠ 1), f a = g (i a h₁ h₂)
⊢ ∀ (a : ι) (ha : a ∈ {x ∈ s | f x ≠ 1}), f a = g (i a ⋯ ⋯)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case succ
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
ih : ∏ r ∈ range (n + 1), f (n - r) = ∏ k ∈ range (n + 1), f k
⊢ ∏ r ∈ range (n + 1 + 1), f (n + 1 - r) = ∏ k ∈ range (n + 1 + 1), f k

Tactic:
rw [prod_range_succ', prod_range_succ _ (Nat.succ n)]

Goal state after:
case succ
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
ih : ∏ r ∈ range (n + 1), f (n - r) = ∏ k ∈ range (n + 1), f k
⊢ (∏ k ∈ range (n + 1), f (n + 1 - (k + 1))) * f (n + 1 - 0) = (∏ x ∈ range n.succ, f x) * f n.succ
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s✝ : Finset ι
inst✝ : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
h : ∏ x ∈ s \ {x, g x hx}, f x = 1
⊢ ∏ x ∈ s, f x = 1

Tactic:
← prod_sdiff this,

Goal state after:
ι : Type u_1
M : Type u_4
s✝ : Finset ι
inst✝ : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
h : ∏ x ∈ s \ {x, g x hx}, f x = 1
⊢ (∏ x ∈ s \ {x, g x hx}, f x) * ∏ x ∈ {x, g x hx}, f x = 1
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case refine_2
G : Type u_3
inst✝ : Group G
S : Set G
hfin : Finite ↑S
φ : FreeGroup ↑S →* G
hφ : Function.Surjective ⇑φ
⊢ FG G

Tactic:
exact Group.fg_of_surjective hφ

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mpr
G : Type u_3
inst✝ : Group G
α : Type
w✝ : Finite α
φ : FreeGroup α →* G
hφ : Function.Surjective ⇑φ
⊢ FG G

Tactic:
exact Group.fg_of_surjective hφ

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

Goal state before:
pp: M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
⊢ (∏ i, f ↑i) * ∏ i, f ↑i = ∏ i, f i

Tactic:
let s := { x | p x }.toFinset
    rw [← Finset.prod_subtype s, ← Finset.prod_subtype sᶜ]
    · exact Finset.prod_mul_prod_compl _ _
    · simp [s]
    · simp [s]

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

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
m : Multiset ι
hms : ∀ a ∈ m, a ∈ s
⊢ ∑ a ∈ s, count a m = m.card

Tactic:
← toFinset_sum_count_eq,

Goal state after:
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
m : Multiset ι
hms : ∀ a ∈ m, a ∈ s
⊢ ∑ a ∈ s, count a m = ∑ a ∈ m.toFinset, count a m
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ H₂ ≤ normalizer ↑⁅H₁, H₂⁆

Tactic:
rw [commutator_comm]
  apply normalizer_commutator_ge_left

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 : α
y₁ y₂ : FreeAbelianGroup α
ih₁ : x * y₁ * of L3 = x * (y₁ * of L3)
ih₂ : x * y₂ * of L3 = x * (y₂ * of L3)
⊢ x * (y₁ + y₂) * of L3 = x * (y₁ * of L3 + y₂ * of L3)

Tactic:
mul_add,

Goal state after:
case of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 : α
y₁ y₂ : FreeAbelianGroup α
ih₁ : x * y₁ * of L3 = x * (y₁ * of L3)
ih₂ : x * y₂ * of L3 = x * (y₂ * of L3)
⊢ (x * y₁ + x * y₂) * of L3 = x * (y₁ * of L3 + y₂ * of L3)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 : α
y₁ y₂ : FreeAbelianGroup α
ih₁ : x * y₁ * of L3 = x * (y₁ * of L3)
ih₂ : x * y₂ * of L3 = x * (y₂ * of L3)
⊢ (x * y₁ + x * y₂) * of L3 = x * (y₁ * of L3 + y₂ * of L3)

Tactic:
mul_add,

Goal state after:
case of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 : α
y₁ y₂ : FreeAbelianGroup α
ih₁ : x * y₁ * of L3 = x * (y₁ * of L3)
ih₂ : x * y₂ * of L3 = x * (y₂ * of L3)
⊢ (x * y₁ + x * y₂) * of L3 = x * (y₁ * of L3) + x * (y₂ * of L3)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y z₁ z₂ : FreeAbelianGroup α
ih₁ : x * y * z₁ = x * (y * z₁)
ih₂ : x * y * z₂ = x * (y * z₂)
⊢ x * y * (z₁ + z₂) = x * (y * (z₁ + z₂))

Tactic:
mul_add,

Goal state after:
case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y z₁ z₂ : FreeAbelianGroup α
ih₁ : x * y * z₁ = x * (y * z₁)
ih₂ : x * y * z₂ = x * (y * z₂)
⊢ x * y * z₁ + x * y * z₂ = x * (y * (z₁ + z₂))
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y z₁ z₂ : FreeAbelianGroup α
ih₁ : x * y * z₁ = x * (y * z₁)
ih₂ : x * y * z₂ = x * (y * z₂)
⊢ x * y * z₁ + x * y * z₂ = x * (y * (z₁ + z₂))

Tactic:
mul_add,

Goal state after:
case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y z₁ z₂ : FreeAbelianGroup α
ih₁ : x * y * z₁ = x * (y * z₁)
ih₂ : x * y * z₂ = x * (y * z₂)
⊢ x * y * z₁ + x * y * z₂ = x * (y * z₁ + y * z₂)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y z₁ z₂ : FreeAbelianGroup α
ih₁ : x * y * z₁ = x * (y * z₁)
ih₂ : x * y * z₂ = x * (y * z₂)
⊢ x * y * z₁ + x * y * z₂ = x * (y * z₁ + y * z₂)

Tactic:
mul_add,

Goal state after:
case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y z₁ z₂ : FreeAbelianGroup α
ih₁ : x * y * z₁ = x * (y * z₁)
ih₂ : x * y * z₂ = x * (y * z₂)
⊢ x * y * z₁ + x * y * z₂ = x * (y * z₁) + x * (y * z₂)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x y1 y2 : FreeAbelianGroup α
ih1 : (lift ⇑f) (x * y1) = (lift ⇑f) x * (lift ⇑f) y1
ih2 : (lift ⇑f) (x * y2) = (lift ⇑f) x * (lift ⇑f) y2
⊢ (lift ⇑f) (x * (y1 + y2)) = (lift ⇑f) x * (lift ⇑f) (y1 + y2)

Tactic:
mul_add,

Goal state after:
case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x y1 y2 : FreeAbelianGroup α
ih1 : (lift ⇑f) (x * y1) = (lift ⇑f) x * (lift ⇑f) y1
ih2 : (lift ⇑f) (x * y2) = (lift ⇑f) x * (lift ⇑f) y2
⊢ (lift ⇑f) (x * y1 + x * y2) = (lift ⇑f) x * (lift ⇑f) (y1 + y2)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x y1 y2 : FreeAbelianGroup α
ih1 : (lift ⇑f) (x * y1) = (lift ⇑f) x * (lift ⇑f) y1
ih2 : (lift ⇑f) (x * y2) = (lift ⇑f) x * (lift ⇑f) y2
⊢ (lift ⇑f) (x * y1) + (lift ⇑f) (x * y2) = (lift ⇑f) x * ((lift ⇑f) y1 + (lift ⇑f) y2)

Tactic:
mul_add,

Goal state after:
case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x y1 y2 : FreeAbelianGroup α
ih1 : (lift ⇑f) (x * y1) = (lift ⇑f) x * (lift ⇑f) y1
ih2 : (lift ⇑f) (x * y2) = (lift ⇑f) x * (lift ⇑f) y2
⊢ (lift ⇑f) (x * y1) + (lift ⇑f) (x * y2) = (lift ⇑f) x * (lift ⇑f) y1 + (lift ⇑f) x * (lift ⇑f) y2
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s : α
y1 y2 : FreeAbelianGroup α
ih1 : of s * y1 = y1 * of s
ih2 : of s * y2 = y2 * of s
⊢ of s * (y1 + y2) = (y1 + y2) * of s

Tactic:
mul_add,

Goal state after:
case of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s : α
y1 y2 : FreeAbelianGroup α
ih1 : of s * y1 = y1 * of s
ih2 : of s * y2 = y2 * of s
⊢ of s * y1 + of s * y2 = (y1 + y2) * of s
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
y x1 x2 : FreeAbelianGroup α
ih1 : x1 * y = y * x1
ih2 : x2 * y = y * x2
⊢ x1 * y + x2 * y = y * (x1 + x2)

Tactic:
mul_add,

Goal state after:
case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
y x1 x2 : FreeAbelianGroup α
ih1 : x1 * y = y * x1
ih2 : x2 * y = y * x2
⊢ x1 * y + x2 * y = y * x1 + y * x2
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
b : Con (M × ↥S)
H : b ∈ {c | ∀ (y : ↥S), c 1 (↑y, y)}
x✝² x✝¹ : M × ↥S
p : M
q : ↥S
x : M
y : ↥S
x✝ : (r' S) (p, q) (x, y)
t : ↥S
ht : ↑t * (↑(x, y).2 * (p, q).1) = ↑t * (↑(p, q).2 * (x, y).1)
⊢ b (1 * (p, q)) (x, y)

Tactic:
← one_mul (x, y)

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
b : Con (M × ↥S)
H : b ∈ {c | ∀ (y : ↥S), c 1 (↑y, y)}
x✝² x✝¹ : M × ↥S
p : M
q : ↥S
x : M
y : ↥S
x✝ : (r' S) (p, q) (x, y)
t : ↥S
ht : ↑t * (↑(x, y).2 * (p, q).1) = ↑t * (↑(p, q).2 * (x, y).1)
⊢ b (1 * (p, q)) (1 * (x, y))
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
j : N →* P
hj : ∀ (x : M), j (f x) = g x
⊢ f.lift hg = j

Tactic:
ext
  rw [lift_spec, ← hj, ← hj, ← j.map_mul]
  apply congr_arg
  rw [← sec_spec']

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
R : Type u_4
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ (c • 1) • a /ₒ (b * 1) = c • a /ₒ b

Tactic:
smul_assoc,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
R : Type u_4
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
c : R
a : M
b : ↥S
⊢ c • 1 • a /ₒ (b * 1) = c • a /ₒ b
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ f.mk' (x₁ * x₂) (y₁ * y₂) = f.mk' x₁ y₁ * f.mk' x₂ y₂

Tactic:
refine (mul_inv_left f.map_units _ _ _).2 ?_
  simp only [map_mul, coe_mul, toMonoidHom_apply, mk', IsUnit.liftRight, Units.liftRight,
    MonoidHom.domRestrict_apply, MonoidHom.coe_mk, OneHom.coe_mk]
  rw [mul_mul_mul_comm (f x₁), mul_left_comm, mul_mul_mul_comm (f y₁)]
  simp

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
⊢ untopD 0 (a * 0) = untopD 0 a * untopD 0 0

Tactic:
mul_zero,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
⊢ untopD 0 0 = untopD 0 a * untopD 0 0
Module: Mathlib.Algebra.Order.Sub.WithTop

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Sub α
inst✝² : Bot α
inst✝¹ : Sub β
inst✝ : Bot β
f : α → β
h : ∀ (x y : α), f (x - y) = f x - f y
h₀ : f ⊥ = ⊥
x✝ : WithTop α
⊢ map f (x✝ - ⊤) = map f x✝ - map f ⊤

Tactic:
simp only [sub_top, map_coe, h₀, map_top]

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹³ : Monoid M
S : Submonoid M
inst✝¹² : OreSet S
inst✝¹¹ : MulAction M X
inst✝¹⁰ : SMul R X
inst✝⁹ : SMul R M
inst✝⁸ : IsScalarTower R M M
inst✝⁷ : IsScalarTower R M X
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R R' M
r : R
m : R'
x : OreLocalization S X
⊢ (m • r • 1) • x = m • r • x

Tactic:
smul_assoc,

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹³ : Monoid M
S : Submonoid M
inst✝¹² : OreSet S
inst✝¹¹ : MulAction M X
inst✝¹⁰ : SMul R X
inst✝⁹ : SMul R M
inst✝⁸ : IsScalarTower R M M
inst✝⁷ : IsScalarTower R M X
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R R' M
r : R
m : R'
x : OreLocalization S X
⊢ m • (r • 1) • x = m • r • x
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
M : Type u_3
X : Type u_4
inst✝⁶ : Monoid M
S : Submonoid M
inst✝⁵ : OreSet S
inst✝⁴ : MulAction M X
inst✝³ : SMul R X
inst✝² : SMul R M
inst✝¹ : IsScalarTower R M M
inst✝ : IsScalarTower R M X
r : R
x : X
⊢ (r • 1) • x /ₒ 1 = r • x /ₒ 1

Tactic:
smul_assoc,

Goal state after:
R : Type u_1
M : Type u_3
X : Type u_4
inst✝⁶ : Monoid M
S : Submonoid M
inst✝⁵ : OreSet S
inst✝⁴ : MulAction M X
inst✝³ : SMul R X
inst✝² : SMul R M
inst✝¹ : IsScalarTower R M M
inst✝ : IsScalarTower R M X
r : R
x : X
⊢ r • 1 • x /ₒ 1 = r • x /ₒ 1
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : b = 0
⊢ unbotD 0 (a * 0) = unbotD 0 a * unbotD 0 0

Tactic:
mul_zero,

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : b = 0
⊢ unbotD 0 0 = unbotD 0 a * unbotD 0 0