mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: case hf
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := ⋯
A : ∀ t < a', η t = 0
A' : ∀ t < a', (γ ∘ η) t = x
B : ∀ (t : ℝ), b' < t → η t = 1
B' : ∀ (t : ℝ), b' < t → (γ ∘ η) t = y
⊢ Monotone fun t ↦ (b' - a')⁻¹ * (t - a')

Tactic:
intro t u htu

Goal state after:
case hf
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := fun t ↦ ((b' - a')⁻¹ * (t - a')).smoothTransition
A : ∀ t < a', η t = 0
A' : ∀ t < a', (γ ∘ η) t = x
B : ∀ (t : ℝ), b' < t → η t = 1
B' : ∀ (t : ℝ), b' < t → (γ ∘ η) t = y
t u : ℝ
htu : t ≤ u
⊢ (fun t ↦ (b' - a')⁻¹ * (t - a')) t ≤ (fun t ↦ (b' - a')⁻¹ * (t - a')) u
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x✝ y✝ x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := fun t ↦ -t
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
this : riemannianEDist I y x ≤ pathELength I ((γ ∘ η) ∘ η) 0 1
⊢ riemannianEDist I y x < r

Tactic:
apply this.trans_lt

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
H : Type u_2
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x✝ y✝ x y : M
r : ℝ≥0∞
hr : riemannianEDist I x y < r
γ : ℝ → M
γ0 : γ 0 = x
γ1 : γ 1 = y
γ_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 γ
hγ : pathELength I γ 0 1 < r
η : ℝ → ℝ := ⋯
h_smooth : ContMDiff 𝓘(ℝ, ℝ) I 1 (γ ∘ η)
this : riemannianEDist I y x ≤ pathELength I ((γ ∘ η) ∘ η) 0 1
⊢ pathELength I ((γ ∘ η) ∘ η) 0 1 < r
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
H' : Type u_6
inst✝¹⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace HM M
N G A A' R : Type u
inst✝¹⁶ : TopologicalSpace N
inst✝¹⁵ : ChartedSpace H N
inst✝¹⁴ : TopologicalSpace G
inst✝¹³ : ChartedSpace H G
inst✝¹² : TopologicalSpace A
inst✝¹¹ : ChartedSpace H A
inst✝¹⁰ : TopologicalSpace A'
inst✝⁹ : ChartedSpace H' A'
inst✝⁸ : TopologicalSpace R
inst✝⁷ : ChartedSpace H R
EP : Type u_7
inst✝⁶ : NormedAddCommGroup EP
inst✝⁵ : NormedSpace 𝕜 EP
HP : Type u_8
inst✝⁴ : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝³ : TopologicalSpace P
inst✝² : ChartedSpace HP P
inst✝¹ : Ring R
inst✝ : ContMDiffRing I ∞ R
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(TopCat.of M)) (smoothPresheafRing IM I M R)

Tactic:
CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget _ _ (CategoryTheory.forget RingCat)

Goal state after:
𝕜 : 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
H' : Type u_6
inst✝¹⁹ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E H'
M : Type u
inst✝¹⁸ : TopologicalSpace M
inst✝¹⁷ : ChartedSpace HM M
N G A A' R : Type u
inst✝¹⁶ : TopologicalSpace N
inst✝¹⁵ : ChartedSpace H N
inst✝¹⁴ : TopologicalSpace G
inst✝¹³ : ChartedSpace H G
inst✝¹² : TopologicalSpace A
inst✝¹¹ : ChartedSpace H A
inst✝¹⁰ : TopologicalSpace A'
inst✝⁹ : ChartedSpace H' A'
inst✝⁸ : TopologicalSpace R
inst✝⁷ : ChartedSpace H R
EP : Type u_7
inst✝⁶ : NormedAddCommGroup EP
inst✝⁵ : NormedSpace 𝕜 EP
HP : Type u_8
inst✝⁴ : TopologicalSpace HP
IP : ModelWithCorners 𝕜 EP HP
P : Type u
inst✝³ : TopologicalSpace P
inst✝² : ChartedSpace HP P
inst✝¹ : Ring R
inst✝ : ContMDiffRing I ∞ R
⊢ CategoryTheory.Presheaf.IsSheaf (Opens.grothendieckTopology ↑(TopCat.of M))
    (CategoryTheory.Functor.comp (smoothPresheafRing IM I M R) (CategoryTheory.forget RingCat))
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖Trivialization.symmL ℝ (trivializationAt E (fun x ↦ TangentSpace I x) x) y‖ < C
hx : (chartAt H x).source ∈ 𝓝 x
y : M
hy : ‖mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y)‖ < C
h'y : y ∈ (chartAt H x).source
⊢ y ∈ (extChartAt I x).source

Tactic:
simpa using h'y

Goal state after:
Module: Mathlib.Geometry.Manifold.Riemannian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
H : Type u_2
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : RiemannianBundle fun x ↦ TangentSpace I x
inst✝¹ : IsManifold I 1 M
inst✝ : IsContinuousRiemannianBundle E fun x ↦ TangentSpace I x
x : M
C : ℝ
C_pos : C > 0
hC : ∀ᶠ (y : M) in 𝓝 x, ‖Trivialization.symmL ℝ (trivializationAt E (fun x ↦ TangentSpace I x) x) y‖ < C
hx : (chartAt H x).source ∈ 𝓝 x
y : M
hy : ‖mfderiv[range ↑I] ↑(extChartAt I x).symm (↑(extChartAt I x) y)‖ < C
h'y : y ∈ (chartAt H x).source
⊢ y ∈ (extChartAt I x).source

Tactic:
by simpa using h'y

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

Goal state before:
pp: case refine_1
𝕜 : 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
U : Opens M
V : Opens ↑↑(ChartedSpace.locallyRingedSpace IM ↥U).toPresheafedSpace
a b : ↑((ChartedSpace.locallyRingedSpace IM M).presheaf.obj (Opposite.op (⋯.functor.obj V)))
hab :
  (ConcreteCategory.hom
        ((LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.c.app
          (Opposite.op (⋯.functor.obj V))))
      a =
    (ConcreteCategory.hom
        ((LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.c.app
          (Opposite.op (⋯.functor.obj V))))
      b
⊢ ↑a = ↑b

Tactic:
ext ⟨x, y, hy, rfl⟩

Goal state after:
case refine_1
𝕜 : 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
U : Opens M
V : Opens ↑↑(ChartedSpace.locallyRingedSpace IM ↥U).toPresheafedSpace
a b : ↑((ChartedSpace.locallyRingedSpace IM M).presheaf.obj (Opposite.op (⋯.functor.obj V)))
hab :
  (ConcreteCategory.hom
        ((LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.c.app
          (Opposite.op (⋯.functor.obj V))))
      a =
    (ConcreteCategory.hom
        ((LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.c.app
          (Opposite.op (⋯.functor.obj V))))
      b
y : ↑↑(ChartedSpace.locallyRingedSpace IM ↥U).toPresheafedSpace
hy : y ∈ ↑V
⊢ ↑a
      ⟨(ConcreteCategory.hom
            (LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.base)
          y,
        ⋯⟩ =
    ↑b
      ⟨(ConcreteCategory.hom
            (LocallyRingedSpace.Hom.toShHom (ChartedSpace.locallyRingedSpaceMap Subtype.val ⋯)).hom.base)
          y,
        ⋯⟩
Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality

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
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
A : Type u_9
inst✝¹ : AddCommGroup A
inst✝ : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : M → 𝕜 := fun x' ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
this✝ : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
this : (MDiffAt fun _x ↦ 1) x
x' : M
hx' : σ x' = σ' x'
⊢ ψ x' = (fun _x ↦ 1) x'

Tactic:
by simp [ψ, hx']

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality

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
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
A : Type u_9
inst✝¹ : AddCommGroup A
inst✝ : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : M → 𝕜 := fun x' ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
this✝ : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
this : (MDiffAt fun _x ↦ 1) x
⊢ MDiffAt ψ x

Tactic:
exact this.congr_of_eventuallyEq (hσσ'.mono fun x' hx' ↦ by simp [ψ, 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₀ Y₀ : TangentSpace I x
⊢ ((hcov.torsion x) X₀) Y₀ = -((hcov.torsion x) Y₀) X₀

Tactic:
simp only [torsion_apply_eq_extend, neg_sub]

Goal state after:
𝕜 : 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₀ Y₀ : TangentSpace I x
⊢ (cov (extend E Y₀) x) X₀ - (cov (extend E X₀) x) Y₀ - VectorField.mlieBracket I (extend E X₀) (extend E Y₀) x =
    VectorField.mlieBracket I (extend E Y₀) (extend E X₀) x - ((cov (extend E X₀) x) Y₀ - (cov (extend E Y₀) x) X₀)
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ #{x * y, x, y, 1} = 4

Tactic:
card_insert_of_notMem

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ #{x, y, 1} + 1 = 4

G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ x * y ∉ {x, y, 1}
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ #{x, y, 1} + 1 = 4

pp: G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ x * y ∉ {x, y, 1}

Tactic:
card_insert_of_notMem

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ #{y, 1} + 1 + 1 = 4

G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ x ∉ {y, 1}

G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ x * y ∉ {x, y, 1}
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ #{y, 1} + 1 + 1 = 4

pp: G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ x ∉ {y, 1}

pp: G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ x * y ∉ {x, y, 1}

Tactic:
card_insert_of_notMem

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ #{1} + 1 + 1 + 1 = 4

G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ y ∉ {1}

G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ x ∉ {y, 1}

G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ x * y ∉ {x, y, 1}
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ #{1} + 1 + 1 + 1 = 4

pp: G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ y ∉ {1}

pp: G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ x ∉ {y, 1}

pp: G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ x * y ∉ {x, y, 1}

Tactic:
card_insert_of_notMem

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ #{1} + 1 + 1 + 1 = 4

G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ y ∉ {1}

G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ x ∉ {y, 1}

G : Type u_1
inst✝³ : Group G
inst✝² : IsKleinFour G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
x y : G
hx : x ≠ 1
hy : y ≠ 1
hxy : x ≠ y
⊢ x * y ∉ {x, y, 1}
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

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

Tactic:
exact congr_arg sr (add_zero a)

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

Goal state before:
pp: case inl
n : ℕ
hn : 0 < n
⊢ r 1 ^ n ≠ 1

Tactic:
r_one_pow,

Goal state after:
case inl
n : ℕ
hn : 0 < n
⊢ r ↑n ≠ 1
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:
· rw [h, zero_mul, div_zero, div_zero]

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: case pos
n : ℕ
h0 : ¬n = 0
h1 : n = 1
⊢ commProb (Product (reciprocalFactors 1)) = 1 / ↑1

Tactic:
reciprocalFactors_one,

Goal state after:
case pos
n : ℕ
h0 : ¬n = 0
h1 : n = 1
⊢ commProb (Product []) = 1 / ↑1
Module: Mathlib.GroupTheory.PresentedGroup

Goal state before:
pp: case mk.C1
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x : PresentedGroup rels
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) 1 ∈ H

Tactic:
exact one_mem H

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
⊢ Subgroup.map (↑(FreeGroup.freeGroupCongr e)) (Subgroup.normalClosure M.relationsSet) =
    Subgroup.normalClosure (CoxeterMatrix.reindex e M).relationsSet

Tactic:
rw [reindex_relationsSet,
        Subgroup.map_normalClosure _ _ (by simpa using (FreeGroup.freeGroupCongr e).surjective),
        MonoidHom.coe_coe]

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

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

Tactic:
simp [← mul_assoc]

Goal state after:
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
⊢ (fun f ↦ (Units.coeHom G).comp (cs.groupLift ⋯)) ((fun ι ↦ ⟨⇑ι ∘ cs.simple, ⋯⟩) ι) = ι

Tactic:
apply cs.ext_simple
    intro i
    dsimp only
    rw [groupLift, simple, MonoidHom.comp_apply, MonoidHom.comp_apply, toMonoidHom_apply_symm_apply,
      PresentedGroup.toGroup.of, CoxeterSystem.restrictUnit, Units.coeHom_apply]
    simp only [comp_apply, simple]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos.mp
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList = []
m₂ : M (w.toList.head hnil).fst
hw : ⟨(w.toList.head hnil).fst, m₂ * (w.toList.head ⋯).snd⟩ ∉ w.toList.tail
hm1 : ¬m₂ * (w.toList.head ⋯).snd = 1
⊢ (∃ m', w.toList.head hnil = ⟨(w.toList.head hnil).fst, m'⟩ ∧ m₂ * (w.toList.head ⋯).snd = m₂ * m') ∨
    ¬w.fstIdx = some (w.toList.head hnil).fst ∧ m₂ * (w.toList.head ⋯).snd = m₂

Tactic:
exact Or.inl ⟨_, rfl, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
hj : j < ω.length
⊢ (cs.wordProd (drop (j + 1) ω))⁻¹ *
      ((Option.map cs.simple (some ω[j])).getD 1 *
        (cs.wordProd (drop (j + 1) ω) *
          ((cs.wordProd (drop (j + 1) ω))⁻¹ *
            ((Option.map cs.simple (some ω[j])).getD 1 * cs.wordProd (drop (j + 1) ω))))) =
    1

Tactic:
simp [← mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
hj : j < ω.length
⊢ cs.wordProd (take j ω) *
      ((Option.map cs.simple (some ω[j])).getD 1 *
        ((cs.wordProd (take j ω))⁻¹ *
          (cs.wordProd (take j ω) * ((Option.map cs.simple (some ω[j])).getD 1 * (cs.wordProd (take j ω))⁻¹)))) =
    1

Tactic:
simp [← mul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
w : Word M
h : w ≠ empty
this : ∃ i j w', w'.toWord.toList = w.toList
⊢ ∃ i j w', w'.toWord = w

Tactic:
by
    rcases this with ⟨i, j, w, h⟩
    refine ⟨i, j, w, ?_⟩
    ext
    rw [h]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
w : Word H
Heq : (lift f) (Word.equiv.symm w) = 1
⊢ Word.equiv.symm w = 1

Tactic:
dsimp [Word.equiv] at *

Goal state after:
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
hcard : 3 ≤ #ι ∨ ∃ i, 3 ≤ #(H i)
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), ¬h = 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
w : Word H
Heq : (lift f) w.prod = 1
⊢ w.prod = 1
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
a : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
⊢ (↑⟨a.den, ⋯⟩ * a.num) • ↑sc • mb < (↑⟨a.den, ⋯⟩ * a.num) • ↑sb • mc

Tactic:
exact (nsmul_right_strictMono (by simpa using ha.ne.symm)).lt_iff_lt.mpr h

Goal state after: