mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ decode n = (decode (unpair n).1).bind fun a ↦ Option.map (Prod.mk a) (decode (unpair n).2)

Tactic:
simp only [decode_ofEquiv, Equiv.symm_symm, decode_sigma_val]
  cases (decode n.unpair.1 : Option α) <;> cases (decode n.unpair.2 : Option β)
  <;> rfl

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Group G''
A : Type u_4
inst✝ : AddGroup A
s : Set G
H : Subgroup G
a : G
h : a ∈ H.normalCore
b c : G
⊢ c * (b * a * b⁻¹) * c⁻¹ ∈ H

Tactic:
rw [mul_assoc, mul_assoc, ← mul_inv_rev, ← mul_assoc, ← mul_assoc]

Goal state after:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : Group G''
A : Type u_4
inst✝ : AddGroup A
s : Set G
H : Subgroup G
a : G
h : a ∈ H.normalCore
b c : G
⊢ c * b * a * (c * b)⁻¹ ∈ H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
s : Set G
f : G →* N
⊢ normalClosure s ≤ comap f (normalClosure (⇑f '' s))

Tactic:
by
  simp [normalClosure_le_normal, ← Set.image_subset_iff, subset_normalClosure]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case inl
M : Type u_3
inst✝² : Monoid M
inst✝¹ : Preorder M
inst✝ : CanonicallyOrderedMul M
L : List M
n : ℕ
h : n < L.length
⊢ (take n L).prod ≤ (take (n + 1) L).prod

Tactic:
rw [prod_take_succ _ _ h]
    exact le_self_mul

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ ↑(closure s) = List.prod '' {l | ∀ x ∈ l, x ∈ s}

Tactic:
by
  rw [closure_eq_mrange, coe_mrange, ← Set.range_list_map_coe, ← Set.range_comp]
  exact congrArg _ (funext <| FreeMonoid.lift_apply _)

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

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * (Int.negSucc m % ↑n).toNat) = x ^ (k * ((↑m.succ % ↑n).toNat * (n - 1)))

Tactic:
Int.negSucc_eq,

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
m k : ℕ
⊢ x ^ (k * (-(↑m + 1) % ↑n).toNat) = x ^ (k * ((↑m.succ % ↑n).toNat * (n - 1)))
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
⊢ ∀ {a m : α} {o : Option α}, a ∈ l → m ∈ foldl (argAux r) o l → ¬r a m

Tactic:
induction l using List.reverseRecOn with
  | nil => simp
  | append_singleton tl a ih => ?_

Goal state after:
case append_singleton
α : Type u_1
r : α → α → Prop
inst✝ : DecidableRel r
l : List α
hr₀ : Std.Irrefl r
hr₁ : IsTrans α r
tl : List α
a : α
ih : ∀ {a m : α} {o : Option α}, a ∈ tl → m ∈ foldl (argAux r) o tl → ¬r a m
⊢ ∀ {a_1 m : α} {o : Option α}, a_1 ∈ tl ++ [a] → m ∈ foldl (argAux r) o (tl ++ [a]) → ¬r a_1 m
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m : α
hm : m ∈ argmax f (hd :: tl)
a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
⊢ idxOf m (hd :: tl) ≤ idxOf a (hd :: tl)

Tactic:
simp only [idxOf_cons, argmax_cons, Option.mem_def] at hm ⊢

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder β
f : α → β
inst✝ : DecidableEq α
hd : α
tl : List α
m a : α
ha : a ∈ hd :: tl
ham : f m ≤ f a
hm : Option.rec (some hd) (fun val ↦ if f hd < f val then some val else some hd) (argmax f tl) = some m
⊢ (bif hd == m then 0 else idxOf m tl + 1) ≤ bif hd == a then 0 else idxOf a tl + 1
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
⊢ (map inl s).card + (map inr t).card = s.card + t.card

Tactic:
card_map,

Goal state after:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
⊢ s.card + (map inr t).card = s.card + t.card
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
inst✝¹ : Denumerable α
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ some (ofNat (Sigma γ) n) = some ⟨ofNat α (unpair n).1, ofNat (γ (ofNat α (unpair n).1)) (unpair n).2⟩

Tactic:
← decode_eq_ofNat,

Goal state after:
α : Type u_1
inst✝¹ : Denumerable α
γ : α → Type u_3
inst✝ : (a : α) → Denumerable (γ a)
n : ℕ
⊢ decode n = some ⟨ofNat α (unpair n).1, ofNat (γ (ofNat α (unpair n).1)) (unpair n).2⟩
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ Disjoint (map Embedding.inl s) (map Embedding.inr t)

Tactic:
simp_rw [disjoint_left, mem_map]
  rintro x ⟨a, _, rfl⟩ ⟨b, _, ⟨⟩⟩

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

Goal state before:
pp: α : Type u
l : List α
⊢ l.revzip.reverse = l.reverse.revzip

Tactic:
← zip_unzip (revzip l).reverse

Goal state after:
α : Type u
l : List α
⊢ l.revzip.reverse.unzip.fst.zip l.revzip.reverse.unzip.snd = l.reverse.revzip
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (powersetAux l).revzip
⊢ x.1 + x.2 = ↑l

Tactic:
rw [revzip, powersetAux_eq_map_coe, ← map_reverse, zip_map, ← revzip, List.mem_map] at h

Goal state after:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : ∃ a, a ∈ l.sublists.revzip ∧ Prod.map ofList ofList a = x
⊢ x.1 + x.2 = ↑l
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
s t : List α
⊢ s ∈ t.sublists ↔ s.reverse <+ t.reverse

Tactic:
← mem_sublists',

Goal state after:
α : Type u
s t : List α
⊢ s ∈ t.sublists ↔ s.reverse ∈ t.reverse.sublists'
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
s₁ s₂ : Finset β
f : β → α
inst✝ : DecidableEq β
c : α
⊢ (s₁ ∪ s₂).sup f ≤ c ↔ s₁.sup f ⊔ s₂.sup f ≤ c

Tactic:
by simp [or_imp, forall_and]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : DecidableEq β
s₁ s₂ : Finset β
h₁ : s₁.Nonempty
h₂ : s₂.Nonempty
f : β → α
a : α
⊢ (s₁ ∪ s₂).sup' ⋯ f ≤ a ↔ s₁.sup' h₁ f ⊔ s₂.sup' h₂ f ≤ a

Tactic:
by simp [or_imp, forall_and]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : SemilatticeSup α
s : Finset β
H : s.Nonempty
t : Finset β
f g : β → α
h₁ : s = t
h₂ : ∀ x ∈ s, f x = g x
⊢ s.sup' H f = t.sup' ⋯ g

