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

Goal state before:
pp: α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
a✝ b✝ : G
ha : a✝ ∈ (↑S)⁻¹
hb : b✝ ∈ (↑S)⁻¹
⊢ b✝⁻¹ * a✝⁻¹ ∈ ↑S

Tactic:
;

Goal state after:
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
a✝ b✝ : G
ha : a✝ ∈ (↑S)⁻¹
hb : b✝ ∈ (↑S)⁻¹
⊢ b✝⁻¹ * a✝⁻¹ ∈ ↑S
Module: Mathlib.Algebra.Group.Submonoid.Pointwise

Goal state before:
pp: α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
⊢ 1 ∈ ↑S

Tactic:
;

Goal state after:
α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
⊢ 1 ∈ ↑S
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ #(Ioi a) = #(Ici a) - 1

Tactic:
by
  rw [Ici_eq_cons_Ioi, card_cons, Nat.add_sub_cancel_right]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)

Tactic:
by
  rw [← coe_inj, coe_inter, coe_Ico, coe_Ico, coe_Ico, Set.Ico_inter_Ico]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Icc (a ⊓ b) (a ⊔ b) = Icc (b ⊓ a) (b ⊔ a)

Tactic:
inf_comm,

Goal state after:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Icc (b ⊓ a) (a ⊔ b) = Icc (b ⊓ a) (b ⊔ a)
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
m k : ℕ
mn : m ≤ m + k
⊢ ↑(fs m) m = ↑(fs (m + k)) m

Tactic:
;

Goal state after:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
m k : ℕ
mn : m ≤ m + k
⊢ ↑(fs m) m = ↑(fs (m + k)) m
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a : α
b : β
⊢ ∀ ⦃x : G⦄, x • a = a → (x • a) • b = a • b

Tactic:
;

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a : α
b : β
⊢ ∀ ⦃x : G⦄, x • a = a → (x • a) • b = a • b
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a✝ : α
b : β
a : G
h : a • a✝ = a✝
⊢ (a • a✝) • b = a✝ • b

Tactic:
;

Goal state after:
G : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G α
inst✝² : MulAction G β
inst✝¹ : SMul α β
inst✝ : IsScalarTower G α β
a✝ : α
b : β
a : G
h : a • a✝ = a✝
⊢ (a • a✝) • b = a✝ • b
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
G' : Type u_4
inst✝³ : Group G'
inst✝² : SMul α β
inst✝¹ : MulAction G' β
inst✝ : SMulCommClass G' α β
a : α
b : β
⊢ ∀ ⦃x : G'⦄, x • b = b → a • x • b = a • b

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
G' : Type u_4
inst✝³ : Group G'
inst✝² : SMul α β
inst✝¹ : MulAction G' β
inst✝ : SMulCommClass G' α β
a : α
b : β
⊢ ∀ ⦃x : G'⦄, x • b = b → a • x • b = a • b
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
G' : Type u_4
inst✝³ : Group G'
inst✝² : SMul α β
inst✝¹ : MulAction G' β
inst✝ : SMulCommClass G' α β
a✝ : α
b : β
a : G'
h : a • b = b
⊢ a✝ • a • b = a✝ • b

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
G' : Type u_4
inst✝³ : Group G'
inst✝² : SMul α β
inst✝¹ : MulAction G' β
inst✝ : SMulCommClass G' α β
a✝ : α
b : β
a : G'
h : a • b = b
⊢ a✝ • a • b = a✝ • b
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
g h : M
Hg : g ∈ Set.center M
u : Mˣ
hu : SemiconjBy (↑u) g h
⊢ g = h

Tactic:
;

Goal state after:
M : Type u_2
inst✝ : Monoid M
g h : M
Hg : g ∈ Set.center M
u : Mˣ
hu : SemiconjBy (↑u) g h
⊢ g = h
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case comm
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
a✝ : N
⊢ Commute (e x) a✝

Tactic:
;

Goal state after:
case comm
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
a✝ : N
⊢ Commute (e x) a✝
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case comm
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
a✝ : N
⊢ e.symm (e x * a✝) = e.symm (a✝ * e x)

Tactic:
;

Goal state after:
case comm
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
a✝ : N
⊢ e.symm (e x * a✝) = e.symm (a✝ * e x)
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case left_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
b✝ c✝ : N
⊢ e x * (b✝ * c✝) = e x * b✝ * c✝

Tactic:
;

Goal state after:
case left_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
b✝ c✝ : N
⊢ e x * (b✝ * c✝) = e x * b✝ * c✝
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case left_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
b✝ c✝ : N
⊢ e.symm (e x * (b✝ * c✝)) = e.symm (e x * b✝ * c✝)

Tactic:
;

Goal state after:
case left_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
b✝ c✝ : N
⊢ e.symm (e x * (b✝ * c✝)) = e.symm (e x * b✝ * c✝)
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case right_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
a✝ b✝ : N
⊢ a✝ * b✝ * e x = a✝ * (b✝ * e x)

Tactic:
;

Goal state after:
case right_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ↑e✝
a✝ b✝ : N
⊢ a✝ * b✝ * e x = a✝ * (b✝ * e x)
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case right_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
a✝ b✝ : N
⊢ e.symm (a✝ * b✝ * e x) = e.symm (a✝ * (b✝ * e x))

Tactic:
;

Goal state after:
case right_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
a✝ b✝ : N
⊢ e.symm (a✝ * b✝ * e x) = e.symm (a✝ * (b✝ * e x))
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
x : M
⊢ IsMulCentral (op x) ↔ IsMulCentral x

Tactic:
isMulCentral_iff,

Goal state after:
M : Type u_2
inst✝ : Mul M
x : M
⊢ ((∀ (a : Mᵐᵒᵖ), Commute (op x) a) ∧
      (∀ (b c : Mᵐᵒᵖ), op x * (b * c) = op x * b * c) ∧ ∀ (a b : Mᵐᵒᵖ), a * b * op x = a * (b * op x)) ↔
    (∀ (a : M), Commute x a) ∧ (∀ (b c : M), x * (b * c) = x * b * c) ∧ ∀ (a b : M), a * b * x = a * (b * x)
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
x : M
⊢ ((∀ (a : M), Commute (op x) (op a)) ∧
      (∀ (a a_1 : M), a_1 * a * x = a_1 * (a * x)) ∧ ∀ (a a_1 : M), x * (a_1 * a) = x * a_1 * a) ↔
    (∀ (a : M), Commute x a) ∧ (∀ (b c : M), x * (b * c) = x * b * c) ∧ ∀ (a b : M), a * b * x = a * (b * x)

Tactic:
;

Goal state after:
M : Type u_2
inst✝ : Mul M
x : M
⊢ ((∀ (a : M), Commute (op x) (op a)) ∧
      (∀ (a a_1 : M), a_1 * a * x = a_1 * (a * x)) ∧ ∀ (a a_1 : M), x * (a_1 * a) = x * a_1 * a) ↔
    (∀ (a : M), Commute x a) ∧ (∀ (b c : M), x * (b * c) = x * b * c) ∧ ∀ (a b : M), a * b * x = a * (b * x)
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
x : (i : ι) → A i
x✝ :
  (∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1) ∧
    (∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1) ∧
      ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
i : ι
h1 : ∀ (a : (i : ι) → A i) (x_1 : ι), x x_1 * a x_1 = a x_1 * x x_1
h2 : ∀ (b c : (i : ι) → A i) (x_1 : ι), x x_1 * (b x_1 * c x_1) = x x_1 * b x_1 * c x_1
h3 : ∀ (a b : (i : ι) → A i) (x_1 : ι), a x_1 * b x_1 * x x_1 = a x_1 * (b x_1 * x x_1)
a b : A i
⊢ a * b * x i = a * (b * x i)

Tactic:
simpa using h3 (update x i a) (update x i b) i

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: ι : Type u_2
A : ι → Type u_3
inst✝ : (i : ι) → Mul (A i)
⊢ center ((i : ι) → A i) = univ.pi fun i ↦ center (A i)

Tactic:
by
  classical
  ext x
  simp only [mem_pi, mem_center_iff, isMulCentral_iff, mem_univ, forall_true_left,
    commute_iff_eq, funext_iff, Pi.mul_def]
  refine ⟨fun ⟨h1, h2, h3⟩ i ↦ ?_, by grind⟩
  exact ⟨fun a ↦ by simpa using h1 (update x i a) i,
    fun b c ↦ by simpa using h2 (update x i b) (update x i c) i,
    fun a b ↦ by simpa using h3 (update x i a) (update x i b) i⟩

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : DivisionMonoid M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a / b ∈ center M

Tactic:
by
  rw [div_eq_mul_inv]
  exact mul_mem_center ha (inv_mem_center hb)

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

Goal state before:
pp: G : Type u_3
inst✝ : Group G
g h : G
⊢ (∃ x, x • h = g) ↔ ∃ c, c * h * c⁻¹ = g

Tactic:
;

Goal state after:
G : Type u_3
inst✝ : Group G
g h : G
⊢ (∃ x, x • h = g) ↔ ∃ c, c * h * c⁻¹ = g
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case e'_5
α : 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' : f c = f c' ∧ rβ (g c) (g c')
⊢ ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩ = ⟨⟨f c', ⋯⟩, ?inr.convert_4⟩

pp: case inr.convert_4
α : 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' : f c = f c' ∧ rβ (g c) (g c')
⊢ { x // x ∈ f ⁻¹' {↑⟨f c', ⋯⟩} }

pp: case inr.convert_6
α : 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' : f c = f c' ∧ rβ (g c) (g c')
⊢ Subrel (rβ on g) (fun x ↦ x ∈ f ⁻¹' {↑⟨f c', ⋯⟩}) ?inr.convert_4 ⟨c', ⋯⟩

Tactic:
;

Goal state after:
case e'_5
α : 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' : f c = f c' ∧ rβ (g c) (g c')
⊢ ⟨⟨f c, ⋯⟩, ⟨c, ⋯⟩⟩ = ⟨⟨f c', ⋯⟩, ?inr.convert_4⟩

case inr.convert_4
α : 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' : f c = f c' ∧ rβ (g c) (g c')
⊢ { x // x ∈ f ⁻¹' {↑⟨f c', ⋯⟩} }

case inr.convert_6
α : 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' : f c = f c' ∧ rβ (g c) (g c')
⊢ Subrel (rβ on g) (fun x ↦ x ∈ f ⁻¹' {↑⟨f c', ⋯⟩}) ?inr.convert_4 ⟨c', ⋯⟩
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:
dsimp only [InvImage, (· on ·)] at h' ⊢
    convert! PSigma.Lex.right (⟨_, c', rfl⟩ : range f) _ using 1; swap
    exacts [⟨c, h'.1⟩, PSigma.subtype_ext (Subtype.ext h'.1) rfl, h'.2]

Goal state after:
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', ⋯⟩, ?inr.convert_4⟩

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 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 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⟩

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', ⋯⟩} }

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', ⋯⟩
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
S : Type u_4
inst✝² : Group G
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
s : S
a : G
ha : a ∈ s
x✝ : G
⊢ x✝ ∈ a • ↑s ↔ x✝ ∈ ↑s

Tactic:
;

Goal state after:
G : Type u_2
S : Type u_4
inst✝² : Group G
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
s : S
a : G
ha : a ∈ s
x✝ : G
⊢ x✝ ∈ a • ↑s ↔ x✝ ∈ ↑s
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
S : Type u_4
inst✝² : Group G
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
s : S
a : G
ha : a ∈ s
x✝ : G
⊢ x✝ ∈ MulOpposite.op a • ↑s ↔ x✝ ∈ ↑s

Tactic:
;

Goal state after:
G : Type u_2
S : Type u_4
inst✝² : Group G
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
s : S
a : G
ha : a ∈ s
x✝ : G
⊢ x✝ ∈ MulOpposite.op a • ↑s ↔ x✝ ∈ ↑s
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

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

Tactic:
by
  rw [toSubmonoid_zpowers]
  exact le_sup_left

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
G : Type u_7
inst✝¹ : FunLike G M N
inst✝ : MonoidHomClass G M N
g : G
f : ι → M
s : Finset ι
⊢ (Multiset.map (⇑g ∘ f) s.val).prod = (Multiset.map (fun x ↦ g (f x)) s.val).prod

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_3
N : Type u_4
inst✝³ : CommMonoid M
inst✝² : CommMonoid N
G : Type u_7
inst✝¹ : FunLike G M N
inst✝ : MonoidHomClass G M N
g : G
f : ι → M
s : Finset ι
⊢ (Multiset.map (⇑g ∘ f) s.val).prod = (Multiset.map (fun x ↦ g (f x)) s.val).prod
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h
α : Type u_3
inst✝ : Monoid α
y : α
a✝ : List α
comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute
h : ∀ x ∈ ⟦a✝⟧, Commute y x
⊢ Commute y (noncommProd ⟦a✝⟧ comm)

Tactic:
simp only [quot_mk_to_coe, noncommProd_coe]

Goal state after:
case h
α : Type u_3
inst✝ : Monoid α
y : α
a✝ : List α
comm : {x | x ∈ ⟦a✝⟧}.Pairwise Commute
h : ∀ x ∈ ⟦a✝⟧, Commute y x
⊢ Commute y a✝.prod
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
⊢ (Multiset.map ((fun x ↦ f x) ∘ ⇑e) s.val).prod = ∏ x ∈ s, f (e x)

Tactic:
;

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
e : ι ↪ κ
f : κ → M
⊢ (Multiset.map ((fun x ↦ f x) ∘ ⇑e) s.val).prod = ∏ x ∈ s, f (e x)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: case mul
G : Type u_2
inst✝¹ : Group G
X : Type u_5
inst✝ : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g x✝ y✝ : G
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : ∀ {x : X}, x ∈ t → x✝ • x ∈ t
h₂ : ∀ {x : X}, x ∈ t → y✝ • x ∈ t
x : X
hx : x ∈ t
⊢ x✝ • y✝ • x ∈ t

Tactic:
;

Goal state after:
case mul
G : Type u_2
inst✝¹ : Group G
X : Type u_5
inst✝ : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g x✝ y✝ : G
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
h₁ : ∀ {x : X}, x ∈ t → x✝ • x ∈ t
h₂ : ∀ {x : X}, x ∈ t → y✝ • x ∈ t
x : X
hx : x ∈ t
⊢ x✝ • y✝ • x ∈ t
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).sum % n = (Multiset.map (fun i ↦ f i % n) s.val).sum % n

Tactic:
;

Goal state after:
ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).sum % n = (Multiset.map (fun i ↦ f i % n) s.val).sum % n
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).prod % n = (Multiset.map (fun i ↦ f i % n) s.val).prod % n

Tactic:
;

Goal state after:
ι : Type u_1
s : Finset ι
n : ℕ
f : ι → ℕ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).prod % n = (Multiset.map (fun i ↦ f i % n) s.val).prod % n
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).sum % n = (Multiset.map (fun i ↦ f i % n) s.val).sum % n

Tactic:
;

Goal state after:
ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).sum % n = (Multiset.map (fun i ↦ f i % n) s.val).sum % n
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).prod % n = (Multiset.map (fun i ↦ f i % n) s.val).prod % n

Tactic:
;

Goal state after:
ι : Type u_1
s : Finset ι
n : ℤ
f : ι → ℤ
⊢ (Multiset.map ((fun x ↦ x % n) ∘ fun i ↦ f i) s.val).prod % n = (Multiset.map (fun i ↦ f i % n) s.val).prod % n
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : List M
⊢ s.prod = s.sum

Tactic:
;

Goal state after:
M : Type u_3
inst✝ : Monoid M
s : List M
⊢ s.prod = s.sum
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : Monoid M
s : List (Additive M)
⊢ s.sum = s.prod

Tactic:
;

Goal state after:
M : Type u_3
inst✝ : Monoid M
s : List (Additive M)
⊢ s.sum = s.prod
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : AddMonoid M
s : List M
⊢ s.sum = s.prod

Tactic:
;

Goal state after:
M : Type u_3
inst✝ : AddMonoid M
s : List M
⊢ s.sum = s.prod
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : AddMonoid M
s : List (Multiplicative M)
⊢ s.prod = s.sum

Tactic:
;

Goal state after:
M : Type u_3
inst✝ : AddMonoid M
s : List (Multiplicative M)
⊢ s.prod = s.sum
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
⊢ s.prod = s.sum

Tactic:
;

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
s : Multiset M
⊢ s.prod = s.sum
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
s : Multiset (Additive M)
⊢ s.sum = s.prod

Tactic:
;

Goal state after:
M : Type u_3
inst✝ : CommMonoid M
s : Multiset (Additive M)
⊢ s.sum = s.prod
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : AddCommMonoid M
s : Multiset M
⊢ s.sum = s.prod

Tactic:
;

Goal state after:
M : Type u_3
inst✝ : AddCommMonoid M
s : Multiset M
⊢ s.sum = s.prod
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: M : Type u_3
inst✝ : AddCommMonoid M
s : Multiset (Multiplicative M)
⊢ s.prod = s.sum

Tactic:
;

Goal state after:
M : Type u_3
inst✝ : AddCommMonoid M
s : Multiset (Multiplicative M)
⊢ s.prod = s.sum