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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ Set.range ⇑(FreeMonoid.lift Subtype.val) = List.prod '' Set.range (List.map Subtype.val)

Tactic:
← Set.range_comp

Goal state after:
M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ Set.range ⇑(FreeMonoid.lift Subtype.val) = Set.range (List.prod ∘ List.map Subtype.val)
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
⊢ ∀ (a : Lex (α × β)), ∃ b, a < b

Tactic:
rw [Lex.forall, Prod.forall]
    intro a b
    obtain ⟨c, h⟩ := exists_gt b
    use toLex (a, c)
    simpa [lt_iff]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
n : ℕ
b : α
h : decode n = some b
⊢ ofNat α n = b

Tactic:
simpa using h

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: case bot
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x ↦ x ∈ s
x : ℕ
hx : x ∈ s
t : List ↑s := List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
ht : t = List.pmap (fun y hy ↦ ⟨y, hy⟩) (List.filter (fun y ↦ decide (y ∈ s)) (List.range x)) ⋯
hmt : ∀ {y : ↑s}, y ∈ t ↔ y < ⟨x, hx⟩
hmax : t.maximum = ⊥
⊢ ∃ a, ofNat s a = ⟨x, hx⟩

Tactic:
| bot =>

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

Goal state before:
pp: case bot
α : Type u_1
inst✝ : LinearOrder α
l : List α
d : α
hy : l.maximum = ⊥
⊢ l.max?.getD d = WithBot.unbotD d ⊥

Tactic:
| bot =>

Goal state after:
Module: Mathlib.Data.Multiset.Powerset

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

Tactic:
powersetAux_eq_map_coe,

Goal state after:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (List.map ofList l.sublists).zip (List.map ofList l.sublists).reverse
⊢ x.1 + x.2 = ↑l
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ (l ++ [a]).sublists = l.sublists ++ map (fun x ↦ x ++ [a]) l.sublists

Tactic:
sublists_append,

Goal state after:
α : Type u
l : List α
a : α
⊢ (do
      let x ← [a].sublists
      map (fun x_1 ↦ x_1 ++ x) l.sublists) =
    l.sublists ++ map (fun x ↦ x ++ [a]) l.sublists
Module: Mathlib.Data.List.Sublists

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

Tactic:
reverse_reverse

Goal state after:
α : Type u
l : List α
⊢ l.sublists = l.sublists
Module: Mathlib.Data.List.Sublists

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

Tactic:
reverse_reverse

Goal state after:
α : Type u
l : List α
⊢ l.sublists' = l.sublists'
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l l' : List α
h : l' <+ l
⊢ l' ∈ sublistsLen l'.length l

Tactic:
induction h with
  | slnil => simp
  | @cons l₁ l₂ a s IH =>
    rcases l₁ with - | ⟨b, l₁⟩
    · simp
    · rw [length, sublistsLen_succ_cons]
      exact mem_append_left _ IH
  | cons_cons a s IH =>
    rw [length, sublistsLen_succ_cons]
    exact mem_append_right _ (mem_map.2 ⟨_, IH, rfl⟩)

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

Goal state before:
pp: α : Type u
l₁ l₂ : List α
h : (l₁, l₂) ∈ [].sublists.zip [].sublists.reverse
⊢ l₁ = [] ∧ l₂ = []

Tactic:
simpa using h

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

Goal state before:
pp: case inr
α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∈ s
ha' : a ≠ ⊥
⊢ id a ≤ (s.erase ⊥).sup id

Tactic:
· exact le_sup (mem_erase.2 ⟨ha', ha⟩)

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
ha : ∃ i, ∃ (_ : i ∈ s), a ∈ g i
hb : ∃ i, ∃ (_ : i ∈ s), b ∈ g i
⊢ (Disjoint on f) a b

Tactic:
obtain ⟨c, hc, ha⟩ := ha

Goal state after:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
hb : ∃ i, ∃ (_ : i ∈ s), b ∈ g i
c : ι'
hc : c ∈ s
ha : a ∈ g c
⊢ (Disjoint on f) a b
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++ flatMap (fun a ↦ sublistsLen (a + 1) tl) (range tl.length) ~ tl.sublists'

Tactic:
← List.flatMap_map Nat.succ fun n => sublistsLen n tl,

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ sublistsLen 0 tl ++ flatMap (fun n ↦ sublistsLen n tl) (map succ (range tl.length)) ~ tl.sublists'
Module: Mathlib.Data.Fintype.Option

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
this : (n : ℕ) → Trunc (P (ULift.{u, 0} (Fin n)))
⊢ Trunc (P α)

Tactic:
apply Trunc.bind (this (Fintype.card α))
    intro h
    apply Trunc.map _ (Fintype.truncEquivFin α)
    intro e
    exact of_equiv (Equiv.ulift.trans e.symm) h

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

Goal state before:
pp: case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
h✝ : Nonempty ι
⊢ ⨆ x, f x ⊔ g x = (⨆ x, f x) ⊔ ⨆ x, g x

Tactic:
apply le_antisymm <| ciSup_le fun x ↦ sup_le_sup (le_ciSup Hf x) (le_ciSup Hg x)

Goal state after:
case inr
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLattice α
f g : ι → α
Hf : BddAbove (range f)
Hg : BddAbove (range g)
h✝ : Nonempty ι
⊢ iSup f ⊔ iSup g ≤ ⨆ x, f x ⊔ g x
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some ⁻¹' Ioo ↑a ↑b = Ioo a b

Tactic:
by simp [← Ioi_inter_Iio]

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, sSup ∅ ≤ f x
⊢ ∃ x ∈ l.toFinset, sSup ∅ ≤ f x

Tactic:
simpa using h

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, f x ≤ sInf ∅
⊢ ∃ x ∈ l.toFinset, f x ≤ sInf ∅

Tactic:
simpa using h

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ∃ x ∈ s.toFinset, sSup ∅ ≤ f x

Tactic:
simpa using h

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Multiset ι
f : ι → α
h : ∃ x ∈ s, f x ≤ sInf ∅
⊢ ∃ x ∈ s.toFinset, f x ≤ sInf ∅

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = max (iSup f) (sSup ∅)

Tactic:
rcases le_or_gt (sSup ∅) (iSup f) with le | gt
  · rw [max_eq_left le]
    by_cases bdd : BddAbove (range f)
    · rw [← ciSup_subtype bdd le]
    · rw [ciSup_of_not_bddAbove bdd, cbiSup_of_not_bddAbove bdd]
  have ⟨i, hi⟩ := not_forall.mp hp
  have : Nonempty ι := ⟨i⟩
  have bdd : BddAbove (range f) := not_not.mp fun h ↦ gt.ne (ciSup_of_not_bddAbove h)
  rw [max_eq_right gt.le]
  refine ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j ↦ ?_) ?_
  · by_cases hj : p j
    · exact ((ciSup_pos hj).trans_le (le_ciSup bdd ⟨j, hj⟩)).trans gt.le
    · exact (ciSup_neg hj).le
  · exact fun w hw ↦ ⟨i, hw.trans_eq (ciSup_neg hi).symm⟩

Goal state after:
Module: Mathlib.Data.Finset.Preimage

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : DecidableEq β
f : α → β
s : Finset β
inst✝ : (x : β) → Decidable (x ∈ Set.range f)
hf : InjOn f (f ⁻¹' ↑s)
⊢ ↑(image f (s.preimage f hf)) = ↑({x ∈ s | x ∈ Set.range f})

Tactic:
simp only [coe_image, coe_preimage, coe_filter, Set.image_preimage_eq_inter_range,
      ← Set.sep_mem_eq]

Goal state after:
α : Type u
β : Type v
inst✝¹ : DecidableEq β
f : α → β
s : Finset β
inst✝ : (x : β) → Decidable (x ∈ Set.range f)
hf : InjOn f (f ⁻¹' ↑s)
⊢ {x | x ∈ ↑s ∧ x ∈ Set.range f} = {x | x ∈ s ∧ x ∈ Set.range f}
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
x : α
s : Set α
inst✝ : Preorder α
h : s.Subsingleton
⊢ Minimal (fun x ↦ x ∈ s) x ↔ x ∈ s

Tactic:
obtain (rfl | ⟨x, rfl⟩) := h.eq_empty_or_singleton <;> simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ (Finset.Ico a b \ Finset.Ico c b).val = (Finset.Ico a (min b c)).val

Tactic:
Finset.Ico_sdiff_Ico_right

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ (Finset.Ico a (min b c)).val = (Finset.Ico a (min b c)).val
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b c : ℕ
h : c ≤ a
x : ℕ
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ a_1 - c = x) ↔ a - c ≤ x ∧ x < b - c

Tactic:
refine ⟨?_, fun h ↦ ⟨x + c, by lia⟩⟩

Goal state after:
a b c : ℕ
h : c ≤ a
x : ℕ
⊢ (∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ a_1 - c = x) → a - c ≤ x ∧ x < b - c
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n : ℕ
⊢ P n

Tactic:
apply Nat.cauchy_induction h _ hs (k * ·) fun x hl hP => ⟨_, hm x hl hP⟩

Goal state after:
P : ℕ → Prop
h : ∀ (n : ℕ), P (n + 1) → P n
k seed : ℕ
hk : 1 < k
hs : P seed.succ
hm : ∀ (x : ℕ), seed < x → P x → P (k * x)
n : ℕ
⊢ ∀ (x : ℕ), seed.succ ≤ x → P x → x < k * x
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a : α
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
β : Type u_3
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
f : α → β
hf : Monotone f
x✝ : α
h : x✝ ∈ Iic a
⊢ x✝ ≤ a

Tactic:
simpa using h

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

Goal state before:
pp: case mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x ↦ g • x) u = a
⊢ a ∈ f ⁻¹' f '' U

Tactic:
Set.mem_preimage,

Goal state after:
case mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
U : Set α
this : Setoid α := orbitRel G α
f : α → Quotient (orbitRel G α) := Quotient.mk'
a : α
g : G
u : α
hu₁ : u ∈ U
hu₂ : (fun x ↦ g • x) u = a
⊢ f a ∈ f '' U
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
x : Quotient G α
⊢ Set.MapsTo (fun x ↦ g • x) x.orbit x.orbit

Tactic:
by
  rw [orbitRel.Quotient.orbit_eq_orbit_out x Quotient.out_eq']
  exact mapsTo_smul_orbit g x.out

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

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
hb : b ∈ MulAction.orbit ↥H ⟦a⟧.out
⊢ Quotient.mk'' a = Quotient.mk'' ⟦a⟧.out

Tactic:
Quotient.out_eq',

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : Subgroup G
x : Quotient G α
a b : ↑x.orbit
c : α
h : ⟦a⟧ = ⟦b⟧
hb : b ∈ MulAction.orbit ↥H ⟦a⟧.out
⊢ Quotient.mk'' a = ⟦a⟧
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type ?u.3
inst✝ : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
⊢ ↑(r * (Units.map (Submonoid.center M).subtype) u) = ↑((Units.map (Submonoid.center M).subtype) u * r)

Tactic:
Units.val_mul,

Goal state after:
M : Type ?u.3
inst✝ : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
⊢ ↑r * ↑((Units.map (Submonoid.center M).subtype) u) = ↑((Units.map (Submonoid.center M).subtype) u * r)
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type ?u.3
inst✝ : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
⊢ ↑r * ↑↑u = ↑((Units.map (Submonoid.center M).subtype) u * r)

Tactic:
Units.val_mul,

Goal state after:
M : Type ?u.3
inst✝ : Monoid M
u : (↥(Submonoid.center M))ˣ
r : Mˣ
⊢ ↑r * ↑↑u = ↑((Units.map (Submonoid.center M).subtype) u) * ↑r
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x✝ : Mˣ
ha : x✝ ∈ Units.val ⁻¹' center M
g✝ : Mˣ
⊢ ↑(g✝ * x✝) = ↑(x✝ * g✝)

Tactic:
Units.val_mul,

Goal state after:
M : Type u_1
inst✝ : Monoid M
x✝ : Mˣ
ha : x✝ ∈ Units.val ⁻¹' center M
g✝ : Mˣ
⊢ ↑g✝ * ↑x✝ = ↑(x✝ * g✝)
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
x✝ : Mˣ
ha : x✝ ∈ Units.val ⁻¹' center M
g✝ : Mˣ
⊢ ↑g✝ * ↑x✝ = ↑(x✝ * g✝)

Tactic:
Units.val_mul,

Goal state after:
M : Type u_1
inst✝ : Monoid M
x✝ : Mˣ
ha : x✝ ∈ Units.val ⁻¹' center M
g✝ : Mˣ
⊢ ↑g✝ * ↑x✝ = ↑x✝ * ↑g✝
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
a : M
inst✝ : Invertible a
ha : a ∈ center M
⊢ ⅟a ∈ center M

Tactic:
by
  rw [Semigroup.mem_center_iff] at *
  exact (Commute.invOf_right <| ha ·)

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
s : Set G
c n : G
hc : c ∈ centralizer s
hn : n ∈ normalizer s
g : G
hg : g ∈ s
⊢ ⁅n * c * n⁻¹, g⁆ = 1

Tactic:
suffices n * (c * (n⁻¹ * g * n) * c⁻¹ * n⁻¹ * g⁻¹) = 1 by simpa [commutatorElement_def, mul_assoc]

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
s : Set G
c n : G
hc : c ∈ centralizer s
hn : n ∈ normalizer s
g : G
hg : g ∈ s
⊢ n * (c * (n⁻¹ * g * n) * c⁻¹ * n⁻¹ * g⁻¹) = 1
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
⊢ ∀ x ∈ Multiset.map f s.val, x = m

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
⊢ mk r a = mk r b ↔ ⊤ ≤ Relation.EqvGen r a b

Tactic:
rw [Quot.eq]

Goal state after:
α : Type u_1
r : α → α → Prop
a b : α
⊢ Relation.EqvGen r a b ↔ ⊤ ≤ Relation.EqvGen r a b
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
c : Con M
p : c.Quotientˣ → Prop
u : c.Quotientˣ
H : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1), p { val := ↑x, inv := ↑y, val_inv := ⋯, inv_val := ⋯ }
⊢ p u

Tactic:
rcases u with ⟨⟨x⟩, ⟨y⟩, h₁, h₂⟩

Goal state after:
case mk.mk
M : Type u_1
inst✝ : Monoid M
c : Con M
p : c.Quotientˣ → Prop
H : ∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1), p { val := ↑x, inv := ↑y, val_inv := ⋯, inv_val := ⋯ }
val✝ inv✝ : c.Quotient
x y : M
h₁ : Quot.mk (⇑c.toSetoid) x * Quot.mk (⇑c.toSetoid) y = 1
h₂ : Quot.mk (⇑c.toSetoid) y * Quot.mk (⇑c.toSetoid) x = 1
⊢ p { val := Quot.mk (⇑c.toSetoid) x, inv := Quot.mk (⇑c.toSetoid) y, val_inv := h₁, inv_val := h₂ }
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:

Tactic:
_ = ∏ j ∈ t, ∏ i ∈ s with g i = j, f (g i) :=
        prod_congr rfl fun j _ ↦ prod_congr rfl fun i hi ↦ by rw [(mem_filter.1 hi).2]
    _ = _ := prod_fiberwise_eq_prod_filter _ _ _ _

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

Goal state before:
pp: α : Type u
a₁ : α
b₁ : Bool
a₂ : α
b₂ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: (a₂, b₂) :: L₁) L₂
⊢ IsReduced ((a₁, b₁) :: (a₂, b₂) :: L₁)

Tactic:
rw [isReduced_cons_cons]
    refine ⟨?_, .of_forall_not_step fun L₂ step ↦ hL₁ _ step.cons⟩
    rintro rfl
    symm
    rw [← Bool.ne_not]
    rintro rfl
    exact hL₁ L₁ <| .not (L₁ := [])

Goal state after:
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
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ x ∈ s, p x
⊢ ∀ x ∈ s, p x

Tactic:
simpa using h

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
P : Submonoid M
Q : Submonoid N
hP : P.FG
hQ : Q.FG
⊢ (P.prod Q).FG

Tactic:
obtain ⟨bM, hbM⟩ := hP
  obtain ⟨bN, hbN⟩ := hQ
  refine ⟨bM ×ˢ singleton 1 ∪ singleton 1 ×ˢ bN, ?_⟩
  push_cast
  simp [closure_union, hbM, hbN]

Goal state after:
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)]
    simp [← ih]

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
e : G ≃* H
⊢ Function.LeftInverse ⇑(Abelianization.map e.symm.toMonoidHom) ⇑(Abelianization.map e.toMonoidHom)

Tactic:
rintro ⟨a⟩
    simp

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
e : G ≃* H
⊢ Function.RightInverse ⇑(Abelianization.map e.symm.toMonoidHom) ⇑(Abelianization.map e.toMonoidHom)

Tactic:
rintro ⟨a⟩
    simp

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

Goal state before:
pp: M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
g : ι → κ
f : ι → M
⊢ ∏ j, ∏ i, f ↑i = ∏ j, ∏ i with g i = j, f i

Tactic:
congr with j

Goal state after:
case e_f
M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
g : ι → κ
f : ι → M
j : κ
⊢ ∏ i, f ↑i = ∏ i with g i = j, f i
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
g : ι → κ
f : κ → M
⊢ ∏ j, ∏ _i, f j = ∏ j, ∏ i with g i = j, f j

Tactic:
congr with j

Goal state after:
case e_f
M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
g : ι → κ
f : κ → M
j : κ
⊢ ∏ _i, f j = ∏ i with g i = j, f j
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
p : α✝
⊢ Prod.mk <$> pure p <*> y = (fun b a ↦ (a, b)) <$> y <*> pure p

Tactic:
| pure p =>

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
⊢ ∑ x ∈ s with count x m ≠ 0, count x m = ∑ a ∈ m.toFinset, count a m

Tactic:
congr with a

Goal state after:
case e_s
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
m : Multiset ι
hms : ∀ a ∈ m, a ∈ s
a : ι
⊢ a ∈ {x ∈ s | count x m ≠ 0} ↔ a ∈ m.toFinset
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Mul α
a : FreeAbelianGroup α
h : 0 * a + 0 * a = 0 * a
⊢ 0 * a = 0

Tactic:
simpa using h

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 L2 : α
ih : x * of L2 * of L3 = x * (of L2 * of L3)
⊢ x * -of L2 * of L3 = x * (-of L2 * of L3)

Tactic:
| neg L2 ih =>

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x : FreeAbelianGroup α
L2 : α
ih : (lift ⇑f) (x * of L2) = (lift ⇑f) x * (lift ⇑f) (of L2)
⊢ (lift ⇑f) (x * -of L2) = (lift ⇑f) x * (lift ⇑f) (-of L2)

Tactic:
| neg L2 ih =>

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative ↥H
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
this : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤
⊢ N ⊔ Subgroup.map H.subtype ⊤ = N ⊔ H ⊔ N

Tactic:
← MonoidHom.range_eq_map

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative ↥H
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
this : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤
⊢ N ⊔ H.subtype.range = N ⊔ H ⊔ N
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)
x : M
v : P
y : ↥S
⊢ (f.lift hg) (f.mk' x y) = v ↔ g x = g ↑y * v

Tactic:
f.lift_mk' hg

Goal state after:
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)
x : M
v : P
y : ↥S
⊢ g x * ↑((IsUnit.liftRight (g.domRestrict S) hg) y)⁻¹ = v ↔ g x = g ↑y * v
Module: Mathlib.Algebra.Order.Hom.Monoid

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
g₁ g₂ : α ≃*o β
f : β ≃*o γ
hf : Injective ⇑f
h : g₁.trans f = g₂.trans f
a : α
⊢ (g₂.trans f) a = f (g₂ a)

Tactic:
trans_apply

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
g₁ g₂ : α ≃*o β
f : β ≃*o γ
hf : Injective ⇑f
h : g₁.trans f = g₂.trans f
a : α
⊢ f (g₂ a) = f (g₂ a)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: case refine_1
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z w : N
a : M × ↥S
ha : z * f ↑a.2 = f a.1
b : M × ↥S
hb : w * f ↑b.2 = f b.1
⊢ z * f ↑(a.2 * b.2) = f (a.1 * ↑b.2)

Tactic:
simp_rw [mul_def, map_mul, ← ha]
    exact (mul_assoc z _ _).symm

Goal state after:
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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
z : N
⊢ j (l (k.sec ((f.map hy k) z)).1) * j (l (g ↑(f.sec z).2)) = j (l ↑(k.sec ((f.map hy k) z)).2) * j (l (g (f.sec z).1))

Tactic:
rw [← map_mul j, ← map_mul j, ← l.map_mul, ← l.map_mul]

Goal state after:
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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝² : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝¹ : CommMonoid A
U : Submonoid A
R : Type u_6
inst✝ : CommMonoid R
j : U.LocalizationMap R
l : P →* A
hl : ∀ (w : ↥T), l ↑w ∈ U
z : N
⊢ j (l ((k.sec ((f.map hy k) z)).1 * g ↑(f.sec z).2)) = j (l (↑(k.sec ((f.map hy k) z)).2 * g (f.sec z).1))