mathlib-initiative/mathlib-tactics huggingface dataset:
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)
i : ι
w✝ : Word M
j : ι
m : M j
w : Word M
h1 : w.fstIdx ≠ some j
h2 : m ≠ 1
x✝ : { p // rcons p = w }
ij : ¬i = j
⊢ (cons m w h1 h2).fstIdx ≠ some i

Tactic:
by simp [cons, fstIdx, Ne.symm ij]

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 ω₁
ω₂ : List B
hω₂ : cs.IsReduced ω₂
this : cs.length (cs.wordProd (ω₁ ++ ω₂)) ≤ (ω₁ ++ ω₂).length
⊢ cs.length (cs.wordProd ω₁ * cs.wordProd ω₂) ≤ cs.length (cs.wordProd ω₁) + cs.length (cs.wordProd ω₂)

Tactic:
simpa using

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω₁ : List B
hω₁ : cs.IsReduced ω₁
ω₂ : List B
hω₂ : cs.IsReduced ω₂
this : cs.length (cs.wordProd (ω₁ ++ ω₂)) ≤ (ω₁ ++ ω₂).length
⊢ cs.length (cs.wordProd ω₁ * cs.wordProd ω₂) ≤ ω₁.length + ω₂.length
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₂ : W
⊢ cs.length w₂ ≤ cs.length (w₁ * w₂) + cs.length w₁

Tactic:
simpa using

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ cs.length w₂ ≤ cs.length w₁ + cs.length (w₁ * w₂)
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₂ : W
⊢ cs.length w₁ ≤ cs.length (w₁ * w₂) + cs.length w₂

Tactic:
simpa using

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w₁ w₂ : W
⊢ cs.length w₁ ≤ cs.length (w₁ * w₂) + cs.length w₂
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case h₁
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.length (cs.simple i) ≤ 1

Tactic:
simpa using

Goal state after:
case h₁
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
⊢ cs.length (cs.simple i) ≤ 1
Module: Mathlib.GroupTheory.Coxeter.Inversion

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 t : W
h : cs.IsReflection (w * t * w⁻¹)
⊢ cs.IsReflection t

Tactic:
simpa using

Goal state after:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w t : W
h : cs.IsReflection (w * t * w⁻¹)
⊢ cs.IsReflection t
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
⊢ cs.length (cs.simple i * w)⁻¹ ≠ cs.length w

Tactic:
simpa using

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

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

Tactic:
simpa using

Goal state after:
case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : cs.length (w * cs.simple i) + 1 ≤ cs.length w
⊢ cs.length w ≤ cs.length (w * cs.simple i) + 1
Module: Mathlib.GroupTheory.Coxeter.Length

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

Tactic:
simpa using

Goal state after:
case inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
h : cs.length w + 1 ≤ cs.length (w * cs.simple i)
⊢ cs.length (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
this : cs.length (cs.simple i * w) = cs.length w⁻¹ + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w⁻¹
⊢ cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w

Tactic:
length_inv

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
this : cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w
⊢ cs.length (cs.simple i * w) = cs.length w + 1 ∨ cs.length (cs.simple i * w) + 1 = cs.length w
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 : cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
⊢ cs.leftInvSeq (i :: ω) = (cs.rightInvSeq (i :: ω).reverse).reverse

Tactic:
leftInvSeq,

Goal state after:
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 : cs.leftInvSeq ω = (cs.rightInvSeq ω.reverse).reverse
⊢ cs.simple i :: List.map (⇑(MulAut.conj (cs.simple i))) (cs.leftInvSeq ω) = (cs.rightInvSeq (i :: ω).reverse).reverse
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case step
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
m✝ : ℕ
m : (M.M i i').succ.le m✝
ih : cs.IsReduced (drop 1 ((if Even m✝ then i' else i) :: alternatingWord i i' m✝))
⊢ cs.IsReduced (alternatingWord i i' m✝)

Tactic:
simpa using

Goal state after:
case step
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
m✝ : ℕ
m : (M.M i i').succ.le m✝
ih : cs.IsReduced (drop 1 ((if Even m✝ then i' else i) :: alternatingWord i i' m✝))
⊢ cs.IsReduced (alternatingWord i i' m✝)
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
⊢ cs.IsRightDescent w⁻¹ i ↔ cs.IsLeftDescent w i

Tactic:
simpa using

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.IsRightDescent w⁻¹ i ↔ cs.IsLeftDescent w i
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
⊢ cs.IsRightDescent w i ↔ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
unfold IsRightDescent
  constructor
  · intro _
    exact (cs.length_mul_simple w i).resolve_left (by lia)
  · lia

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x y : (i : ι) × M i
l : List ((i : ι) × M i)
hnot1✝ : ∀ l_1 ∈ x :: y :: l, l_1.snd ≠ 1
hnot1 : x.snd ≠ 1 ∧ ∀ x ∈ y :: l, x.snd ≠ 1
hchain✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (x :: y :: l)
hchain : x.fst ≠ y.fst ∧ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (y :: l)
h : { toList := x :: y :: l, ne_one := hnot1✝, chain_ne := hchain✝ } ≠ empty
i j : ι
w' : NeWord M i j
hw' : w'.toList = y :: l
⊢ y = ⟨i, w'.head⟩

Tactic:
simpa using

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x y : (i : ι) × M i
l : List ((i : ι) × M i)
hnot1✝ : ∀ l_1 ∈ x :: y :: l, l_1.snd ≠ 1
hnot1 : x.snd ≠ 1 ∧ ∀ x ∈ y :: l, x.snd ≠ 1
hchain✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (x :: y :: l)
hchain : x.fst ≠ y.fst ∧ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (y :: l)
h : { toList := x :: y :: l, ne_one := hnot1✝, chain_ne := hchain✝ } ≠ empty
i j : ι
w' : NeWord M i j
hw' : w'.toList = y :: l
⊢ y = ⟨i, w'.head⟩
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case cons.cons
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) × M i
l : List ((i : ι) × M i)
i j : ι
w' : NeWord M i j
hnot1✝ : ∀ l_1 ∈ x :: ⟨i, w'.head⟩ :: l, l_1.snd ≠ 1
hnot1 : x.snd ≠ 1 ∧ ∀ x ∈ ⟨i, w'.head⟩ :: l, x.snd ≠ 1
hchain✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (x :: ⟨i, w'.head⟩ :: l)
hchain : x.fst ≠ ⟨i, w'.head⟩.fst ∧ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (⟨i, w'.head⟩ :: l)
h : { toList := x :: ⟨i, w'.head⟩ :: l, ne_one := hnot1✝, chain_ne := hchain✝ } ≠ empty
hw' : w'.toList = ⟨i, w'.head⟩ :: l
⊢ ((singleton x.snd ⋯).append ⋯ w').toWord.toList =
    { toList := x :: ⟨i, w'.head⟩ :: l, ne_one := hnot1✝, chain_ne := hchain✝ }.toList

Tactic:
simpa using

Goal state after:
case cons.cons
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) × M i
l : List ((i : ι) × M i)
i j : ι
w' : NeWord M i j
hnot1✝ : ∀ l_1 ∈ x :: ⟨i, w'.head⟩ :: l, l_1.snd ≠ 1
hnot1 : x.snd ≠ 1 ∧ ∀ x ∈ ⟨i, w'.head⟩ :: l, x.snd ≠ 1
hchain✝ : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (x :: ⟨i, w'.head⟩ :: l)
hchain : x.fst ≠ ⟨i, w'.head⟩.fst ∧ List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (⟨i, w'.head⟩ :: l)
h : { toList := x :: ⟨i, w'.head⟩ :: l, ne_one := hnot1✝, chain_ne := hchain✝ } ≠ empty
hw' : w'.toList = ⟨i, w'.head⟩ :: l
⊢ w'.toList = ⟨i, w'.head⟩ :: l
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' < (cs.rightInvSeq ω).length
dup : (cs.rightInvSeq ω)[j]? = (cs.rightInvSeq ω)[j']?
⊢ j' < ω.length

Tactic:
simpa using

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' < (cs.rightInvSeq ω).length
dup : (cs.rightInvSeq ω)[j]? = (cs.rightInvSeq ω)[j']?
⊢ j' < ω.length
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 < (cs.leftInvSeq (alternatingWord i j (2 * p))).length

Tactic:
simpa using

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.CoprodI

Goal state before:
pp: case singleton
ι : 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 i✝ : ι
x : H i✝
hne_one : x ≠ 1
k : ι
hk : i✝ ≠ k
⊢ (lift f) (NeWord.singleton x hne_one).prod • X k ⊆ X i✝

Tactic:
simpa using

Goal state after:
case singleton
ι : 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 i✝ : ι
x : H i✝
hne_one : x ≠ 1
k : ι
hk : i✝ ≠ k
⊢ (f i✝) x • X k ⊆ X i✝
Module: Mathlib.GroupTheory.DivisibleHull

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

Tactic:
simpa using

Goal state after:
case inl.e_m.e_a
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : 0 ≤ a
⊢ 0 ≤ a
Module: Mathlib.GroupTheory.DivisibleHull

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

Tactic:
simpa using

Goal state after:
case e_a
M : Type u_2
inst✝ : AddCommGroup M
a : ℚ
m : M
s : ℕ+
h : a ≤ 0
⊢ a ≤ 0
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
i j k : ι
w : NeWord H i j
hhead : k ≠ i
hlast : k ≠ j
heq1 : (lift f) w.prod = 1
⊢ X k ⊆ X i

Tactic:
simpa using

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
i j k : ι
w : NeWord H i j
hhead : k ≠ i
hlast : k ≠ j
heq1 : (lift f) w.prod = 1
⊢ X k ⊆ X i
Module: Mathlib.GroupTheory.DoubleCoset

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

Tactic:
simpa using

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

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
y : ↥K
h_h : x * ((↑y)⁻¹ * a⁻¹) ∈ H
⊢ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y

Tactic:
refine ⟨x * (y⁻¹ * a⁻¹), h_h, y, y.2, ?_⟩

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a x : G
y : ↥K
h_h : x * ((↑y)⁻¹ * a⁻¹) ∈ H
⊢ x = x * (↑y⁻¹ * a⁻¹) * a * ↑y
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case neg
ι : 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)
hl : j ≠ i
⊢ (lift f) w.prod ≠ 1

Tactic:
exact lift_word_prod_nontrivial_of_head_card f X hXnonempty hXdisj hpp w hcard hl.symm

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos
ι : 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 j)
hh : i ≠ j
this : (lift f) w.inv.prod ≠ 1
heq : (lift f) w.prod = 1
⊢ (lift f) w.inv.prod = 1

Tactic:
simpa using

Goal state after:
case pos
ι : 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 j)
hh : i ≠ j
this : (lift f) w.inv.prod ≠ 1
heq : (lift f) w.prod = 1
⊢ (lift f) w.prod = 1
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
a : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
⊢ ↑⟨a.den, ⋯⟩ * a.num ≠ 0

Tactic:
simpa using

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

Goal state before:
pp: case mk.refine_2
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : ↑s • 0 < ↑1 • m
⊢ 0 < m

Tactic:
simpa using

Goal state after:
case mk.refine_2
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
b c : ℚ≥0
h : b < c
m : M
s : ℕ+
ha : ↑s • 0 < ↑1 • m
⊢ 0 < m
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a b : M
h : a ≤ b
⊢ (↑(coeAddMonoidHom M)).toFun a ≤ (↑(coeAddMonoidHom M)).toFun b

Tactic:
simpa using

Goal state after:
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a b : M
h : a ≤ b
⊢ a ≤ b
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
x : DivisibleHull M
x✝³ x✝² : M
x✝¹ x✝ : ℕ+
h : ArchimedeanClass.mk (mk x✝³ x✝¹) = ArchimedeanClass.mk (mk x✝² x✝)
⊢ (archimedeanClassOrderHom M) (ArchimedeanClass.mk x✝³) = (archimedeanClassOrderHom M) (ArchimedeanClass.mk x✝²)

Tactic:
simpa using

Goal state after:
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
x : DivisibleHull M
x✝³ x✝² : M
x✝¹ x✝ : ℕ+
h : ArchimedeanClass.mk (mk x✝³ x✝¹) = ArchimedeanClass.mk (mk x✝² x✝)
⊢ (archimedeanClassOrderHom M) (ArchimedeanClass.mk x✝³) = (archimedeanClassOrderHom M) (ArchimedeanClass.mk x✝²)
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
t : Finset (Quotient ↑H ↑K)
ht : ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K ≠ Set.univ
x : G
y : Quotient ↑H ↑K
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) ↑H ↑K
hx : Quot.mk (⇑(rightRel H)) q = Quot.mk (⇑(rightRel H)) x
a : ↥H
ha : x = ↑a * q
⊢ x = ↑a * q * 1

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
t : Finset (Quotient ↑H ↑K)
ht : ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K ≠ Set.univ
x : G
y : Quotient ↑H ↑K
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) ↑H ↑K
hx : Quot.mk (⇑(rightRel H)) q = Quot.mk (⇑(rightRel H)) x
a : ↥H
ha : x = ↑a * q
⊢ x = ↑a * q
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
num✝¹ : M
den✝¹ : ℕ+
num✝ : M
den✝ : ℕ+
h : (archimedeanClassOrderHom M) (ArchimedeanClass.mk num✝¹) ≤ (archimedeanClassOrderHom M) (ArchimedeanClass.mk num✝)
⊢ (mk num✝¹ den✝¹).liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯ ≤
    (mk num✝ den✝).liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯

Tactic:
simpa using

Goal state after:
case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
num✝¹ : M
den✝¹ : ℕ+
num✝ : M
den✝ : ℕ+
h : (archimedeanClassOrderHom M) (ArchimedeanClass.mk num✝¹) ≤ (archimedeanClassOrderHom M) (ArchimedeanClass.mk num✝)
⊢ ArchimedeanClass.mk num✝¹ ≤ ArchimedeanClass.mk num✝
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: ι : Type u_1
G : Type u_2
inst✝ : Monoid G
n : ι → ℕ
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i)))
i : ι
⊢ n i = orderOf (e.symm (Pi.mulSingle i (Multiplicative.ofAdd 1)))

Tactic:
simpa using

Goal state after:
ι : Type u_1
G : Type u_2
inst✝ : Monoid G
n : ι → ℕ
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i)))
i : ι
⊢ n i = addOrderOf 1
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
g g' : G
h : ∀ (φ : G →* Mˣ), φ g = φ g'
⊢ g = g'

Tactic:
simpa using

Goal state after:
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
g g' : G
h : ∀ (φ : G →* Mˣ), φ g = φ g'
⊢ g = g'
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
ι : Type
w✝ : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h₂.some
e' : (((i : ι) → Multiplicative (ZMod (n i))) →* Mˣ) ≃* ((i : ι) → Multiplicative (ZMod (n i)) →* Mˣ) :=
  Pi.monoidHomMulEquiv (fun i ↦ Multiplicative (ZMod (n i))) Mˣ
this : ∀ (i : ι), NeZero (n i)
i : ι
⊢ Nat.card (Multiplicative (ZMod (n i))) ∣ Monoid.exponent G

Tactic:
simpa using

Goal state after:
G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
ι : Type
w✝ : Fintype ι
n : ι → ℕ
h₁ : ∀ (i : ι), 1 < n i
h₂ : Nonempty (G ≃* ((i : ι) → Multiplicative (ZMod (n i))))
e : G ≃* ((i : ι) → Multiplicative (ZMod (n i))) := h₂.some
e' : (((i : ι) → Multiplicative (ZMod (n i))) →* Mˣ) ≃* ((i : ι) → Multiplicative (ZMod (n i)) →* Mˣ) :=
  Pi.monoidHomMulEquiv (fun i ↦ Multiplicative (ZMod (n i))) Mˣ
this : ∀ (i : ι), NeZero (n i)
i : ι
⊢ n i ∣ Monoid.exponent G
Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Type u_2
N : Type u_3
inst✝¹ : Group H
inst✝ : Group N
f : G →* H
K : FiniteIndexNormalSubgroup H
g : G →* H ⧸ K.toSubgroup := (QuotientGroup.mk' K.toSubgroup).comp f
⊢ Subgroup.comap f K.toSubgroup = g.ker

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝² : Group G
H : Type u_2
N : Type u_3
inst✝¹ : Group H
inst✝ : Group N
f : G →* H
K : FiniteIndexNormalSubgroup H
g : G →* H ⧸ K.toSubgroup := (QuotientGroup.mk' K.toSubgroup).comp f
⊢ Subgroup.comap f K.toSubgroup = g.ker
Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Type u_2
N : Type u_3
inst✝¹ : Group H
inst✝ : Group N
f : G →* H
K : FiniteIndexNormalSubgroup H
g : G →* H ⧸ K.toSubgroup := (QuotientGroup.mk' K.toSubgroup).comp f
hker : Subgroup.comap f K.toSubgroup = g.ker
⊢ (Subgroup.comap f K.toSubgroup).FiniteIndex

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝² : Group G
H : Type u_2
N : Type u_3
inst✝¹ : Group H
inst✝ : Group N
f : G →* H
K : FiniteIndexNormalSubgroup H
g : G →* H ⧸ K.toSubgroup := (QuotientGroup.mk' K.toSubgroup).comp f
hker : Subgroup.comap f K.toSubgroup = g.ker
⊢ g.ker.FiniteIndex
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
⊢ n < -1 + 1

Tactic:
simpa using

Goal state after:
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := fun _i ↦ FreeGroup Unit
f : (i : ι) → H i →* G := fun i ↦ FreeGroup.lift fun x ↦ a i
X' : ι → Set α := fun i ↦ X i ∪ Y i
i j : ι
hij : i ≠ j
n : ℤ
hnne0 : n ≠ 0
hgt : n < 0
⊢ n < 0