mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.Submersion

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
H : Type u_7
G : Type u_9
E : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
hf : IsSubmersionAt I J n f x
hfg : f =ᶠ[𝓝 x] g
⊢ NormedAddCommGroup hf.complement

Tactic:
by infer_instance

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

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
H : Type u_7
G : Type u_9
E : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f g : M → N
x : M
hf : IsSubmersionAt I J n f x
hfg : f =ᶠ[𝓝 x] g
⊢ NormedSpace 𝕜 hf.complement

Tactic:
by infer_instance

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

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsSubmersionOfComplement F I J n f
hM : IsEmpty M
⊢ NormedAddCommGroup PUnit.{u + 1}

Tactic:
by infer_instance

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

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsSubmersionOfComplement F I J n f
hM : IsEmpty M
⊢ NormedSpace 𝕜 PUnit.{u + 1}

Tactic:
by infer_instance

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

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsSubmersionOfComplement F I J n f
hM : Nonempty M
inhabited_h : Inhabited M
x : M := default
⊢ NormedAddCommGroup ⋯.smallComplement

Tactic:
by infer_instance

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

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
F : Type u_5
H : Type u_7
G : Type u_9
E : Type u
inst✝¹² : NontriviallyNormedField 𝕜
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedAddCommGroup E''
inst✝⁸ : NormedSpace 𝕜 E''
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsSubmersionOfComplement F I J n f
hM : Nonempty M
inhabited_h : Inhabited M
x : M := default
⊢ NormedSpace 𝕜 ⋯.smallComplement

Tactic:
by infer_instance

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

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
H : Type u_7
G : Type u_9
E : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsSubmersion I J n f
x : M
⊢ NormedAddCommGroup h.complement

Tactic:
by infer_instance

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

Goal state before:
pp: 𝕜 : Type u_1
E'' : Type u_3
H : Type u_7
G : Type u_9
E : Type u
inst✝¹⁰ : NontriviallyNormedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup E''
inst✝⁶ : NormedSpace 𝕜 E''
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace G
I : ModelWithCorners 𝕜 E H
J : ModelWithCorners 𝕜 E'' G
M : Type u_11
N : Type u_13
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
h : IsSubmersion I J n f
x : M
⊢ NormedSpace 𝕜 h.complement

Tactic:
by infer_instance

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

Goal state before:
pp: 𝕜 : Type u_1
H : Type u_7
E : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
⊢ NormedAddCommGroup PUnit.{u + 1}

Tactic:
by infer_instance

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

Goal state before:
pp: 𝕜 : Type u_1
H : Type u_7
E : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
n : ℕ∞ω
inst✝ : IsManifold I n M
⊢ NormedSpace 𝕜 PUnit.{u + 1}

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.LocalFrame

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
inst✝² : VectorBundle 𝕜 F V
ι : Type u_7
e : Trivialization F TotalSpace.proj
inst✝¹ : MemTrivializationAtlas e
b : Basis ι 𝕜 F
inst✝ : ContMDiffVectorBundle 1 F V I
x : M
hx : x ∈ e.baseSet
s : (x : M) → V x
i : ι
he : IsLocalFrameOn I F 1 (e.localFrame b) e.baseSet
⊢ (localFrameCoeff I e b i x) (s x) = ((e.basisAt b hx).repr (s x)) i

Tactic:
have hbasis : e.basisAt b hx = he.toBasisAt hx := by
    ext j
    simp [IsLocalFrameOn.toBasisAt, localFrame, basisAt, hx]

Goal state after:
𝕜 : 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
inst✝² : VectorBundle 𝕜 F V
ι : Type u_7
e : Trivialization F TotalSpace.proj
inst✝¹ : MemTrivializationAtlas e
b : Basis ι 𝕜 F
inst✝ : ContMDiffVectorBundle 1 F V I
x : M
hx : x ∈ e.baseSet
s : (x : M) → V x
i : ι
he : IsLocalFrameOn I F 1 (e.localFrame b) e.baseSet
hbasis : e.basisAt b hx = he.toBasisAt hx
⊢ (localFrameCoeff I e b i x) (s x) = ((e.basisAt b hx).repr (s x)) i
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion

Goal state before:
pp: case mp
𝕜 : 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
inst✝³ : CompleteSpace 𝕜
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : IsManifold I 2 M
cov : CovariantDerivative I E (TangentSpace I)
⊢ cov.torsion = 0 →
    ∀ {X Y : (x : M) → TangentSpace I x} {x : M},
      MDiffAt (T% X) x → MDiffAt (T% Y) x → (↑cov Y x) (X x) - (↑cov X x) (Y x) = mlieBracket I X Y x

Tactic:
intro h X Y x hX hY
    replace h := congr($h x (X x) (Y x))
    rw [cov.torsion_apply hX hY] at h
    simpa [sub_eq_iff_eq_add'] using h

Goal state after:
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'' φ
ω : Quotient (orbitRel α β)
⊢ Nonempty ↥(stabilizer α (φ ω))

Tactic:
by infer_instance

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Star

Goal state before:
pp: A : Type u_1
inst✝¹ : AddMonoid A
inst✝ : StarAddMonoid A
r : A → A → Prop
hr : ∀ (a b : A), r a b → r (Star.star a) (Star.star b)
a b w✝ x✝ y✝ z✝ : A
h1 : Rel r w✝ x✝
h2 : Rel r y✝ z✝
⊢ Rel r (Star.star (w✝ + y✝)) (Star.star (x✝ + z✝))

Tactic:
rw [star_add, star_add]

Goal state after:
A : Type u_1
inst✝¹ : AddMonoid A
inst✝ : StarAddMonoid A
r : A → A → Prop
hr : ∀ (a b : A), r a b → r (Star.star a) (Star.star b)
a b w✝ x✝ y✝ z✝ : A
h1 : Rel r w✝ x✝
h2 : Rel r y✝ z✝
⊢ Rel r (Star.star w✝ + Star.star y✝) (Star.star x✝ + Star.star z✝)
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

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

Tactic:
zero_add,

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

Goal state before:
pp: case of_mul
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
x : G ⊕ H
xs : FreeMonoid (G ⊕ H)
ihx : mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList xs)).reverse) * mk xs = 1
⊢ mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList xs)).reverse) *
      (mk (of (Sum.map Inv.inv Inv.inv x)) * mk (of x) * mk xs) =
    1

Tactic:
mk_of_inv_mul,

Goal state after:
case of_mul
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
x : G ⊕ H
xs : FreeMonoid (G ⊕ H)
ihx : mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList xs)).reverse) * mk xs = 1
⊢ mk (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList xs)).reverse) * (1 * mk xs) = 1
Module: Mathlib.GroupTheory.Coxeter.Basic

Goal state before:
pp: case mul_right
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x ↦ p w
y : W
my : y ∈ Submonoid.closure (Set.range cs.simple)
i : W
mi : i ∈ Set.range cs.simple
ih : p y
⊢ p (y * i)

Tactic:
rw [Set.mem_range] at mi
    exact mi.choose_spec ▸ mul_simple_right _ _ ih

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
⊢ take (k + 1) (alternatingWord i j (2 * p)) = i :: take k (alternatingWord j i (2 * p))

Tactic:
listTake_alternatingWord j i p k (by lia),

Goal state after:
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ take (k + 1) (alternatingWord i j (2 * p)) = i :: if Even k then alternatingWord j i k else alternatingWord i j k
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 : ℤ
⊢ (if Even (2 * k) then 1 else cs.simple i') * (cs.simple i * cs.simple i') ^ (2 * k / 2) =
    (if Even (↑(M.M i i') * 2 - 2 * k) then 1 else cs.simple i) *
      (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') * 2 - 2 * k) / 2)

Tactic:
rw [if_pos (by use k; ring), if_pos (by use -k + (M i i'); ring), mul_comm 2 k, ← sub_mul]

Goal state after:
case inl
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
k : ℤ
⊢ 1 * (cs.simple i * cs.simple i') ^ (k * 2 / 2) = 1 * (cs.simple i' * cs.simple i) ^ ((↑(M.M i i') - k) * 2 / 2)
Module: Mathlib.GroupTheory.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
⊢ 1 • w = w

Tactic:
apply (equivPair i).symm_apply_eq.mpr
    simp [equivPair]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

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

Tactic:
· dsimp only
      intro i m w ih
      rw [prod_smul, mul_smul, ih]

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

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

Tactic:
| cons k ω _ =>

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)
x : (i : ι) × M i
l : List ((i : ι) × M i)
hi :
  ∀ (hnot1 : ∀ l_1 ∈ l, l_1.snd ≠ 1) (hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) l),
    { toList := l, ne_one := hnot1, chain_ne := hchain } ≠ empty →
      ∃ i j w', w'.toWord.toList = { toList := l, ne_one := hnot1, chain_ne := hchain }.toList
hnot1 : ∀ l_1 ∈ x :: l, l_1.snd ≠ 1
hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (x :: l)
h : { toList := x :: l, ne_one := hnot1, chain_ne := hchain } ≠ empty
⊢ ∃ i j w', w'.toWord.toList = { toList := x :: l, ne_one := hnot1, chain_ne := hchain }.toList

Tactic:
rw [List.forall_mem_cons] at hnot1

Goal state after:
case cons
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
x : (i : ι) × M i
l : List ((i : ι) × M i)
hi :
  ∀ (hnot1 : ∀ l_1 ∈ l, l_1.snd ≠ 1) (hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) l),
    { toList := l, ne_one := hnot1, chain_ne := hchain } ≠ empty →
      ∃ i j w', w'.toWord.toList = { toList := l, ne_one := hnot1, chain_ne := hchain }.toList
hnot1✝ : ∀ l_1 ∈ x :: l, l_1.snd ≠ 1
hnot1 : x.snd ≠ 1 ∧ ∀ x ∈ l, x.snd ≠ 1
hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) (x :: l)
h : { toList := x :: l, ne_one := hnot1✝, chain_ne := hchain } ≠ empty
⊢ ∃ i j w', w'.toWord.toList = { toList := x :: l, ne_one := hnot1✝, chain_ne := hchain }.toList
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
lt : j < ω.length
⊢ cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) *
      ((cs.wordProd (drop (j + 1) ω))⁻¹ * (Option.map cs.simple ω[j]?).getD 1 * cs.wordProd (drop (j + 1) ω)) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)

Tactic:
simp only [getElem?_eq_getElem lt, wordProd_append, mul_assoc]

Goal state after:
case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
lt : j < ω.length
⊢ cs.wordProd (take j ω) *
      (cs.wordProd (some ω[j]).toList *
        (cs.wordProd (drop (j + 1) ω) *
          ((cs.wordProd (drop (j + 1) ω))⁻¹ *
            ((Option.map cs.simple (some ω[j])).getD 1 * cs.wordProd (drop (j + 1) ω))))) =
    cs.wordProd (take j ω) * cs.wordProd (drop (j + 1) ω)
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
lt : j < ω.length
⊢ cs.wordProd (take j ω) * (Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹ *
      cs.wordProd (take j ω ++ ω[j]?.toList ++ drop (j + 1) ω) =
    cs.wordProd (take j ω ++ drop (j + 1) ω)

Tactic:
simp only [getElem?_eq_getElem lt, wordProd_append, mul_assoc]

Goal state after:
case inl
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
lt : j < ω.length
⊢ cs.wordProd (take j ω) *
      ((Option.map cs.simple (some ω[j])).getD 1 *
        ((cs.wordProd (take j ω))⁻¹ *
          (cs.wordProd (take j ω) * (cs.wordProd (some ω[j]).toList * cs.wordProd (drop (j + 1) ω))))) =
    cs.wordProd (take j ω) * cs.wordProd (drop (j + 1) ω)
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
⊢ ∃ i_1 j_1 w'_1,
    w'_1.toWord.toList = { toList := x :: ⟨i, w'.head⟩ :: l, ne_one := hnot1✝, chain_ne := hchain✝ }.toList

Tactic:
refine ⟨x.1, j, append (singleton x.2 hnot1.1) hchain.1 w', ?_⟩

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
⊢ ((singleton x.snd ⋯).append ⋯ w').toWord.toList =
    { toList := x :: ⟨i, w'.head⟩ :: l, ne_one := hnot1✝, chain_ne := hchain✝ }.toList
Module: Mathlib.GroupTheory.DoubleCoset

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

Tactic:
have := eq H K (mk H K g : Quotient ↑H ↑K).out g
  rw [out_eq'] at this
  obtain ⟨h, h_h, k, hk, T⟩ := this.1 rfl
  refine ⟨h⁻¹, k⁻¹, H.inv_mem h_h, K.inv_mem hk, eq_mul_inv_of_mul_eq (eq_inv_mul_of_mul_eq ?_)⟩
  rw [← mul_assoc, ← T]

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
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 ι
⊢ ∀ (a : CoprodI H), (lift f) a = 1 → a = 1

Tactic:
rw [(CoprodI.Word.equiv).forall_congr_left]

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: case refine_3
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝¹ : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
ι : Type u_1
⊢ (lift fun i ↦ FreeGroup.lift fun x ↦ FreeGroup.of i).comp (FreeGroup.lift fun i ↦ of (FreeGroup.of ())) =
    MonoidHom.id (FreeGroup ι)

pp: case refine_4
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝¹ : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
ι : Type u_1
⊢ (FreeGroup.lift fun i ↦ of (FreeGroup.of ())).comp (lift fun i ↦ FreeGroup.lift fun x ↦ FreeGroup.of i) =
    MonoidHom.id (CoprodI fun x ↦ FreeGroup Unit)

Tactic:
· ext; simp

Goal state after:
case refine_4
ι✝ : Type u_1
M : ι✝ → Type u_2
inst✝¹ : (i : ι✝) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
ι : Type u_1
⊢ (FreeGroup.lift fun i ↦ of (FreeGroup.of ())).comp (lift fun i ↦ FreeGroup.lift fun x ↦ FreeGroup.of i) =
    MonoidHom.id (CoprodI fun x ↦ FreeGroup Unit)
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
hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K
y : Quotient ↑H ↑K
hy : y ∈ t
⊢ ∀ x_1 ∈ doubleCoset (out y) ↑H ↑K, ¬Quot.mk (⇑(leftRel K)) x_1 = Quot.mk (⇑(leftRel K)) x

Tactic:
q

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
hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K
y : Quotient ↑H ↑K
hy : y ∈ t
q : G
⊢ q ∈ doubleCoset (out y) ↑H ↑K → ¬Quot.mk (⇑(leftRel K)) q = Quot.mk (⇑(leftRel K)) 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
hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K
y : Quotient ↑H ↑K
hy : y ∈ t
⊢ ∀ x_1 ∈ doubleCoset (out y) ↑H ↑K, ¬Quot.mk (⇑(rightRel H)) x_1 = Quot.mk (⇑(rightRel H)) x

Tactic:
q

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
hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K
y : Quotient ↑H ↑K
hy : y ∈ t
q : G
⊢ q ∈ doubleCoset (out y) ↑H ↑K → ¬Quot.mk (⇑(rightRel H)) q = Quot.mk (⇑(rightRel H)) x
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : ↥S) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
hf : Function.Surjective ⇑f
⊢ Nat.card G ∣ ∏ _x, Monoid.exponent G

Tactic:
replace hf := card_dvd_of_surjective f hf

Goal state after:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : Group.FG G
S : Finset G
hS1 : #S = Group.rank G
hS2 : closure ↑S = ⊤
f : ((g : ↥S) → ↥(zpowers ↑g)) →* G := noncommPiCoprod ⋯
hf : Nat.card G ∣ Nat.card ((g : ↥S) → ↥(zpowers ↑g))
⊢ Nat.card G ∣ ∏ _x, Monoid.exponent G
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
T : H.LeftTransversal
inst✝ : H.FiniteIndex
g : G
⊢ ϕ.transfer g = diff ϕ T (g • T)

Tactic:
rw [transfer, ← diff_mul_diff, ← smul_diff_smul, mul_comm, diff_mul_diff] <;> rfl

Goal state after: