mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case neg.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ z ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}

pp: case neg.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ y ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}

Tactic:
·

Goal state after:
case neg.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ z ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : x = a
⊢ f x = 1

pp: case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : ¬x = a
⊢ f x = 1

Tactic:
·

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : x = a
⊢ f x = 1
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ y ∈ P

pp: case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ y ≠ 1

pp: case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ y ≤ z * y

pp: case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ ¬z * y ≤ y

Tactic:
·

Goal state after:
case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ y ∈ P
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : ¬x = a
⊢ f x = 1

Tactic:
·

Goal state after:
case neg
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : ¬x = a
⊢ f x = 1
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ y ≠ 1

pp: case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ y ≤ z * y

pp: case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ ¬z * y ≤ y

Tactic:
·

Goal state after:
case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ y ≠ 1
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ y ≤ z * y

pp: case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ ¬z * y ≤ y

Tactic:
·

Goal state after:
case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ y ≤ z * y
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ ¬z * y ≤ y

Tactic:
·

Goal state after:
case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ ¬z * y ≤ y
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
⊢ (↑s).PairwiseDisjoint t'

pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
⊢ ∏ x ∈ s, ∏ i ∈ t' x, f i = ∏ x ∈ s, ∏ i ∈ t x, f i

Tactic:
·

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
⊢ (↑s).PairwiseDisjoint t'
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
⊢ ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i

Tactic:
let t' k := (t k).filter (fun i ↦ f i ≠ 1)
  have : s.biUnion t' = (s.biUnion t).filter (fun i ↦ f i ≠ 1) := by grind
  rw [← prod_filter_ne_one, ← this, prod_biUnion]
  swap
  · intro i hi j hj hij a hai haj k hk
    have hki : k ∈ t' i := hai hk
    have hkj : k ∈ t' j := haj hk
    simp only [ne_eq, mem_filter, t'] at hki hkj
    exact (hki.2 (hs hi hj hij k (by grind))).elim
  exact Finset.prod_congr rfl (fun i hi ↦ prod_filter_ne_one (t i))

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

Goal state before:
pp: M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ (∏ a ∈ s, f a) * ∏ a ∈ sᶜ, f a = ∏ i, f i

pp: case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ sᶜ ↔ ¬p x

pp: case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ s ↔ p x

Tactic:
·

Goal state after:
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ (∏ a ∈ s, f a) * ∏ a ∈ sᶜ, f a = ∏ i, f i
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ sᶜ ↔ ¬p x

pp: case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ s ↔ p x

Tactic:
·

Goal state after:
case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ sᶜ ↔ ¬p x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ s ↔ p x

Tactic:
·

Goal state after:
case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ s ↔ p x
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ ⁅z, ⁅x, y⁆⁆ = x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹

pp: G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹ = 1

Tactic:
·

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ ⁅z, ⁅x, y⁆⁆ = x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹ = 1

Tactic:
·

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹ = 1
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K
⊢ ⁅H, K⁆ ≤ K

pp: case refine_2
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : ⁅H, K⁆ ≤ K
h : G
hh : h ∈ H
k : G
hk : k ∈ K
⊢ h * k * h⁻¹ ∈ K

Tactic:
·

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : ∀ h ∈ H, ∀ k ∈ K, h * k * h⁻¹ ∈ K
⊢ ⁅H, K⁆ ≤ K
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : ⁅H, K⁆ ≤ K
h : G
hh : h ∈ H
k : G
hk : k ∈ K
⊢ h * k * h⁻¹ ∈ K

Tactic:
·

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : ⁅H, K⁆ ≤ K
h : G
hh : h ∈ H
k : G
hk : k ∈ K
⊢ h * k * h⁻¹ ∈ K
Module: Mathlib.GroupTheory.Commutator.Basic

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

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

Tactic:
·

Goal state after:
case left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅f g₁, f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

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

Tactic:
·

Goal state after:
case right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ ∀ g₁ ∈ map f H₁, ∀ g₂ ∈ map f H₂, ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁.prod K₁, H₂.prod K₂⁆ ≤ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆

pp: case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
·

Goal state after:
case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁.prod K₁, H₂.prod K₂⁆ ≤ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
·

Goal state after:
case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case a.left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
·

Goal state after:
case a.left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case a.right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
·

Goal state after:
case a.right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

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

Tactic:
·

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

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

Tactic:
·

Goal state after:
case hy
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ map f ⊤ = f.range
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case h₁
G : Type u_1
inst✝ : Group G
⊢ ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G) ⊆ commutatorSet G

pp: case h₂
G : Type u_1
inst✝ : Group G
⊢ commutatorSet G ⊆ ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G)

Tactic:
·

Goal state after:
case h₁
G : Type u_1
inst✝ : Group G
⊢ ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G) ⊆ commutatorSet G
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case h₂
G : Type u_1
inst✝ : Group G
⊢ commutatorSet G ⊆ ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G)

Tactic:
·

Goal state after:
case h₂
G : Type u_1
inst✝ : Group G
⊢ commutatorSet G ⊆ ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G)
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : IsMulCommutative (G ⧸ N)
⊢ _root_.commutator G ≤ N

pp: case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x' y' : G ⧸ N
⊢ x' * y' = y' * x'

Tactic:
·

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : IsMulCommutative (G ⧸ N)
⊢ _root_.commutator G ≤ N
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x' y' : G ⧸ N
⊢ x' * y' = y' * x'

Tactic:
·

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hGN : _root_.commutator G ≤ N
x' y' : G ⧸ N
⊢ x' * y' = y' * x'
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
⊢ ∀ {x y : X × ↥S},
    (∃ u v, u • y.fst = v • x.fst ∧ ↑u * ↑y.snd = v * ↑x.snd) → ∃ u v, u • x.fst = v • y.fst ∧ ↑u * ↑x.snd = v * ↑y.snd

pp: case refine_2
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
⊢ ∀ {x y z : X × ↥S},
    (∃ u v, u • y.fst = v • x.fst ∧ ↑u * ↑y.snd = v * ↑x.snd) →
      (∃ u v, u • z.fst = v • y.fst ∧ ↑u * ↑z.snd = v * ↑y.snd) →
        ∃ u v, u • z.fst = v • x.fst ∧ ↑u * ↑z.snd = v * ↑x.snd

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
⊢ ∀ {x y : X × ↥S},
    (∃ u v, u • y.fst = v • x.fst ∧ ↑u * ↑y.snd = v * ↑x.snd) → ∃ u v, u • x.fst = v • y.fst ∧ ↑u * ↑x.snd = v * ↑y.snd