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

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c ↦ (f c, g c)) c c'
h' : rα ((fun c ↦ (f c, g c)) c).1 ((fun c ↦ (f c, g c)) c').1
⊢ ((PSigma.Lex (Subrel rα fun x ↦ x ∈ range f) fun a ↦ Subrel (rβ on g) fun x ↦ x ∈ f ⁻¹' {↑a}) on fun c ↦
      ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩)
    c c'

pp: case inr
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c ↦ (f c, g c)) c c'
h' :
  ((fun c ↦ (f c, g c)) c).1 = ((fun c ↦ (f c, g c)) c').1 ∧ rβ ((fun c ↦ (f c, g c)) c).2 ((fun c ↦ (f c, g c)) c').2
⊢ ((PSigma.Lex (Subrel rα fun x ↦ x ∈ range f) fun a ↦ Subrel (rβ on g) fun x ↦ x ∈ f ⁻¹' {↑a}) on fun c ↦
      ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩)
    c c'

Tactic:
·

Goal state after:
case inl
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c ↦ (f c, g c)) c c'
h' : rα ((fun c ↦ (f c, g c)) c).1 ((fun c ↦ (f c, g c)) c').1
⊢ ((PSigma.Lex (Subrel rα fun x ↦ x ∈ range f) fun a ↦ Subrel (rβ on g) fun x ↦ x ∈ f ⁻¹' {↑a}) on fun c ↦
      ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩)
    c c'
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ centralizer s
h : G
hh : h ∈ s
⊢ g * h * g⁻¹ ∈ s

pp: case refine_2
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ centralizer s
h : G
hh : g * h * g⁻¹ ∈ s
⊢ h ∈ s

Tactic:
·

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ centralizer s
h : G
hh : h ∈ s
⊢ g * h * g⁻¹ ∈ s
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c ↦ (f c, g c)) c c'
h' :
  ((fun c ↦ (f c, g c)) c).1 = ((fun c ↦ (f c, g c)) c').1 ∧ rβ ((fun c ↦ (f c, g c)) c).2 ((fun c ↦ (f c, g c)) c').2
⊢ ((PSigma.Lex (Subrel rα fun x ↦ x ∈ range f) fun a ↦ Subrel (rβ on g) fun x ↦ x ∈ f ⁻¹' {↑a}) on fun c ↦
      ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩)
    c c'

Tactic:
·

Goal state after:
case inr
α : Type u_2
β : Type u_3
γ : Type u_4
rα : α → α → Prop
rβ : β → β → Prop
f : γ → α
g : γ → β
hα : WellFounded (rα on f)
hβ : ∀ (a : α), (f ⁻¹' {a}).WellFoundedOn (rβ on g)
c c' : γ
h : (Prod.Lex rα rβ on fun c ↦ (f c, g c)) c c'
h' :
  ((fun c ↦ (f c, g c)) c).1 = ((fun c ↦ (f c, g c)) c').1 ∧ rβ ((fun c ↦ (f c, g c)) c).2 ((fun c ↦ (f c, g c)) c').2
⊢ ((PSigma.Lex (Subrel rα fun x ↦ x ∈ range f) fun a ↦ Subrel (rβ on g) fun x ↦ x ∈ f ⁻¹' {↑a}) on fun c ↦
      ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩)
    c c'
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ centralizer s
h : G
hh : g * h * g⁻¹ ∈ s
⊢ h ∈ s

Tactic:
·

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
s : Set G
g : G
hg : g ∈ centralizer s
h : G
hh : g * h * g⁻¹ ∈ s
⊢ h ∈ s
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}

pp: case refine_2
G : Type u_1
inst✝ : Group G
g h : G
⊢ h ∈ centralizer {g} → h ∈ normalizer {g}

Tactic:
·

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
g h : G
⊢ h ∈ normalizer {g} → h ∈ centralizer {g}
Module: Mathlib.GroupTheory.Subgroup.Centralizer

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

Tactic:
·

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
g h : G
⊢ h ∈ centralizer {g} → h ∈ normalizer {g}
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inl
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : rι ((fun c ↦ ⟨f c, g (f c) c⟩) c).fst ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst
⊢ ((PSigma.Lex (Subrel rι fun x ↦ x ∈ range f) fun a ↦ Subrel (rπ ↑a on g ↑a) fun x ↦ x ∈ f ⁻¹' {↑a}) on fun c ↦
      ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩)
    c c'

pp: case inr
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : ((fun c ↦ ⟨f c, g (f c) c⟩) c).fst = ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ ((PSigma.Lex (Subrel rι fun x ↦ x ∈ range f) fun a ↦ Subrel (rπ ↑a on g ↑a) fun x ↦ x ∈ f ⁻¹' {↑a}) on fun c ↦
      ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩)
    c c'

Tactic:
·

Goal state after:
case inl
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : rι ((fun c ↦ ⟨f c, g (f c) c⟩) c).fst ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst
⊢ ((PSigma.Lex (Subrel rι fun x ↦ x ∈ range f) fun a ↦ Subrel (rπ ↑a on g ↑a) fun x ↦ x ∈ f ⁻¹' {↑a}) on fun c ↦
      ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩)
    c c'
Module: Mathlib.GroupTheory.Subgroup.Centralizer

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

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

Tactic:
·

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

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

Tactic:
·

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

Goal state before:
pp: case inr
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : ((fun c ↦ ⟨f c, g (f c) c⟩) c).fst = ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ ((PSigma.Lex (Subrel rι fun x ↦ x ∈ range f) fun a ↦ Subrel (rπ ↑a on g ↑a) fun x ↦ x ∈ f ⁻¹' {↑a}) on fun c ↦
      ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩)
    c c'

Tactic:
·

Goal state after:
case inr
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : ((fun c ↦ ⟨f c, g (f c) c⟩) c).fst = ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ ((PSigma.Lex (Subrel rι fun x ↦ x ∈ range f) fun a ↦ Subrel (rπ ↑a on g ↑a) fun x ↦ x ∈ f ⁻¹' {↑a}) on fun c ↦
      ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩)
    c c'
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr.convert_4
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ { x // x ∈ f ⁻¹' {↑⟨f c', ⋯⟩} }

pp: case e'_5
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩ = ⟨⟨f c', ⋯⟩, ?inr.convert_4⟩

pp: case inr.convert_6
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ Subrel (rπ ↑⟨f c', ⋯⟩ on g ↑⟨f c', ⋯⟩) (fun x ↦ x ∈ f ⁻¹' {↑⟨f c', ⋯⟩}) ?inr.convert_4 ⟨c', ⋯⟩

Tactic:
·

Goal state after:
case inr.convert_4
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ { x // x ∈ f ⁻¹' {↑⟨f c', ⋯⟩} }
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case e'_5
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩ = ⟨⟨f c', ⋯⟩, ⟨c, h'⟩⟩

pp: case inr.convert_6
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ Subrel (rπ ↑⟨f c', ⋯⟩ on g ↑⟨f c', ⋯⟩) (fun x ↦ x ∈ f ⁻¹' {↑⟨f c', ⋯⟩}) ⟨c, h'⟩ ⟨c', ⋯⟩

Tactic:
·

Goal state after:
case e'_5
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩ = ⟨⟨f c', ⋯⟩, ⟨c, h'⟩⟩
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case inr.convert_6
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ Subrel (rπ ↑⟨f c', ⋯⟩ on g ↑⟨f c', ⋯⟩) (fun x ↦ x ∈ f ⁻¹' {↑⟨f c', ⋯⟩}) ⟨c, h'⟩ ⟨c', ⋯⟩

Tactic:
·

Goal state after:
case inr.convert_6
ι : Type u_1
γ : Type u_4
π : ι → Type u_5
rι : ι → ι → Prop
rπ : (i : ι) → π i → π i → Prop
f : γ → ι
g : (i : ι) → γ → π i
hι : WellFounded (rι on f)
hπ : ∀ (i : ι), (f ⁻¹' {i}).WellFoundedOn (rπ i on g i)
c c' : γ
h : (Sigma.Lex rι rπ on fun c ↦ ⟨f c, g (f c) c⟩) c c'
h' : f c = f c'
h'' :
  rπ ((fun c ↦ ⟨f c, g (f c) c⟩) c').fst (h' ▸ ((fun c ↦ ⟨f c, g (f c) c⟩) c).snd) ((fun c ↦ ⟨f c, g (f c) c⟩) c').snd
⊢ Subrel (rπ ↑⟨f c', ⋯⟩ on g ↑⟨f c', ⋯⟩) (fun x ↦ x ∈ f ⁻¹' {↑⟨f c', ⋯⟩}) ⟨c, h'⟩ ⟨c', ⋯⟩
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
S : Set G
x : G
hx : x ∈ (closure S).toSubmonoid
⊢ x ∈ Submonoid.closure (S ∪ S⁻¹)

pp: case refine_2
G : Type u_2
inst✝ : Group G
S : Set G
⊢ S ∪ S⁻¹ ⊆ ↑(closure S).toSubmonoid

Tactic:
·

Goal state after:
case refine_1
G : Type u_2
inst✝ : Group G
S : Set G
x : G
hx : x ∈ (closure S).toSubmonoid
⊢ x ∈ Submonoid.closure (S ∪ S⁻¹)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case refine_2
G : Type u_2
inst✝ : Group G
S : Set G
⊢ S ∪ S⁻¹ ⊆ ↑(closure S).toSubmonoid

Tactic:
·

Goal state after:
case refine_2
G : Type u_2
inst✝ : Group G
S : Set G
⊢ S ∪ S⁻¹ ⊆ ↑(closure S).toSubmonoid
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : G
hx✝ : x✝ ∈ ⨆ i, S i
i : ι
x : G
hx : x ∈ S i
⊢ ∃ (h : x ∈ ⨆ i, S i), C x h

pp: case refine_2
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x : G
hx : x ∈ ⨆ i, S i
⊢ ∃ (h : 1 ∈ ⨆ i, S i), C 1 h

pp: case refine_3
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : G
hx : x✝ ∈ ⨆ i, S i
x y : G
⊢ (∃ (h : x ∈ ⨆ i, S i), C x h) → (∃ (h : y ∈ ⨆ i, S i), C y h) → ∃ (h : x * y ∈ ⨆ i, S i), C (x * y) h

Tactic:
·

Goal state after:
case refine_1
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : G
hx✝ : x✝ ∈ ⨆ i, S i
i : ι
x : G
hx : x ∈ S i
⊢ ∃ (h : x ∈ ⨆ i, S i), C x h
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h.cons
α : 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 * hd * tl.prod = hd * a * tl.prod

pp: case h.cons
α : 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 | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute

Tactic:
·

Goal state after:
case h.cons
α : 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 * hd * tl.prod = hd * a * tl.prod
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case refine_2
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x : G
hx : x ∈ ⨆ i, S i
⊢ ∃ (h : 1 ∈ ⨆ i, S i), C 1 h

pp: case refine_3
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : G
hx : x✝ ∈ ⨆ i, S i
x y : G
⊢ (∃ (h : x ∈ ⨆ i, S i), C x h) → (∃ (h : y ∈ ⨆ i, S i), C y h) → ∃ (h : x * y ∈ ⨆ i, S i), C (x * y) h

Tactic:
·

Goal state after:
case refine_2
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x : G
hx : x ∈ ⨆ i, S i
⊢ ∃ (h : 1 ∈ ⨆ i, S i), C 1 h
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case refine_3
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : G
hx : x✝ ∈ ⨆ i, S i
x y : G
⊢ (∃ (h : x ∈ ⨆ i, S i), C x h) → (∃ (h : y ∈ ⨆ i, S i), C y h) → ∃ (h : x * y ∈ ⨆ i, S i), C (x * y) h

Tactic:
·

Goal state after:
case refine_3
G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → x ∈ ⨆ i, S i → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x✝ : G
hx : x✝ ∈ ⨆ i, S i
x y : G
⊢ (∃ (h : x ∈ ⨆ i, S i), C x h) → (∃ (h : y ∈ ⨆ i, S i), C y h) → ∃ (h : x * y ∈ ⨆ i, S i), C (x * y) h
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h.cons
α : 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 | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute

Tactic:
·

Goal state after:
case h.cons
α : 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 | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ ↑(normalizer ↑N)
⊢ ⋃ a ∈ S, (fun x ↦ a * x) '' ↑N = ⋃ a ∈ S, (fun x ↦ x * a) '' ↑N

Tactic:
simp only [image_mul_left, image_mul_right, Set.preimage]

Goal state after:
G : Type u_2
inst✝ : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ ↑(normalizer ↑N)
⊢ ⋃ a ∈ S, {x | a⁻¹ * x ∈ ↑N} = ⋃ a ∈ S, {x | x * a⁻¹ ∈ ↑N}
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case mul.refine_1
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 ↦ x1 * x2) x y ∈ closure (↑H * ↑N)
x' : G
hx' : x' ∈ ↑H
y' : G
hy' : y' ∈ ↑N
hy✝ : (fun x1 x2 ↦ x1 * x2) x' y' ∈ closure (↑H * ↑N)
⊢ x'⁻¹ * y * x' ∈ N

pp: case mul.refine_2
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 ↦ x1 * x2) x y ∈ closure (↑H * ↑N)
x' : G
hx' : x' ∈ ↑H
y' : G
hy' : y' ∈ ↑N
hy✝ : (fun x1 x2 ↦ x1 * x2) x' y' ∈ closure (↑H * ↑N)
⊢ (fun x1 x2 ↦ x1 * x2) (x * x') (x'⁻¹ * y * x' * y') = (fun x1 x2 ↦ x1 * x2) x y * (fun x1 x2 ↦ x1 * x2) x' y'

Tactic:
·

Goal state after:
case mul.refine_1
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 ↦ x1 * x2) x y ∈ closure (↑H * ↑N)
x' : G
hx' : x' ∈ ↑H
y' : G
hy' : y' ∈ ↑N
hy✝ : (fun x1 x2 ↦ x1 * x2) x' y' ∈ closure (↑H * ↑N)
⊢ x'⁻¹ * y * x' ∈ N
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case mul.refine_2
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 ↦ x1 * x2) x y ∈ closure (↑H * ↑N)
x' : G
hx' : x' ∈ ↑H
y' : G
hy' : y' ∈ ↑N
hy✝ : (fun x1 x2 ↦ x1 * x2) x' y' ∈ closure (↑H * ↑N)
⊢ (fun x1 x2 ↦ x1 * x2) (x * x') (x'⁻¹ * y * x' * y') = (fun x1 x2 ↦ x1 * x2) x y * (fun x1 x2 ↦ x1 * x2) x' y'

Tactic:
·

Goal state after:
case mul.refine_2
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hLE : H ≤ normalizer ↑N
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 ↦ x1 * x2) x y ∈ closure (↑H * ↑N)
x' : G
hx' : x' ∈ ↑H
y' : G
hy' : y' ∈ ↑N
hy✝ : (fun x1 x2 ↦ x1 * x2) x' y' ∈ closure (↑H * ↑N)
⊢ (fun x1 x2 ↦ x1 * x2) (x * x') (x'⁻¹ * y * x' * y') = (fun x1 x2 ↦ x1 * x2) x y * (fun x1 x2 ↦ x1 * x2) x' y'
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h.cons.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
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ x ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

pp: case h.cons.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
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ y ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

Tactic:
·

Goal state after:
case h.cons.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
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ x ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

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

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

Tactic:
·

Goal state after:
case mp
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : A ≤ C
x✝ : G
⊢ (∃ x ∈ ↑A, ∃ y, (y ∈ ↑B ∧ y ∈ ↑C) ∧ x * y = x✝) → (∃ x ∈ ↑A, ∃ y ∈ ↑B, x * y = x✝) ∧ x✝ ∈ ↑C
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h.cons.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
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ y ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

Tactic:
·

Goal state after:
case h.cons.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
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ y ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

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

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

Tactic:
·

Goal state after:
case mp
G : Type u_2
inst✝ : Group G
A B C : Subgroup G
h : C ≤ A
x✝ : G
⊢ (∃ x, (x ∈ ↑A ∧ x ∈ ↑B) ∧ ∃ y ∈ ↑C, x * y = x✝) → x✝ ∈ ↑A ∧ ∃ x ∈ ↑B, ∃ y ∈ ↑C, x * y = x✝
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Type u_5
s : Set ι
H : ι → Subgroup G
h : ∀ i ∈ s, (H i).Normal
this : ∀ (i : ↑s), (H ↑i).Normal
⊢ (⨆ i, H ↑i).Normal

Tactic:
apply iSup_normal

Goal state after: