mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Sphere.SecondInter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : Sphere P
n : ℕ
inst✝ : n.AtLeastTwo
sx : Affine.Simplex ℝ P n
i : Fin (n + 1)
hi : sx.points i ∈ s
hsx : ∀ (j : Fin (n + 1)), dist (sx.points j) s.center ≤ s.radius
w : Fin (n + 1) → ℝ
hw : ∑ i, w i = 1
hw01 : ∀ (i : Fin (n + 1)), w i ∈ Set.Ioo 0 1
r : ℝ := (1 - w i)⁻¹
hrpos : 0 < r
p' : P := (AffineMap.lineMap (sx.points i) ((Finset.affineCombination ℝ Finset.univ sx.points) w)) r
hp' : p' -ᵥ sx.points i = r • ((Finset.affineCombination ℝ Finset.univ sx.points) w -ᵥ sx.points i)
j : Fin (n + 1)
hj : ¬j = i
⊢ 0 < r * (w j - Pi.single i 1 j) + Pi.single i 1 j

Tactic:
simp [hj, hrpos, (hw01 j).1]

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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
⊢ ¬I.IsBoundaryPoint x → I.IsInteriorPoint x

Tactic:
by simpa only [or_iff_not_imp_right] using isInteriorPoint_or_isBoundaryPoint x (I := I)

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
n : WithTop ℕ∞
hn : n ≠ 0
f : M → N
x : M
hf : IsLocalDiffeomorphAt I I' n f x
⊢ I.IsBoundaryPoint x ↔ I'.IsBoundaryPoint (f x)

Tactic:
by
  simp [isBoundaryPoint_iff_not_isInteriorPoint, hf.isInteriorPoint_iff hn]

Goal state after:
Module: Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary

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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
N : Type u_7
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace H' N
J : ModelWithCorners 𝕜 E' H'
⊢ (ModelWithCorners.interior (M × N))ᶜ = (ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N)ᶜ

Tactic:
by rw [interior_prod]

Goal state after:
Module: Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation

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
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : ChartedSpace H G
inst✝¹ : Monoid G
inst✝ : ContMDiffMul I ∞ G
g : G
X : LeftInvariantDerivation I G
f : C^∞⟮I, G; 𝓘(𝕜, 𝕜), 𝕜⟯
⊢ (X f).comp (𝑳 I g) = X (f.comp (𝑳 I g))

Tactic:
ext h
  rw [ContMDiffMap.comp_apply, L_apply, ← evalAt_apply, evalAt_mul, hfdifferential_apply,
    fdifferential_apply, evalAt_apply]

Goal state after:
Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
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
E' : Type u_5
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁷ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁶ : TopologicalSpace M'
inst✝⁵ : ChartedSpace H' M'
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J 1 N
Is : IsManifold I 1 M
I's : IsManifold I' 1 M'
x₀ : N
f : N → M → M'
g : N → M
t : Set N
u : Set M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g t x₀
hx₀ : x₀ ∈ t
hu : MapsTo g t u
hmn : m + 1 ≤ n
h'u : UniqueMDiff[u]
t' : Set N := t ∩ g ⁻¹' (extChartAt I (g x₀)).source
ht't : t' ⊆ t
hx₀gx₀ : (x₀, g x₀) ∈ t ×ˢ u
h4f✝ : ContinuousWithinAt (fun x ↦ f x (g x)) t x₀
h4f : (fun x ↦ f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source ∈ 𝓝[t] x₀
h3f : ∀ᶠ (x' : N × M) in 𝓝[t ×ˢ u] (x₀, g x₀), ContMDiffWithinAt (J.prod I) I' 1 (uncurry f) (t ×ˢ u) x'
this : MapsTo (fun x ↦ (x, g x)) t (t ×ˢ u)
x : N
hx : ContMDiffWithinAt (J.prod I) I' 1 (uncurry f) (t ×ˢ u) (id x, g x)
h'x : x ∈ t
y : M
hy : y ∈ u
⊢ (id x, y) ∈ t ×ˢ u

Tactic:
simp [h'x, hy]

Goal state after:
Module: Mathlib.Geometry.Manifold.MFDeriv.NormedSpace

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
V : Type u_18
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace 𝕜 V
f : M → 𝕜
g : M → V
f' : TangentSpace I x →L[𝕜] 𝕜
hs : HasMFDerivAt% f x (↑(fromTangentSpace (f x)).symm ∘SL f')
g' : TangentSpace I x →L[𝕜] V
hg : HasMFDerivAt% g x (↑(fromTangentSpace (g x)).symm ∘SL g')
⊢ HasMFDerivAt% (f • g) x
    (f x • ↑(fromTangentSpace ((f • g) x)).symm ∘SL g' +
      toSpanSingleton 𝕜 ((fromTangentSpace ((f • g) x)).symm (g x)) ∘SL f')

Tactic:
constructor
  · exact hs.1.smul hg.1
  · simpa using! hs.2.smul hg.2

Goal state after:
Module: Mathlib.Geometry.Manifold.Instances.Real

Goal state before:
pp: x y : ℝ
hxy : Fact (x < y)
z : ↑(Icc x y)
h : y ≤ ↑z
⊢ chartAt (EuclideanHalfSpace 1) z = IccRightChart x y

Tactic:
by
  simp [Icc_chartedSpaceChartAt, reduceIte, not_lt.mpr h]

Goal state after:
Module: Mathlib.Geometry.Manifold.Immersion

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁷ : NontriviallyNormedField 𝕜
E : Type u_2
E''' : Type u_4
E'' : Type u
F : Type u_5
inst✝¹⁶ : NormedAddCommGroup E
inst✝¹⁵ : NormedSpace 𝕜 E
inst✝¹⁴ : NormedAddCommGroup E''
inst✝¹³ : NormedSpace 𝕜 E''
inst✝¹² : NormedAddCommGroup E'''
inst✝¹¹ : NormedSpace 𝕜 E'''
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
H : Type u_7
inst✝⁸ : TopologicalSpace H
G : Type u_9
inst✝⁷ : TopologicalSpace G
G' : Type u_10
inst✝⁶ : TopologicalSpace G'
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
J' : ModelWithCorners 𝕜 E''' G'
M : Type u_11
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
N : Type u_13
inst✝³ : TopologicalSpace N
inst✝² : ChartedSpace G N
N' : Type u_14
inst✝¹ : TopologicalSpace N'
inst✝ : ChartedSpace G' N'
n : ℕ∞ω
x : M
f : M → N
φ : N → N'
h : IsImmersionAtOfComplement F J J' n φ (f x)
h' : ContMDiffAt I J' n (φ ∘ f) x
t : Set M
ht : t ⊆ f ⁻¹' h.domChart.source
hxt : x ∈ t
f' : E → E'' := ↑(h.domChart.extend J) ∘ f ∘ ↑(extChartAt I x).symm
φ' : E'' → E''' := ↑(h.codChart.extend J') ∘ φ ∘ ↑(h.domChart.extend J).symm
x' : E := ↑(extChartAt I x) x
s : Set E := ↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I
hx' : ↑(extChartAt I x) x ∈ s
h'loc :
  ContDiffWithinAt 𝕜 n (↑(h.codChart.extend J') ∘ (φ ∘ f) ∘ ↑(extChartAt I x).symm)
    (↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I) (↑(extChartAt I x) x)
y : E
hy : y ∈ ↑(extChartAt I x).symm ⁻¹' t ∩ range ↑I
⊢ f (↑(chartAt H x).symm (↑I.symm y)) ∈ h.domChart.source

Tactic:
apply ht hy.1

Goal state after:
Module: Mathlib.Geometry.Manifold.IntegralCurve.Transform

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ a : ℝ
ha : a ≠ 0
ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
t : ℝ
⊢ |t * a - t₀ / a * a| < ε ↔ |t * a - t₀| < ε

Tactic:
div_mul_cancel₀ _ ha

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
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ a : ℝ
ha : a ≠ 0
ε : ℝ
hε : ε > 0
h : IsMIntegralCurveOn γ v (Metric.ball t₀ ε)
t : ℝ
⊢ |t * a - t₀| < ε ↔ |t * a - t₀| < ε
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 : M
a b : ℝ
γ : ℝ → M
hγ : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc a b)
ha : γ a = x
hb : γ b = y
hab : a ≤ b
η : ℝ →ᴬ[ℝ] ℝ := ContinuousAffineMap.lineMap a b
hη : ContMDiffOn 𝓘(ℝ, ℝ) I 1 (γ ∘ ⇑η) (Icc 0 1)
f : ↑unitInterval → M := fun t ↦ (γ ∘ ⇑η) ↑t
hf : ContMDiff (𝓡∂ 1) I 1 f
g : Path x y := { toFun := f, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
A : riemannianEDist I x y ≤ ∫⁻ (x_1 : ↑unitInterval), ‖(mfderiv% ⇑g x_1) 1‖ₑ
E : pathELength I (⇑g ∘ projIcc 0 1 ⋯) 0 1 = pathELength I (γ ∘ ⇑η) 0 1
⊢ MonotoneOn (⇑η) (Icc 0 1)

Tactic:
· apply (AffineMap.lineMap_mono hab).monotoneOn

Goal state after:
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
η : ℝ → ℝ := 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

Tactic:
dsimp only

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
⊢ (b' - a')⁻¹ * (t - a') ≤ (b' - a')⁻¹ * (u - a')
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
x : M
f : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)
⊢ ¬IsUnit f ↔ f ∈ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x))

Tactic:
not_iff_comm,

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
x : M
f : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)
⊢ f ∉ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)) ↔ IsUnit f
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

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

Tactic:
exact orderOf_r_one.symm

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

Goal state before:
pp: n : ℕ
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
h' : IsMulCommutative (DihedralGroup (n + 3))
this : sr (-1) = sr 1
⊢ False

Tactic:
sr.injEq,

Goal state after:
n : ℕ
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
h' : IsMulCommutative (DihedralGroup (n + 3))
this : -1 = 1
⊢ False
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h✝ : Commute (sr i, sr j).1 (sr i, sr j).2
h : i = j
⊢ (↑((fun x ↦
              match x with
              | Sum.inl i => ⟨(sr i, r 0), ⋯⟩
              | Sum.inr (Sum.inl j) => ⟨(r 0, sr j), ⋯⟩
              | Sum.inr (Sum.inr (Sum.inl k)) => ⟨(sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)), ⋯⟩
              | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(r i, r j), ⋯⟩)
            ((fun x ↦
                match x with
                | ⟨(sr i, r a), property⟩ => Sum.inl i
                | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j)
                | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j)))
                | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j))))
              ⟨(sr i, sr j), h✝⟩))).1 =
      (↑⟨(sr i, sr j), h✝⟩).1 ∧
    (↑((fun x ↦
              match x with
              | Sum.inl i => ⟨(sr i, r 0), ⋯⟩
              | Sum.inr (Sum.inl j) => ⟨(r 0, sr j), ⋯⟩
              | Sum.inr (Sum.inr (Sum.inl k)) => ⟨(sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)), ⋯⟩
              | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(r i, r j), ⋯⟩)
            ((fun x ↦
                match x with
                | ⟨(sr i, r a), property⟩ => Sum.inl i
                | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j)
                | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j)))
                | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j))))
              ⟨(sr i, sr j), h✝⟩))).2 =
      (↑⟨(sr i, sr j), h✝⟩).2

Tactic:
sr.injEq,

Goal state after:
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h✝ : Commute (sr i, sr j).1 (sr i, sr j).2
h : i = j
⊢ ↑u⁻¹ * (i + j) = i ∧
    (↑((fun x ↦
              match x with
              | Sum.inl i => ⟨(sr i, r 0), ⋯⟩
              | Sum.inr (Sum.inl j) => ⟨(r 0, sr j), ⋯⟩
              | Sum.inr (Sum.inr (Sum.inl k)) => ⟨(sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)), ⋯⟩
              | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(r i, r j), ⋯⟩)
            ((fun x ↦
                match x with
                | ⟨(sr i, r a), property⟩ => Sum.inl i
                | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j)
                | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j)))
                | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j))))
              ⟨(sr i, sr j), h✝⟩))).2 =
      (↑⟨(sr i, sr j), h✝⟩).2
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h✝ : Commute (sr i, sr j).1 (sr i, sr j).2
h : i = j
⊢ ↑u⁻¹ * (i + j) = i ∧
    (↑((fun x ↦
              match x with
              | Sum.inl i => ⟨(sr i, r 0), ⋯⟩
              | Sum.inr (Sum.inl j) => ⟨(r 0, sr j), ⋯⟩
              | Sum.inr (Sum.inr (Sum.inl k)) => ⟨(sr (↑u⁻¹ * k), sr (↑u⁻¹ * k)), ⋯⟩
              | Sum.inr (Sum.inr (Sum.inr (i, j))) => ⟨(r i, r j), ⋯⟩)
            ((fun x ↦
                match x with
                | ⟨(sr i, r a), property⟩ => Sum.inl i
                | ⟨(r a, sr j), property⟩ => Sum.inr (Sum.inl j)
                | ⟨(sr i, sr j), property⟩ => Sum.inr (Sum.inr (Sum.inl (i + j)))
                | ⟨(r i, r j), property⟩ => Sum.inr (Sum.inr (Sum.inr (i, j))))
              ⟨(sr i, sr j), h✝⟩))).2 =
      (↑⟨(sr i, sr j), h✝⟩).2

Tactic:
sr.injEq,

Goal state after:
n : ℕ
hn : Odd n
u : (ZMod n)ˣ := ZMod.unitOfCoprime 2 ⋯
hu : ∀ (a : ZMod n), a + a = 0 ↔ a = 0
i j : ZMod n
h✝ : Commute (sr i, sr j).1 (sr i, sr j).2
h : i = j
⊢ ↑u⁻¹ * (i + j) = i ∧ ↑u⁻¹ * (i + j) = j
Module: Mathlib.GroupTheory.PresentedGroup

Goal state before:
pp: α : Type u_1
rels : Set (FreeGroup α)
⊢ Subgroup.closure (Set.range of) = ⊤

Tactic:
have : (PresentedGroup.of : α → PresentedGroup rels) = QuotientGroup.mk' _ ∘ FreeGroup.of := rfl

Goal state after:
α : Type u_1
rels : Set (FreeGroup α)
this : of = ⇑(QuotientGroup.mk' (Subgroup.normalClosure rels)) ∘ FreeGroup.of
⊢ Subgroup.closure (Set.range of) = ⊤
Module: Mathlib.GroupTheory.PresentedGroup

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

pp: case mk.mul
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x : PresentedGroup rels
x✝ y✝ : FreeGroup α
a✝¹ : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) x✝ ∈ H
a✝ : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) y✝ ∈ H
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) (x✝ * y✝) ∈ H

Tactic:
· exact (Subgroup.inv_mem_iff H).mpr (by assumption)

Goal state after:
case mk.mul
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x : PresentedGroup rels
x✝ y✝ : FreeGroup α
a✝¹ : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) x✝ ∈ H
a✝ : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) y✝ ∈ H
⊢ Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) (x✝ * y✝) ∈ H
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
⊢ ((fun f ↦ (Units.coeHom G).comp (cs.groupLift ⋯)) ((fun ι ↦ ⟨⇑ι ∘ cs.simple, ⋯⟩) ι)) (cs.simple i) = ι (cs.simple i)

Tactic:
dsimp only

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 (cs.groupLift ⋯)) (cs.simple i) = ι (cs.simple i)
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
ω : List B
⊢ cs.wordProd ω.reverse = (cs.wordProd ω)⁻¹

Tactic:
induction ω with

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

Goal state before:
pp: case neg
B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : ¬Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
⊢ (if Even (2 * p + k) then i else j) = j

Tactic:
simp [(by apply Nat.odd_add.mpr; simp [h_even] : Odd (2 * p + k))]

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

Goal state before:
pp: case inl
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ 1 * (cs.simple i * cs.simple i') ^ (k * 2 / 2) = 1 * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - k * 2) / 2)

Tactic:
← sub_mul

Goal state after:
case inl
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ 1 * (cs.simple i * cs.simple i') ^ (k * 2 / 2) = 1 * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') - k) * 2 / 2)
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
i : B
⊢ cs.rightInvSeq (ω.concat i) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)

Tactic:
induction ω with

Goal state after:
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
⊢ cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse

Tactic:
induction ω with

Goal state after:
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
⊢ (cs.rightInvSeq ω).length = ω.length

Tactic:
induction ω with

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
m : CoprodI M
⊢ (fun w ↦ w.prod) ((fun m ↦ m • empty) m) = m

Tactic:
dsimp only

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
m : CoprodI M
⊢ (m • empty).prod = m
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case empty
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
⊢ (fun m ↦ m • empty) ((fun w ↦ w.prod) empty) = empty

Tactic:
dsimp only

Goal state after:
case empty
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
⊢ empty.prod • empty = empty
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case smul
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
⊢ ∀ (i : ι) (m : M i) (w : Word M),
    (fun m ↦ m • empty) ((fun w ↦ w.prod) w) = w → (fun m ↦ m • empty) ((fun w ↦ w.prod) (of m • w)) = of m • w

Tactic:
dsimp only

Goal state after:
case smul
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
⊢ ∀ (i : ι) (m : M i) (w : Word M), w.prod • empty = w → (of m • w).prod • empty = of m • w
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ ⟨i✝, (singleton x✝ a✝).last⟩ ∈ (singleton x✝ a✝).toList.getLast?

Tactic:
rw [Option.mem_def]

Goal state after:
case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ (singleton x✝ a✝).toList.getLast? = some ⟨i✝, (singleton x✝ a✝).last⟩
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
j : ℕ
ih₁ : ∀ (ω : List B), cs.rightInvSeq (drop j ω) = drop j (cs.rightInvSeq ω)
ω : List B
⊢ cs.rightInvSeq (drop (j + 1) ω) = drop (j + 1) (cs.rightInvSeq ω)

Tactic:
induction ω with

Goal state after:
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
t : W
ht : t ∈ cs.rightInvSeq ω
⊢ cs.IsReflection t

Tactic:
induction ω with

Goal state after:
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
j : ℕ
⊢ cs.wordProd ω * (cs.rightInvSeq ω).getD j 1 = cs.wordProd (ω.eraseIdx j)

Tactic:
by
  rw [getD_rightInvSeq, eraseIdx_eq_take_drop_succ]
  nth_rw 1 [← take_append_drop (j + 1) ω]
  rw [take_add_one]
  obtain lt | le := lt_or_ge j ω.length
  · simp only [getElem?_eq_getElem lt, wordProd_append, mul_assoc]
    simp
  · simp only [getElem?_eq_none le]
    simp

Goal state after: