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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h✝ : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
h : Abelianization.of.ker ≤ Subgroup.center ↥(commutator ↥H)
⊢ IsCyclic ↥(commutator ↥H)

Tactic:
]

Goal state after:
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h✝ : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
h : Abelianization.of.ker ≤ Subgroup.center ↥(commutator ↥H)
⊢ IsCyclic ↥(commutator ↥H)
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case ind.inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
⊢ commutator ↥H ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆

Tactic:
]

Goal state after:
case ind.inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
⊢ commutator ↥H ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case ind.inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h✝ : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
x✝ : CommGroup (MulAut ↥⁅commutator ↥H, commutator ↥H⁆) :=
  (IsCyclic.mulAutMulEquiv ↥⁅commutator ↥H, commutator ↥H⁆).toMonoidHom.commGroupOfInjective ⋯
h : ⁅⊤, ⊤⁆ ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆
⊢ commutator ↥H ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆

Tactic:
]

Goal state after:
case ind.inr
G : Type u_1
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsZGroup G
H : Subgroup G
h✝ : H ≠ ⊥
hH : IsCyclic ↥⁅commutator ↥H, commutator ↥H⁆
x✝ : CommGroup (MulAut ↥⁅commutator ↥H, commutator ↥H⁆) :=
  (IsCyclic.mulAutMulEquiv ↥⁅commutator ↥H, commutator ↥H⁆).toMonoidHom.commGroupOfInjective ⋯
h : ⁅⊤, ⊤⁆ ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆
⊢ commutator ↥H ≤ Subgroup.centralizer ↑⁅commutator ↥H, commutator ↥H⁆
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case cons.refine_1
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
i : ι
g : G i
w : Word G
hIdx : w.fstIdx ≠ some i
hg1 : g ≠ 1
ih : Reduced φ w → ∃ w', w'.prod = ofCoprodI w.prod ∧ List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
hw : Reduced φ (Word.cons g w hIdx hg1)
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
⊢ Option.map Sigma.fst w.toList.head? ≠ some i

Tactic:
]

Goal state after:
case cons.refine_1
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
i : ι
g : G i
w : Word G
hIdx : w.fstIdx ≠ some i
hg1 : g ≠ 1
ih : Reduced φ w → ∃ w', w'.prod = ofCoprodI w.prod ∧ List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
hw : Reduced φ (Word.cons g w hIdx hg1)
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
⊢ Option.map Sigma.fst w.toList.head? ≠ some i
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case pos
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : Subsingleton K ∧ Nonempty K
hc : Nat.card G = 0
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ k q, k • q * q⁻¹ = g

Tactic:
]

Goal state after:
case pos
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : Subsingleton K ∧ Nonempty K
hc : Nat.card G = 0
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ k q, k • q * q⁻¹ = g
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
g : G
k : K
n : ℤ
h : ϕ k = ↑(n + 1)
⊢ k • g * g⁻¹ = g ^ n

Tactic:
]

Goal state after:
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
g : G
k : K
n : ℤ
h : ϕ k = ↑(n + 1)
⊢ k • g * g⁻¹ = g ^ n
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic G
hG : IsPGroup p G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
g : G
k : K
n : ℤ
h : ϕ k = ↑(n + 1)
⊢ g ^ n = g ^ n

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : IsCyclic G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h : ∀ (g : G) (k : K) (n : ℤ), ϕ k - 1 = ↑n → k • g * g⁻¹ = g ^ n
hG : ∀ (k : K), ϕ k = 1 ∨ IsUnit (ϕ k - 1)
hϕ : ∀ (a : K), ϕ a = 1
p : G
k : K
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : IsCyclic G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h : ∀ (g : G) (k : K) (n : ℤ), ϕ k - 1 = ↑n → k • g * g⁻¹ = g ^ n
hG : ∀ (k : K), ϕ k = 1 ∨ IsUnit (ϕ k - 1)
hϕ : ∀ (a : K), ϕ a = 1
p : G
k : K
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
h : H
heq : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = w'.prod
this : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h
⊢ w = Word.empty

Tactic:
]

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
h : H
heq : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = w'.prod
this : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h
⊢ w = Word.empty
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case neg.inr
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h : ∀ (g : G) (k : K) (n : ℤ), ϕ k - 1 = ↑n → k • g * g⁻¹ = g ^ n
hG : ∀ (k : K), ϕ k = 1 ∨ IsUnit (ϕ k - 1)
k : K
hk : ¬ϕ k = 1
u v : ZMod (Nat.card G)
hvu : v * ↑u.cast = 1
hu : ↑u.cast = ϕ k - 1
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ k q, k • q * q⁻¹ = g

Tactic:
]

Goal state after:
case neg.inr
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h : ∀ (g : G) (k : K) (n : ℤ), ϕ k - 1 = ↑n → k • g * g⁻¹ = g ^ n
hG : ∀ (k : K), ϕ k = 1 ∨ IsUnit (ϕ k - 1)
k : K
hk : ¬ϕ k = 1
u v : ZMod (Nat.card G)
hvu : v * ↑u.cast = 1
hu : ↑u.cast = ϕ k - 1
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ k q, k • q * q⁻¹ = g
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
w : Word G
hw : Reduced φ w
d : Transversal φ
w' : NormalWord d
hw'prod : w'.prod = ofCoprodI w.prod
hw'map : List.map Sigma.fst w'.toList = List.map Sigma.fst w.toList
h : H
heq : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = w'.prod
this : { toWord := Word.empty, head := h, normalized := ⋯ }.prod = (base φ) h
⊢ { toWord := Word.empty, head := h, normalized := ⋯ }.toWord = Word.empty

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case neg.inr
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h : ∀ (g : G) (k : K) (n : ℤ), ϕ k - 1 = ↑n → k • g * g⁻¹ = g ^ n
hG : ∀ (k : K), ϕ k = 1 ∨ IsUnit (ϕ k - 1)
k : K
hk : ¬ϕ k = 1
u v : ZMod (Nat.card G)
hvu : v.cast * u.cast ≡ 1 [ZMOD ↑(Nat.card G)]
hu : ↑u.cast = ϕ k - 1
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ k q, k • q * q⁻¹ = g

Tactic:
]

Goal state after:
case neg.inr
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : IsCyclic G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h : ∀ (g : G) (k : K) (n : ℤ), ϕ k - 1 = ↑n → k • g * g⁻¹ = g ^ n
hG : ∀ (k : K), ϕ k = 1 ∨ IsUnit (ϕ k - 1)
k : K
hk : ¬ϕ k = 1
u v : ZMod (Nat.card G)
hvu : v.cast * u.cast ≡ 1 [ZMOD ↑(Nat.card G)]
hu : ↑u.cast = ϕ k - 1
⊢ (∀ (g : G) (k : K), k • g * g⁻¹ = 1) ∨ ∀ (g : G), ∃ k q, k • q * q⁻¹ = g
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case neg.inr
G : Type u_1
inst✝⁴ : Group G
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : IsCyclic G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h : ∀ (g : G) (k : K) (n : ℤ), ϕ k - 1 = ↑n → k • g * g⁻¹ = g ^ n
hG : ∀ (k : K), ϕ k = 1 ∨ IsUnit (ϕ k - 1)
k : K
hk : ¬ϕ k = 1
u v : ZMod (Nat.card G)
hvu : v.cast * u.cast ≡ 1 [ZMOD ↑(Nat.card G)]
hu : ↑u.cast = ϕ k - 1
p : G
⊢ v.cast * u.cast ≡ 1 [ZMOD ↑(orderOf p)]

Tactic:
]

Goal state after:
case neg.inr
G : Type u_1
inst✝⁴ : Group G
p✝ : ℕ
inst✝³ : Fact (Nat.Prime p✝)
inst✝² : IsCyclic G
K : Type u_4
inst✝¹ : Group K
inst✝ : MulDistribMulAction K G
hGK : (Nat.card G).Coprime (Nat.card K)
hc : ¬Nat.card G = 0
this : Finite G
ϕ : K →* ZMod (Nat.card G) := MulDistribMulAction.toMonoidHomZModOfIsCyclic G K ⋯
h : ∀ (g : G) (k : K) (n : ℤ), ϕ k - 1 = ↑n → k • g * g⁻¹ = g ^ n
hG : ∀ (k : K), ϕ k = 1 ∨ IsUnit (ϕ k - 1)
k : K
hk : ¬ϕ k = 1
u v : ZMod (Nat.card G)
hvu : v.cast * u.cast ≡ 1 [ZMOD ↑(Nat.card G)]
hu : ↑u.cast = ϕ k - 1
p : G
⊢ v.cast * u.cast ≡ 1 [ZMOD ↑(orderOf p)]
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_1
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P K : Subgroup G
inst✝ : IsCyclic ↥P
hP : IsPGroup p ↥P
hKP : K ≤ Subgroup.normalizer ↑P
hPK : (Nat.card ↥P).Coprime (Nat.card ↥K)
x✝ : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P) (k : ↥K), k • g * g⁻¹ = 1
⊢ ∀ g₁ ∈ K, ∀ g₂ ∈ P, ⁅g₁, g₂⁆ ∈ ⊥

Tactic:
]

Goal state after:
case refine_1
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P K : Subgroup G
inst✝ : IsCyclic ↥P
hP : IsPGroup p ↥P
hKP : K ≤ Subgroup.normalizer ↑P
hPK : (Nat.card ↥P).Coprime (Nat.card ↥K)
x✝ : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P) (k : ↥K), k • g * g⁻¹ = 1
⊢ ∀ g₁ ∈ K, ∀ g₂ ∈ P, ⁅g₁, g₂⁆ ∈ ⊥
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_2
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P K : Subgroup G
inst✝ : IsCyclic ↥P
hP : IsPGroup p ↥P
hKP : K ≤ Subgroup.normalizer ↑P
hPK : (Nat.card ↥P).Coprime (Nat.card ↥K)
x✝ : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P), ∃ k q, k • q * q⁻¹ = g
⊢ (∀ g₁ ∈ K, ∀ g₂ ∈ P, ⁅g₁, g₂⁆ ∈ P) ∧ P ≤ ⁅K, P⁆

Tactic:
]

Goal state after:
case refine_2
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P K : Subgroup G
inst✝ : IsCyclic ↥P
hP : IsPGroup p ↥P
hKP : K ≤ Subgroup.normalizer ↑P
hPK : (Nat.card ↥P).Coprime (Nat.card ↥K)
x✝ : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P), ∃ k q, k • q * q⁻¹ = g
⊢ (∀ g₁ ∈ K, ∀ g₂ ∈ P, ⁅g₁, g₂⁆ ∈ P) ∧ P ≤ ⁅K, P⁆
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_2
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P K : Subgroup G
inst✝ : IsCyclic ↥P
hP : IsPGroup p ↥P
hKP : K ≤ Subgroup.normalizer ↑P
hPK : (Nat.card ↥P).Coprime (Nat.card ↥K)
x✝ : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P), ∃ k q, k • q * q⁻¹ = g
g : G
hg : g ∈ P
k : ↥K
q : ↥P
hkq : k • q * q⁻¹ = ⟨g, hg⟩
⊢ ↑(k • q * q⁻¹) ∈ ⁅K, P⁆

Tactic:
]

Goal state after:
case refine_2
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P K : Subgroup G
inst✝ : IsCyclic ↥P
hP : IsPGroup p ↥P
hKP : K ≤ Subgroup.normalizer ↑P
hPK : (Nat.card ↥P).Coprime (Nat.card ↥K)
x✝ : MulDistribMulAction ↥K ↥P := MulDistribMulAction.compHom (↥P) (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
h : ∀ (g : ↥P), ∃ k q, k • q * q⁻¹ = g
g : G
hg : g ∈ P
k : ↥K
q : ↥P
hkq : k • q * q⁻¹ = ⟨g, hg⟩
⊢ ↑(k • q * q⁻¹) ∈ ⁅K, P⁆
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
i j : ι
hij : i ≠ j
⊢ ((of i).comp (φ i)).range ≤ (of i).range

Tactic:
]

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
i j : ι
hij : i ≠ j
⊢ ((of i).comp (φ i)).range ≤ (of i).range
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
i j : ι
hij : i ≠ j
⊢ ((of j).comp (φ j)).range ≤ (of j).range

Tactic:
]

Goal state after:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Group (G i)
inst✝ : Group H
φ : (i : ι) → H →* G i
hφ : ∀ (i : ι), Injective ⇑(φ i)
i j : ι
hij : i ≠ j
⊢ ((of j).comp (φ j)).range ≤ (of j).range
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_1
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : Finite G
P : Sylow p G
inst✝¹ : IsCyclic ↥↑P
inst✝ : (↑P).Normal
K : Subgroup G
hK : K.IsComplement' ↑P
h : ↑↑P ⊆ ↑(Subgroup.center G)
⊢ ↑P ≤ Subgroup.center G

Tactic:
]

Goal state after:
case refine_1
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : Finite G
P : Sylow p G
inst✝¹ : IsCyclic ↥↑P
inst✝ : (↑P).Normal
K : Subgroup G
hK : K.IsComplement' ↑P
h : ↑↑P ⊆ ↑(Subgroup.center G)
⊢ ↑P ≤ Subgroup.center G
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_2
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : Finite G
P : Sylow p G
inst✝¹ : IsCyclic ↥↑P
inst✝ : (↑P).Normal
K : Subgroup G
hK : K.IsComplement' ↑P
h : ⁅K, ↑P⁆ = ↑P
⊢ ⁅K, ↑P⁆ ≤ ⁅⊤, ⊤⁆

Tactic:
]

Goal state after:
case refine_2
G : Type u_1
inst✝⁴ : Group G
p : ℕ
inst✝³ : Fact (Nat.Prime p)
inst✝² : Finite G
P : Sylow p G
inst✝¹ : IsCyclic ↥↑P
inst✝ : (↑P).Normal
K : Subgroup G
hK : K.IsComplement' ↑P
h : ⁅K, ↑P⁆ = ↑P
⊢ ⁅K, ↑P⁆ ≤ ⁅⊤, ⊤⁆
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : Subgroup.normalizer ↑P ≤ Subgroup.map (Subgroup.normalizer ↑P).subtype (Subgroup.centralizer ↑↑Q)
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P

Tactic:
]

Goal state after:
case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : Subgroup.normalizer ↑P ≤ Subgroup.map (Subgroup.normalizer ↑P).subtype (Subgroup.centralizer ↑↑Q)
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : Subgroup.normalizer ↑↑P ≤ Subgroup.centralizer ↑↑P
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P

Tactic:
]

Goal state after:
case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : Subgroup.normalizer ↑↑P ≤ Subgroup.centralizer ↑↑P
⊢ Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_2
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : ↑P ≤ ⁅Subgroup.normalizer ↑↑P, Subgroup.normalizer ↑↑P⁆
⊢ ↑P ≤ commutator G

Tactic:
]

Goal state after:
case refine_2
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
Q : Sylow p ↥(Subgroup.normalizer ↑P) := P.subtype ⋯
this✝ : (↑Q).Normal
this : IsCyclic ↥↑Q
h : ↑P ≤ ⁅Subgroup.normalizer ↑↑P, Subgroup.normalizer ↑↑P⁆
⊢ ↑P ≤ commutator G
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
I : Finset ι
κ : ι → Kernel α β
a : α
s : Set β
⊢ ∑ i ∈ I, ((κ i) a) s = ∑ i ∈ I, ((κ i) a) s

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
hP : Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P
h : p ∣ Nat.card ↥(commutator G)
⊢ Nat.card ↥(commutator G) ∣ Nat.card ↥(MonoidHom.transferSylow P hP).ker

Tactic:
]

Goal state after:
case refine_1
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite G
P : Sylow p G
inst✝ : IsCyclic ↥↑P
hP : Subgroup.normalizer ↑P ≤ Subgroup.centralizer ↑P
h : p ∣ Nat.card ↥(commutator G)
⊢ Nat.card ↥(commutator G) ∣ Nat.card ↥(MonoidHom.transferSylow P hP).ker
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case inl
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
f : G →* G'
f' : G' →* G''
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : IsZGroup G''
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
h : ↑P ≤ f'.ker
h_le : ↑P ≤ f.range
Q : Sylow p G
hQ : Subgroup.map f.rangeRestrict ↑Q = (↑P).subgroupOf f.range
⊢ IsCyclic ↥((↑P).subgroupOf f.range)

Tactic:
]

Goal state after:
case inl
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
f : G →* G'
f' : G' →* G''
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : IsZGroup G''
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
h : ↑P ≤ f'.ker
h_le : ↑P ≤ f.range
Q : Sylow p G
hQ : Subgroup.map f.rangeRestrict ↑Q = (↑P).subgroupOf f.range
⊢ IsCyclic ↥((↑P).subgroupOf f.range)
Module: Mathlib.GroupTheory.SpecificGroups.ZGroup

Goal state before:
pp: case inr
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
f : G →* G'
f' : G' →* G''
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : IsZGroup G''
h_le : f'.ker ≤ f.range
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this✝ : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker ↑P
this : IsCyclic ↥(Subgroup.map f' ↑P)
⊢ Disjoint f'.ker ↑P

Tactic:
]

Goal state after:
case inr
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst✝⁵ : Group G
inst✝⁴ : Group G'
inst✝³ : Group G''
f : G →* G'
f' : G' →* G''
inst✝² : Finite G
inst✝¹ : IsZGroup G
inst✝ : IsZGroup G''
h_le : f'.ker ≤ f.range
p : ℕ
hp : Nat.Prime p
P : Sylow p G'
this✝ : Fact (Nat.Prime p)
h_cop : (Nat.card ↥f'.ker).Coprime f'.ker.index
h : Disjoint f'.ker ↑P
this : IsCyclic ↥(Subgroup.map f' ↑P)
⊢ Disjoint f'.ker ↑P
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x : (i : ι) → β i
⊢ ∀ ⦃x_1 : ι⦄, x_1 ∈ univ → ¬x x_1 ≠ x x_1

Tactic:
]

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x : (i : ι) → β i
⊢ ∀ ⦃x_1 : ι⦄, x_1 ∈ univ → ¬x x_1 ≠ x x_1
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
a : α
s : Set β
hs : MeasurableSet s
h : (κ a) s = (η a) s
⊢ (η a) s = (η a) s

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : κ = η
a : α
f : β → ℝ≥0∞
x✝ : Measurable f
⊢ ∫⁻ (b : β), f b ∂η a = ∫⁻ (b : β), f b ∂η a

Tactic:
]

Goal state after:
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ {i | x i ≠ z i} ⊆ {a | x a ≠ y a ∨ y a ≠ z a}

Tactic:
]

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ {i | x i ≠ z i} ⊆ {a | x a ≠ y a ∨ y a ≠ z a}
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ hammingDist x y ≤ hammingDist x z + hammingDist z y

Tactic:
]

Goal state after:
ι : Type u_2
β : ι → Type u_3
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (β i)
x y z : (i : ι) → β i
⊢ hammingDist x y ≤ hammingDist x z + hammingDist z y