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

Goal state before:
pp: case hσσ'
𝕜 : 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
F' : Type u_7
inst✝¹⁸ : NormedAddCommGroup F'
inst✝¹⁷ : NormedSpace 𝕜 F'
V' : M → Type u_8
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'
A : Type u_9
inst✝¹¹ : AddCommGroup A
inst✝¹⁰ : Module 𝕜 A
Φ✝ : ((x : M) → V x) → A
x✝ : M
inst✝⁹ : VectorBundle 𝕜 F V
inst✝⁸ : VectorBundle 𝕜 F' V'
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : FiniteDimensional 𝕜 F
inst✝⁵ : FiniteDimensional 𝕜 F'
inst✝⁴ : ContMDiffVectorBundle 1 F V I
inst✝³ : ContMDiffVectorBundle 1 F' V' I
inst✝² : TopologicalSpace A
inst✝¹ : IsTopologicalAddGroup A
inst✝ : ContinuousSMul 𝕜 A
Φ : ((x : M) → V x) → ((x : M) → V' x) → A
x : M
hΦ₁ : ∀ (τ : (x : M) → V' x), MDiffAt (T% τ) x → TensorialAt I F (fun x ↦ Φ x τ) x
hΦ₂ : ∀ (σ : (x : M) → V x), MDiffAt (T% σ) x → TensorialAt I F' (Φ σ) x
this✝⁶ : T2Space (V x)
this✝⁵ : FiniteDimensional 𝕜 (V x)
this✝⁴ : T2Space (V' x)
this✝³ : FiniteDimensional 𝕜 (V' x)
this✝² : IsTopologicalAddGroup (V x)
this✝¹ : IsTopologicalAddGroup (V' x)
this✝ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
this : ∀ (x : M), ContinuousSMul 𝕜 (V' x)
v : V x
w₁ w₂ : V' x
⊢ extend F v x = extend F v x

Tactic:
rfl

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

Goal state before:
pp: case hσσ'
𝕜 : 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
F' : Type u_7
inst✝¹⁸ : NormedAddCommGroup F'
inst✝¹⁷ : NormedSpace 𝕜 F'
V' : M → Type u_8
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'
A : Type u_9
inst✝¹¹ : AddCommGroup A
inst✝¹⁰ : Module 𝕜 A
Φ✝ : ((x : M) → V x) → A
x✝ : M
inst✝⁹ : VectorBundle 𝕜 F V
inst✝⁸ : VectorBundle 𝕜 F' V'
inst✝⁷ : CompleteSpace 𝕜
inst✝⁶ : FiniteDimensional 𝕜 F
inst✝⁵ : FiniteDimensional 𝕜 F'
inst✝⁴ : ContMDiffVectorBundle 1 F V I
inst✝³ : ContMDiffVectorBundle 1 F' V' I
inst✝² : TopologicalSpace A
inst✝¹ : IsTopologicalAddGroup A
inst✝ : ContinuousSMul 𝕜 A
Φ : ((x : M) → V x) → ((x : M) → V' x) → A
x : M
hΦ₁ : ∀ (τ : (x : M) → V' x), MDiffAt (T% τ) x → TensorialAt I F (fun x ↦ Φ x τ) x
hΦ₂ : ∀ (σ : (x : M) → V x), MDiffAt (T% σ) x → TensorialAt I F' (Φ σ) x
this✝⁶ : T2Space (V x)
this✝⁵ : FiniteDimensional 𝕜 (V x)
this✝⁴ : T2Space (V' x)
this✝³ : FiniteDimensional 𝕜 (V' x)
this✝² : IsTopologicalAddGroup (V x)
this✝¹ : IsTopologicalAddGroup (V' x)
this✝ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
this : ∀ (x : M), ContinuousSMul 𝕜 (V' x)
c : 𝕜
v : V x
w : V' x
⊢ extend F v x = extend F v x

Tactic:
rfl

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric

Goal state before:
pp: E : Type u_1
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
H : Type u_2
inst✝⁸ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝⁷ : TopologicalSpace M
inst✝⁶ : ChartedSpace H M
F : Type u_4
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
V : M → Type u_5
inst✝³ : TopologicalSpace (TotalSpace F V)
inst✝² : (x : M) → NormedAddCommGroup (V x)
inst✝¹ : (x : M) → InnerProductSpace ℝ (V x)
inst✝ : FiberBundle F V
cov : CovariantDerivative I F V
σ τ : (x : M) → V x
x : M
X₀ : TangentSpace I x
⊢ (derivMetricTensorAux I cov σ τ x) X₀ =
    ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) X₀ - inner ℝ (τ x) ((↑cov σ x) X₀) - inner ℝ (σ x) ((↑cov τ x) X₀)

Tactic:
rfl

Goal state after:
Module: Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic

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✝⁶ : ∀ (x : M), IsTopologicalAddGroup (V x)
inst✝⁵ : ∀ (x : M), ContinuousSMul 𝕜 (V x)
inst✝⁴ : FiberBundle F V
cov cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x
s : Set M
hcov : IsCovariantDerivativeOn F cov s
hcov' : IsCovariantDerivativeOn F cov' s
inst✝³ : CompleteSpace 𝕜
inst✝² : FiniteDimensional 𝕜 F
inst✝¹ : VectorBundle 𝕜 F V
inst✝ : ContMDiffVectorBundle 1 F V I
x : M
hx : x ∈ s
σ : (x : M) → V x
hσ : MDiffAt (T% σ) x
⊢ differenceAux cov cov' σ x = cov σ x - cov' σ x

Tactic:
rfl

Goal state after:
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
poly : Polygon P 3
h : HasNondegenerateVertices R poly
⊢ Affine.Triangle.toPolygon (toTriangle R poly h) = poly

Tactic:
rfl

Goal state after:
Module: Mathlib.Geometry.Polygon.Basic

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AffineSpace V P
t : Triangle R P
⊢ Polygon.toTriangle R (toPolygon t) ⋯ = t

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.ClassEquation

Goal state before:
pp: case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card ↥(Subgroup.center G) = ∑ x ∈ Finset.univ \ (noncenter G).toFinset, Fintype.card ↑x.carrier

Tactic:
calc
    Fintype.card (Subgroup.center G) = Fintype.card ((noncenter G)ᶜ : Set _) :=
      Fintype.card_congr ((mk_bijOn G).equiv _)
    _ = Finset.card (Finset.univ \ (noncenter G).toFinset) := by
      rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]
    _ = _ := ?_

Goal state after:
case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ (Finset.univ \ (noncenter G).toFinset).card = ∑ x ∈ Finset.univ \ (noncenter G).toFinset, Fintype.card ↑x.carrier
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
⊢ δ * C * ((g x) (G.symm w)) (G.symm w) + ((g' y) w) w =
    δ * C * ((g x) ((trivializationAt F E x).symm x w)) ((trivializationAt F E x).symm x w) + ((g' y) w) w

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case r
n : ℕ
x : ZMod n
⊢ (fun x ↦
        match x with
        | Sum.inl j => r j
        | Sum.inr j => sr j)
      ((fun x ↦
          match x with
          | r j => Sum.inl j
          | sr j => Sum.inr j)
        (r x)) =
    r x

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case sr
n : ℕ
x : ZMod n
⊢ (fun x ↦
        match x with
        | Sum.inl j => r j
        | Sum.inr j => sr j)
      ((fun x ↦
          match x with
          | r j => Sum.inl j
          | sr j => Sum.inr j)
        (sr x)) =
    sr x

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inl
n : ℕ
x : ZMod n
⊢ (fun x ↦
        match x with
        | r j => Sum.inl j
        | sr j => Sum.inr j)
      ((fun x ↦
          match x with
          | Sum.inl j => r j
          | Sum.inr j => sr j)
        (Sum.inl x)) =
    Sum.inl x

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: case inr
n : ℕ
x : ZMod n
⊢ (fun x ↦
        match x with
        | r j => Sum.inl j
        | sr j => Sum.inr j)
      ((fun x ↦
          match x with
          | Sum.inl j => r j
          | Sum.inr j => sr j)
        (Sum.inr x)) =
    Sum.inr x

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ Fintype.card (DihedralGroup n) = 2 * n

Tactic:
rw [← Fintype.card_eq.mpr ⟨equivSum.symm⟩, Fintype.card_sum, ZMod.card, two_mul]

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: α : Type u_2
i : α → Type u_3
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) / ↑(Nat.card ((a : α) → i a)) ^ 2 =
    ∏ a, ↑(Nat.card { p // Commute p.1 p.2 }) / ↑(Nat.card (i a)) ^ 2

Tactic:
Finset.prod_div_distrib,

Goal state after:
α : Type u_2
i : α → Type u_3
inst✝¹ : Fintype α
inst✝ : (a : α) → Mul (i a)
⊢ ↑(Nat.card { p // Commute p.1 p.2 }) / ↑(Nat.card ((a : α) → i a)) ^ 2 =
    (∏ x, ↑(Nat.card { p // Commute p.1 p.2 })) / ∏ x, ↑(Nat.card (i x)) ^ 2
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
hn : Odd n
⊢ (↑n + 3) / 2 / (2 * ↑n) = (↑n + 3) / (4 * ↑n)

Tactic:
rw [div_div, ← mul_assoc]

Goal state after:
n : ℕ
hn : Odd n
⊢ (↑n + 3) / (2 * 2 * ↑n) = (↑n + 3) / (4 * ↑n)
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: ⊢ (if x : 0 = 0 then [0]
    else
      if x : 0 = 1 then []
      else if Even 0 then 3 :: reciprocalFactors (0 / 2) else 0 % 4 * 0 :: reciprocalFactors (0 / 4 + 1)) =
    [0]

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: ⊢ (if x : 1 = 0 then [0]
    else
      if x : 1 = 1 then []
      else if Even 1 then 3 :: reciprocalFactors (1 / 2) else 1 % 4 * 1 :: reciprocalFactors (1 / 4 + 1)) =
    []

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Dihedral

Goal state before:
pp: n : ℕ
hodd : Odd n
hne1 : n ≠ 1
i : ZMod n
h : ∀ (g : DihedralGroup n), g * sr i = sr i * g
heq : i - 1 = i + 1
⊢ 1 < n

Tactic:
grind

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Odd n
⊢ Odd (n % 4)

Tactic:
grind

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

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

Tactic:
ofRepr.injEq,

Goal state after:
ι : Type u_1
ι' : Type u_2
G : Type u_3
H✝ : Type u_4
inst✝¹ : Group G
inst✝ : Group H✝
b b' : G ≃* FreeGroup ι
hbb' : (fun b i ↦ b.repr.symm (FreeGroup.of i)) { repr := b } = (fun b i ↦ b.repr.symm (FreeGroup.of i)) { repr := b' }
H : ↑b.symm = ↑b'.symm
this : b.symm = b'.symm
⊢ b = b'
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) =
    Submonoid.closure (Set.range ((⇑mk ∘ of) ∘ Sum.inl) ∪ Set.range ((⇑mk ∘ of) ∘ Sum.inr))

Tactic:
rfl

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

Goal state before:
pp: case h₁
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ (fst.prod snd).comp inl = toProd.comp inl

Tactic:
rfl

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

Goal state before:
pp: case h₂
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ (fst.prod snd).comp inr = toProd.comp inr

Tactic:
rfl

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 = ((MonoidHom.fst M N).comp toProd) x

Tactic:
rfl

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 = ((MonoidHom.snd M N).comp toProd) x

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.PresentedGroup

Goal state before:
pp: case mk.mul
α : Type u_1
rels : Set (FreeGroup α)
H : Subgroup (PresentedGroup rels)
h : ∀ (j : α), of j ∈ H
x : PresentedGroup rels
x✝ y✝ : FreeGroup α
h1 : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) x✝ ∈ H
h2 : Quot.mk (⇑(QuotientGroup.leftRel (Subgroup.normalClosure rels))) y✝ ∈ H
⊢ ↑x✝ * ↑y✝ ∈ H.carrier

Tactic:
exact Subgroup.mul_mem _ h1 h2

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
this : Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹
⊢ (Subgroup.closure (Set.range cs.simple)).toSubmonoid = ⊤

Tactic:
subgroup_closure_range_simple,

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
this : Set.range cs.simple = Set.range cs.simple ∪ (Set.range cs.simple)⁻¹
⊢ ⊤.toSubmonoid = ⊤
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
i : ι
x : M i
⊢ ((fun f x ↦ f.comp of) ((fun fi ↦ (conGen (Rel M)).lift (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd) ⋯) fi) i) x =
    (fi i) x

Tactic:
rfl

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 : CoprodI M →* N
i : ι
x : M i
⊢ (((fun fi ↦ (conGen (Rel M)).lift (FreeMonoid.lift fun p ↦ (fi p.fst) p.snd) ⋯) ((fun f x ↦ f.comp of) f)).comp of)
      x =
    (f.comp of) x

Tactic:
rfl

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

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case inr
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i : ι
m : M i
w : Word M
hmw : w.fstIdx ≠ some i
h1 : m ≠ 1
l : (i : ι) × M i
hl : l ∈ w.toList
⊢ l.snd ≠ 1

Tactic:
exact w.ne_one l hl

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

Goal state before:
pp: case zero
B : Type u_1
i j : B
⊢ ∀ (k : ℕ) (hk : k < 0), (alternatingWord i j 0)[k] = if Even (0 + k) then i else j

Tactic:
grind

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
p : Pair M i
m : M j
⊢ ⟨j, m⟩ ∈
      (if h : p.head = 1 then p.tail
        else { toList := ⟨i, p.head⟩ :: p.tail.toList, ne_one := ⋯, chain_ne := ⋯ }).toList ↔
    ⟨j, m⟩ ∈ p.tail.toList ∨ ¬m = 1 ∧ ∃ (h : i = j), m = h ▸ p.head

Tactic:
grind

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos.mpr.inl
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
w : Word M
hnil : ¬w.toList = []
m₂ : M (w.toList.head hnil).fst
hw : ⟨(w.toList.head hnil).fst, m₂ * (w.toList.head hnil).snd⟩ ∉ w.toList.tail
hm1 : ¬m₂ * (w.toList.head hnil).snd = 1
⊢ m₂ * (w.toList.head hnil).snd = m₂ * (w.toList.head ⋯).snd

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * ↑f.range = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h (f x)
inst✝ : Northcott h
q : G → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : (↑U)ᶜ.Nonempty
⊢ False

Tactic:
obtain ⟨x, hx₁, hx₂⟩ := Northcott.exists_min_image h Uᶜ H

Goal state after:
G : Type u_1
inst✝¹ : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * ↑f.range = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h (f x)
inst✝ : Northcott h
q : G → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : (↑U)ᶜ.Nonempty
x : G
hx₁ : x ∈ (↑U)ᶜ
hx₂ : ∀ a' ∈ (↑U)ᶜ, h x ≤ h a'
⊢ False
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
⊢ (singleton x✝ a✝).toList.getLast? = some ⟨i✝, (singleton x✝ a✝).last⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * ↑f.range = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h (f x)
inst✝ : Northcott h
q : G → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : (↑U)ᶜ.Nonempty
g : G
hg : g ∈ s
y : G
hx₁ : g * f y ∈ (↑U)ᶜ
hx₂ : ∀ a' ∈ (↑U)ᶜ, h (g * f y) ≤ h a'
this : 2 * c < (b - a) * h (g * f y)
⊢ a * h (g * f y) + 2 * c < b * h (g * f y)

Tactic:
grind

Goal state after:
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
f : G →* G
hf : ∀ (U : Subgroup G), map f U ≤ U
s : Set G
h : G → ℝ
a b c : ℝ
ha : 0 ≤ a
H₀ : a < b
hs : s.Finite
H₁ : s * ↑f.range = Set.univ
H₂ : ∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c
H₃ : ∀ (x : G), b * h x - c ≤ h (f x)
inst✝ : Northcott h
q : G → G ⧸ map f ⊤ := QuotientGroup.mk
S : Set G := s ∪ {x | h x ≤ 2 * c / (b - a)}
U : Subgroup G := closure S
H : (↑U)ᶜ.Nonempty
g : G
hg : g ∈ s
y : G
hx₁ : g * f y ∈ (↑U)ᶜ
hx₂ : ∀ a' ∈ (↑U)ᶜ, h (g * f y) ≤ h a'
this : g * f y ∉ S
⊢ 2 * c / (b - a) < h (g * f y)

Tactic:
grind

Goal state after:
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : CommGroup G
n : ℕ
h : G → ℝ
a b c₀ : ℝ
c : G → ℝ
ha : 0 ≤ a
H₀ : a < b
H₁ : (powMonoidHom n).range.FiniteIndex
H₂ : ∀ (g x : G), h x ≤ a * h (g * x) + c g
H₃ : ∀ (x : G), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
f : G →* G := powMonoidHom n
q : G → G ⧸ f.range := QuotientGroup.mk
qi : G ⧸ f.range → G := Function.surjInv ⋯
s : Set G := Set.range qi
g : G
hg₁ : g ∈ s
hg₂ : ∀ b ∈ s, c b ≤ c g
H₁' : s * ↑f.range = Set.univ
c' : ℝ := max c₀ (c g)
H₃' : ∀ (x : G), b * h x - c' ≤ h (f x)
g' : G
hg' : g' ∈ s
x : G
⊢ h x ≤ a * h (g' * x) + c'

Tactic:
grind

Goal state after:
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
n : ℕ
h : M → ℝ
b c₀ : ℝ
hb : 1 < b
H : ∀ (x : M), b * h x - c₀ ≤ h (x ^ n)
inst✝ : Northcott h
t : M
ht : t ∈ {x | IsOfFinOrder x}
this : Finite ↥(Submonoid.powers t)
C : ℝ := ⨆ g, h ↑g
hC : ∀ g ∈ Submonoid.powers t, h g ≤ C
t₀ : ↥(Submonoid.powers t)
ht₀ : h ↑t₀ = C
⊢ 0 < b - 1

Tactic:
grind

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case singleton
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ : ι
x✝ : M i✝
a✝ : x✝ ≠ 1
x : M i✝
hnotone : x ≠ 1
⊢ (replaceHead x hnotone (singleton x✝ a✝)).head = x

Tactic:
rfl

Goal state after: