mathlib-initiative/mathlib-tactics huggingface dataset:
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
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), (lift f) (of a) = f a
⊢ (FreeGroup.lift of).comp (lift FreeGroup.of) = MonoidHom.id G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : IsFreeGroup G
H : Type u_2
inst✝ : Group H
f : Generators G → H
⊢ ∃! F, ∀ (a : Generators G), F (of a) = f a

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
motive : M ∗ N → Prop
m : M ∗ N
one : motive 1
inl_mul : ∀ (m : M) (x : M ∗ N), motive x → motive (inl m * x)
inr_mul : ∀ (n : N) (x : M ∗ N), motive x → motive (inr n * x)
⊢ motive m

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
motive : M ∗ N → Prop
m : M ∗ N
inl : ∀ (m : M), motive (Coprod.inl m)
inr : ∀ (n : N), motive (Coprod.inr n)
mul : ∀ (x y : M ∗ N), motive x → motive y → motive (x * y)
⊢ motive 1

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ Submonoid.closure (Set.range ⇑inl ∪ Set.range ⇑inr) = ⊤

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_5
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
f : M ∗ N →* P
⊢ MonoidHom.mrange f = MonoidHom.mrange (f.comp inl) ⊔ MonoidHom.mrange (f.comp inr)

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : MulOneClass M'
inst✝¹ : MulOneClass N'
inst✝ : MulOneClass P
f : M →* M'
g : N →* N'
⊢ (mk.comp (FreeMonoid.map (Sum.map ⇑f ⇑g))) (of (Sum.inl 1)) = 1

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : MulOneClass M'
inst✝¹ : MulOneClass N'
inst✝ : MulOneClass P
f : M →* M'
g : N →* N'
⊢ (mk.comp (FreeMonoid.map (Sum.map ⇑f ⇑g))) (of (Sum.inr 1)) = 1

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : MulOneClass M'
inst✝¹ : MulOneClass N'
inst✝ : MulOneClass P
f : M →* M'
g : N →* N'
x y : M
⊢ (mk.comp (FreeMonoid.map (Sum.map ⇑f ⇑g))) (of (Sum.inl (x * y))) =
    (mk.comp (FreeMonoid.map (Sum.map ⇑f ⇑g))) (of (Sum.inl x) * of (Sum.inl y))

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : MulOneClass M'
inst✝¹ : MulOneClass N'
inst✝ : MulOneClass P
f : M →* M'
g : N →* N'
x y : N
⊢ (mk.comp (FreeMonoid.map (Sum.map ⇑f ⇑g))) (of (Sum.inr (x * y))) =
    (mk.comp (FreeMonoid.map (Sum.map ⇑f ⇑g))) (of (Sum.inr x) * of (Sum.inr y))

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : MulOneClass M'
inst✝¹ : MulOneClass N'
inst✝ : MulOneClass P
⊢ (mk.comp (FreeMonoid.map Sum.swap)) (of (Sum.inl 1)) = 1

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : MulOneClass M'
inst✝¹ : MulOneClass N'
inst✝ : MulOneClass P
⊢ (mk.comp (FreeMonoid.map Sum.swap)) (of (Sum.inr 1)) = 1

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : MulOneClass M'
inst✝¹ : MulOneClass N'
inst✝ : MulOneClass P
x y : M
⊢ (mk.comp (FreeMonoid.map Sum.swap)) (of (Sum.inl (x * y))) =
    (mk.comp (FreeMonoid.map Sum.swap)) (of (Sum.inl x) * of (Sum.inl y))

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
M' : Type u_3
N' : Type u_4
P : Type u_5
inst✝⁴ : MulOneClass M
inst✝³ : MulOneClass N
inst✝² : MulOneClass M'
inst✝¹ : MulOneClass N'
inst✝ : MulOneClass P
x y : N
⊢ (mk.comp (FreeMonoid.map Sum.swap)) (of (Sum.inr (x * y))) =
    (mk.comp (FreeMonoid.map Sum.swap)) (of (Sum.inr x) * of (Sum.inr y))

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : Monoid P
P' : Type u_4
inst✝ : Monoid P'
f : P →* P'
g₁ : M →* P
g₂ : N →* P
⊢ (f.comp (lift g₁ g₂)).comp inl = (lift (f.comp g₁) (f.comp g₂)).comp inl

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M
inst✝² : MulOneClass N
inst✝¹ : Monoid P
P' : Type u_4
inst✝ : Monoid P'
f : P →* P'
g₁ : M →* P
g₂ : N →* P
⊢ (f.comp (lift g₁ g₂)).comp inr = (lift (f.comp g₁) (f.comp g₂)).comp inr

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : Monoid P
f : M →* P
g : N →* P
⊢ MonoidHom.mrange (lift f g) = MonoidHom.mrange f ⊔ MonoidHom.mrange g

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ fst.prod snd = toProd

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M ∗ N
⊢ (fst x, snd x) = toProd x

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ (MonoidHom.fst M N).comp toProd = fst

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M ∗ N
⊢ (toProd x).1 = fst x

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ (MonoidHom.snd M N).comp toProd = snd

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M ∗ N
⊢ (toProd x).2 = snd x

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M × N
⊢ toProd (inl x.1 * inr x.2) = x

Tactic:
by

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
x : FreeMonoid (G ⊕ H)
⊢ (coprodCon G H) (ofList (List.map (Sum.map Inv.inv Inv.inv) (toList x)).reverse * x) 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
⊢ inl.range ⊔ inr.range = ⊤

Tactic:
by

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : Group H
K : Type u_3
inst✝ : Group K
f : G ∗ H →* K
⊢ f.range = (f.comp inl).range ⊔ (f.comp inr).range

Tactic:
by

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

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝² : Group G
inst✝¹ : Group H
K : Type u_3
inst✝ : Group K
f : G →* K
g : H →* K
⊢ (lift f g).range = f.range ⊔ g.range

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
⊢ (Coprod.lift (inl.comp inl) (Coprod.map inr (MonoidHom.id P))).comp
      (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (inr.comp inr)) =
    MonoidHom.id ((M ∗ N) ∗ P)

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
⊢ (Coprod.lift (Coprod.map (MonoidHom.id M) inl) (inr.comp inr)).comp
      (Coprod.lift (inl.comp inl) (Coprod.map inr (MonoidHom.id P))) =
    MonoidHom.id (M ∗ (N ∗ P))

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PresentedGroup

Goal state before:
pp: α : Type u_1
rels : Set (FreeGroup α)
⊢ Subgroup.closure (Set.range of) = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PresentedGroup

Goal state before:
pp: α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x : PresentedGroup rels
x✝ : α
a✝ : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) (FreeGroup.of x✝) ∈ H
⊢ ?m.50 ∈ H

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PresentedGroup

Goal state before:
pp: α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x : PresentedGroup rels
⊢ x ∈ H

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PresentedGroup

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

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PresentedGroup

Goal state before:
pp: α : Type u_1
G : Type u_3
inst✝ : Group G
rels : Set (FreeGroup α)
φ ψ : PresentedGroup rels →* G
hx : ∀ (x : α), φ (of x) = ψ (of x)
⊢ φ = ψ

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.PresentedGroup

Goal state before:
pp: α : Type u_1
β : Type u_2
rels₁ : Set (FreeGroup α)
rels₂ : Set (FreeGroup β)
r : FreeGroup (α ⊕ β)
hr : r ∈ ⇑(FreeGroup.map Sum.inl) '' rels₁ ∪ ⇑(FreeGroup.map Sum.inr) '' rels₂
⊢ (FreeGroup.lift (toCoprod rels₁ rels₂)) r = 1

Tactic:
obtain ⟨r, hr, rfl⟩ | ⟨r, hr, rfl⟩ := hr

Goal state after:
case inl
α : Type u_1
β : Type u_2
rels₁ : Set (FreeGroup α)
rels₂ : Set (FreeGroup β)
r : FreeGroup α
hr : r ∈ rels₁
⊢ (FreeGroup.lift (toCoprod rels₁ rels₂)) ((FreeGroup.map Sum.inl) r) = 1

case inr
α : Type u_1
β : Type u_2
rels₁ : Set (FreeGroup α)
rels₂ : Set (FreeGroup β)
r : FreeGroup β
hr : r ∈ rels₂
⊢ (FreeGroup.lift (toCoprod rels₁ rels₂)) ((FreeGroup.map Sum.inr) r) = 1
Module: Mathlib.GroupTheory.PresentedGroup

Goal state before:
pp: α : Type u_1
β : Type u_2
rels₁ : Set (FreeGroup α)
rels₂ : Set (FreeGroup β)
r : FreeGroup (α ⊕ β)
hr : r ∈ ⇑(FreeGroup.map Sum.inl) '' rels₁ ∪ ⇑(FreeGroup.map Sum.inr) '' rels₂
⊢ (FreeGroup.lift (toCoprod rels₁ rels₂)) r = 1

Tactic:
by

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
⊢ Set.range (uncurry M'.relation) = Set.range (uncurry M'.relation ∘ Prod.map ⇑e ⇑e)

Tactic:
by

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
⊢ Set.range (uncurry M'.relation ∘ Prod.map ⇑e ⇑e) = Set.range (⇑(FreeGroup.freeGroupCongr e) ∘ uncurry M.relation)

Tactic:
by

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
M' : CoxeterMatrix B' := CoxeterMatrix.reindex e M
⊢ Set.range (⇑(FreeGroup.freeGroupCongr e) ∘ uncurry M.relation) = ⇑(FreeGroup.freeGroupCongr e) '' M.relationsSet

Tactic:
by

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
⊢ Surjective ⇑↑(FreeGroup.freeGroupCongr e)

Tactic:
by

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
⊢ Subgroup.map (↑(FreeGroup.freeGroupCongr e)) (Subgroup.normalClosure M.relationsSet) =
    Subgroup.normalClosure (CoxeterMatrix.reindex e M).relationsSet

Tactic:
by

Goal state after:
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 : B
⊢ uncurry M.relation (i, i) = FreeGroup.of i * FreeGroup.of i

Tactic:
by

Goal state after:
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 : B
⊢ cs.simple i * cs.simple i = 1

Tactic:
by

Goal state after:
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
w : W
i : B
⊢ w * cs.simple i * cs.simple i = w

Tactic:
by

Goal state after:
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
w : W
i : B
⊢ cs.simple i * (cs.simple i * w) = w

Tactic:
by

Goal state after:
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
⊢ (cs.simple i * cs.simple i') ^ M.M i i' = 1

Tactic:
by

Goal state after:
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
f g : CoprodI M →* N
h : ∀ (i : ι), f.comp of = g.comp of
x✝ : (i : ι) × M i
i : ι
x : M i
⊢ (f.comp (conGen (Rel M)).mk') (FreeMonoid.of ⟨i, x⟩) = (g.comp (conGen (Rel M)).mk') (FreeMonoid.of ⟨i, x⟩)

Tactic:
by

Goal state after:
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
⊢ Subgroup.closure (Set.range cs.simple) = ⊤

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
⊢ 0 < r' ^ 2

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
⊢ Submonoid.closure (Set.range cs.simple) = ⊤

Tactic:
by

Goal state after:
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
⊢ Function.LeftInverse (fun f x ↦ f.comp of) fun fi ↦ (conGen (Rel M)).lift (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd) ⋯

Tactic:
by

Goal state after:
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
p : W → Prop
w : W
simple : ∀ (i : B), p (cs.simple i)
one : p 1
mul : ∀ (w w' : W), p w → p w' → p (w * w')
⊢ p w

Tactic:
by

Goal state after:
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
⊢ Function.RightInverse (fun f x ↦ f.comp of) fun fi ↦
    (conGen (Rel M)).lift (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : DecidableEq ι
i : ι
x : M i
⊢ (lift (Pi.mulSingle i (MonoidHom.id (M i)))) (of x) = x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i : ι
⊢ Function.Injective ⇑of

Tactic:
by

Goal state after:
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
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
⊢ p w

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
⊢ MonoidHom.mrange (lift f) = ⨆ i, MonoidHom.mrange (f i)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
s : Submonoid N
⊢ MonoidHom.mrange (lift f) ≤ s ↔ ∀ (i : ι), MonoidHom.mrange (f i) ≤ s

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ ⨆ i, MonoidHom.mrange of = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
⊢ Submonoid.closure (⋃ i, range ⇑of) = ⊤

Tactic:
by

Goal state after:
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
p : W → Prop
w : W
one : p 1
mul_simple_right : ∀ (w : W) (i : B), p w → p (w * cs.simple i)
⊢ p w

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
motive : CoprodI M → Prop
one : motive 1
mul : ∀ {i : ι} (m : M i) (x : CoprodI M), motive x → motive (of m * x)
x : CoprodI M
hx : x ∈ ⋃ i, range ⇑of
y : CoprodI M
ihy : motive y
⊢ ∃ i m, of m = x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
motive : CoprodI M → Prop
m : CoprodI M
one : motive 1
mul : ∀ {i : ι} (m : M i) (x : CoprodI M), motive x → motive (of m * x)
⊢ motive m

Tactic:
by

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

Goal state before:
pp: B : Type u_1
M : CoxeterMatrix B
G : Type u_5
inst✝ : Group G
f : B → G
hf : M.IsLiftable f
r : FreeGroup B
hr : r ∈ M.relationsSet
⊢ (FreeGroup.lift f) r = 1

Tactic:
by

Goal state after:
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
a : PresentedGroup M.relationsSet
⊢ cs.mulEquiv.toMonoidHom (cs.mulEquiv.symm a) = cs.mulEquiv (cs.mulEquiv.symm a)

Tactic:
by

Goal state after:
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
a : PresentedGroup M.relationsSet
⊢ cs.mulEquiv (cs.mulEquiv.symm a) = a

Tactic:
by

Goal state after:
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

Goal state after:
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
⊢ ∀ᶠ (y : B) in 𝓝 x,
    ‖Trivialization.symmL ℝ (trivializationAt F E x) x ∘SL
          Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ <
      r

Tactic:
by

Goal state after:
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
⊢ (1 + ‖Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖) * 2 > 0

Tactic:
by

Goal state after:
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
f : { f // M.IsLiftable f }
⊢ (fun ι ↦ ⟨⇑ι ∘ cs.simple, ⋯⟩) ((fun f ↦ (Units.coeHom G).comp (cs.groupLift ⋯)) f) = f

Tactic:
by

Goal state after: