mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝⁴ : VectorBundle ℝ F V
inst✝³ : IsContMDiffRiemannianBundle I 1 F V
inst✝² : ContMDiffVectorBundle 1 F V I
inst✝¹ : IsManifold I 1 M
inst✝ : FiniteDimensional ℝ F
h :
  ∀ {x : M} {X : (x : M) → TangentSpace I x} {σ τ : (x : M) → V x},
    MDiffAt (T% X) x →
      MDiffAt (T% σ) x →
        MDiffAt (T% τ) x →
          ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) =
            (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x +
              (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x
x : M
σ : (x : M) → V x
hσ : MDiffAt (T% σ) x
⊢ (fun A Z x_1 ↦ A (Z x)) (cov.derivMetricTensor x) σ hσ = (fun A Z x_1 ↦ A (Z x)) (0 x) σ hσ

Tactic:
apply VectorBundle.injective_eval_mdifferentiableAt_sec I F

Goal state after:
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
inst✝⁴ : VectorBundle ℝ F V
inst✝³ : IsContMDiffRiemannianBundle I 1 F V
inst✝² : ContMDiffVectorBundle 1 F V I
inst✝¹ : IsManifold I 1 M
inst✝ : FiniteDimensional ℝ F
h :
  ∀ {x : M} {X : (x : M) → TangentSpace I x} {σ τ : (x : M) → V x},
    MDiffAt (T% X) x →
      MDiffAt (T% σ) x →
        MDiffAt (T% τ) x →
          ((d% fun x ↦ inner ℝ (σ x) (τ x)) x) (X x) =
            (fun x ↦ inner ℝ ((fun x ↦ (↑cov σ x) (X x)) x) (τ x)) x +
              (fun x ↦ inner ℝ (σ x) ((fun x ↦ (↑cov τ x) (X x)) x)) x
x : M
σ : (x : M) → V x
hσ : MDiffAt (T% σ) x
⊢ (fun A Z x_1 ↦ A (Z x)) ((fun A Z x_1 ↦ A (Z x)) (cov.derivMetricTensor x) σ hσ) =
    (fun A Z x_1 ↦ A (Z x)) ((fun A Z x_1 ↦ A (Z x)) (0 x) σ hσ)
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)
X Y : (x : M) → TangentSpace I x
x : M
hX : MDiffAt (T% X) x
hY : MDiffAt (T% Y) x
h : (↑cov Y x) (X x) - (↑cov X x) (Y x) - mlieBracket I X Y x = ((0 x) (X x)) (Y x)
⊢ (↑cov Y x) (X x) - (↑cov X x) (Y x) = mlieBracket I X Y x

Tactic:
simpa [sub_eq_iff_eq_add'] using h

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 : (1 - δ * C) * ((g' x) w) w ≤ ((g' y) w) w
⊢ 0 ≤ (r' ^ 2)⁻¹

Tactic:
by positivity

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
⊢ (x.1, 1) * toProd (inr x.2) = x

Tactic:
toProd_apply_inr,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
x : M × N
⊢ (x.1, 1) * (1, x.2) = x
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 positivity

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 positivity

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
⊢ cs.wordProd [] = 1

Tactic:
simp [wordProd]

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
ω : List B
⊢ cs.wordProd (i :: ω) = cs.simple i * cs.wordProd ω

Tactic:
simp [wordProd]

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.wordProd [i] = cs.simple i

Tactic:
simp [wordProd]

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
ω : List B
⊢ cs.wordProd (ω.concat i) = cs.wordProd ω * cs.simple i

Tactic:
simp [wordProd]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case inl
ι : 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
⊢ ⟨i, m⟩.snd ≠ 1

Tactic:
exact h1

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
ω ω' : List B
⊢ cs.wordProd (ω ++ ω') = cs.wordProd ω * cs.wordProd ω'

Tactic:
simp [wordProd]

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
i j : B
p k : ℕ
h : k + 1 < p
⊢ k < (alternatingWord j i p).length

Tactic:
by simp; lia

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

Goal state before:
pp: B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ k < (alternatingWord i j (2 * p)).length

Tactic:
by simp; lia

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

Goal state before:
pp: B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord i j k
⊢ Even (2 * p + k)

Tactic:
apply Nat.even_add.mpr; simp [h_even]

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

Goal state before:
pp: B : Type u_1
i j : B
p k : ℕ
h' : k < 2 * p → take k (alternatingWord i j (2 * p)) = if Even k then alternatingWord i j k else alternatingWord j i k
h : k + 1 < 2 * p
h_even : ¬Even k
hk : take k (alternatingWord i j (2 * p)) = alternatingWord j i k
⊢ k < (alternatingWord i j (2 * p)).length

Tactic:
by simp; lia

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

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
⊢ t⁻¹ = t

Tactic:
rcases ht with ⟨w, i, rfl⟩
  simp [mul_assoc]

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

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.length (w * t) ≠ cs.length w

Tactic:
suffices cs.lengthParity (w * t) ≠ cs.lengthParity w by
    contrapose this
    simp only [lengthParity_eq_ofAdd_length, this]
  rcases ht with ⟨w, i, rfl⟩
  simp [lengthParity_simple]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case neg
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : ⟨j, m₁⟩ ∉ w.toList.tail
hm1 : ¬m₁ = 1
⊢ (¬∃ (h : ¬w.toList = []), (w.toList.head h).fst = j) →
    (m₁ = m₂ * 1 ↔ (∃ m', w.toList.head? = some ⟨j, m'⟩ ∧ m₁ = m₂ * m') ∨ ¬w.fstIdx = some j ∧ m₁ = m₂)

Tactic:
fstIdx

Goal state after:
case neg
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
j : ι
m₂ : M j
w : Word M
m₁ : M j
hw : ⟨j, m₁⟩ ∉ w.toList.tail
hm1 : ¬m₁ = 1
⊢ (¬∃ (h : ¬w.toList = []), (w.toList.head h).fst = j) →
    (m₁ = m₂ * 1 ↔
      (∃ m', w.toList.head? = some ⟨j, m'⟩ ∧ m₁ = m₂ * m') ∨ ¬Option.map Sigma.fst w.toList.head? = some j ∧ m₁ = m₂)
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ cs.IsRightInversion (w⁻¹ * t) t ↔ ¬cs.IsRightInversion w⁻¹ t

Tactic:
ht.isRightInversion_mul_left_iff

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
ht : cs.IsReflection t
w : W
⊢ ¬cs.IsRightInversion w⁻¹ t ↔ ¬cs.IsRightInversion w⁻¹ t
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
ls : Word M
h1 : ls.fstIdx ≠ some i
h2 : m ≠ 1
⊢ ls.fstIdx ≠ some i

Tactic:
exact h1

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

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

Tactic:
by
  induction w
  · rfl
  · simp [*, replaceHead]

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

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

Tactic:
by simp; lia

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

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

Tactic:
by simp; lia

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

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k < (cs.leftInvSeq (alternatingWord j i (2 * p))).length

Tactic:
by simp; lia

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

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k + 1 < 2 * p
⊢ k < (alternatingWord j i (2 * p)).length

Tactic:
by simp; lia

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

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i j : B
p k : ℕ
h : k < 2 * p
⊢ k < (cs.leftInvSeq (alternatingWord i j (2 * p))).length

Tactic:
by simp; lia

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

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

Tactic:
rw [← out_eq' _ _ i] at hg

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
i : Quotient ↑H ↑K
a : G
hg : mk H K a = mk H K (Quotient.out i)
⊢ a ∈ quotToDoubleCoset H K i
Module: Mathlib.GroupTheory.DoubleCoset

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

Tactic:
contrapose
  intro h
  simpa [out_eq'] using mk_eq_of_doubleCoset_eq (eq_of_not_disjoint h)

Goal state after:
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
⊢ ⋃ i ∈ t, Quot.mk ⇑(rightRel H) '' doubleCoset (out i) ↑H ↑K ≠ Set.univ

Tactic:
refine (Set.ne_univ_iff_exists_notMem _).mpr ⟨Quot.mk (rightRel H) x, ?_⟩

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
⊢ Quot.mk (⇑(rightRel H)) x ∉ ⋃ i ∈ t, Quot.mk ⇑(rightRel H) '' doubleCoset (out i) ↑H ↑K
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
H : ∀ (n : ℕ), n ∣ Monoid.exponent G → ∀ (a : ZMod n), a ≠ 0 → ∃ φ, φ (Multiplicative.ofAdd a) ≠ 1
a : G
ha : a ≠ 1
⊢ ∃ φ, φ a ≠ 1

Tactic:
by
  obtain ⟨ι, _, n, _, h⟩ := CommGroup.equiv_prod_multiplicative_zmod_of_finite G
  let e := h.some
  obtain ⟨i, hi⟩ : ∃ i : ι, e a i ≠ 1 := by
    contrapose! ha
    exact (MulEquiv.map_eq_one_iff e).mp <| funext ha
  obtain ⟨φi, hφi⟩ := H (n i) (dvd_exponent e i) ((e a i).toAdd) hi
  use (φi.comp (Pi.evalMonoidHom (fun (i : ι) ↦ Multiplicative (ZMod (n i))) i)).comp e
  simpa only [coe_comp, coe_coe, Function.comp_apply, Pi.evalMonoidHom_apply, ne_eq] using! hφi

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'δ : 1 + δ * C < r' ^ 2
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' y - g' x‖ ≤ δ
v : E x
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x) v
this : ‖(Trivialization.symmL ℝ (trivializationAt F E x) y) w‖ ^ 2 ≤ r' ^ 2 * ‖v‖ ^ 2
⊢ 0 ≤ r' * ‖v‖

Tactic:
by positivity

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case hpp
ι : 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
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i

Tactic:
rcases (lt_or_gt_of_ne hnne0).symm with hlt | hgt

Goal state after:
case hpp.inl
ι : 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
hlt : 0 < n
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i

case hpp.inr
ι : 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
⊢ a i ^ n • (X j ∪ Y j) ⊆ X i ∪ Y i
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 := 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
hlt : 0 < n
h1n : 1 ≤ n
⊢ a i ^ n • (Y i)ᶜ ⊆ X i

Tactic:
clear hnne0 hlt

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 : ℤ
h1n : 1 ≤ n
⊢ a i ^ n • (Y i)ᶜ ⊆ X i
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg.inl
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : k = 0
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime (Nat.card (MulAut ↥↑P))

pp: case neg.inr
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime (Nat.card (MulAut ↥↑P))

Tactic:
· rw [hP.card_mulAut, hk, h0, pow_zero, Nat.totient_one]
    apply Nat.coprime_one_right

Goal state after:
case neg.inr
G : Type u_3
inst✝¹ : Group G
inst✝ : Finite G
P : Sylow (Nat.card G).minFac G
hP : IsCyclic ↥↑P
hn : ¬Nat.card G = 1
this : Fact (Nat.Prime (Nat.card G).minFac)
key : (centralizer ↑↑P).relIndex (normalizer ↑↑P) ∣ Nat.card (MulAut ↥↑P)
k : ℕ
hk : Nat.card ↥↑P = (Nat.card G).minFac ^ k
h0 : 0 < k
⊢ ((centralizer ↑P).relIndex (normalizer ↑P)).Coprime (Nat.card (MulAut ↥↑P))
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Characteristic
d : ℕ
a✝ : (S.lowerCentralSeries d).Characteristic
⊢ (S.lowerCentralSeries (d + 1)).Characteristic

Tactic:
| succ d _ =>

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
⊢ ⊥ = ⊤ ↔ Subsingleton G

Tactic:
subsingleton_iff_bot_eq_top,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : IsNilpotent G
⊢ Subsingleton (Subgroup G) ↔ Subsingleton G
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: η : Type u_2
Gs : η → Type u_3
inst✝² : (i : η) → Group (Gs i)
inst✝¹ : Fintype η
inst✝ : ∀ (i : η), IsNilpotent (Gs i)
k : ℕ
⊢ nilpotencyClass ((i : η) → Gs i) ≤ k ↔ (Finset.univ.sup fun i ↦ nilpotencyClass (Gs i)) ≤ k

Tactic:
simp only [Finset.sup_le_iff, ← lowerCentralSeries_eq_bot_iff_nilpotencyClass_le,
    top_lowerCentralSeries_pi_of_finite, pi_eq_bot_iff, Finset.mem_univ, true_imp_iff]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsCoatom (stabilizer G a) ↔ IsPreprimitive G X

Tactic:
rw [← isSimpleOrder_blockMem_iff_isPreprimitive G a, ← Set.isSimpleOrder_Ici_iff_isCoatom]
  simp only [isSimpleOrder_iff_isCoatom_bot]
  rw [← OrderIso.isCoatom_iff (block_stabilizerOrderIso G a), OrderIso.map_bot]

Goal state after: