mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.Sheaf.Smooth

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
U : (OpenNhds x)ᵒᵖ
⊢ colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M R).presheaf) U ≫ (forgetStalk IM I M R x).inv =
    ↾⇑(CommRingCat.Hom.hom (colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U))

Tactic:
dsimp
  rw [Iso.comp_inv_eq, ← smoothSheafCommRing.ι_forgetStalk_hom]
  rfl

Goal state after:
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: 𝕜 : Type u
inst✝¹⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝¹⁴ : NormedAddCommGroup EM
inst✝¹³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝¹² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace HM M
EN : Type u_3
inst✝⁹ : NormedAddCommGroup EN
inst✝⁸ : NormedSpace 𝕜 EN
HN : Type u_4
inst✝⁷ : TopologicalSpace HN
IN : ModelWithCorners 𝕜 EN HN
N : Type u
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace HN N
EP : Type u_5
inst✝⁴ : NormedAddCommGroup EP
inst✝³ : NormedSpace 𝕜 EP
HP : Type u_6
inst✝² : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace HP P
x : M
⊢ ∀ (a b : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)),
    a ∈ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)) →
      b ∈ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)) → a + b ∈ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x))

Tactic:
intro f g

Goal state after:
𝕜 : Type u
inst✝¹⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝¹⁴ : NormedAddCommGroup EM
inst✝¹³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝¹² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace HM M
EN : Type u_3
inst✝⁹ : NormedAddCommGroup EN
inst✝⁸ : NormedSpace 𝕜 EN
HN : Type u_4
inst✝⁷ : TopologicalSpace HN
IN : ModelWithCorners 𝕜 EN HN
N : Type u
inst✝⁶ : TopologicalSpace N
inst✝⁵ : ChartedSpace HN N
EP : Type u_5
inst✝⁴ : NormedAddCommGroup EP
inst✝³ : NormedSpace 𝕜 EP
HP : Type u_6
inst✝² : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝¹ : TopologicalSpace P
inst✝ : ChartedSpace HP P
x : M
f g : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)
⊢ f ∈ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)) →
    g ∈ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)) → f + g ∈ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x))
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
equiv : E ≃L[𝕜] E'' × F
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : domChart ∈ IsManifold.maximalAtlas I n M
hcodChart : codChart ∈ IsManifold.maximalAtlas J n N
hsource : domChart.source ⊆ f ⁻¹' codChart.source
hwrittenInExtend :
  EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (Prod.fst ∘ ⇑equiv) (domChart.extend I).target
⊢ IsSubmersionAtOfComplement F I J n f x

Tactic:
use domChart, codChart

Goal state after:
case property
𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
x : M
equiv : E ≃L[𝕜] E'' × F
domChart : OpenPartialHomeomorph M H
codChart : OpenPartialHomeomorph N G
hx : x ∈ domChart.source
hfx : f x ∈ codChart.source
hdomChart : domChart ∈ IsManifold.maximalAtlas I n M
hcodChart : codChart ∈ IsManifold.maximalAtlas J n N
hsource : domChart.source ⊆ f ⁻¹' codChart.source
hwrittenInExtend :
  EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (Prod.fst ∘ ⇑equiv) (domChart.extend I).target
⊢ SubmersionAtProp F I J M N f domChart codChart
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: case h
𝕜 : Type u_1
E' : Type u_2
E'' : Type u_3
E''' : Type u_4
F : Type u_5
F' : Type u_6
H : Type u_7
H' : Type u_8
G : Type u_9
G' : Type u_10
E : Type u
inst✝²⁸ : NontriviallyNormedField 𝕜
inst✝²⁷ : NormedAddCommGroup E
inst✝²⁶ : NormedSpace 𝕜 E
inst✝²⁵ : NormedAddCommGroup E'
inst✝²⁴ : NormedSpace 𝕜 E'
inst✝²³ : NormedAddCommGroup E''
inst✝²² : NormedSpace 𝕜 E''
inst✝²¹ : NormedAddCommGroup E'''
inst✝²⁰ : NormedSpace 𝕜 E'''
inst✝¹⁹ : NormedAddCommGroup F
inst✝¹⁸ : NormedSpace 𝕜 F
inst✝¹⁷ : NormedAddCommGroup F'
inst✝¹⁶ : NormedSpace 𝕜 F'
inst✝¹⁵ : TopologicalSpace H
inst✝¹⁴ : TopologicalSpace H'
inst✝¹³ : TopologicalSpace G
inst✝¹² : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
I' : ModelWithCorners 𝕜 E' H'
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
M' : Type u_12
N : Type u_13
N' : Type u_14
inst✝¹¹ : TopologicalSpace M
inst✝¹⁰ : ChartedSpace H M
inst✝⁹ : TopologicalSpace M'
inst✝⁸ : ChartedSpace H' M'
inst✝⁷ : TopologicalSpace N
inst✝⁶ : ChartedSpace G N
inst✝⁵ : TopologicalSpace N'
inst✝⁴ : ChartedSpace G' N'
n : ℕ∞ω
x : M
f✝ : M → N
g✝ : M' → N'
x' : M'
inst✝³ : IsManifold I n M
inst✝² : IsManifold I' n M'
inst✝¹ : IsManifold J n N
inst✝ : IsManifold J' n N'
hf : IsSubmersionAtOfComplement F I J n f✝ x
hg : IsSubmersionAtOfComplement F' I' J' n g✝ x'
f : M → N
φ₁ : OpenPartialHomeomorph M H
ψ₁ : OpenPartialHomeomorph N G
g : M' → N'
φ₂ : OpenPartialHomeomorph M' H'
ψ₂ : OpenPartialHomeomorph N' G'
equiv₁ : E ≃L[𝕜] E'' × F
hfprop : EqOn (↑(ψ₁.extend J) ∘ f ∘ ↑(φ₁.extend I).symm) (Prod.fst ∘ ⇑equiv₁) (φ₁.extend I).target
equiv₂ : E' ≃L[𝕜] E''' × F'
hgprop : EqOn (↑(ψ₂.extend J') ∘ g ∘ ↑(φ₂.extend I').symm) (Prod.fst ∘ ⇑equiv₂) (φ₂.extend I').target
⊢ EqOn (Prod.fst ∘ ↑((ψ₁.extend J).prod (ψ₂.extend J')) ∘ Prod.map f g ∘ ↑((φ₁.extend I).prod (φ₂.extend I')).symm)
      (Prod.fst ∘
        Prod.fst ∘ ⇑((equiv₁.prodCongr equiv₂).trans (ContinuousLinearEquiv.prodProdProdComm 𝕜 E'' F E''' F')))
      ((φ₁.extend I).target ×ˢ (φ₂.extend I').target) ∧
    EqOn (Prod.snd ∘ ↑((ψ₁.extend J).prod (ψ₂.extend J')) ∘ Prod.map f g ∘ ↑((φ₁.extend I).prod (φ₂.extend I')).symm)
      (Prod.snd ∘
        Prod.fst ∘ ⇑((equiv₁.prodCongr equiv₂).trans (ContinuousLinearEquiv.prodProdProdComm 𝕜 E'' F E''' F')))
      ((φ₁.extend I).target ×ˢ (φ₂.extend I').target)

Tactic:
exact ⟨fun x ⟨hx, hx'⟩ ↦ by simpa using hfprop hx, fun x ⟨hx, hx'⟩ ↦ by simpa using hgprop hx'⟩

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
x : M
inst✝³ : IsManifold I 2 M
inst✝² : CompleteSpace E
cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 E
hcov : IsCovariantDerivativeOn E cov
X₀ : TangentSpace I x
⊢ ((hcov.torsion x) X₀) X₀ = 0

Tactic:
by
  simp [torsion_apply_eq_extend]

Goal state after:
Module: Mathlib.GroupTheory.Commensurable

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a✝ b✝ : ConjAct G
ha : a✝ ∈ {g | (g • H).Commensurable H}
hb : b✝ ∈ {g | (g • H).Commensurable H}
⊢ a✝ * b✝ ∈ {g | (g • H).Commensurable H}

Tactic:
Set.mem_ofPred_eq,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a✝ b✝ : ConjAct G
ha : a✝ ∈ {g | (g • H).Commensurable H}
hb : b✝ ∈ {g | (g • H).Commensurable H}
⊢ ((a✝ * b✝) • H).Commensurable H
Module: Mathlib.GroupTheory.Commensurable

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ 1 ∈ {g | (g • H).Commensurable H}

Tactic:
Set.mem_ofPred_eq,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ (1 • H).Commensurable H
Module: Mathlib.GroupTheory.Commensurable

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝¹ : ConjAct G
x✝ : x✝¹ ∈ {g | (g • H).Commensurable H}
⊢ x✝¹⁻¹ ∈ {g | (g • H).Commensurable H}

Tactic:
Set.mem_ofPred_eq,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
x✝¹ : ConjAct G
x✝ : x✝¹ ∈ {g | (g • H).Commensurable H}
⊢ (x✝¹⁻¹ • H).Commensurable H
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsKleinFour G
⊢ Nat.card (Additive G) = Nat.card G

Tactic:
congr!

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

Goal state before:
pp: G : Type u_1
inst✝¹ : AddGroup G
inst✝ : IsAddKleinFour G
⊢ Nat.card (Multiplicative G) = Nat.card G

Tactic:
congr!

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

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

Tactic:
Nat.card_eq_fintype_card,

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(Nat.card ↑{x | Commute x.1 x.2}) / ↑(Nat.card M) ^ 2 = 1 ↔ IsMulCommutative M

Tactic:
Nat.card_eq_fintype_card,

Goal state after:
M : Type u_1
inst✝¹ : Mul M
inst✝ : Finite M
h : Nonempty M
this : Fintype M
⊢ ↑(card ↑{x | Commute x.1 x.2}) / ↑(Nat.card M) ^ 2 = 1 ↔ IsMulCommutative M
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M ∗ N
⊢ (toProd x).2 = snd x

Tactic:
rw [← snd_comp_toProd]; rfl

Goal state after:
Module: Mathlib.GroupTheory.Coprod.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
⊢ inl.range ⊔ inr.range = Subgroup.closure ↑inl.range ⊔ Subgroup.closure ↑inr.range

Tactic:
Subgroup.closure_eq,

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
⊢ inl.range ⊔ inr.range = inl.range ⊔ Subgroup.closure ↑inr.range
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
ι : W →* G
i : B
⊢ ((Units.coeHom G).comp
        ((PresentedGroup.toGroup (@CoxeterSystem.relations_liftable B M Gˣ Units.instGroup (restrictUnit ⋯) ⋯)).comp
          cs.mulEquiv.toMonoidHom))
      (cs.simple i) =
    ι (cs.simple i)

Tactic:
simple,

Goal state after:
B : Type u_1
B' : Type u_2
e : B ≃ B'
W : Type u_3
H : Type u_4
inst✝² : Group W
inst✝¹ : Group H
M : CoxeterMatrix B
cs : CoxeterSystem M W
G : Type u_5
inst✝ : Monoid G
ι : W →* G
i : B
⊢ ((Units.coeHom G).comp
        ((PresentedGroup.toGroup (@CoxeterSystem.relations_liftable B M Gˣ Units.instGroup (restrictUnit ⋯) ⋯)).comp
          cs.mulEquiv.toMonoidHom))
      (cs.mulEquiv.symm (PresentedGroup.of i)) =
    ι (cs.mulEquiv.symm (PresentedGroup.of i))
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
w : Word M
h : w.fstIdx ≠ some i
m' : M i
w' : Word M
hm : ¬m = 1
h' : (cons m w ⋯ ⋯).fstIdx ≠ some i
hm' : m' = 1
he : cons m w ⋯ ⋯ = w'
⊢ False

Tactic:
exact h' rfl

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m₁ : M i
m₂ : M j
w : Word M
⊢ (⟨i, m₁⟩ ∈ w.toList.tail ∨
      (i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m₁⟩) ∨
        m₁ ≠ 1 ∧
          ∃ (h : j = i),
            m₁ =
              h ▸
                (have __src := (equivPair j) w;
                  {
                    head :=
                      m₂ *
                        if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = j then ⋯ ▸ (w.toList.head ⋯).snd else 1,
                    tail := __src.tail, fstIdx_ne := ⋯ }).head) ↔
    ¬i = j ∧ ⟨i, m₁⟩ ∈ w.toList ∨
      m₁ ≠ 1 ∧
        ∃ (hij : i = j),
          ⟨i, m₁⟩ ∈ w.toList.tail ∨
            (∃ m', ⟨j, m'⟩ ∈ w.toList.head? ∧ m₁ = ⋯ ▸ (m₂ * m')) ∨ w.fstIdx ≠ some j ∧ m₁ = ⋯ ▸ m₂

Tactic:
by_cases hij : i = j

Goal state after:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m₁ : M i
m₂ : M j
w : Word M
hij : i = j
⊢ (⟨i, m₁⟩ ∈ w.toList.tail ∨
      (i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m₁⟩) ∨
        m₁ ≠ 1 ∧
          ∃ (h : j = i),
            m₁ =
              h ▸
                (have __src := (equivPair j) w;
                  {
                    head :=
                      m₂ *
                        if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = j then ⋯ ▸ (w.toList.head ⋯).snd else 1,
                    tail := __src.tail, fstIdx_ne := ⋯ }).head) ↔
    ¬i = j ∧ ⟨i, m₁⟩ ∈ w.toList ∨
      m₁ ≠ 1 ∧
        ∃ (hij : i = j),
          ⟨i, m₁⟩ ∈ w.toList.tail ∨
            (∃ m', ⟨j, m'⟩ ∈ w.toList.head? ∧ m₁ = ⋯ ▸ (m₂ * m')) ∨ w.fstIdx ≠ some j ∧ m₁ = ⋯ ▸ m₂

case neg
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m₁ : M i
m₂ : M j
w : Word M
hij : ¬i = j
⊢ (⟨i, m₁⟩ ∈ w.toList.tail ∨
      (i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m₁⟩) ∨
        m₁ ≠ 1 ∧
          ∃ (h : j = i),
            m₁ =
              h ▸
                (have __src := (equivPair j) w;
                  {
                    head :=
                      m₂ *
                        if h : ∃ (h : w.toList ≠ []), (w.toList.head h).fst = j then ⋯ ▸ (w.toList.head ⋯).snd else 1,
                    tail := __src.tail, fstIdx_ne := ⋯ }).head) ↔
    ¬i = j ∧ ⟨i, m₁⟩ ∈ w.toList ∨
      m₁ ≠ 1 ∧
        ∃ (hij : i = j),
          ⟨i, m₁⟩ ∈ w.toList.tail ∨
            (∃ m', ⟨j, m'⟩ ∈ w.toList.head? ∧ m₁ = ⋯ ▸ (m₂ * m')) ∨ w.fstIdx ≠ some j ∧ m₁ = ⋯ ▸ m₂
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω' : List B
h : cs.IsReduced (i :: ω')
hw : cs.wordProd (i :: ω') ≠ 1
h₁ : i :: ω' ≠ []
⊢ cs.length (cs.simple i * (cs.simple i * cs.wordProd ω')) < (i :: ω').length

Tactic:
simple_mul_simple_cancel_left

Goal state after:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω' : List B
h : cs.IsReduced (i :: ω')
hw : cs.wordProd (i :: ω') ≠ 1
h₁ : i :: ω' ≠ []
⊢ cs.length (cs.wordProd ω') < (i :: ω').length
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) + 1 = cs.length w ↔
    cs.length (cs.simple i * (cs.simple i * w)) = cs.length (cs.simple i * w) + 1

Tactic:
simple_mul_simple_cancel_left

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (cs.simple i * w) + 1 = cs.length w ↔ cs.length w = cs.length (cs.simple i * w) + 1
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
h₄ : t * t' = 1
h₅ : cs.wordProd ω = cs.wordProd ((ω.eraseIdx j).eraseIdx (j' - 1))
⊢ False

Tactic:
have h₆ := calc
    ω.length = ℓ (π ω) := rω.symm
    _ = ℓ (π ((ω.eraseIdx j).eraseIdx (j' - 1))) := congrArg cs.length h₅
    _ ≤ ((ω.eraseIdx j).eraseIdx (j' - 1)).length := cs.length_wordProd_le _

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
h₄ : t * t' = 1
h₅ : cs.wordProd ω = cs.wordProd ((ω.eraseIdx j).eraseIdx (j' - 1))
h₆ : ω.length ≤ ((ω.eraseIdx j).eraseIdx (j' - 1)).length
⊢ False
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
h : mk ma sa ≤ mk mb sb
h' : mk mb sb ≤ mk ma sa
⊢ mk ma sa = mk mb sb

Tactic:
rw [mk_le_mk] at h h'

Goal state after:
case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
h : ↑sb • ma ≤ ↑sa • mb
h' : ↑sa • mb ≤ ↑sb • ma
⊢ mk ma sa = mk mb sb
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
N : Subgroup H
f : G →* H
hf : Surjective ⇑f
T : Set G
hT_fin : T.Finite
hT : normalClosure T = f.ker
S : Set G
hS_fin : S.Finite
hS : normalClosure (⇑f '' S) = N
⊢ (comap f N).IsFinitelyNormallyGenerated

Tactic:
refine ⟨S ∪ T, hS_fin.union hT_fin, ?_⟩

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
N : Subgroup H
f : G →* H
hf : Surjective ⇑f
T : Set G
hT_fin : T.Finite
hT : normalClosure T = f.ker
S : Set G
hS_fin : S.Finite
hS : normalClosure (⇑f '' S) = N
⊢ normalClosure (S ∪ T) = comap f N
Module: Mathlib.GroupTheory.FixedPointFree

Goal state before:
pp: F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
n : ℕ
hn : (⇑φ)^[n] = _root_.id
g : G
⊢ g / _root_.id g = 1

Tactic:
Function.id_def,

Goal state after:
F : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : FunLike F G G
inst✝¹ : MonoidHomClass F G G
φ : F
inst✝ : Finite G
hφ : FixedPointFree ⇑φ
n : ℕ
hn : (⇑φ)^[n] = _root_.id
g : G
⊢ g / (fun x ↦ x) g = 1
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg.inr.refine_1
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime (Nat.card G).minFac

Tactic:
apply Nat.Coprime.coprime_dvd_left (relIndex_dvd_of_le_left _ P.le_centralizer)
    apply Nat.Coprime.coprime_dvd_left (relIndex_dvd_index_of_le P.le_normalizer)
    rw [Nat.coprime_comm, Nat.Prime.coprime_iff_not_dvd Fact.out]
    exact P.not_dvd_index

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ _root_.commutator G ⊓ ↑P = (↑P).focalSubgroup

Tactic:
apply le_antisymm

Goal state after:
case a
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ _root_.commutator G ⊓ ↑P ≤ (↑P).focalSubgroup

case a
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ (↑P).focalSubgroup ≤ _root_.commutator G ⊓ ↑P
Module: Mathlib.GroupTheory.FreeGroup.CyclicallyReduced

Goal state before:
pp: α : Type u
L : List (α × Bool)
a b : α × Bool
⊢ (IsReduced (b :: L ++ [a]) ∧
      ∀ a_1 ∈ (b :: L ++ [a]).getLast?, ∀ b_1 ∈ (b :: L ++ [a]).head?, a_1.1 = b_1.1 → a_1.2 = b_1.2) ↔
    IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)

Tactic:
List.getLast?_concat

Goal state after:
α : Type u
L : List (α × Bool)
a b : α × Bool
⊢ (IsReduced (b :: L ++ [a]) ∧ ∀ a_1 ∈ some a, ∀ b_1 ∈ (b :: L ++ [a]).head?, a_1.1 = b_1.1 → a_1.2 = b_1.2) ↔
    IsReduced (b :: L ++ [a]) ∧ (a.1 = b.1 → a.2 = b.2)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x ∈ H (n - m)
g : G
hm : n ≤ m
⊢ ⁅x, g⁆ ∈ (fun m ↦ H (n - m)) (m + 1)

Tactic:
tsub_eq_zero_of_le hm,

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊤
h0 : H 0 = ⊥
hH : ∀ (x : G) (n : ℕ), x ∈ H (n + 1) → ∀ (g : G), ⁅x, g⁆ ∈ H n
x : G
m : ℕ
hx : x ∈ H 0
g : G
hm : n ≤ m
⊢ ⁅x, g⁆ ∈ (fun m ↦ H (n - m)) (m + 1)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
hm : n ≤ m
⊢ ⁅x, g⁆ ∈ H (n - m)

Tactic:
have hnm : n - m = 0 := tsub_eq_zero_iff_le.mpr hm

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
n : ℕ
hn : H n = ⊥
h0 : H 0 = ⊤
hH : ∀ (x : G) (n : ℕ), x ∈ H n → ∀ (g : G), ⁅x, g⁆ ∈ H (n + 1)
x : G
m : ℕ
hx : x ∈ H (n - (m + 1))
g : G
hm : n ≤ m
hnm : n - m = 0
⊢ ⁅x, g⁆ ∈ H (n - m)
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : e ∈ wideSubquiverSymmetrify T a b
⊢ (treeHom T
          (have this := a;
          this) ≫
        of e) ≫
      inv (treeHom T b) =
    𝟙 (root' T)

Tactic:
IsIso.comp_inv_eq,

Goal state after:
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : e ∈ wideSubquiverSymmetrify T a b
⊢ treeHom T
        (have this := a;
        this) ≫
      of e =
    𝟙 (root' T) ≫ treeHom T b
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
this : IsNilpotent G'
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ upperCentralSeries G' n = ⊤

Tactic:
eq_top_iff

Goal state after:
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
this : IsNilpotent G'
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ ⊤ ≤ upperCentralSeries G' n