mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
⊢ { finsetIcc := h₀_finset_Icc, finsetIco := h₀_finset_Ico, finsetIoc := h₀_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := h₀_finset_mem_Icc, finset_mem_Ico := h₀_finset_mem_Ico, finset_mem_Ioc := h₀_finset_mem_Ioc,
      finset_mem_Ioo := h₀_finset_mem_Ioo } =
    { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₁_finset_Ioc, finsetIoo := h₁_finset_Ioo,
      finset_mem_Icc := h₁_finset_mem_Icc, finset_mem_Ico := h₁_finset_mem_Ico, finset_mem_Ioc := h₁_finset_mem_Ioc,
      finset_mem_Ioo := h₁_finset_mem_Ioo }

Tactic:
have hIco : h₀_finset_Ico = h₁_finset_Ico := by
      ext a b x
      rw [h₀_finset_mem_Ico, h₁_finset_mem_Ico]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
⊢ { finsetIcc := h₀_finset_Icc, finsetIco := h₀_finset_Ico, finsetIoc := h₀_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := h₀_finset_mem_Icc, finset_mem_Ico := h₀_finset_mem_Ico, finset_mem_Ioc := h₀_finset_mem_Ioc,
      finset_mem_Ioo := h₀_finset_mem_Ioo } =
    { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₁_finset_Ioc, finsetIoo := h₁_finset_Ioo,
      finset_mem_Icc := h₁_finset_mem_Icc, finset_mem_Ico := h₁_finset_mem_Ico, finset_mem_Ioc := h₁_finset_mem_Ioc,
      finset_mem_Ioo := h₁_finset_mem_Ioo }
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
r : α → α → Prop
f : ℕ → α
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
let bad : Set ℕ := { m | ∀ n, m < n → ¬r (f m) (f n) }

Goal state after:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k : ℕ
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hkl : k % a = n % a
hln : n + a ≠ n
this : k = n
⊢ k = n + a

Tactic:
contradiction

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

Goal state before:
pp: n a : ℕ
⊢ Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))

Tactic:
by
  induction n with
  | zero =>
    simp only [zero_add, Ico_zero_eq_range]
    rintro k hk l hl (hkl : k % a = l % a)
    simp only [Finset.mem_range, Finset.mem_coe] at hk hl
    rwa [mod_eq_of_lt hk, mod_eq_of_lt hl] at hkl
  | succ n ih =>
    rw [Ico_succ_left_eq_erase_Ico, succ_add, succ_eq_add_one,
      Ico_succ_right_eq_insert_Ico (by lia)]
    rintro k hk l hl (hkl : k % a = l % a)
    have ha : 0 < a := Nat.pos_iff_ne_zero.2 <| by rintro rfl; simp at hk
    simp only [Finset.mem_coe, Finset.mem_insert, Finset.mem_erase] at hk hl
    rcases hk with ⟨hkn, rfl | hk⟩ <;> rcases hl with ⟨hln, rfl | hl⟩
    · rfl
    · rw [add_mod_right] at hkl
      refine (hln <| ih hl ?_ hkl.symm).elim
      simpa using Nat.lt_add_of_pos_right (n := n) ha
    · rw [add_mod_right] at hkl
      suffices k = n by contradiction
      refine ih hk ?_ hkl
      simpa using Nat.lt_add_of_pos_right (n := n) ha
    · refine ih ?_ ?_ hkl <;> simp only [Finset.mem_coe, hk, hl]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
⊢ a m ≤ monotonicSequenceLimit a

Tactic:
rcases le_or_gt m (monotonicSequenceLimitIndex a) with hm | hm

Goal state after:
case inl
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : m ≤ monotonicSequenceLimitIndex a
⊢ a m ≤ monotonicSequenceLimit a

case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
⊢ a m ≤ monotonicSequenceLimit a
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Icc a b₁ ⊆ Ico a b₂

Tactic:
rw [← coe_subset, coe_Icc, coe_Ico]
  exact Set.Icc_subset_Ico_right h

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), ↑(f (g n)) ∈ t
⊢ ∃ m n, m < n ∧ Subrel r (fun x ↦ x ∈ s ∪ t) (f m) (f n)

Tactic:
rcases ht.exists_lt hgt with ⟨m, n, hlt, hr⟩

Goal state after:
case inr
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), ↑(f (g n)) ∈ t
m n : ℕ
hlt : m < n
hr : r ↑(f (g m)) ↑(f (g n))
⊢ ∃ m n, m < n ∧ Subrel r (fun x ↦ x ∈ s ∪ t) (f m) (f n)
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr.refine_1.inr.inl
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
m : ℕ
a✝ : (f ∘ ⇑g) m ≠ (f ∘ ⇑g) m
hf : (f ∘ ⇑g) m ≤ (f ∘ ⇑g) m
⊢ False

Tactic:
contradiction

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

Goal state before:
pp: case mul
M : Type u_3
inst✝³ : Monoid M
N : Type u_7
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ x y : N
hx✝ : x ∈ closure s
hy✝ : y ∈ closure s
hx : ∃ n, r ^ n • x ∈ closure (r • s)
hy : ∃ n, r ^ n • y ∈ closure (r • s)
⊢ ∃ n, r ^ n • (x * y) ∈ closure (r • s)

Tactic:
| mul x y _ _ hx hy =>

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ [[a, b]] = [[b, a]]

Tactic:
by
  rw [uIcc, uIcc, inf_comm, sup_comm]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ((fun x ↦ (ofLex x).1) '' s).IsPWO
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ f m ≤ f n

Tactic:
isPWO_iff_exists_monotone_subseq

Goal state after:
α : 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
⊢ ∃ m n, m < n ∧ f m ≤ f n
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : 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
hc : ∀ (n : ℕ), ¬(ofLex f (g 0)).1 < (ofLex f (g n)).1
hhc : ∀ (n : ℕ), (ofLex f (g 0)).1 = (ofLex f (g n)).1
⊢ ∃ g', Monotone fun n ↦ (ofLex f (g (g' n))).2

Tactic:
isPWO_iff_exists_monotone_subseq

Goal state after:
α : 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)
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
hc : ∀ (n : ℕ), ¬(ofLex f (g 0)).1 < (ofLex f (g n)).1
hhc : ∀ (n : ℕ), (ofLex f (g 0)).1 = (ofLex f (g n)).1
hβ : ∀ (a : α) (f : ℕ → β), (∀ (n : ℕ), f n ∈ {y | toLex (a, y) ∈ s}) → ∃ g, Monotone (f ∘ ⇑g)
⊢ ∃ g', Monotone fun n ↦ (ofLex f (g (g' n))).2
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g k : G
⊢ k ∈ centralizer {g} ↔ k ∈ comap toConjAct.toMonoidHom (stabilizer (ConjAct G) g)

Tactic:
simp only [mem_centralizer_iff, Set.mem_singleton_iff, forall_eq]

Goal state after:
G : Type u_3
inst✝ : Group G
g k : G
⊢ g * k = k * g ↔ k ∈ comap toConjAct.toMonoidHom (stabilizer (ConjAct G) g)
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g k : G
⊢ k ∈ centralizer {g} ↔ k * g = g * k

Tactic:
simp only [mem_centralizer_iff, Set.mem_singleton_iff, forall_eq]

Goal state after:
G : Type u_1
inst✝ : Group G
g k : G
⊢ g * k = k * g ↔ k * g = g * k
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
g : G
⊢ (zpowers g).toSubmonoid = Submonoid.powers g ⊔ Submonoid.powers g⁻¹

Tactic:
by
  rw [zpowers_eq_closure, closure_toSubmonoid, Submonoid.closure_union,
    Submonoid.powers_eq_closure, Submonoid.powers_eq_closure, Set.inv_singleton]

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

Goal state before:
pp: case mem
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x✝ : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ i, ↑(S i)
⊢ C x

Tactic:
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx

Goal state after:
case mem
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x✝ : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ i, ↑(S i)
i : ι
hi : x ∈ ↑(S i)
⊢ C x
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case inv_mem
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x✝ : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ i, ↑(S i)
⊢ C x⁻¹

Tactic:
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx

Goal state after:
case inv_mem
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x✝ : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : x ∈ ⋃ i, ↑(S i)
i : ι
hi : x ∈ ↑(S i)
⊢ C x⁻¹
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case cons
α : Type u_3
β : Type u_4
inst✝ : Monoid β
f g : α → β
x : α
s : Finset α
hnotMem : x ∉ s
ih :
  ∀ (comm_ff : (↑s).Pairwise (Commute on f)) (comm_gg : (↑s).Pairwise (Commute on g))
    (comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)),
    s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
comm_ff : (↑(cons x s hnotMem)).Pairwise (Commute on f)
comm_gg : (↑(cons x s hnotMem)).Pairwise (Commute on g)
comm_gf : (↑(cons x s hnotMem)).Pairwise fun x y ↦ Commute (g x) (f y)
⊢ (cons x s hnotMem).noncommProd (f * g) ⋯ =
    (cons x s hnotMem).noncommProd f comm_ff * (cons x s hnotMem).noncommProd g comm_gg

Tactic:
rw [Finset.noncommProd_cons, Finset.noncommProd_cons, Finset.noncommProd_cons, Pi.mul_apply,
      ih (comm_ff.mono fun _ => mem_cons_of_mem) (comm_gg.mono fun _ => mem_cons_of_mem)
        (comm_gf.mono fun _ => mem_cons_of_mem),
      (noncommProd_commute _ _ _ _ fun y hy => ?_).mul_mul_mul_comm]

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
f g : α → β
x : α
s : Finset α
hnotMem : x ∉ s
ih :
  ∀ (comm_ff : (↑s).Pairwise (Commute on f)) (comm_gg : (↑s).Pairwise (Commute on g))
    (comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)),
    s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
comm_ff : (↑(cons x s hnotMem)).Pairwise (Commute on f)
comm_gg : (↑(cons x s hnotMem)).Pairwise (Commute on g)
comm_gf : (↑(cons x s hnotMem)).Pairwise fun x y ↦ Commute (g x) (f y)
y : α
hy : y ∈ s
⊢ Commute (g x) (f y)
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: case mul
M : Type u_1
inst✝ : CommMonoid M
x✝ : M
s : Set M
x y : M
hx✝ : x ∈ closure s
hy✝ : y ∈ closure s
hx : ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = x
hy : ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = y
⊢ ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = x * y

Tactic:
| mul x y _ _ hx hy =>

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
q : Quotient piSetoid
⊢ (fun x ↦ Quotient.mk'' fun i ↦ (x i).out) ((fun q ↦ q.liftOn' (fun x i ↦ Quotient.mk'' (x i)) ⋯) q) = q

Tactic:
induction q using Quotient.inductionOn'
    simp only [Quotient.liftOn'_mk'', Quotient.eq'']
    intro i
    change Setoid.r _ _
    rw [← Quotient.eq'']
    simp

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

Goal state before:
pp: case cons
α : Type u
L₁ L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
p : α × Bool
L₃ L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = p :: L₃ ++ L₄
h₁ : Red (p :: L₃) [(x2, b2)]
h₂ : Red L₄ L₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

Tactic:
cases eq
    change Red (L₃ ++ L₄) ([(x1, not b1), (x2, b2)] ++ L₂)
    apply append_append _ h₂
    have h₁ : Red ((x1, not b1) :: (x1, b1) :: L₃) [(x1, not b1), (x2, b2)] := cons_cons h₁
    have h₂ : Red ((x1, not b1) :: (x1, b1) :: L₃) L₃ := Step.cons_not_rev.to_red
    rcases church_rosser h₁ h₂ with ⟨L', h₁, h₂⟩
    rw [red_iff_irreducible H1] at h₁
    rwa [h₁] at h₂

Goal state after:
Module: Mathlib.GroupTheory.Coset.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x ↦ x ∈ s
x y : α
⊢ Decidable ((rightRel s) x y)

Tactic:
rw [rightRel_eq]
  exact ‹DecidablePred (· ∈ s)› _

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ : Type u
x✝ x y : FreeGroup α✝
ihx : id <$> x = x
ihy : id <$> y = y
⊢ id <$> x * id <$> y = x * y

Tactic:
ihx,

Goal state after:
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β α✝ : Type u
x✝ x y : FreeGroup α✝
ihx : id <$> x = x
ihy : id <$> y = y
⊢ x * id <$> y = x * y
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
⊢ ∏ k ∈ range 1, f k = f 0

Tactic:
range_one,

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
⊢ ∏ k ∈ {0}, f k = f 0
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : κ → ι
g : ι → M
I : Finset κ
hf : (↑I).Pairwise fun i j ↦ f i = f j → g (f i) = 1
⊢ ∏ s ∈ image f I, g s = ∏ i ∈ I, g (f i)

Tactic:
rw [prod_image']

Goal state after:
case eq
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : κ → ι
g : ι → M
I : Finset κ
hf : (↑I).Pairwise fun i j ↦ f i = f j → g (f i) = 1
⊢ ∀ i ∈ I, g (f i) = ∏ j ∈ I with f j = f i, g (f j)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ : Type u
x✝ x y : FreeAbelianGroup α✝
ihx : id <$> x = x
ihy : id <$> y = y
⊢ id <$> x + id <$> y = x + y

Tactic:
ihx,

Goal state after:
α : Type u
G : Type u_1
β α✝ : Type u
x✝ x y : FreeAbelianGroup α✝
ihx : id <$> x = x
ihy : id <$> y = y
⊢ x + id <$> y = x + y
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f) + (y >>= f) >>= g = x + y >>= fun x ↦ f x >>= g

Tactic:
ihx,

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f) + (y >>= f) >>= g = x + y >>= fun x ↦ f x >>= g
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f >>= g) + (y >>= f >>= g) = x + y >>= fun x ↦ f x >>= g

Tactic:
ihx,

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= fun x ↦ f x >>= g) + (y >>= f >>= g) = x + y >>= fun x ↦ f x >>= g
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
α : Type u_5
inst✝ : CommMonoid M
m : Multiset ι
s : Finset α
f : ι → α → M
⊢ (map (fun i ↦ ∏ a ∈ s, f i a) m).prod = ∏ a ∈ s, (map (fun i ↦ f i a) m).prod

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih => simp [Finset.prod_insert ha, prod_map_mul, ih]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅H, ⊤⁆ = ⊥ ↔ H ≤ center G

Tactic:
rw [commutator_eq_bot_iff_le_centralizer, coe_top, centralizer_univ]

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

Goal state before:
pp: case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
rw [prod_le_iff]

Goal state after:
case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆ ∧
    map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ commutator G = closure (commutatorSet G)

Tactic:
by
  simp [commutator, Subgroup.commutator_def, commutatorSet]

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

Goal state before:
pp: case mpr
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
⊢ (∃ a ∈ S, ∃ v, a * y.1 = v * x.1 ∧ a * ↑y.2 = v * ↑x.2) → ∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)

Tactic:
rintro ⟨u, hu, v, e₁, e₂⟩

Goal state after:
case mpr
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
u : M
hu : u ∈ S
v : M
e₁ : u * y.1 = v * x.1
e₂ : u * ↑y.2 = v * ↑x.2
⊢ ∃ a ∈ S, a * (↑y.2 * x.1) = a * (↑x.2 * y.1)
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 : ↥S
⊢ f.mk' x₂ y * f x₁ = f.mk' (x₁ * x₂) y

Tactic:
rw [mul_comm, mul_mk'_eq_mk'_of_mul]

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R ≃+* S
x : R
⊢ f x = -1 ↔ x = -1

Tactic:
rw [← neg_eq_iff_eq_neg, ← neg_eq_iff_eq_neg, ← map_neg, RingEquiv.map_eq_one_iff]

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

Goal state before:
pp: case inr.inr.inr.coe
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
b c : WithTop α
hb : b ≠ 0
hc : c ≠ 0
a : α
ha : ↑a ≠ 0
⊢ ↑a * b * c = ↑a * (b * c)

Tactic:
cases b with | top => simp [mul_top ha, top_mul hc] | coe b => ?_

Goal state after:
case inr.inr.inr.coe.coe
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : SemigroupWithZero α
inst✝ : NoZeroDivisors α
c : WithTop α
hc : c ≠ 0
a : α
ha : ↑a ≠ 0
b : α
hb : ↑b ≠ 0
⊢ ↑a * ↑b * c = ↑a * (↑b * c)
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case inr
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
nh : ¬v₂ ≤ v₁
h : v₂ ≤ v₁
⊢ v₁ < v₂

Tactic:
contradiction

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsLUB s a
ha : a ∉ s
b : α
hb : b ⋖ a
hc : a ∈ s
hbc : b < a
hca : a ≤ a
⊢ False

Tactic:
contradiction

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
s : Set α
b : α
hb : b ∈ s
hs : IsLUB s b
ha : b ∉ s
⊢ ¬IsMin b

Tactic:
contradiction

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b : α
⊢ a ≤ b → ∃ n, pred^[n] b = a

Tactic:
by
    refine WellFounded.fix (C := fun b => a ≤ b → ∃ n, Nat.iterate pred n b = a)
      h.wf ?_ b
    intro b ih hab
    replace hab := eq_or_lt_of_le hab
    rcases hab with (rfl | hab)
    · exact ⟨0, rfl⟩
    rcases eq_or_lt_of_le (pred_le b) with hb | hb
    · cases (min_of_le_pred hb.ge).not_lt hab
    obtain ⟨k, hk⟩ := ih (pred b) hb (le_pred_of_lt hab)
    refine ⟨k + 1, ?_⟩
    rw [iterate_add_apply, iterate_one, hk]

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

Goal state before:
pp: case succ
m n n✝ : ℕ
ha : n✝ + 1 ≤ (n✝ + 1).pred
⊢ IsMin (n✝ + 1)

Tactic:
· exact (not_succ_le_self _ ha).elim

Goal state after:
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∈ s
⊢ pred^[n] ⟨pred ↑⟨c, hc⟩, h⟩ = ⟨b, hb⟩

Tactic:
dsimp only at h ⊢
        apply hi _ _ _ hn
        · rw [← hn]
          apply Order.pred_iterate_le

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

Goal state before:
pp: case none
hx : none < ⊤
⊢ lift none hx = toNat none

Tactic:
contradiction

Goal state after:
Module: Mathlib.Data.Countable.Small

Goal state before:
pp: α : Type v
h : ¬Small.{w, v} α
⊢ ¬Countable α

Tactic:
exact mt (@Countable.toSmall α) h

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

Goal state before:
pp: κ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : Finset α
u : Finset κ
f : γ → α → κ → β
⊢ ∏ x ∈ s, ∏ y ∈ t, ∏ z ∈ u, f x y z = ∏ z ∈ u, ∏ x ∈ s, ∏ y ∈ t, f x y z

Tactic:
simp_rw [prod_comm (s := t), prod_comm (s := s)]

Goal state after:
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
n : ℕ
h : [].length = n.succ
⊢ cons (head ⟨[], h⟩) (tail ⟨[], h⟩) = ⟨[], h⟩

Tactic:
contradiction

Goal state after: