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

Goal state before:
pp: case pos
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
    (if n < g 0 then f n else (f (g (n - g 0))).tail)
hn : n < g 0
⊢ False

Tactic:
apply hf1.2 m n mn

Goal state after:
case pos
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
    (if n < g 0 then f n else (f (g (n - g 0))).tail)
hn : n < g 0
⊢ List.SublistForall₂ r (f m) (f n)
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
⊢ ((centralizer s).subgroupOf (normalizer s)).Normal

Tactic:
by
  refine (Subgroup.normal_subgroupOf_iff <| centralizer_le_normalizer s).mpr fun c n hc hn ↦ ?_
  refine mem_centralizer_iff_commutator_eq_one'.mpr fun g hg ↦ ?_
  suffices n * (c * (n⁻¹ * g * n) * c⁻¹ * n⁻¹ * g⁻¹) = 1 by simpa [commutatorElement_def, mul_assoc]
  simp [← hc _ <| mem_set_normalizer_iff''.mp hn g |>.mp hg]

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

Goal state before:
pp: case refine_2.refine_1
G : Type u_1
inst✝ : Group G
g✝ h : G
hh : h ∈ centralizer {g✝}
g : G
⊢ g ∈ {g✝} → h * g * h⁻¹ ∈ {g✝}

pp: case refine_2.refine_2
G : Type u_1
inst✝ : Group G
g✝ h : G
hh : h ∈ centralizer {g✝}
g : G
⊢ h * g * h⁻¹ ∈ {g✝} → g ∈ {g✝}

Tactic:
<;>

Goal state after:
case refine_2.refine_1
G : Type u_1
inst✝ : Group G
g✝ h : G
hh : h ∈ centralizer {g✝}
g : G
⊢ g ∈ {g✝} → h * g * h⁻¹ ∈ {g✝}

case refine_2.refine_2
G : Type u_1
inst✝ : Group G
g✝ h : G
hh : h ∈ centralizer {g✝}
g : G
⊢ h * g * h⁻¹ ∈ {g✝} → g ∈ {g✝}
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β → β
l : List α
comm : {x | x ∈ ↑l}.Pairwise fun x y ↦ ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ List.foldr f b (List.map Subtype.val (List.pmap Subtype.mk l ⋯)) = List.foldr f b l

Tactic:
simp [List.map_pmap]

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

Goal state before:
pp: case h.cons.e_a.a
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ a ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

pp: case h.cons.e_a.a
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ hd ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

Tactic:
<;>

Goal state after:
case h.cons.e_a.a
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ a ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

case h.cons.e_a.a
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ hd ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case zero
G : Type u_2
inst✝ : Group G
s : Set G
H : Subgroup G
hs : s ⊆ ↑H
⊢ s ^ 0 ⊆ ↑H

pp: case succ
G : Type u_2
inst✝ : Group G
s : Set G
H : Subgroup G
hs : s ⊆ ↑H
n✝ : ℕ
a✝ : s ^ n✝ ⊆ ↑H
⊢ s ^ (n✝ + 1) ⊆ ↑H

Tactic:
<;>

Goal state after:
case zero
G : Type u_2
inst✝ : Group G
s : Set G
H : Subgroup G
hs : s ⊆ ↑H
⊢ s ^ 0 ⊆ ↑H

case succ
G : Type u_2
inst✝ : Group G
s : Set G
H : Subgroup G
hs : s ⊆ ↑H
n✝ : ℕ
a✝ : s ^ n✝ ⊆ ↑H
⊢ s ^ (n✝ + 1) ⊆ ↑H
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h.cons.a.inl
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x y : α
hy : y ∈ {x | x = a ∨ x ∈ tl}
h✝ : x = a
⊢ x ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

pp: case h.cons.a.inr
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x y : α
hy : y ∈ {x | x = a ∨ x ∈ tl}
h✝ : x ∈ tl
⊢ x ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

Tactic:
<;>

Goal state after:
case h.cons.a.inl
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x y : α
hy : y ∈ {x | x = a ∨ x ∈ tl}
h✝ : x = a
⊢ x ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

case h.cons.a.inr
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x y : α
hy : y ∈ {x | x = a ∨ x ∈ tl}
h✝ : x ∈ tl
⊢ x ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h.cons.a.inl
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
h✝ : y = a
⊢ y ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

pp: case h.cons.a.inr
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
h✝ : y ∈ tl
⊢ y ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

Tactic:
<;>

Goal state after:
case h.cons.a.inl
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
h✝ : y = a
⊢ y ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

case h.cons.a.inr
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
h✝ : y ∈ tl
⊢ y ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
p : α → Prop
hom : ∀ (a b : α), p a → p b → p (a * b)
unit : p 1
base : ∀ x ∈ s, p x
⊢ p (s.noncommProd comm)

Tactic:
by
  induction s using Quotient.inductionOn with | _ l
  simp only [quot_mk_to_coe, noncommProd_coe, mem_coe] at base ⊢
  exact l.prod_induction p hom unit base

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
e : ι ↪ κ
f : κ → M
⊢ ∏ x ∈ map e s, f x = ∏ x ∈ s, f (e x)

Tactic:
by
  rw [Finset.prod, Finset.map_val, Multiset.map_map]; rfl

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

Goal state before:
pp: case refine_1
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t
hfg : ∀ i ∈ s, f i = g (e i)
⊢ ∀ a ∈ s, e a ∈ t

pp: case refine_2
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t
hfg : ∀ i ∈ s, f i = g (e i)
⊢ ∀ a ∈ t, e.symm a ∈ s

pp: case refine_3
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t
hfg : ∀ i ∈ s, f i = g (e i)
⊢ ∀ a ∈ s, e.symm (e a) = a

pp: case refine_4
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t
hfg : ∀ i ∈ s, f i = g (e i)
⊢ ∀ a ∈ t, e (e.symm a) = a

Tactic:
<;>

Goal state after:
case refine_1
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t
hfg : ∀ i ∈ s, f i = g (e i)
⊢ ∀ a ∈ s, e a ∈ t

case refine_2
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t
hfg : ∀ i ∈ s, f i = g (e i)
⊢ ∀ a ∈ t, e.symm a ∈ s

case refine_3
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t
hfg : ∀ i ∈ s, f i = g (e i)
⊢ ∀ a ∈ s, e.symm (e a) = a

case refine_4
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
e : ι ≃ κ
hst : ∀ (i : ι), i ∈ s ↔ e i ∈ t
hfg : ∀ i ∈ s, f i = g (e i)
⊢ ∀ a ∈ t, e (e.symm a) = a
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: case h₁
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
r : M → N → Prop
f : ι → M
g : ι → N
s : Finset ι
h₁ : r 1 1
h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a * b) (g a * c)
⊢ r 1 1

pp: case h₂
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
r : M → N → Prop
f : ι → M
g : ι → N
s : Finset ι
h₁ : r 1 1
h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a * b) (g a * c)
⊢ ∀ ⦃a : ι⦄ ⦃b : M⦄ ⦃c : N⦄, r b c → r (f a * b) (g a * c)

Tactic:
<;>

Goal state after:
case h₁
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
r : M → N → Prop
f : ι → M
g : ι → N
s : Finset ι
h₁ : r 1 1
h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a * b) (g a * c)
⊢ r 1 1

case h₂
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
r : M → N → Prop
f : ι → M
g : ι → N
s : Finset ι
h₁ : r 1 1
h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a * b) (g a * c)
⊢ ∀ ⦃a : ι⦄ ⦃b : M⦄ ⦃c : N⦄, r b c → r (f a * b) (g a * c)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f g : ι → M
h : p
⊢ ∏ x ∈ s, f x = ∏ x ∈ s, f x

pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f g : ι → M
h : ¬p
⊢ ∏ x ∈ s, g x = ∏ x ∈ s, g x

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f g : ι → M
h : p
⊢ ∏ x ∈ s, f x = ∏ x ∈ s, f x

case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f g : ι → M
h : ¬p
⊢ ∏ x ∈ s, g x = ∏ x ∈ s, g x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f : p → ι → M
g : ¬p → ι → M
h : p
⊢ ∏ x ∈ s, f h x = ∏ x ∈ s, f h x

pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f : p → ι → M
g : ¬p → ι → M
h : ¬p
⊢ ∏ x ∈ s, g h x = ∏ x ∈ s, g h x

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f : p → ι → M
g : ¬p → ι → M
h : p
⊢ ∏ x ∈ s, f h x = ∏ x ∈ s, f h x

case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
p : Prop
inst✝ : Decidable p
s : Finset ι
f : p → ι → M
g : ¬p → ι → M
h : ¬p
⊢ ∏ x ∈ s, g h x = ∏ x ∈ s, g h x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ a ∈ univ, ↑a ∈ m.toFinset

pp: case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ (a : ι) (ha : a ∈ m.toFinset), ⟨a, ⋯⟩ ∈ univ

pp: case refine_3
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ (a : { x // x ∈ m }) (ha : a ∈ univ), ⟨↑a, ⋯⟩ = a

pp: case refine_4
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ (a : ι) (ha : a ∈ m.toFinset), ↑⟨a, ⋯⟩ = a

pp: case refine_5
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ a ∈ univ, f a = g ↑a

Tactic:
<;>

Goal state after:
case refine_1
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ a ∈ univ, ↑a ∈ m.toFinset

case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ (a : ι) (ha : a ∈ m.toFinset), ⟨a, ⋯⟩ ∈ univ

case refine_3
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ (a : { x // x ∈ m }) (ha : a ∈ univ), ⟨↑a, ⋯⟩ = a

case refine_4
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ (a : ι) (ha : a ∈ m.toFinset), ↑⟨a, ⋯⟩ = a

case refine_5
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
m : Multiset ι
f : { x // x ∈ m } → M
g : ι → M
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
⊢ ∀ a ∈ univ, f a = g ↑a
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case hac
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
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)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) ((f * g) y)

pp: case hbc
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
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)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) ((f * g) y)

Tactic:
<;>

Goal state after:
case hac
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
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)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) ((f * g) y)

case hbc
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
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)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) ((f * g) y)
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: case mul.e_a
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∏ x ∈ t ∪ u, x ^ f x = ∏ x ∈ t, x ^ f x

pp: case mul.e_a
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∏ x ∈ t ∪ u, x ^ g x = ∏ x ∈ u, x ^ g x

Tactic:
<;>

Goal state after:
case mul.e_a
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∏ x ∈ t ∪ u, x ^ f x = ∏ x ∈ t, x ^ f x

case mul.e_a
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∏ x ∈ t ∪ u, x ^ g x = ∏ x ∈ u, x ^ g x
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case false
α : Type u
L₁ L₂ : List (α × Bool)
x : α
⊢ Step (L₁ ++ (x, !false) :: (x, false) :: L₂) (L₁ ++ L₂)

pp: case true
α : Type u
L₁ L₂ : List (α × Bool)
x : α
⊢ Step (L₁ ++ (x, !true) :: (x, true) :: L₂) (L₁ ++ L₂)

Tactic:
<;>

Goal state after:
case false
α : Type u
L₁ L₂ : List (α × Bool)
x : α
⊢ Step (L₁ ++ (x, !false) :: (x, false) :: L₂) (L₁ ++ L₂)

case true
α : Type u
L₁ L₂ : List (α × Bool)
x : α
⊢ Step (L₁ ++ (x, !true) :: (x, true) :: L₂) (L₁ ++ L₂)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case mp.nil
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
hL : (a, b) :: L₁ = [] ++ (a', b') :: (a', !b') :: e
⊢ (∃ L, Step L₁ L ∧ [] ++ e = (a, b) :: L) ∨ L₁ = (a, !b) :: ([] ++ e)

pp: case mp.cons
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
p : α × Bool
s' : List (α × Bool)
hL : (a, b) :: L₁ = p :: s' ++ (a', b') :: (a', !b') :: e
⊢ (∃ L, Step L₁ L ∧ p :: s' ++ e = (a, b) :: L) ∨ L₁ = (a, !b) :: (p :: s' ++ e)

Tactic:
<;>

Goal state after:
case mp.nil
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
hL : (a, b) :: L₁ = [] ++ (a', b') :: (a', !b') :: e
⊢ (∃ L, Step L₁ L ∧ [] ++ e = (a, b) :: L) ∨ L₁ = (a, !b) :: ([] ++ e)

case mp.cons
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
e : List (α × Bool)
a' : α
b' : Bool
p : α × Bool
s' : List (α × Bool)
hL : (a, b) :: L₁ = p :: s' ++ (a', b') :: (a', !b') :: e
⊢ (∃ L, Step L₁ L ∧ p :: s' ++ e = (a, b) :: L) ∨ L₁ = (a, !b) :: (p :: s' ++ e)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : a ∉ s → f a = 1
h✝ : a ∈ s
⊢ ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x

pp: case neg
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : a ∉ s → f a = 1
h✝ : a ∉ s
⊢ ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : a ∉ s → f a = 1
h✝ : a ∈ s
⊢ ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x

case neg
ι : Type u_1
M : Type u_4
s : Finset ι
a : ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
h : a ∉ s → f a = 1
h✝ : a ∉ s
⊢ ∏ x ∈ insert a s, f x = ∏ x ∈ s, f x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case empty
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : Subsingleton Mˣ
⊢ ∏ i ∈ ∅, f i = 1 ↔ ∀ i ∈ ∅, f i = 1

pp: case cons
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : Subsingleton Mˣ
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∏ i ∈ s✝, f i = 1 ↔ ∀ i ∈ s✝, f i = 1
⊢ ∏ i ∈ cons a✝¹ s✝ h✝, f i = 1 ↔ ∀ i ∈ cons a✝¹ s✝ h✝, f i = 1

Tactic:
<;>

Goal state after:
case empty
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : Subsingleton Mˣ
⊢ ∏ i ∈ ∅, f i = 1 ↔ ∀ i ∈ ∅, f i = 1

case cons
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : Subsingleton Mˣ
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ∏ i ∈ s✝, f i = 1 ↔ ∀ i ∈ s✝, f i = 1
⊢ ∏ i ∈ cons a✝¹ s✝ h✝, f i = 1 ↔ ∀ i ∈ cons a✝¹ s✝ h✝, f i = 1
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂ : Red ((x, !b) :: (x, b) :: L) L
⊢ Red L [(x, !b)]

Tactic:
let ⟨L', h₁, h₂⟩ := church_rosser h₁ h₂

Goal state after:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁✝ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : Red [(x, !b)] L'
h₂ : Red L L'
⊢ Red L [(x, !b)]
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 κ
s : Finset ι
t : Finset κ
g : ι → κ
f : κ → M
j : κ
x✝ : j ∈ t
i : ι
hi : i ∈ {i ∈ s | g i = j}
⊢ f j = f (g i)

Tactic:
rw [(mem_filter.1 hi).2]

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

Goal state before:
pp: case C1
α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
this : ∀ (x : α), f (of x)⁻¹ = g (of x)⁻¹
⊢ f 1 = g 1

pp: case of
α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
this : ∀ (x : α), f (of x)⁻¹ = g (of x)⁻¹
x✝ : α
⊢ f (of x✝) = g (of x✝)

pp: case inv_of
α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
this : ∀ (x : α), f (of x)⁻¹ = g (of x)⁻¹
x✝ : α
a✝ : f (of x✝) = g (of x✝)
⊢ f (of x✝)⁻¹ = g (of x✝)⁻¹

pp: case mul
α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
this : ∀ (x : α), f (of x)⁻¹ = g (of x)⁻¹
x✝ y✝ : FreeGroup α
a✝¹ : f x✝ = g x✝
a✝ : f y✝ = g y✝
⊢ f (x✝ * y✝) = g (x✝ * y✝)

Tactic:
<;>

Goal state after:
case C1
α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
this : ∀ (x : α), f (of x)⁻¹ = g (of x)⁻¹
⊢ f 1 = g 1

case of
α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
this : ∀ (x : α), f (of x)⁻¹ = g (of x)⁻¹
x✝ : α
⊢ f (of x✝) = g (of x✝)

case inv_of
α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
this : ∀ (x : α), f (of x)⁻¹ = g (of x)⁻¹
x✝ : α
a✝ : f (of x✝) = g (of x✝)
⊢ f (of x✝)⁻¹ = g (of x✝)⁻¹

case mul
α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
this : ∀ (x : α), f (of x)⁻¹ = g (of x)⁻¹
x✝ y✝ : FreeGroup α
a✝¹ : f x✝ = g x✝
a✝ : f y✝ = g y✝
⊢ f (x✝ * y✝) = g (x✝ * y✝)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case false
α : Type u
β : Type v
inst✝ : Group β
f : α → β
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
⊢ Lift.aux f (L₁✝ ++ (x✝, false) :: (x✝, !false) :: L₂✝) = Lift.aux f (L₁✝ ++ L₂✝)

pp: case true
α : Type u
β : Type v
inst✝ : Group β
f : α → β
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
⊢ Lift.aux f (L₁✝ ++ (x✝, true) :: (x✝, !true) :: L₂✝) = Lift.aux f (L₁✝ ++ L₂✝)

Tactic:
<;>

Goal state after:
case false
α : Type u
β : Type v
inst✝ : Group β
f : α → β
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
⊢ Lift.aux f (L₁✝ ++ (x✝, false) :: (x✝, !false) :: L₂✝) = Lift.aux f (L₁✝ ++ L₂✝)

case true
α : Type u
β : Type v
inst✝ : Group β
f : α → β
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
⊢ Lift.aux f (L₁✝ ++ (x✝, true) :: (x✝, !true) :: L₂✝) = Lift.aux f (L₁✝ ++ L₂✝)