mathlib-initiative/mathlib-tactics huggingface dataset:
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)
a b : ℝ
γ : ℝ → M
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
f : ℝ → ℝ
h : a ≤ b
hf : AntitoneOn f (Icc a b)
h'f : DifferentiableOn ℝ f (Icc a b)
hγ : MDiff[Icc (f b) (f a)] γ
⊢ pathELength I (γ ∘ f) a b = pathELength I γ (f b) (f a)

Tactic:
rcases h.eq_or_lt with rfl | h
  · simp
  have f_im : f '' (Icc a b) = Icc (f b) (f a) := h'f.continuousOn.image_Icc_of_antitoneOn h.le hf
  simp only [pathELength_eq_lintegral_mfderivWithin_Icc, ← f_im]
  have B (t) (ht : t ∈ Icc a b) : HasDerivWithinAt f (derivWithin f (Icc a b) t) (Icc a b) t :=
    (h'f t ht).hasDerivWithinAt
  rw [lintegral_image_eq_lintegral_deriv_mul_of_antitoneOn measurableSet_Icc B hf]
  apply setLIntegral_congr_fun measurableSet_Icc (fun t ht ↦ ?_)
  have : (mfderiv[Icc a b] (γ ∘ f) t)
      = (mfderiv[Icc (f b) (f a)] γ (f t)) ∘L mfderiv[Icc a b] f t := by
    rw [← f_im] at hγ ⊢
    apply mfderivWithin_comp
    · apply hγ _ (mem_image_of_mem _ ht)
    · rw [mdifferentiableWithinAt_iff_differentiableWithinAt]
      exact h'f _ ht
    · exact subset_preimage_image _ _
    · rw [uniqueMDiffWithinAt_iff_uniqueDiffWithinAt]
      exact uniqueDiffOn_Icc h _ ht
  rw [this]
  simp only [Function.comp_apply, ContinuousLinearMap.comp_apply]
  have : mfderiv[Icc a b] f t 1
      = derivWithin f (Icc a b) t • (1 : TangentSpace% (f t)) := by
    simp only [mfderivWithin_eq_fderivWithin, ← fderivWithin_derivWithin, smul_eq_mul, mul_one]
    rfl
  rw [this]
  have : 0 ≤ -derivWithin f (Icc a b) t := by simp [hf.derivWithin_nonpos]
  simp only [map_smul, enorm_smul, f_im, ← Real.enorm_of_nonneg this, enorm_neg]

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

Goal state before:
pp: F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
v : TangentSpace 𝓘(ℝ, F) x
⊢ √⟪v, v⟫ = ‖v‖

Tactic:
norm_eq_sqrt_real_inner

Goal state after:
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x : F
v : TangentSpace 𝓘(ℝ, F) x
⊢ √⟪v, v⟫ = √⟪v, v⟫
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 z : M
⊢ riemannianEDist I x z ≤ riemannianEDist I x y + riemannianEDist I y z

Tactic:
by
  apply le_of_forall_gt (fun r hr ↦ ?_)
  rcases ENNReal.exists_add_lt_of_add_lt hr with ⟨u, hu, v, hv, huv⟩
  rcases exists_lt_locally_constant_of_riemannianEDist_lt hu zero_lt_one with
    ⟨γ₁, hγ₁0, hγ₁1, hγ₁_smooth, hγ₁, -, hγ₁_const⟩
  rcases exists_lt_locally_constant_of_riemannianEDist_lt hv one_lt_two with
    ⟨γ₂, hγ₂1, hγ₂2, hγ₂_smooth, hγ₂, hγ₂_const, -⟩
  let γ := piecewise (Iic 1) γ₁ γ₂
  have : riemannianEDist I x z ≤ pathELength I γ 0 2 := by
    apply riemannianEDist_le_pathELength
    · apply ContMDiff.contMDiffOn
      exact ContMDiff.piecewise_Iic hγ₁_smooth hγ₂_smooth (hγ₁_const.trans hγ₂_const.symm)
    · simp [γ, hγ₁0]
    · simp [γ, hγ₂2]
    · exact zero_le_two
  apply this.trans_lt (lt_trans ?_ huv)
  rw [← pathELength_add zero_le_one one_le_two]
  gcongr
  · convert! hγ₁ using 1
    apply pathELength_congr
    intro t ht
    simp [γ, ht.2]
  · convert! hγ₂ using 1
    apply pathELength_congr_Ioo
    intro t ht
    simp [γ, ht.1]

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
inst✝³ : VectorBundle 𝕜 F V
inst✝² : CompleteSpace 𝕜
inst✝¹ : FiniteDimensional 𝕜 F
inst✝ : ContMDiffVectorBundle 1 F V I
hΦ : TensorialAt I F Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : σ x = σ' x
t : Trivialization F TotalSpace.proj := trivializationAt F V x
x_mem : x ∈ t.baseSet
b : Basis (↑(Basis.ofVectorSpaceIndex 𝕜 F)) 𝕜 F := Basis.ofVectorSpace 𝕜 F
s : ↑(Basis.ofVectorSpaceIndex 𝕜 F) → (x : M) → V x := t.localFrame b
c : ↑(Basis.ofVectorSpaceIndex 𝕜 F) → (x : M) → V x →ₗ[𝕜] 𝕜 := Trivialization.localFrameCoeff I t b
hs : ∀ (i : ↑(Basis.ofVectorSpaceIndex 𝕜 F)), MDiffAt (T% s) x
hc :
  ∀ {σ : (x : M) → V x},
    MDiffAt (T% σ) x → ∀ (i : ↑(Basis.ofVectorSpaceIndex 𝕜 F)), MDiffAt ((LinearMap.piApply (c i)) σ) x
hΦ_eq : ∀ {σ : (x : M) → V x}, MDiffAt (T% σ) x → Φ σ = Φ fun x' ↦ ∑ i, (c i x') (σ x') • s i x'
⊢ (∑ i, Φ fun x' ↦ (c i x') (σ x') • s i x') = ∑ i, Φ fun x' ↦ (c i x') (σ' x') • s i x'

Tactic:
congr! 1 with i
    calc Φ ((LinearMap.piApply (c i) σ) • (s i))
        = c i x (σ x) • Φ (s i) := hΦ.smul (hc hσ i) (hs i)
      _ = c i x (σ' x) • Φ (s i) := by rw [hσσ']
      _ = Φ ((LinearMap.piApply (c i) σ') • (s i)) :=
          hΦ.smul (hc hσ' i) (hs i) |>.symm

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
F' : Type u_7
inst✝¹⁸ : NormedAddCommGroup F'
inst✝¹⁷ : NormedSpace 𝕜 F'
V' : M → Type u_8
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
inst✝⁹ : VectorBundle 𝕜 F V
inst✝⁸ : VectorBundle 𝕜 F' V'
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : FiniteDimensional 𝕜 F
inst✝⁵ : FiniteDimensional 𝕜 F'
inst✝⁴ : ContMDiffVectorBundle 1 F V I
inst✝³ : ContMDiffVectorBundle 1 F' V' I
inst✝² : TopologicalSpace A
inst✝¹ : IsTopologicalAddGroup A
inst✝ : ContinuousSMul 𝕜 A
Φ : ((x : M) → V x) → ((x : M) → V' x) → A
x : M
hΦ₁ : ∀ (τ : (x : M) → V' x), MDiffAt (T% τ) x → TensorialAt I F (fun x ↦ Φ x τ) x
hΦ₂ : ∀ (σ : (x : M) → V x), MDiffAt (T% σ) x → TensorialAt I F' (Φ σ) x
this✝⁶ : T2Space (V x)
this✝⁵ : FiniteDimensional 𝕜 (V x)
this✝⁴ : T2Space (V' x)
this✝³ : FiniteDimensional 𝕜 (V' x)
this✝² : IsTopologicalAddGroup (V x)
this✝¹ : IsTopologicalAddGroup (V' x)
this✝ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
this : ∀ (x : M), ContinuousSMul 𝕜 (V' x)
v : V x
w₁ w₂ : V' x
⊢ Φ (extend F v) (extend F' (w₁ + w₂)) = Φ (extend F v) (extend F' w₁) + Φ (extend F v) (extend F' w₂)

Tactic:
by
      rw [← (hΦ₂ _ (mdifferentiableAt_extend ..)).add (mdifferentiableAt_extend ..)
        (mdifferentiableAt_extend ..)]
      apply TensorialAt.pointwise₂ hΦ₁ hΦ₂ (mdifferentiableAt_extend ..)
        (mdifferentiableAt_extend ..) (mdifferentiableAt_extend ..) <|
        mdifferentiableAt_add_section (mdifferentiableAt_extend ..) (mdifferentiableAt_extend ..)
      · rfl
      · simp

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

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

Tactic:
exact congr_arg r (zero_add a)

Goal state after:
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)) * 0 / (0 * 0) = ↑(Nat.card (ConjClasses G)) / 0

Tactic:
zero_mul,

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ MonoidHom.mrange inl ⊔ MonoidHom.mrange inr = ⊤

Tactic:
by
  rw [← mclosure_range_inl_union_inr, Submonoid.closure_union, ← MonoidHom.coe_mrange,
    ← MonoidHom.coe_mrange, Submonoid.closure_eq, Submonoid.closure_eq]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
e : M ≃* N
e' : M' ≃* N'
⊢ (Coprod.map ↑e.symm ↑e'.symm).comp (Coprod.map ↑e ↑e') = MonoidHom.id (M ∗ M')

Tactic:
ext <;> simp

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

Goal state before:
pp: M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : MulOneClass M'
inst✝ : MulOneClass N'
e : M ≃* N
e' : M' ≃* N'
⊢ (Coprod.map ↑e ↑e').comp (Coprod.map ↑e.symm ↑e'.symm) = MonoidHom.id (N ∗ N')

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.GroupTheory.PresentedGroup

Goal state before:
pp: α : Type u_1
G : Type u_3
inst✝ : Group G
f : α → G
rels : Set (FreeGroup α)
h : ∀ r ∈ rels, (FreeGroup.lift f) r = 1
g : PresentedGroup rels →* G
hg : ∀ (x : α), g (PresentedGroup.of x) = f x
⊢ ∀ {x : PresentedGroup rels}, g x = (toGroup h) x

Tactic:
intro x
  refine QuotientGroup.induction_on x ?_
  exact fun _ ↦ FreeGroup.lift_unique (g.comp (QuotientGroup.mk' _)) hg

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
⊢ ⨆ i, (f i).range ≤ (lift f).range

Tactic:
apply iSup_le _

Goal state after:
ι : Type u_1
G : ι → Type u_4
inst✝¹ : (i : ι) → Group (G i)
N : Type u_5
inst✝ : Group N
f : (i : ι) → G i →* N
⊢ ∀ (i : ι), (f i).range ≤ (lift f).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
i j : B
p k : ℕ
h : k + 1 < p
⊢ k < p

Tactic:
lia

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

Goal state before:
pp: B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
⊢ k + 1 < p

Tactic:
lia

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

Goal state before:
pp: B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
⊢ k < p

Tactic:
lia

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

Goal state before:
pp: 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
⊢ k < 2 * p

Tactic:
lia

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case neg
ι : 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
h' : w'.fstIdx ≠ some i
he : rcons { head := m, tail := w, fstIdx_ne := h } = rcons { head := m', tail := w', fstIdx_ne := h' }
hm : m = 1
hm' : ¬m' = 1
⊢ { head := m, tail := w, fstIdx_ne := h } = { head := m', tail := w', fstIdx_ne := h' }

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
h' : w'.fstIdx ≠ some i
he : rcons { head := m, tail := w, fstIdx_ne := h } = rcons { head := m', tail := w', fstIdx_ne := h' }
hm : ¬m = 1
hm' : m' = 1
⊢ { head := m, tail := w, fstIdx_ne := h } = { head := m', tail := w', fstIdx_ne := h' }

pp: case neg
ι : 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
h' : w'.fstIdx ≠ some i
he : rcons { head := m, tail := w, fstIdx_ne := h } = rcons { head := m', tail := w', fstIdx_ne := h' }
hm : ¬m = 1
hm' : ¬m' = 1
⊢ { head := m, tail := w, fstIdx_ne := h } = { head := m', tail := w', fstIdx_ne := h' }

Tactic:
· exfalso
    simp only [rcons, dif_pos hm, dif_neg hm'] at he
    rw [he] at h
    exact h rfl

Goal state after:
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
h' : w'.fstIdx ≠ some i
he : rcons { head := m, tail := w, fstIdx_ne := h } = rcons { head := m', tail := w', fstIdx_ne := h' }
hm : ¬m = 1
hm' : m' = 1
⊢ { head := m, tail := w, fstIdx_ne := h } = { head := m', tail := w', fstIdx_ne := h' }

case neg
ι : 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
h' : w'.fstIdx ≠ some i
he : rcons { head := m, tail := w, fstIdx_ne := h } = rcons { head := m', tail := w', fstIdx_ne := h' }
hm : ¬m = 1
hm' : ¬m' = 1
⊢ { head := m, tail := w, fstIdx_ne := h } = { head := m', tail := w', fstIdx_ne := h' }
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: 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 i j k
⊢ k < 2 * p

Tactic:
lia

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case cons
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
motive : Word M → Sort u_4
empty : motive Word.empty
cons :
  (i : ι) → (m : M i) → (w : Word M) → (h1 : w.fstIdx ≠ some i) → (h2 : m ≠ 1) → motive w → motive (Word.cons m w h1 h2)
m : (i : ι) × M i
w : List ((i : ι) × M i)
ih :
  (h1 : ∀ l ∈ w, l.snd ≠ 1) →
    (h2 : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) w) → motive { toList := w, ne_one := h1, chain_ne := h2 }
h1 : ∀ l ∈ m :: w, l.snd ≠ 1
h2 : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (m :: w)
⊢ motive { toList := m :: w, ne_one := h1, chain_ne := h2 }

Tactic:
refine cons m.1 m.2 ⟨w, fun _ hl => h1 _ (List.mem_cons_of_mem _ hl), h2.tail⟩ ?_ ?_ (ih _ _)
    · rw [List.isChain_cons] at h2
      simp only [fstIdx, ne_eq, Option.map_eq_some_iff,
        Sigma.exists, exists_and_right, exists_eq_right, not_exists]
      intro m' hm'
      exact h2.1 _ hm' rfl
    · exact h1 _ List.mem_cons_self

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

Goal state before:
pp: 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
⊢ k < 2 * p

Tactic:
lia

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

Goal state before:
pp: B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k < 2 * p

Tactic:
lia

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 = 1 * (cs.simple i' * cs.simple i) ^ (↑(M.M i i') - k)

Tactic:
rw [zpow_sub, zpow_natCast, simple_mul_simple_pow' cs i i', ← inv_zpow]

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 = 1 * (1 * (cs.simple i' * cs.simple i)⁻¹ ^ k)
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ cs.length w = 1 → ∃ i, w = cs.simple i

pp: case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ (∃ i, w = cs.simple i) → cs.length w = 1

Tactic:
· intro h
    rcases cs.exists_isReduced w with ⟨ω, hω, rfl⟩
    rcases List.length_eq_one_iff.mp (hω.symm.trans h) with ⟨i, rfl⟩
    exact ⟨i, cs.wordProd_singleton i⟩

Goal state after:
case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ (∃ i, w = cs.simple i) → cs.length w = 1
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
eq : cs.length (w * cs.simple i) = cs.length w
length_mod_two : cs.length w % 2 = (cs.length w + 1) % 2
⊢ False

Tactic:
lia

Goal state after:
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
ω : List B
hω : cs.IsReduced ω
j : ℕ
h₁ : cs.length (cs.wordProd (take j ω)) ≤ (take j ω).length
h₂ : cs.length (cs.wordProd (drop j ω)) ≤ (drop j ω).length
h₃ : (take j ω).length + (drop j ω).length ≤ cs.length (cs.wordProd (take j ω)) + cs.length (cs.wordProd (drop j ω))
⊢ cs.length (cs.wordProd (take j ω)) = (take j ω).length ∧ cs.length (cs.wordProd (drop j ω)) = (drop j ω).length

Tactic:
lia

Goal state after:
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
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
h : cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
⊢ ¬cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) = M.M i i' + 1

Tactic:
lia

Goal state after:
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
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
this : M.M i i' + 1 ≤ M.M i i' * 2
⊢ M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1

Tactic:
lia

Goal state after:
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
a✝ : cs.length (cs.simple i * w) < cs.length w
⊢ ¬cs.length (cs.simple i * w) = cs.length w + 1

Tactic:
lia

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

Goal state before:
pp: case cons
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  ∀ (j : ℕ),
    (cs.rightInvSeq ω).getD j 1 =
      (cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)
j : ℕ
⊢ (cs.rightInvSeq (i :: ω)).getD j 1 =
    (cs.wordProd (drop (j + 1) (i :: ω)))⁻¹ * (Option.map cs.simple (i :: ω)[j]?).getD 1 *
      cs.wordProd (drop (j + 1) (i :: ω))

Tactic:
dsimp only [rightInvSeq]
    rcases j with _ | j'
    · simp
    · simp only [getD_eq_getElem?_getD] at ih
      simp [ih j']

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

Goal state before:
pp: case mpr
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 * w) < cs.length w

Tactic:
lia

Goal state after:
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
a✝ : ¬cs.length (cs.simple i * w) < cs.length w
⊢ ¬cs.length (cs.simple i * w) + 1 = cs.length w

Tactic:
lia

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

Goal state before:
pp: case mpr
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) = cs.length w + 1 → ¬cs.length (cs.simple i * w) < cs.length w

Tactic:
lia

Goal state after:
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
a✝ : cs.length (w * cs.simple i) < cs.length w
⊢ ¬cs.length (w * cs.simple i) = cs.length w + 1

Tactic:
lia

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

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

Tactic:
lia

Goal state after:
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
a✝ : ¬cs.length (w * cs.simple i) < cs.length w
⊢ ¬cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
lia

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

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

Tactic:
lia

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 : ι
w : Word M
⊢ (equivPair i).symm ((equivPair i) w) = w

Tactic:
Equiv.symm_apply_apply

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
w : Word M
⊢ w = w
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case of
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i✝ : ι
m✝ : M i✝
w✝ : Word M
⊢ of m✝ * ((equivPair i✝).symm ((equivPair i✝) w✝)).prod = of m✝ * w✝.prod

Tactic:
Equiv.symm_apply_apply

Goal state after:
case of
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i✝ : ι
m✝ : M i✝
w✝ : Word M
⊢ of m✝ * w✝.prod = of m✝ * w✝.prod
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:
by dsimp only; rw [prod_smul, prod_empty, mul_one]

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 : ℕ
nhj : ¬j < ω.length
⊢ ω.length ≤ j

Tactic:
lia

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
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
dup : (cs.rightInvSeq ω)[j]? = (cs.rightInvSeq ω)[j']?
j'_lt_length : j' < ω.length
⊢ j < ω.length

Tactic:
lia

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
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : some (cs.rightInvSeq ω)[j] = (cs.rightInvSeq ω)[j']?
⊢ j' < ω.length

Tactic:
lia

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
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k < 2 * p

Tactic:
lia

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
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k + 1 < 2 * p

Tactic:
lia

Goal state after: