mathlib-initiative/mathlib-tactics huggingface dataset:
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] = some (cs.rightInvSeq ω)[j']
⊢ False

Tactic:
]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : some (cs.rightInvSeq ω)[j] = some (cs.rightInvSeq ω)[j']
⊢ False
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
⊢ False

Tactic:
]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
⊢ False
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
⊢ (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
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
⊢ (cs.rightInvSeq ω).getD j' 1 * (cs.rightInvSeq ω).getD j' 1 = 1
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
m m' : M
s s' : ℕ+
⊢ (∃ u, u • ↑ⁿ s' • m = u • ↑ⁿ s • m') ↔ ∃ b, ↑(↑ⁿ.symm b) • ↑s' • m = ↑(↑ⁿ.symm b) • ↑s • m'

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
m m' : M
s s' : ℕ+
⊢ (∃ u, u • ↑ⁿ s' • m = u • ↑ⁿ s • m') ↔ ∃ b, ↑(↑ⁿ.symm b) • ↑s' • m = ↑(↑ⁿ.symm b) • ↑s • m'
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
h₄ : t * t' = 1
⊢ cs.wordProd ω = cs.wordProd ω * 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
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
t' : W := (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₂ : t' = (cs.rightInvSeq (ω.eraseIdx j)).getD (j' - 1) 1
h₃ : t' = (cs.rightInvSeq ω).getD j' 1
h₄ : t * t' = 1
⊢ cs.wordProd ω = cs.wordProd ω * 1
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
m1 m2 : M
s : ℕ+
⊢ ∃ u, ↑u • ↑s • (↑s • m1 + ↑s • m2) = ↑u • ↑(s * s) • (m1 + m2)

Tactic:
]

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
m1 m2 : M
s : ℕ+
⊢ ∃ u, ↑u • ↑s • (↑s • m1 + ↑s • m2) = ↑u • ↑(s * s) • (m1 + m2)
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 ω
⊢ cs.IsReduced ω

Tactic:
]

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
⊢ cs.IsReduced ω
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case inl
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : 0 ≤ a
⊢ mk
      (↑(have this := ⟨a, h⟩;
            this).num •
        m)
      (⟨(have this := ⟨a, h⟩;
            this).den,
          ⋯⟩ *
        s) =
    mk (a.num • m) (⟨a.den, ⋯⟩ * s)

Tactic:
]

Goal state after:
case inl
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : 0 ≤ a
⊢ mk
      (↑(have this := ⟨a, h⟩;
            this).num •
        m)
      (⟨(have this := ⟨a, h⟩;
            this).den,
          ⋯⟩ *
        s) =
    mk (a.num • m) (⟨a.den, ⋯⟩ * s)
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
⊢ cs.wordProd (take (k + 1) (alternatingWord i j (2 * p))) * cs.simple (alternatingWord i j (2 * p))[k + 1] *
      (cs.wordProd (take (k + 1) (alternatingWord i j (2 * p))))⁻¹ =
    (MulAut.conj (cs.simple i))
      (cs.wordProd (take k (alternatingWord j i (2 * p))) * cs.simple (alternatingWord j i (2 * p))[k] *
        (cs.wordProd (take k (alternatingWord j i (2 * p))))⁻¹)

Tactic:
]

Goal state after:
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
⊢ cs.wordProd (take (k + 1) (alternatingWord i j (2 * p))) * cs.simple (alternatingWord i j (2 * p))[k + 1] *
      (cs.wordProd (take (k + 1) (alternatingWord i j (2 * p))))⁻¹ =
    (MulAut.conj (cs.simple i))
      (cs.wordProd (take k (alternatingWord j i (2 * p))) * cs.simple (alternatingWord j i (2 * p))[k] *
        (cs.wordProd (take k (alternatingWord j i (2 * p))))⁻¹)
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case inr
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
⊢ -((have this := ⟨-a, ⋯⟩;
        this) •
        mk m s) =
    mk (a.num • m) (⟨a.den, ⋯⟩ * s)

Tactic:
]

Goal state after:
case inr
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
⊢ -((have this := ⟨-a, ⋯⟩;
        this) •
        mk m s) =
    mk (a.num • m) (⟨a.den, ⋯⟩ * s)
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
⊢ ↑a.num.natAbs • m = -a.num • m

Tactic:
]

Goal state after:
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
⊢ ↑a.num.natAbs • m = -a.num • m
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
⊢ cs.simple (alternatingWord j i (2 * p))[k] = cs.simple (alternatingWord j i (2 * p))[k]

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:
]

Goal state after:
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
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case inr
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
⊢ a • mk m s = mk (a.num • m) (⟨a.den, ⋯⟩ * s)

Tactic:
rw [qsmul_of_nonpos h]
    have : a.num.natAbs • m = -a.num • m := by
      rw [← natCast_zsmul]
      congr
      simpa using h
    simp [nnqsmul_mk, this, ← neg_mk]

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
p k : ℕ
hk :
  ∀ (i j : B) (h : k < 2 * p),
    (cs.leftInvSeq (alternatingWord i j (2 * p)))[k] = cs.wordProd (alternatingWord j i (2 * k + 1))
i j : B
h : k + 1 < 2 * p
⊢ 2 * (k + 1) = 2 * k + 1 + 1

Tactic:
by ring

Goal state after:
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
p k : ℕ
hk :
  ∀ (i j : B) (h : k < 2 * p),
    (cs.leftInvSeq (alternatingWord i j (2 * p)))[k] = cs.wordProd (alternatingWord j i (2 * k + 1))
i j : B
h : k + 1 < 2 * p
⊢ cs.simple i * cs.wordProd (alternatingWord i j (2 * k + 1)) * cs.simple i =
    cs.simple i * (cs.wordProd (alternatingWord i j (2 * k + 1)) * cs.simple i)

Tactic:
]

Goal state after:
case succ
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p k : ℕ
hk :
  ∀ (i j : B) (h : k < 2 * p),
    (cs.leftInvSeq (alternatingWord i j (2 * p)))[k] = cs.wordProd (alternatingWord j i (2 * k + 1))
i j : B
h : k + 1 < 2 * p
⊢ cs.simple i * cs.wordProd (alternatingWord i j (2 * k + 1)) * cs.simple i =
    cs.simple i * (cs.wordProd (alternatingWord i j (2 * k + 1)) * cs.simple i)
Module: Mathlib.GroupTheory.DivisibleHull

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

Tactic:
]

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
α : 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 ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ w.head⁻¹
⊢ h / w.head⁻¹ ≠ 1

Tactic:
]

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
α : 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 ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H i)
hheadtail : i ≠ j
h : H i
hn1 : h ≠ 1
hnh : h ≠ w.head⁻¹
⊢ h / w.head⁻¹ ≠ 1
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a h : G
hh : h ∈ ↑H
k : G
hk : k ∈ ↑K
hb : h * a * k ∈ doubleCoset a ↑H ↑K
⊢ ↑H * {a} * ↑K = ↑H * {a} * ↑K

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ∃ x ∈ doubleCoset a ↑H ↑K, x ∈ doubleCoset b ↑H ↑K
⊢ b ∈ doubleCoset a ↑H ↑K

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ∃ x ∈ doubleCoset a ↑H ↑K, x ∈ doubleCoset b ↑H ↑K
⊢ b ∈ doubleCoset a ↑H ↑K
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ y * b * r' = l * a * r

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ y * b * r' = l * a * r
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doubleCoset b ↑H ↑K) (doubleCoset a ↑H ↑K)
⊢ doubleCoset a ↑H ↑K = doubleCoset b ↑H ↑K

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doubleCoset b ↑H ↑K) (doubleCoset a ↑H ↑K)
⊢ doubleCoset a ↑H ↑K = doubleCoset b ↑H ↑K
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ ⊥, ∃ b_1 ∈ H, b = a_1 * a * b_1) ↔ a⁻¹ * b ∈ H

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ ⊥, ∃ b_1 ∈ H, b = a_1 * a * b_1) ↔ a⁻¹ * b ∈ H
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ b ∈ H

Tactic:
]

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ b ∈ H
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
h : a⁻¹ * b ∈ H
⊢ b = b

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ H, ∃ b_1 ∈ ⊥, b = a_1 * a * b_1) ↔ b * a⁻¹ ∈ H

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
⊢ (∃ a_1 ∈ H, ∃ b_1 ∈ ⊥, b = a_1 * a * b_1) ↔ b * a⁻¹ ∈ H
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
a b : G
h : b * a⁻¹ ∈ H
⊢ b = b

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

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

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
⊢ (setoid ↑H ↑K) a b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
⊢ (setoid ↑H ↑K) a b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: 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'
⊢ (↑t • m ≤ ↑s • n) = (↑t' • m' ≤ ↑s' • n')

Tactic:
]

Goal state after:
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'
⊢ (↑t • m ≤ ↑s • n) = (↑t' • m' ≤ ↑s' • n')
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k
⊢ ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out (mk H K g) = h * g * k

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k
⊢ ∃ h k, h ∈ H ∧ k ∈ K ∧ Quotient.out (mk H K g) = h * g * k
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: 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') • ↑s • n ↔ ↑t' • m' ≤ ↑s' • n'

Tactic:
]

Goal state after:
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') • ↑s • n ↔ ↑t' • m' ≤ ↑s' • n'
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k
h : G
h_h : h ∈ H
k : G
hk : k ∈ K
T : g = h * Quotient.out (mk H K g) * k
⊢ g = g

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : doubleCoset a ↑H ↑K = doubleCoset b ↑H ↑K
⊢ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : doubleCoset a ↑H ↑K = doubleCoset b ↑H ↑K
⊢ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
i : Quotient ↑H ↑K
a : G
hg : mk H K a = mk H K (Quotient.out i)
⊢ a ∈ quotToDoubleCoset H K i

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
i : Quotient ↑H ↑K
a : G
hg : mk H K a = mk H K (Quotient.out i)
⊢ a ∈ quotToDoubleCoset H K i
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 : ℕ+
hab : ↑sb • ma ≤ ↑sa • mb
mc : M
sc : ℕ+
hbc : ↑sc • mb ≤ ↑sb • mc
⊢ ↑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 : ℕ+
hab : ↑sb • ma ≤ ↑sa • mb
mc : M
sc : ℕ+
hbc : ↑sc • mb ≤ ↑sb • mc
⊢ ↑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 : ℕ+
hab : ↑sb • ma ≤ ↑sa • mb
mc : M
sc : ℕ+
hbc : ↑sc • mb ≤ ↑sb • mc
⊢ ↑sc • ↑sb • ma ≤ ↑sa • ↑sb • 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 : ℕ+
hab : ↑sb • ma ≤ ↑sa • mb
mc : M
sc : ℕ+
hbc : ↑sc • mb ≤ ↑sb • mc
⊢ ↑sc • ↑sb • ma ≤ ↑sa • ↑sb • 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 : ℕ+
hab : ↑sc • ↑sb • ma ≤ ↑sa • ↑sc • mb
hbc : ↑sc • mb ≤ ↑sb • mc
⊢ ↑sc • ↑sb • ma ≤ ↑sa • ↑sb • 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 : ℕ+
hab : ↑sc • ↑sb • ma ≤ ↑sa • ↑sc • mb
hbc : ↑sc • mb ≤ ↑sb • mc
⊢ ↑sc • ↑sb • ma ≤ ↑sa • ↑sb • 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 : ℕ+
hab : ↑sc • ↑sb • ma ≤ ↑sa • ↑sc • mb
hbc : ↑sa • ↑sc • mb ≤ ↑sa • ↑sb • mc
⊢ ↑sc • ↑sb • ma ≤ ↑sa • ↑sb • 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 : ℕ+
hab : ↑sc • ↑sb • ma ≤ ↑sa • ↑sc • mb
hbc : ↑sa • ↑sc • mb ≤ ↑sa • ↑sb • mc
⊢ ↑sc • ↑sb • ma ≤ ↑sa • ↑sb • mc
Module: Mathlib.GroupTheory.DivisibleHull

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

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 : ℕ+
h : ↑sb • ma ≤ ↑sa • mb
h' : ↑sa • mb ≤ ↑sb • ma
⊢ mk ma sa = mk mb sb
Module: Mathlib.GroupTheory.DivisibleHull

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

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 : ℕ+
h : ↑sb • ma ≤ ↑sa • mb
h' : ↑sa • mb ≤ ↑sb • ma
⊢ ↑sb • ma = ↑sa • mb
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.DoubleCoset

Goal state before:
pp: case mpr
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), x ∈ ↑I

Tactic:
]

Goal state after:
case mpr
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), x ∈ ↑I
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
⊢ ∀ (x : Quot ⇑(leftRel K)), ∃ i, x ∈ Quot.mk ⇑(leftRel K) '' doubleCoset (out i) ↑H ↑K

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
⊢ ∀ (x : Quot ⇑(leftRel K)), ∃ i, x ∈ Quot.mk ⇑(leftRel K) '' doubleCoset (out i) ↑H ↑K
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 ι
⊢ ∀ (b : Word H), (lift f) (Word.equiv.symm b) = 1 → Word.equiv.symm b = 1

Tactic:
]

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 ι
⊢ ∀ (b : Word H), (lift f) (Word.equiv.symm b) = 1 → Word.equiv.symm b = 1
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) w.prod = 1
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
⊢ ∀ (x : Quot ⇑(rightRel H)), ∃ i, x ∈ Quot.mk ⇑(rightRel H) '' doubleCoset (out i) ↑H ↑K

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
⊢ ∀ (x : Quot ⇑(rightRel H)), ∃ i, x ∈ Quot.mk ⇑(rightRel H) '' doubleCoset (out i) ↑H ↑K