mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.VectorBundle.Pullback

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
E : B → Type u_5
n : WithTop ℕ∞
inst✝¹⁹ : NontriviallyNormedField 𝕜
inst✝¹⁸ : (x : B) → AddCommMonoid (E x)
inst✝¹⁷ : (x : B) → Module 𝕜 (E x)
inst✝¹⁶ : NormedAddCommGroup F
inst✝¹⁵ : NormedSpace 𝕜 F
inst✝¹⁴ : TopologicalSpace (TotalSpace F E)
inst✝¹³ : (x : B) → TopologicalSpace (E x)
EB : Type u_6
inst✝¹² : NormedAddCommGroup EB
inst✝¹¹ : NormedSpace 𝕜 EB
HB : Type u_7
inst✝¹⁰ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁹ : TopologicalSpace B
inst✝⁸ : ChartedSpace HB B
EB' : Type u_8
inst✝⁷ : NormedAddCommGroup EB'
inst✝⁶ : NormedSpace 𝕜 EB'
HB' : Type u_9
inst✝⁵ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁴ : TopologicalSpace B'
inst✝³ : ChartedSpace HB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : ContMDiffVectorBundle n F E IB
f : C^n⟮IB', B'; IB, B⟯
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : f b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ (↑(e'.pullback f) (↑(e.pullback f).symm (b, v))).2 = (↑e' ⟨f b, e.symm (f b) v⟩).2

pp: case hb
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
E : B → Type u_5
n : WithTop ℕ∞
inst✝¹⁹ : NontriviallyNormedField 𝕜
inst✝¹⁸ : (x : B) → AddCommMonoid (E x)
inst✝¹⁷ : (x : B) → Module 𝕜 (E x)
inst✝¹⁶ : NormedAddCommGroup F
inst✝¹⁵ : NormedSpace 𝕜 F
inst✝¹⁴ : TopologicalSpace (TotalSpace F E)
inst✝¹³ : (x : B) → TopologicalSpace (E x)
EB : Type u_6
inst✝¹² : NormedAddCommGroup EB
inst✝¹¹ : NormedSpace 𝕜 EB
HB : Type u_7
inst✝¹⁰ : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst✝⁹ : TopologicalSpace B
inst✝⁸ : ChartedSpace HB B
EB' : Type u_8
inst✝⁷ : NormedAddCommGroup EB'
inst✝⁶ : NormedSpace 𝕜 EB'
HB' : Type u_9
inst✝⁵ : TopologicalSpace HB'
IB' : ModelWithCorners 𝕜 EB' HB'
inst✝⁴ : TopologicalSpace B'
inst✝³ : ChartedSpace HB' B'
inst✝² : FiberBundle F E
inst✝¹ : VectorBundle 𝕜 F E
inst✝ : ContMDiffVectorBundle n F E IB
f : C^n⟮IB', B'; IB, B⟯
e : Trivialization F TotalSpace.proj
he : MemTrivializationAtlas e
e' : Trivialization F TotalSpace.proj
he' : MemTrivializationAtlas e'
b : B'
hb : f b ∈ e.baseSet ∩ e'.baseSet
v : F
⊢ b ∈ (e.pullback f).baseSet ∩ (e'.pullback f).baseSet

Tactic:
exacts [rfl, hb]

Goal state after:
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: case «0»
P : Type u_3
n : ℕ
inst✝ : NeZero 0
poly : Polygon P 0
h : poly.HasNondegenerateEdges
hlt : 0 < 2
⊢ False

pp: case «1»
P : Type u_3
n : ℕ
inst✝ : NeZero 1
poly : Polygon P 1
h : poly.HasNondegenerateEdges
hlt : 1 < 2
⊢ False

Tactic:
·

Goal state after:
case «0»
P : Type u_3
n : ℕ
inst✝ : NeZero 0
poly : Polygon P 0
h : poly.HasNondegenerateEdges
hlt : 0 < 2
⊢ False
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: case «1»
P : Type u_3
n : ℕ
inst✝ : NeZero 1
poly : Polygon P 1
h : poly.HasNondegenerateEdges
hlt : 1 < 2
⊢ False

Tactic:
·

Goal state after:
case «1»
P : Type u_3
n : ℕ
inst✝ : NeZero 1
poly : Polygon P 1
h : poly.HasNondegenerateEdges
hlt : 1 < 2
⊢ False
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Fintype.card ↑x.carrier =
    ∑ x ∈ (noncenter G).toFinset, Fintype.card ↑x.carrier

pp: case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card ↥(Subgroup.center G) = ∑ x ∈ Finset.univ \ (noncenter G).toFinset, Fintype.card ↑x.carrier

Tactic:
·

Goal state after:
case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Fintype.card ↑x.carrier =
    ∑ x ∈ (noncenter G).toFinset, Fintype.card ↑x.carrier
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: case e'_2.e'_5
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card ↥(Subgroup.center G) = Nat.card ↥(Subgroup.center G)

pp: case e'_2.e'_6
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ x ∈ (noncenter G).toFinset, x.carrier.toFinset.card =
    ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier

pp: case e'_3
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card G = Nat.card G

Tactic:
·

Goal state after:
case e'_2.e'_5
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card ↥(Subgroup.center G) = Nat.card ↥(Subgroup.center G)
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: case e'_2.e'_6
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ x ∈ (noncenter G).toFinset, x.carrier.toFinset.card =
    ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier

pp: case e'_3
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card G = Nat.card G

Tactic:
·

Goal state after:
case e'_2.e'_6
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ x ∈ (noncenter G).toFinset, x.carrier.toFinset.card =
    ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: case e'_2.e'_6
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ x ∈ (noncenter G).toFinset, x.carrier.toFinset.card =
    ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier

Tactic:
rw [← finsum_set_coe_eq_finsum_mem (noncenter G), finsum_eq_sum_of_fintype,
      ← Finset.sum_set_coe]

Goal state after:
case e'_2.e'_6
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ i, (↑i).carrier.toFinset.card = ∑ i, Nat.card ↑(↑i).carrier
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: case e'_3
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card G = Nat.card G

Tactic:
·

Goal state after:
case e'_3
G : Type u_2
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑x.carrier
inst✝² : Fintype G
inst✝¹ : Fintype ↥(Subgroup.center G)
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card G = Nat.card G
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: case h₁
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ map (MonoidHom.mulSingle Gs i) (H i) ≤ pi Set.univ H

Tactic:
·

Goal state after:
case h₁
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ map (MonoidHom.mulSingle Gs i) (H i) ≤ pi Set.univ H
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: case pos
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(H i)
h : j = i
⊢ (MonoidHom.mulSingle Gs i) x ∈ comap (Pi.evalMonoidHom Gs j) (H j)

pp: case neg
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(H i)
h : ¬j = i
⊢ (MonoidHom.mulSingle Gs i) x ∈ comap (Pi.evalMonoidHom Gs j) (H j)

Tactic:
·

Goal state after:
case pos
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(H i)
h : j = i
⊢ (MonoidHom.mulSingle Gs i) x ∈ comap (Pi.evalMonoidHom Gs j) (H j)
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: case neg
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(H i)
h : ¬j = i
⊢ (MonoidHom.mulSingle Gs i) x ∈ comap (Pi.evalMonoidHom Gs j) (H j)

Tactic:
·

Goal state after:
case neg
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(H i)
h : ¬j = i
⊢ (MonoidHom.mulSingle Gs i) x ∈ comap (Pi.evalMonoidHom Gs j) (H j)
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: case h₂
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ map (MonoidHom.mulSingle Gs i) (K i) ≤ pi Set.univ K

Tactic:
·

Goal state after:
case h₂
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ map (MonoidHom.mulSingle Gs i) (K i) ≤ pi Set.univ K
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: case pos
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(K i)
h : j = i
⊢ (MonoidHom.mulSingle Gs i) x ∈ comap (Pi.evalMonoidHom Gs j) (K j)

pp: case neg
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(K i)
h : ¬j = i
⊢ (MonoidHom.mulSingle Gs i) x ∈ comap (Pi.evalMonoidHom Gs j) (K j)

Tactic:
·

Goal state after:
case pos
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(K i)
h : j = i
⊢ (MonoidHom.mulSingle Gs i) x ∈ comap (Pi.evalMonoidHom Gs j) (K j)
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: case neg
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(K i)
h : ¬j = i
⊢ (MonoidHom.mulSingle Gs i) x ∈ comap (Pi.evalMonoidHom Gs j) (K j)

Tactic:
·

Goal state after:
case neg
η : Type u_2
inst✝¹ : Finite η
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(K i)
h : ¬j = i
⊢ (MonoidHom.mulSingle Gs i) x ∈ comap (Pi.evalMonoidHom Gs j) (K j)
Module: Mathlib.GroupTheory.GroupAction.CardCommute

Goal state before:
pp: case inr
G : Type u_3
inst✝ : Group G
val✝ : Infinite G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

pp: case inl
G : Type u_3
inst✝ : Group G
val✝ : Fintype G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G

Tactic:
·

Goal state after:
case inr
G : Type u_3
inst✝ : Group G
val✝ : Infinite G
⊢ Nat.card { p // Commute p.1 p.2 } = Nat.card (ConjClasses G) * Nat.card G
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: case pos
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : ¬x = 1
hy : ¬y = 1
hxy : x = y
⊢ e (x * y) = e x * e y

pp: case neg
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : ¬x = 1
hy : ¬y = 1
hxy : ¬x = y
⊢ e (x * y) = e x * e y

Tactic:
·

Goal state after:
case pos
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : ¬x = 1
hy : ¬y = 1
hxy : x = y
⊢ e (x * y) = e x * e y
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: case neg
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : ¬x = 1
hy : ¬y = 1
hxy : ¬x = y
⊢ e (x * y) = e x * e y

Tactic:
·

Goal state after:
case neg
G : Type u_1
inst✝⁴ : Group G
inst✝³ : IsKleinFour G
G₁ : Type u_2
G₂ : Type u_3
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : IsKleinFour G₁
e : G₁ ≃ G₂
he : e 1 = 1
h : Monoid.exponent G₂ = 2
_inst₁ : Fintype G₁ := Fintype.ofFinite G₁
_inst₂ : Fintype G₂ := Fintype.ofEquiv G₁ e
x y : G₁
hx : ¬x = 1
hy : ¬y = 1
hxy : ¬x = y
⊢ e (x * y) = e x * e y
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case r
n : ℕ
a : ZMod n
⊢ 1 * r a = r a

pp: case sr
n : ℕ
a : ZMod n
⊢ 1 * sr a = sr a

Tactic:
·

Goal state after:
case r
n : ℕ
a : ZMod n
⊢ 1 * r a = r a
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case sr
n : ℕ
a : ZMod n
⊢ 1 * sr a = sr a

Tactic:
·

Goal state after:
case sr
n : ℕ
a : ZMod n
⊢ 1 * sr a = sr a
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case r
n : ℕ
a : ZMod n
⊢ r a * 1 = r a

pp: case sr
n : ℕ
a : ZMod n
⊢ sr a * 1 = sr a

Tactic:
·

Goal state after:
case r
n : ℕ
a : ZMod n
⊢ r a * 1 = r a
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case sr
n : ℕ
a : ZMod n
⊢ sr a * 1 = sr a

Tactic:
·

Goal state after:
case sr
n : ℕ
a : ZMod n
⊢ sr a * 1 = sr a
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case r
n : ℕ
a : ZMod n
⊢ (r a).inv * r a = 1

pp: case sr
n : ℕ
a : ZMod n
⊢ (sr a).inv * sr a = 1

Tactic:
·

Goal state after:
case r
n : ℕ
a : ZMod n
⊢ (r a).inv * r a = 1
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case sr
n : ℕ
a : ZMod n
⊢ (sr a).inv * sr a = 1

Tactic:
·

Goal state after:
case sr
n : ℕ
a : ZMod n
⊢ (sr a).inv * sr a = 1
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case zero
⊢ Nat.card (DihedralGroup 0) = 2 * 0

pp: case succ
n✝ : ℕ
⊢ Nat.card (DihedralGroup (n✝ + 1)) = 2 * (n✝ + 1)

Tactic:
·

Goal state after:
case zero
⊢ Nat.card (DihedralGroup 0) = 2 * 0
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case succ
n✝ : ℕ
⊢ Nat.card (DihedralGroup (n✝ + 1)) = 2 * (n✝ + 1)

Tactic:
·

Goal state after:
case succ
n✝ : ℕ
⊢ Nat.card (DihedralGroup (n✝ + 1)) = 2 * (n✝ + 1)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case hg
n : ℕ
i : ZMod n
⊢ sr i ^ 2 = 1

pp: case hg1
n : ℕ
i : ZMod n
⊢ sr i ≠ 1

Tactic:
·

Goal state after:
case hg
n : ℕ
i : ZMod n
⊢ sr i ^ 2 = 1
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case hg1
n : ℕ
i : ZMod n
⊢ sr i ≠ 1

Tactic:
·

Goal state after:
case hg1
n : ℕ
i : ZMod n
⊢ sr i ≠ 1
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inl
⊢ orderOf (r 1) = 0

pp: case inr
n : ℕ
hn : NeZero n
⊢ orderOf (r 1) = n

Tactic:
·

Goal state after:
case inl
⊢ orderOf (r 1) = 0
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inr
n : ℕ
hn : NeZero n
⊢ orderOf (r 1) = n

Tactic:
·

Goal state after:
case inr
n : ℕ
hn : NeZero n
⊢ orderOf (r 1) = n
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inl
⊢ Monoid.exponent (DihedralGroup 0) = lcm 0 2

pp: case inr
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (DihedralGroup n) = lcm n 2

Tactic:
·

Goal state after:
case inl
⊢ Monoid.exponent (DihedralGroup 0) = lcm 0 2
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inr.a
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (DihedralGroup n) ∣ lcm n 2

pp: case inr.a
n : ℕ
hn : NeZero n
⊢ lcm n 2 ∣ Monoid.exponent (DihedralGroup n)

Tactic:
·

Goal state after:
case inr.a
n : ℕ
hn : NeZero n
⊢ Monoid.exponent (DihedralGroup n) ∣ lcm n 2
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inr.a.r
n : ℕ
hn : NeZero n
m : ZMod n
⊢ r m ^ lcm n 2 = 1

pp: case inr.a.sr
n : ℕ
hn : NeZero n
m : ZMod n
⊢ sr m ^ lcm n 2 = 1

Tactic:
·

Goal state after:
case inr.a.r
n : ℕ
hn : NeZero n
m : ZMod n
⊢ r m ^ lcm n 2 = 1
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inr.a.sr
n : ℕ
hn : NeZero n
m : ZMod n
⊢ sr m ^ lcm n 2 = 1

Tactic:
·

Goal state after:
case inr.a.sr
n : ℕ
hn : NeZero n
m : ZMod n
⊢ sr m ^ lcm n 2 = 1
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inr.a.sr
n : ℕ
hn : NeZero n
m : ZMod n
⊢ sr m ^ lcm n 2 = 1

Tactic:
rw [← orderOf_dvd_iff_pow_eq_one, orderOf_sr]

Goal state after:
case inr.a.sr
n : ℕ
hn : NeZero n
m : ZMod n
⊢ 2 ∣ lcm n 2
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inr.a
n : ℕ
hn : NeZero n
⊢ lcm n 2 ∣ Monoid.exponent (DihedralGroup n)

Tactic:
·

Goal state after:
case inr.a
n : ℕ
hn : NeZero n
⊢ lcm n 2 ∣ Monoid.exponent (DihedralGroup n)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inr.a.hab
n : ℕ
hn : NeZero n
⊢ n ∣ Monoid.exponent (DihedralGroup n)

pp: case hcb
n : ℕ
hn : NeZero n
⊢ 2 ∣ Monoid.exponent (DihedralGroup n)

Tactic:
·

Goal state after:
case inr.a.hab
n : ℕ
hn : NeZero n
⊢ n ∣ Monoid.exponent (DihedralGroup n)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case hcb
n : ℕ
hn : NeZero n
⊢ 2 ∣ Monoid.exponent (DihedralGroup n)

Tactic:
·

Goal state after:
case hcb
n : ℕ
hn : NeZero n
⊢ 2 ∣ Monoid.exponent (DihedralGroup n)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case pos
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : n = 2
⊢ False

pp: case neg
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : ¬n = 2
⊢ False

Tactic:
·

Goal state after:
case pos
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : n = 2
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case neg
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : ¬n = 2
⊢ False

Tactic:
·

Goal state after:
case neg
n : ℕ
h1 : n ≠ 1
h : IsCyclic (DihedralGroup n)
h2 : ¬n = 2
⊢ False
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Mul β
⊢ commProb (α → β) = commProb β ^ card α

Tactic:
rw [commProb_pi, Finset.prod_const, Finset.card_univ]

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ (∀ (x : M × M), x ∈ {x | Commute x.1 x.2}) ↔ IsMulCommutative M

pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card M) ^ 2 ≠ 0

Tactic:
·

Goal state after:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ (∀ (x : M × M), x ∈ {x | Commute x.1 x.2}) ↔ IsMulCommutative M
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card M) ^ 2 ≠ 0

Tactic:
·

Goal state after:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card M) ^ 2 ≠ 0
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case pos
G : Type u_2
inst✝ : Group G
h : ↑(Nat.card G) = 0
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)

pp: case neg
G : Type u_2
inst✝ : Group G
h : ¬↑(Nat.card G) = 0
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)

Tactic:
·

Goal state after:
case pos
G : Type u_2
inst✝ : Group G
h : ↑(Nat.card G) = 0
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case neg
G : Type u_2
inst✝ : Group G
h : ¬↑(Nat.card G) = 0
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)

Tactic:
·

Goal state after:
case neg
G : Type u_2
inst✝ : Group G
h : ¬↑(Nat.card G) = 0
⊢ ↑(Nat.card (ConjClasses G)) * ↑(Nat.card G) / (↑(Nat.card G) * ↑(Nat.card G)) =
    ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ Nat.card { p // Commute p.1 p.2 } ≤ Nat.card { p // Commute p.1 p.2 }

pp: case h
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ ↑(Nat.card G) ^ 2 ≠ 0

pp: G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ 0 < ↑(Nat.card ↥H) ^ 2

Tactic:
·

Goal state after:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ Nat.card { p // Commute p.1 p.2 } ≤ Nat.card { p // Commute p.1 p.2 }
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case h
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ ↑(Nat.card G) ^ 2 ≠ 0

pp: G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ 0 < ↑(Nat.card ↥H) ^ 2

Tactic:
·

Goal state after:
case h
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ ↑(Nat.card G) ^ 2 ≠ 0
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ 0 < ↑(Nat.card ↥H) ^ 2

Tactic:
·

Goal state after:
G : Type u_2
inst✝¹ : Group G
inst✝ : Finite G
H : Subgroup G
⊢ 0 < ↑(Nat.card ↥H) ^ 2
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ Nat.card (ConjClasses (G ⧸ H)) ≤ Nat.card (ConjClasses G)

pp: case h
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ ↑(Nat.card G) ≠ 0

pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ 0 < ↑(Nat.card (G ⧸ H))

Tactic:
·

Goal state after:
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ Nat.card (ConjClasses (G ⧸ H)) ≤ Nat.card (ConjClasses G)
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case h
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ ↑(Nat.card G) ≠ 0

pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ 0 < ↑(Nat.card (G ⧸ H))

Tactic:
·

Goal state after:
case h
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ ↑(Nat.card G) ≠ 0
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ 0 < ↑(Nat.card (G ⧸ H))

Tactic:
·

Goal state after:
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ 0 < ↑(Nat.card (G ⧸ H))