Tactic:
by
  subst s
  refine eq_of_forall_ge_iff fun c => ?_
  simp +contextual only [sup'_le_iff, h₂]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ a < s.sup' H f ↔ ∃ b ∈ s, a < f b

Tactic:
by
  rw [← WithBot.coe_lt_coe, coe_sup', Finset.lt_sup_iff]
  exact exists_congr (fun _ => and_congr_right' WithBot.coe_lt_coe)

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg.inl
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
h✝ : IsEmpty ι
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

Tactic:
simp [h, iSup_of_empty', ciSup_const]

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case neg.inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
h✝ : Nonempty ι
⊢ ⨆ (ih : Exists p), f ih ≤ ⨆ i, ⨆ (h : p i), f ⋯

Tactic:
simp [h, iSup_of_empty', ciSup_const]

Goal state after:
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : x ∉ t
⊢ ⨆ i ∈ insert x t, update f x s i = s ⊔ ⨆ i ∈ t, f i

Tactic:
rw [Finset.iSup_insert]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CompleteLattice β
inst✝ : DecidableEq α
x : α
t : Finset α
f : α → β
s : β
hx : x ∉ t
⊢ update f x s x ⊔ ⨆ x_1 ∈ t, update f x s x_1 = s ⊔ ⨆ i ∈ t, f i
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case mpr
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
n : α
this : OrderBot α
⊢ ((∃ i, f i = n) ∧ ∀ (i : ι), n ≤ f i) → ⨅ i, f i = n

Tactic:
rintro ⟨⟨i, rfl⟩, h⟩
    exact le_antisymm (ciInf_le (OrderBot.bddBelow ..) _) (le_ciInf h)

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ico a b = 0 ↔ ¬a < b

Tactic:
rw [Ico, Finset.val_eq_zero, Finset.Ico_eq_empty_iff]

Goal state after:
Module: Mathlib.Order.Lattice.Nat

Goal state before:
pp: s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ sInf s ≤ m

Tactic:
by
  classical
  rw [Nat.sInf_def ⟨m, hm⟩]
  exact Nat.find_min' ⟨m, hm⟩ hm

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

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIci : α → Finset α
mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x
a x : α
⊢ x ∈ {x ∈ finsetIci a | a ≠ x} ↔ a < x

Tactic:
rw [mem_filter, mem_Ici, lt_iff_le_and_ne]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ ∃ g, (∀ (n : ℕ), e (g n) ∈ s) ∨ ∀ (n : ℕ), e (g n) ∈ t

Tactic:
have : Infinite (e ⁻¹' s) ∨ Infinite (e ⁻¹' t) := by
      simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
        Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]

Goal state after:
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
this : Infinite ↑(e ⁻¹' s) ∨ Infinite ↑(e ⁻¹' t)
⊢ ∃ g, (∀ (n : ℕ), e (g n) ∈ s) ∨ ∀ (n : ℕ), e (g n) ∈ t
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: n a : ℕ
⊢ image (fun x ↦ x % a) (Ico n (n + a)) = range a

Tactic:
by
  obtain rfl | ha := eq_or_ne a 0
  · rw [range_zero, add_zero, Ico_self, image_empty]
  ext i
  simp only [mem_image, mem_range, mem_Ico]
  constructor
  · rintro ⟨i, _, rfl⟩
    exact mod_lt i ha.bot_lt
  intro hia
  have hn := Nat.mod_add_div n a
  obtain hi | hi := lt_or_ge i (n % a)
  · refine ⟨i + a * (n / a + 1), ⟨?_, ?_⟩, ?_⟩
    · rw [add_comm (n / a), Nat.mul_add, mul_one, ← add_assoc]
      refine hn.symm.le.trans (Nat.add_le_add_right ?_ _)
      simpa only [zero_add] using add_le_add (zero_le i) (Nat.mod_lt n ha.bot_lt).le
    · refine lt_of_lt_of_le (Nat.add_lt_add_right hi (a * (n / a + 1))) ?_
      rw [Nat.mul_add, mul_one, ← add_assoc, hn]
    · rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]
  · refine ⟨i + a * (n / a), ⟨?_, ?_⟩, ?_⟩
    · lia
    · lia
    · rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt hia]

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

Goal state before:
pp: a : ℕ
⊢ (range' 1 a).toFinset = Icc 1 a

Tactic:
by
  ext x
  rw [List.mem_toFinset, List.mem_range'_1, add_comm, Nat.lt_succ_iff, Finset.mem_Icc]

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case refine_2
ι : Type u_3
α : ι → Type u_4
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
hr : ∀ (i : ι), WellQuasiOrdered (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (f : ℕ → (i : ι) → α i), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
f : ℕ → (i : ι) → α i
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r i (f (g m) i) (f (g n) i)
g' : ℕ ↪o ℕ
hg' : ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s, r i (((f ∘ ⇑g) ∘ ⇑g') a i) (((f ∘ ⇑g) ∘ ⇑g') b i)
a b : ℕ
hab : a ≤ b
⊢ r i ((f ∘ ⇑(RelEmbedding.trans g' g)) a i) ((f ∘ ⇑(RelEmbedding.trans g' g)) b i) ∧
    ∀ x ∈ s, r x ((f ∘ ⇑(RelEmbedding.trans g' g)) a x) ((f ∘ ⇑(RelEmbedding.trans g' g)) b x)

Tactic:
exact ⟨hg _ _ (OrderHomClass.mono g' hab), hg' hab⟩

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_1
α : Type u_2
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
inst✝ : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
⊢ m = n

Tactic:
obtain h | h | h := lt_trichotomy m n
    · refine (H _ _ h ?_).elim
      rw [hmn]
      exact refl _
    · exact h
    · refine (H _ _ h ?_).elim
      rw [hmn]
      exact refl _

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : Preorder α
inst✝³ : PartialOrder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b : α
c : β
⊢ map (Embedding.sectL α c) (Ioc a b) = Ioc (a, c) (b, c)

Tactic:
by
  aesop (add safe forward [le_antisymm, le_of_lt])

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : Preorder α
inst✝³ : PartialOrder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b : α
c : β
⊢ map (Embedding.sectL α c) (Ico a b) = Ico (a, c) (b, c)

Tactic:
by
  aesop (add safe forward [le_antisymm, le_of_lt])

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : Preorder α
inst✝³ : PartialOrder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
a b : α
c : β
⊢ map (Embedding.sectL α c) (Ioo a b) = Ioo (a, c) (b, c)

Tactic:
by
  aesop (add safe forward [le_antisymm, le_of_lt])

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
c : α
a b : β
⊢ map (Embedding.sectR c β) (Ioc a b) = Ioc (c, a) (c, b)

Tactic:
by
  aesop (add safe forward [le_antisymm, le_of_lt])

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
c : α
a b : β
⊢ map (Embedding.sectR c β) (Ico a b) = Ico (c, a) (c, b)

Tactic:
by
  aesop (add safe forward [le_antisymm, le_of_lt])

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableLE (α × β)
c : α
a b : β
⊢ map (Embedding.sectR c β) (Ioo a b) = Ioo (c, a) (c, b)

Tactic:
by
  aesop (add safe forward [le_antisymm, le_of_lt])

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ∈ (Iic b).erase b ↔ a✝ ∈ Iio b

Tactic:
simp_rw [Finset.mem_erase, mem_Iic, mem_Iio, lt_iff_le_and_ne, and_comm]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderBot α
b : α
⊢ Iic b = cons b (Iio b) ⋯

Tactic:
by
  classical rw [cons_eq_insert, Iio_insert]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
t : Finset ι
hi : i ∉ t
ih :
  ∀ (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
f : ℕ → (i : ι) → α i
hf : ∀ (n : ℕ) (i : ι), f n i ∈ s i
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r i (f (g m) i) (f (g n) i)
g' : ℕ ↪o ℕ
hg' : ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i (((f ∘ ⇑g) ∘ ⇑g') a i) (((f ∘ ⇑g) ∘ ⇑g') b i)
a b : ℕ
hab : a ≤ b
⊢ r i ((f ∘ ⇑(RelEmbedding.trans g' g)) a i) ((f ∘ ⇑(RelEmbedding.trans g' g)) b i) ∧
    ∀ x ∈ t, r x ((f ∘ ⇑(RelEmbedding.trans g' g)) a x) ((f ∘ ⇑(RelEmbedding.trans g' g)) b x)

Tactic:
exact ⟨hg _ _ (OrderHomClass.mono g' hab), hg' hab⟩

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
g h : G
⊢ h ∈ normalizer {g} → h ∈ centralizer {g}

Tactic:
rintro hh g rfl
    exact mul_eq_of_eq_mul_inv (hh g |>.mp rfl).symm

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
Hs : Set (Subgroup G)
h : ∀ H ∈ Hs, H.Normal
⊢ (sSup Hs).Normal

Tactic:
rw [sSup_eq_iSup]

Goal state after:
G : Type u_2
inst✝ : Group G
Hs : Set (Subgroup G)
h : ∀ H ∈ Hs, H.Normal
⊢ (⨆ a ∈ Hs, a).Normal
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
l : List α
f : α → β
comm : (↑l.toFinset).Pairwise (Commute on f)
hl : l.Nodup
⊢ l.toFinset.noncommProd f comm = (List.map f l).prod

Tactic:
← List.dedup_eq_self

Goal state after:
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
l : List α
f : α → β
comm : (↑l.toFinset).Pairwise (Commute on f)
hl : l.dedup = l
⊢ l.toFinset.noncommProd f comm = (List.map f l).prod
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ s.noncommProd f comm = m ^ #s

Tactic:
rw [noncommProd, Multiset.noncommProd_eq_pow_card _ _ m]
  · simp only [Finset.card_def, Multiset.card_map]
  · simpa using h

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c d y : Con M
x : M → M → Prop
iseqv✝ : Equivalence x
mul'✝ :
  ∀ {w x_1 y z : M},
    { r := x, iseqv := iseqv✝ } w x_1 → { r := x, iseqv := iseqv✝ } y z → { r := x, iseqv := iseqv✝ } (w * y) (x_1 * z)
h : (fun c ↦ ⇑c.toSetoid) { r := x, iseqv := iseqv✝, mul' := mul'✝ } = (fun c ↦ ⇑c.toSetoid) y
⊢ { r := x, iseqv := iseqv✝, mul' := mul'✝ } = y

Tactic:
rcases y with ⟨⟨y, _⟩, _⟩

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
c d : Con M
x : M → M → Prop
iseqv✝¹ : Equivalence x
mul'✝¹ :
  ∀ {w x_1 y z : M},
    { r := x, iseqv := iseqv✝¹ } w x_1 →
      { r := x, iseqv := iseqv✝¹ } y z → { r := x, iseqv := iseqv✝¹ } (w * y) (x_1 * z)
y : M → M → Prop
iseqv✝ : Equivalence y
mul'✝ :
  ∀ {w x y_1 z : M},
    { r := y, iseqv := iseqv✝ } w x → { r := y, iseqv := iseqv✝ } y_1 z → { r := y, iseqv := iseqv✝ } (w * y_1) (x * z)
h :
  (fun c ↦ ⇑c.toSetoid) { r := x, iseqv := iseqv✝¹, mul' := mul'✝¹ } =
    (fun c ↦ ⇑c.toSetoid) { r := y, iseqv := iseqv✝, mul' := mul'✝ }
⊢ { r := x, iseqv := iseqv✝¹, mul' := mul'✝¹ } = { r := y, iseqv := iseqv✝, mul' := mul'✝ }
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L' : List (α × Bool)
eq : [(x1, !b1), (x2, b2)] = L'
⊢ ∀ (b : List (α × Bool)), ¬Step L' b

Tactic:
intro L h'

Goal state after:
α : Type u
L✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L' : List (α × Bool)
eq : [(x1, !b1), (x2, b2)] = L'
L : List (α × Bool)
h' : Step L' L
⊢ False
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∈ s
h₂ : b ∉ s
⊢ ∏ x ∈ s, f x = f a

Tactic:
apply prod_eq_single_of_mem a h₁

Goal state after:
case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
h₁ : a ∈ s
h₂ : b ∉ s
⊢ ∀ b ∈ s, b ≠ a → f b = 1
Module: Mathlib.GroupTheory.OreLocalization.OreSet

Goal state before:
pp: R✝ : Type u_1
inst✝² : Monoid R✝
S✝ : Submonoid R✝
inst✝¹ : OreSet S✝
R : Type ?u.10
inst✝ : CommMonoid R
S : Submonoid R
m n : R
s : ↥S
h : m * ↑s = n * ↑s
⊢ ↑s * m = ↑s * n

Tactic:
by rw [mul_comm (s : R) n, mul_comm (s : R) m, 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
inst✝ : Unique ι
f : ι → M
⊢ ∏ x, f x = f default

Tactic:
rw [univ_unique, prod_singleton]

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

Goal state before:
pp: case left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅f g₁, f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆

Tactic:
intro p hp q hq
    exact commutator_mem_commutator (mem_map_of_mem _ hp) (mem_map_of_mem _ hq)

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

Goal state before:
pp: case hx
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ map f ⊤ = f.range

Tactic:
Subgroup.map_eq_range_iff

Goal state after:
case hx
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ Codisjoint ⊤ f.ker
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case hy
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ map f ⊤ = f.range

Tactic:
Subgroup.map_eq_range_iff

Goal state after:
case hy
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ Codisjoint ⊤ f.ker
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : AddCommGroup α
inst✝⁴ : PartialOrder α
inst✝³ : IsOrderedAddMonoid α
inst✝² : AddCommGroup β
inst✝¹ : PartialOrder β
inst✝ : IsOrderedAddMonoid β
i : FunLike F α β
f : F
iamhc : AddMonoidHomClass F α β
h : ∀ (a : α), 0 ≤ a → 0 ≤ f a
a b : α
hl : a ≤ b
⊢ f a ≤ f (b - a) + f a

Tactic:
exact le_add_of_nonneg_left (h _ <| sub_nonneg.2 hl)

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

Goal state before:
pp: case h.right
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
this : r₃ * v * ↑s₂ = ↑s₃ * v₀ * ↑s₂
s₄ : ↥S
hs₄ : ↑s₄ * (r₃ * v) = ↑s₄ * (↑s₃ * v₀)
⊢ ↑s₄ * (r₃ * ↑u) * ↑s₁ = ↑s₄ * r₃ * (↑u * ↑s₁)

Tactic:
simp only [mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
⊢ ↑s₄' * r₃' * (↑s₂' * ↑s) ∈ S

Tactic:
rw [mul_assoc, ← mul_assoc r₃', ← h₃]

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
⊢ ↑s₄' * (↑s₃' * ↑s₁' * ↑s) ∈ S
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
⊢ r /ₒ s * 1 = r /ₒ s

Tactic:
simp [OreLocalization.one_def, oreDiv_mul_char r (1 : R) s (1 : S) r 1 (by simp)]

Goal state after: