mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.CardCommute

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Group α
inst✝⁴ : MulAction α β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
this :
  ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card ↥(stabilizer α (φ ω)) = Fintype.card (α ⧸ stabilizer α (φ ω))
⊢ Fintype.card β = ∑ ω, Fintype.card α / Fintype.card ↥(stabilizer α (φ ω))

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : Group α
inst✝⁴ : MulAction α β
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype (Quotient (orbitRel α β))
inst✝ : (b : β) → Fintype ↥(stabilizer α b)
φ : Quotient (orbitRel α β) → β
hφ : LeftInverse Quotient.mk'' φ
this :
  ∀ (ω : Quotient (orbitRel α β)),
    Fintype.card α / Fintype.card ↥(stabilizer α (φ ω)) = Fintype.card (α ⧸ stabilizer α (φ ω))
⊢ Fintype.card β = ∑ ω, Fintype.card α / Fintype.card ↥(stabilizer α (φ ω))
Module: Mathlib.GroupTheory.SpecificGroups.KleinFour

Goal state before:
pp: G₁ : Type u_2
G₂ : Type u_3
inst✝³ : Group G₁
inst✝² : Group G₂
inst✝¹ : IsKleinFour G₁
inst✝ : IsKleinFour G₂
⊢ Nonempty (G₁ ≃* G₂)

Tactic:
by
  classical
  let _inst₁ := Fintype.ofFinite G₁
  let _inst₁ := Fintype.ofFinite G₂
  exact ⟨mulEquiv ((Fintype.equivOfCardEq <| by simp).setValue 1 1) <| by simp⟩

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ commProb (M × M') = commProb M * commProb M'

Tactic:
[

Goal state after:
M : Type u_1
inst✝¹ : Mul M
M' : Type u_2
inst✝ : Mul M'
⊢ commProb (M × M') = commProb M * commProb M'
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: α : Type u_2
i : α → Type u_3
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ commProb ((a : α) → i a) = ∏ a, commProb (i a)

Tactic:
[

Goal state after:
α : Type u_2
i : α → Type u_3
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ commProb ((a : α) → i a) = ∏ a, commProb (i a)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
hn : Odd n
hn' : NeZero n
⊢ Nat.card { p // Commute p.1 p.2 } = n * (n + 3)

Tactic:
[

Goal state after:
n : ℕ
hn : Odd n
hn' : NeZero n
⊢ Nat.card { p // Commute p.1 p.2 } = n * (n + 3)
Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
G : Type u_3
H✝ : Type u_4
inst✝¹ : Group G
inst✝ : Group H✝
b b' : G ≃* FreeGroup ι
hbb' : (fun b i ↦ b.repr.symm (FreeGroup.of i)) { repr := b } = (fun b i ↦ b.repr.symm (FreeGroup.of i)) { repr := b' }
H : ↑b.symm = ↑b'.symm
this : b.symm = b'.symm
⊢ b.symm.symm = b'.symm.symm

Tactic:
this

Goal state after:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H✝ : Type u_4
inst✝¹ : Group G
inst✝ : Group H✝
b b' : G ≃* FreeGroup ι
hbb' : (fun b i ↦ b.repr.symm (FreeGroup.of i)) { repr := b } = (fun b i ↦ b.repr.symm (FreeGroup.of i)) { repr := b' }
H : ↑b.symm = ↑b'.symm
this : b.symm = b'.symm
⊢ b'.symm.symm = b'.symm.symm
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
hδ : (r' ^ 2)⁻¹ < 1 - δ * C
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝² : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this✝¹ : ‖g' x - g' y‖ ≤ δ
v : E y
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y) v
hgy : ((g y) v) v = ((g' y) w) w
hgx : ((g x) ((trivializationAt F E x).symm x w)) ((trivializationAt F E x).symm x w) = ((g' x) w) w
this✝ : ((g' x) w) w ≤ δ * C * ((g' x) w) w + ((g' y) w) w
this : ((g' x) w) w ≤ (1 - δ * C)⁻¹ * ((g' y) w) w
⊢ ((g' x) w) w ≤ r' ^ 2 * ((g' y) w) w

Tactic:
this

Goal state after:
B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
hδ : (r' ^ 2)⁻¹ < 1 - δ * C
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝² : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this✝¹ : ‖g' x - g' y‖ ≤ δ
v : E y
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y) v
hgy : ((g y) v) v = ((g' y) w) w
hgx : ((g x) ((trivializationAt F E x).symm x w)) ((trivializationAt F E x).symm x w) = ((g' x) w) w
this✝ : ((g' x) w) w ≤ δ * C * ((g' x) w) w + ((g' y) w) w
this : ((g' x) w) w ≤ (1 - δ * C)⁻¹ * ((g' y) w) w
⊢ (1 - δ * C)⁻¹ * ((g' y) w) w ≤ r' ^ 2 * ((g' y) w) w
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
fi : (i : ι) → M i →* N
x✝¹ x✝ : FreeMonoid ((i : ι) × M i)
⊢ Rel M x✝¹ x✝ ≤ (Con.ker (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd)) x✝¹ x✝

Tactic:
[

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
fi : (i : ι) → M i →* N
x✝¹ x✝ : FreeMonoid ((i : ι) × M i)
⊢ Rel M x✝¹ x✝ ≤ (Con.ker (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd)) x✝¹ x✝
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
⊢ Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹

Tactic:
[

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹
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 i' : B
⊢ ((⇑ι ∘ cs.simple) i * (⇑ι ∘ cs.simple) i') ^ M.M i i' = 1

Tactic:
by
    rw [comp_apply, comp_apply, ← map_mul, ← map_pow, simple_mul_simple_pow, map_one]

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

Goal state before:
pp: case mul_simple_left
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ ∀ (w : W) (i : B), (∃ a, cs.wordProd a = w) → ∃ a, cs.wordProd a = cs.simple i * w

Tactic:
rintro _ i ⟨ω, rfl⟩
    use i :: ω
    rw [wordProd_cons]

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

Goal state before:
pp: case pos
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : Even (p + k)
⊢ (if Even (p + (k + 1)) then i else j) = if Even (p + k) then j else i

Tactic:
if_pos h_even,

Goal state after:
case pos
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < p
h_even : Even (p + k)
⊢ (if Even (p + (k + 1)) then i else j) = j
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
i i' : B
m : ℕ
hm : m ≤ M.M i i' * 2
⊢ cs.wordProd (alternatingWord i i' m) = cs.wordProd (alternatingWord i' i (M.M i i' * 2 - m))

Tactic:
[

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hm : m ≤ M.M i i' * 2
⊢ cs.wordProd (alternatingWord i i' m) = cs.wordProd (alternatingWord i' i (M.M i i' * 2 - m))
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
i i' : B
m : ℕ
hm : m ≤ M.M i i' * 2
⊢ (if Even ↑m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2) =
    (if Even ↑(M.M i i' * 2 - m) then 1 else cs.simple i) * (cs.simple i' * cs.simple i) ^ ((M.M i i' * 2 - m) / 2)

Tactic:
[

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hm : m ≤ M.M i i' * 2
⊢ (if Even ↑m then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (m / 2) =
    (if Even ↑(M.M i i' * 2 - m) then 1 else cs.simple i) * (cs.simple i' * cs.simple i) ^ ((M.M i i' * 2 - m) / 2)
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case cons
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m : M i
k : ι
g : M k
tail : Word M
h1 : tail.fstIdx ≠ some k
h2 : g ≠ 1
ih :
  ⟨i, m⟩ ∈
      (↑(consRecOn tail ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j_1 m w h1 h2 x ↦
              if ij : j = j_1 then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
              else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔
    ⟨i, m⟩ ∈ tail.toList.tail ∨ ¬i = j ∧ ∃ (h : ¬tail.toList = []), tail.toList.head h = ⟨i, m⟩
⊢ ⟨i, m⟩ ∈
      (↑(consRecOn (cons g tail h1 h2) ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j_1 m w h1 h2 x ↦
              if ij : j = j_1 then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
              else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔
    ⟨i, m⟩ ∈ (cons g tail h1 h2).toList.tail ∨
      ¬i = j ∧ ∃ (h : ¬(cons g tail h1 h2).toList = []), (cons g tail h1 h2).toList.head h = ⟨i, m⟩

Tactic:
simp only [consRecOn_cons]
    split_ifs with h
    · subst k
      by_cases hij : j = i <;> simp_all
    · by_cases hik : i = k
      · subst i; simp_all [@eq_comm _ m g, @eq_comm _ k j, or_comm]
      · simp [hik, Ne.symm hik]

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
⊢ M.IsLiftable fun x ↦ Multiplicative.ofAdd 1

Tactic:
[

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
⊢ M.IsLiftable fun x ↦ Multiplicative.ofAdd 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
w t : W
⊢ cs.IsLeftInversion w⁻¹ t ↔ cs.IsRightInversion w t

Tactic:
convert! cs.isRightInversion_inv_iff.symm
  simp

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
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsLeftInversion (t * w) t ↔ ¬cs.IsLeftInversion w t

Tactic:
← isRightInversion_inv_iff,

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsRightInversion (t * w)⁻¹ t ↔ ¬cs.IsLeftInversion w t
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
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsRightInversion (t * w)⁻¹ t ↔ ¬cs.IsLeftInversion w t

Tactic:
← isRightInversion_inv_iff,

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsRightInversion (t * w)⁻¹ t ↔ ¬cs.IsRightInversion w⁻¹ t
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case refl
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
this : M.M i i' * 2 - (M.M i i' + 1) = M.M i i' - 1
⊢ cs.length (cs.wordProd (alternatingWord i' i (M.M i i' * 2 - (M.M i i' + 1)))) < M.M i i' + 1

Tactic:
this

Goal state after:
case refl
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
this : M.M i i' * 2 - (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
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.rightInvSeq ω).getD j 1 * (cs.rightInvSeq ω).getD j 1 = 1

Tactic:
[

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
⊢ (cs.rightInvSeq ω).getD j 1 * (cs.rightInvSeq ω).getD j 1 = 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
j : ℕ
⊢ (cs.leftInvSeq ω).getD j 1 * (cs.leftInvSeq ω).getD j 1 = 1

Tactic:
[

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
⊢ (cs.leftInvSeq ω).getD j 1 * (cs.leftInvSeq ω).getD j 1 = 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
this : List.map (fun x ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ (List.map (fun x ↦ x⁻¹) (cs.rightInvSeq ω.reverse)).prod = cs.wordProd ω

Tactic:
this

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
this : List.map (fun x ↦ x⁻¹) (cs.rightInvSeq ω.reverse) = cs.rightInvSeq ω.reverse
⊢ (cs.rightInvSeq ω.reverse).prod = cs.wordProd ω
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsAddTorsionFree M
s : ℕ+
m n : M
h : mk m s = mk n s
⊢ m = n

Tactic:
[

Goal state after:
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsAddTorsionFree M
s : ℕ+
m n : M
h : mk m s = mk n s
⊢ m = n
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
α : Type u_6
inst✝ : MulAction G α
X : ι → Set α
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
i j k : ι
w : NeWord H i j
hk : j ≠ k
⊢ (lift f) w.prod • X k ⊆ X i

Tactic:
by
  induction w generalizing k with
  | singleton x hne_one => simpa using hpp hk _ hne_one
  | @append i j k l w₁ hne w₂ hIw₁ hIw₂ =>
    calc
      lift f (NeWord.append w₁ hne w₂).prod • X k = lift f w₁.prod • lift f w₂.prod • X k := by
        simp [mul_smul]
      _ ⊆ lift f w₁.prod • X _ := smul_set_subset_smul_set_iff.mpr (hIw₂ hk)
      _ ⊆ X i := hIw₁ hne

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
⊢ (a * b) • mk m s = a • b • mk m s

Tactic:
[

Goal state after:
case mk
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
⊢ (a * b) • mk m s = a • b • mk m s
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
a : α
s t : Set α
⊢ doubleCoset a s t = Set.image2 (fun x1 x2 ↦ x1 * a * x2) s t

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : Mul α
a : α
s t : Set α
⊢ doubleCoset a s t = Set.image2 (fun x1 x2 ↦ x1 * a * x2) s t
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
⊢ (a + b) • mk m s = a • mk m s + b • mk m s

Tactic:
[

Goal state after:
case mk
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
⊢ (a + b) • mk m s = a • mk m s + b • mk m s
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case e'_1.e'_3
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : ↑s' • m = ↑s • m'
h' : ↑t' • n = ↑t • n'
⊢ (↑s' * ↑t') • ↑t • m = (↑s * ↑t) • ↑t' • m'

Tactic:
[

Goal state after:
case e'_1.e'_3
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : ↑s' • m = ↑s • m'
h' : ↑t' • n = ↑t • n'
⊢ (↑s' * ↑t') • ↑t • m = (↑s * ↑t) • ↑t' • m'
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case e'_1.e'_4
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : ↑s' • m = ↑s • m'
h' : ↑t' • n = ↑t • n'
⊢ (↑s' * ↑t') • ↑s • n = (↑s * ↑t) • ↑s' • n'

Tactic:
[

Goal state after:
case e'_1.e'_4
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : ↑s' • m = ↑s • m'
h' : ↑t' • n = ↑t • n'
⊢ (↑s' * ↑t') • ↑s • n = (↑s * ↑t) • ↑s' • n'
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 : ℕ+
⊢ mk ma sa ≤ mk mb sb ∨ mk mb sb ≤ mk ma sa

Tactic:
[

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 : ℕ+
⊢ mk ma sa ≤ mk mb sb ∨ mk mb sb ≤ mk ma sa
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
⊢ DecidableLE (DivisibleHull M)

Tactic:
unfold DecidableLE LE.le instLE liftOn₂ LocalizedModule.liftOn₂

Goal state after:
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m m' : M
s s' : ℕ+
⊢ mk m s < mk m' s' ↔ ↑s' • m < ↑s • m'

Tactic:
[

Goal state after:
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m m' : M
s s' : ℕ+
⊢ mk m s < mk m' s' ↔ ↑s' • m < ↑s • m'
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a✝ b✝ : G
⊢ (setoid ↑⊥ ↑H) a✝ b✝ ↔ (leftRel H) a✝ b✝

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a✝ b✝ : G
⊢ (setoid ↑⊥ ↑H) a✝ b✝ ↔ (leftRel H) a✝ b✝
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk.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 : ℕ+
mc : M
sc : ℕ+
h : mk mb sb < mk mc sc
⊢ mk ma sa + mk mb sb < mk ma sa + mk mc sc

Tactic:
[

Goal state after:
case mk.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 : ℕ+
mc : M
sc : ℕ+
h : mk mb sb < mk mc sc
⊢ mk ma sa + mk mb sb < mk ma sa + mk mc sc
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a✝ b✝ : G
⊢ (setoid ↑H ↑⊥) a✝ b✝ ↔ (rightRel H) a✝ b✝

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a✝ b✝ : G
⊢ (setoid ↑H ↑⊥) a✝ b✝ ↔ (rightRel H) a✝ b✝
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk.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 : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
⊢ ↑(sa * sc) • (↑sb • ma + ↑sa • mb) < ↑(sa * sb) • (↑sc • ma + ↑sa • mc)

Tactic:
[

Goal state after:
case mk.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 : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
⊢ ↑(sa * sc) • (↑sb • ma + ↑sa • mb) < ↑(sa * sb) • (↑sc • ma + ↑sa • mc)
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk.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 : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
this : (↑sa * ↑sb * ↑sc) • ma + ↑(sa * sa) • ↑sc • mb < (↑sa * ↑sb * ↑sc) • ma + ↑(sa * sa) • ↑sb • mc
⊢ (↑sa * (↑sc * ↑sb)) • ma + (↑sa * (↑sc * ↑sa)) • mb < (↑sa * (↑sb * ↑sc)) • ma + (↑sa * (↑sb * ↑sa)) • mc

Tactic:
[

Goal state after:
case mk.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 : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
this : (↑sa * ↑sb * ↑sc) • ma + ↑(sa * sa) • ↑sc • mb < (↑sa * ↑sb * ↑sc) • ma + ↑(sa * sa) • ↑sb • mc
⊢ (↑sa * (↑sc * ↑sb)) • ma + (↑sa * (↑sc * ↑sa)) • mb < (↑sa * (↑sb * ↑sc)) • ma + (↑sa * (↑sb * ↑sa)) • mc
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
I : Finset (Quotient ↑H ↑K)
hI : ⋃ i ∈ I, quotToDoubleCoset H K i = Set.univ
this : ↑I = Set.univ
⊢ Finite (Quotient ↑H ↑K)

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
I : Finset (Quotient ↑H ↑K)
hI : ⋃ i ∈ I, quotToDoubleCoset H K i = Set.univ
this : ↑I = Set.univ
⊢ Finite (Quotient ↑H ↑K)
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: case mpr.mk
G : Type u_1
inst✝ : Group G
H K : Subgroup G
I : Finset (Quotient ↑H ↑K)
hI : ∀ (x : G), x ∈ ⋃ i ∈ I, quotToDoubleCoset H K i
x✝ : Quotient ↑H ↑K
g : G
i : Quotient ↑H ↑K
hi : i ∈ I
hT : g ∈ quotToDoubleCoset H K i
⊢ Quot.mk (⇑(setoid ↑H ↑K)) g ∈ ↑I

Tactic:
simpa [← (mem_quotToDoubleCoset_iff _ _).mp hT] using! hi

Goal state after:
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 : mk mb sb < mk mc sc
⊢ a • mk mb sb < a • mk mc sc

Tactic:
[

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
a : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : mk mb sb < mk mc sc
⊢ a • mk mb sb < a • mk mc sc
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 • mk mb sb < a • mk mc sc

Tactic:
[

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
a : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
⊢ a • mk mb sb < a • mk mc sc