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

Goal state before:
pp: case e'_10
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurve (γ ∘ fun x ↦ x * a) (a • v)
⊢ γ = (γ ∘ fun x ↦ x * a) ∘ fun x ↦ x * a⁻¹

pp: case e'_11
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurve (γ ∘ fun x ↦ x * a) (a • v)
⊢ v = a⁻¹ • a • v

Tactic:
· ext t
    simp only [Function.comp_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one]

Goal state after:
case e'_11
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
γ : ℝ → M
v : (x : M) → TangentSpace I x
a : ℝ
ha : a ≠ 0
hγ : IsMIntegralCurve (γ ∘ fun x ↦ x * a) (a • v)
⊢ v = a⁻¹ • a • v
Module: Mathlib.Geometry.Manifold.IntegralCurve.UniformTime

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
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
x : M
⊢ (∃ γ, γ 0 = x ∧ IsMIntegralCurve γ v) ↔ ∀ (a : ℝ), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)

Tactic:
refine ⟨fun ⟨γ, h1, h2⟩ _ ↦ ⟨γ, h1, h2.isMIntegralCurveOn _⟩, fun h ↦ ?_⟩

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
inst✝² : IsManifold I 1 M
inst✝¹ : T2Space M
v : (x : M) → TangentSpace I x
inst✝ : BoundarylessManifold I M
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
x : M
h : ∀ (a : ℝ), ∃ γ, γ 0 = x ∧ IsMIntegralCurveOn γ v (Ioo (-a) a)
⊢ ∃ γ, γ 0 = x ∧ IsMIntegralCurve γ v
Module: Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique

Goal state before:
pp: case refine_2
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
inst✝² : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
⊢ Periodic γ |a - b|

Tactic:
by_cases! hab : a - b < 0

Goal state after:
case pos
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
inst✝² : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
hab : a - b < 0
⊢ Periodic γ |a - b|

case neg
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
inst✝² : IsManifold I 1 M
γ : ℝ → M
v : (x : M) → TangentSpace I x
inst✝¹ : T2Space M
inst✝ : BoundarylessManifold I M
hγ : IsMIntegralCurve γ v
hv : ContMDiff I I.tangent 1 fun x ↦ ⟨x, v x⟩
a b : ℝ
heq : γ a = γ b
hne : a ≠ b
hab : 0 ≤ a - b
⊢ Periodic γ |a - b|
Module: Mathlib.Geometry.Manifold.VectorField.LieBracket

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹³ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝¹² : TopologicalSpace H
E : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁹ : TopologicalSpace M
inst✝⁸ : ChartedSpace H M
H' : Type u_5
inst✝⁷ : TopologicalSpace H'
E' : Type u_6
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝⁴ : TopologicalSpace M'
inst✝³ : ChartedSpace H' M'
inst✝² : IsManifold I 2 M
inst✝¹ : IsManifold I' 2 M'
inst✝ : CompleteSpace E
f : M → M'
V W : (x : M') → TangentSpace I' x
x₀ : M
s : Set M
t : Set M'
hV : MDiffAt[t] (T% V) (f x₀)
hW : MDiffAt[t] (T% W) (f x₀)
hu : UniqueMDiff[s]
hf : ContMDiffWithinAt I I' 2 f s x₀
hx₀ : x₀ ∈ s
hst : f ⁻¹' t ∈ 𝓝[s] x₀
hsymm :
  IsSymmSndFDerivWithinAt 𝕜 (↑(extChartAt I' (f x₀)) ∘ f ∘ ↑(extChartAt I x₀).symm)
    (↑(extChartAt I x₀).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x₀) x₀)
A : ↑(extChartAt I x₀).symm (↑(extChartAt I x₀) x₀) = x₀
hfi : (mfderiv[s] f x₀).IsInvertible
this : CompleteSpace E'
⊢ ∃ u,
    IsOpen[inst✝⁹] u ∧
      x₀ ∈ u ∧ s ∩ u ⊆ f ⁻¹' t ∧ s ∩ u ⊆ f ⁻¹' (extChartAt I' (f x₀)).source ∧ ContMDiffOn I I' 2 f (s ∩ u)

Tactic:
obtain ⟨u, u_open, x₀u, hu⟩ : ∃ u, IsOpen u ∧ x₀ ∈ u ∧ CMDiff[insert x₀ s ∩ u] 2 f :=
      hf.contMDiffOn' le_rfl (by simp)
    have : f ⁻¹' (extChartAt I' (f x₀)).source ∈ 𝓝[s] x₀ :=
      hf.continuousWithinAt.preimage_mem_nhdsWithin (extChartAt_source_mem_nhds (f x₀))
    rcases mem_nhdsWithin.1 (Filter.inter_mem hst this) with ⟨w, w_open, x₀w, hw⟩
    refine ⟨u ∩ w, u_open.inter w_open, by simp [x₀u, x₀w], ?_, ?_, ?_⟩
    · apply Subset.trans _ (hw.trans inter_subset_left)
      exact fun y hy ↦ ⟨hy.2.2, hy.1⟩
    · apply Subset.trans _ (hw.trans inter_subset_right)
      exact fun y hy ↦ ⟨hy.2.2, hy.1⟩
    · apply hu.mono
      exact fun y hy ↦ ⟨subset_insert _ _ hy.1, hy.2.1⟩

Goal state after:
Module: Mathlib.Geometry.Manifold.Riemannian.PathELength

Goal state before:
pp: case refine_1.st
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
inst✝¹ : (x : M) → ENorm (TangentSpace I x)
inst✝ : ∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)
x y : M
r : ℝ≥0∞
a b : ℝ
hr : riemannianEDist I x y < r
hab : a < b
γ : ℝ → M
hγx : γ 0 = x
hγy : γ 1 = y
γ_smooth : ContMDiffOn 𝓘(ℝ, ℝ) I 1 γ (Icc 0 1)
hγ : pathELength I γ 0 1 < r
a' : ℝ
haa' : a < a'
ha'b : a' < b
b' : ℝ
ha'b' : a' < b'
hb'b : b' < b
η : ℝ → ℝ := ⋯
A : ∀ t < a', η t = 0
A' : ∀ t < a', (γ ∘ η) t = x
B : ∀ (t : ℝ), b' < t → η t = 1
B' : ∀ (t : ℝ), b' < t → (γ ∘ η) t = y
⊢ univ ⊆ η ⁻¹' Icc 0 1

Tactic:
· intro t ht
      exact ⟨Real.smoothTransition.nonneg _, Real.smoothTransition.le_one _⟩

Goal state after:
Module: Mathlib.GroupTheory.Commutator.Finite

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank ↥(closureCommutatorRepresentatives G) ≤ 2 * Nat.card ↑(commutatorSet G)

Tactic:
rw [two_mul]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
⊢ Group.rank ↥(closureCommutatorRepresentatives G) ≤ Nat.card ↑(commutatorSet G) + Nat.card ↑(commutatorSet G)
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 α β)
⊢ Fintype.card α / Fintype.card ↥(stabilizer α (φ ω)) = Fintype.card (α ⧸ stabilizer α (φ ω))

Tactic:
rw [Fintype.card_congr (@Subgroup.groupEquivQuotientProdSubgroup α _ (stabilizer α <| φ ω)),
        Fintype.card_prod, Nat.mul_div_cancel]

Goal state after:
case H
α : 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 α β)
⊢ 0 < Fintype.card ↥(stabilizer α (φ ω))
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case h
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
H : Subgroup G
inst✝ : H.Normal
⊢ ↑(Nat.card G) ≠ 0

Tactic:
exact Nat.cast_ne_zero.mpr Finite.card_pos.ne'

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
h0 : n ≠ 0
h2 : Even n
⊢ reciprocalFactors n = 3 :: reciprocalFactors (n / 2)

Tactic:
have h1 : n ≠ 1 := by
    rintro rfl
    norm_num at h2

Goal state after:
n : ℕ
h0 : n ≠ 0
h2 : Even n
h1 : n ≠ 1
⊢ reciprocalFactors n = 3 :: reciprocalFactors (n / 2)
Module: Mathlib.GroupTheory.Coxeter.Basic

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

pp: case neg
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
h_even : ¬Even k
⊢ (if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)) =
    i :: if Even k then alternatingWord j i k else alternatingWord i j k

Tactic:
· simp [Nat.not_even_iff_odd.mpr (Even.add_one h_even), alternatingWord_succ', h_even]

Goal state after:
case neg
B : Type u_1
i j : B
p k : ℕ
h : k + 1 < 2 * p
h_even : ¬Even k
⊢ (if Even (k + 1) then alternatingWord i j (k + 1) else alternatingWord j i (k + 1)) =
    i :: if Even k then alternatingWord j i k else alternatingWord i j k
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
⊢ (∃ i, w = cs.simple i) → cs.length w = 1

Tactic:
· rintro ⟨i, rfl⟩
    exact cs.length_simple i

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

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
eq : cs.length (w * cs.simple i) = cs.length w
⊢ False

Tactic:
have length_mod_two := cs.length_mul_mod_two w (s i)

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

Tactic:
by
  simp [leftInvSeq_eq_reverse_rightInvSeq_reverse]

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
⊢ cs.leftInvSeq ω.reverse = (cs.rightInvSeq ω).reverse

Tactic:
by
  simp [leftInvSeq_eq_reverse_rightInvSeq_reverse]

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
⊢ (cs.leftInvSeq ω).length = ω.length

Tactic:
by
  simp [leftInvSeq_eq_reverse_rightInvSeq_reverse]

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

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.IsRightDescent w⁻¹ i ↔ cs.IsLeftDescent w i

Tactic:
by
  simpa using (cs.isLeftDescent_inv_iff (w := w⁻¹)).symm

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

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

Tactic:
rw [getElem?_eq_none_iff.mpr (by lia)]
    simp

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
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
⊢ Function.RightInverse (fun w ↦ w.prod) fun m ↦ m • empty

Tactic:
apply smul_induction
    · dsimp only
      rw [prod_empty, one_smul]
    · 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 inr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
j : ℕ
nhj : ¬j < ω.length
⊢ cs.wordProd (take j ω) *
      ((Option.map cs.simple ω[j]?).getD 1 *
        ((cs.wordProd (take j ω))⁻¹ *
          (cs.wordProd (take j ω) * ((Option.map cs.simple ω[j]?).getD 1 * (cs.wordProd (take j ω))⁻¹)))) =
    1

Tactic:
rw [getElem?_eq_none_iff.mpr (by lia)]
    simp

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

Goal state before:
pp: case cons.head
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω ∈ cs.rightInvSeq ω →
    cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)
⊢ cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)

pp: case cons.tail
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
i : B
ω : List B
ih : t ∈ cs.rightInvSeq ω → cs.IsReflection t
mem : Mem t (cs.rightInvSeq ω)
⊢ cs.IsReflection t

Tactic:
· use (π ω)⁻¹, i
      group

Goal state after:
case cons.tail
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
t : W
i : B
ω : List B
ih : t ∈ cs.rightInvSeq ω → cs.IsReflection t
mem : Mem t (cs.rightInvSeq ω)
⊢ cs.IsReflection t
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case right
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
hω : cs.IsReduced ω
t : W
ht : t ∈ cs.rightInvSeq ω
⊢ cs.length (cs.wordProd ω * t) < cs.length (cs.wordProd ω)

Tactic:
· obtain ⟨j, hj, rfl⟩ := List.mem_iff_getElem.mp ht
    rw [← List.getD_eq_getElem _ 1 hj, wordProd_mul_getD_rightInvSeq]
    rw [cs.length_rightInvSeq] at hj
    calc
      ℓ (π (ω.eraseIdx j))
      _ ≤ (ω.eraseIdx j).length := cs.length_wordProd_le _
      _ < ω.length := by rw [← List.length_eraseIdx_add_one hj]; exact lt_add_one _
      _ = ℓ (π ω) := hω.symm

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
⊢ C ≤ c₀ / (b - 1)

Tactic:
obtain ⟨t₀, ht₀⟩ : ∃ g : Submonoid.powers t, h g = C := exists_eq_ciSup_of_finite

Goal state after:
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
⊢ C ≤ c₀ / (b - 1)
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
⊢ ⋃ q, Quot.mk ⇑(leftRel K) '' doubleCoset (out q) ↑H ↑K = Set.univ

Tactic:
Set.iUnion_eq_univ_iff

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
⊢ ∀ (x : Quot ⇑(leftRel K)), ∃ i, x ∈ Quot.mk ⇑(leftRel K) '' doubleCoset (out i) ↑H ↑K
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
⊢ ⋃ q, Quot.mk ⇑(rightRel H) '' doubleCoset (out q) ↑H ↑K = Set.univ

Tactic:
Set.iUnion_eq_univ_iff

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
⊢ ∀ (x : Quot ⇑(rightRel H)), ∃ i, x ∈ Quot.mk ⇑(rightRel H) '' doubleCoset (out i) ↑H ↑K
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
⊢ (↑⟨a.den, ⋯⟩ * ↑sc * a.num) • mb < (↑⟨a.den, ⋯⟩ * ↑sb * a.num) • mc

Tactic:
simp_rw [mul_right_comm _ _ a.num, mul_smul _ _ mc, mul_smul _ _ mb]

Goal state after:
case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
a : ℚ≥0
ha : 0 < a
mb : M
sb : ℕ+
mc : M
sc : ℕ+
h : ↑sc • mb < ↑sb • mc
⊢ (↑⟨a.den, ⋯⟩ * a.num) • ↑sc • mb < (↑⟨a.den, ⋯⟩ * a.num) • ↑sb • mc
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s s' : ℕ+
this : ↑↑s • mk m s = ↑↑s' • mk m s'
⊢ ArchimedeanClass.mk (mk m s) = ArchimedeanClass.mk (mk m s')

Tactic:
apply_fun ArchimedeanClass.mk at this
    rw [ArchimedeanClass.mk_smul _ (by simp)] at this
    rw [ArchimedeanClass.mk_smul _ (by simp)] at this
    exact this

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

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

Tactic:
intro i j hij

Goal state after:
case hXdisj
ι : 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
⊢ (Disjoint on X') i j
Module: Mathlib.GroupTheory.CoprodI

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

pp: case hXdisj.ht.hu
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
⊢ Disjoint (Y i) (Y j)

Tactic:
· exact (hXYdisj j i).symm

Goal state after:
case hXdisj.ht.hu
ι : Type u_1
inst✝² : Nontrivial ι
G : Type u_1
inst✝¹ : Group G
a : ι → G
α : Type u_4
inst✝ : MulAction G α
X Y : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hYdisj : Pairwise (Disjoint on Y)
hXYdisj : ∀ (i j : ι), Disjoint (X i) (Y j)
hX : ∀ (i : ι), a i • (Y i)ᶜ ⊆ X i
hY : ∀ (i : ι), a⁻¹ i • (X i)ᶜ ⊆ Y i
H : ι → Type := ⋯
f : (i : ι) → H i →* G := ⋯
X' : ι → Set α := ⋯
i j : ι
hij : i ≠ j
⊢ Disjoint (Y i) (Y j)
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun x ↦ g • x) (Quotient.out q))
⊢ ↑(⋯.leftQuotientEquiv (g ^ k.cast • Quotient.out q)) = g ^ k.cast * Quotient.out (Quotient.out q)

Tactic:
transferTransversal_apply,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun x ↦ g • x) (Quotient.out q))
⊢ H.transferFunction g (g ^ k.cast • Quotient.out q) = g ^ k.cast * Quotient.out (Quotient.out q)
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun x ↦ g • x) (Quotient.out q))
⊢ g • ↑(⋯.leftQuotientEquiv (g⁻¹ • g ^ k.cast • Quotient.out q)) =
    if k = 0 then g ^ minimalPeriod (fun x ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else g ^ k.cast * Quotient.out (Quotient.out q)

Tactic:
transferTransversal_apply,

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient (↥(zpowers g)) (G ⧸ H)
k : ZMod (minimalPeriod (fun x ↦ g • x) (Quotient.out q))
⊢ g • H.transferFunction g (g⁻¹ • g ^ k.cast • Quotient.out q) =
    if k = 0 then g ^ minimalPeriod (fun x ↦ g • x) (Quotient.out q) * Quotient.out (Quotient.out q)
    else g ^ k.cast * Quotient.out (Quotient.out q)
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg.inr.refine_1
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
⊢ (↑P).index.Coprime (Nat.card G).minFac

Tactic:
rw [Nat.coprime_comm, Nat.Prime.coprime_iff_not_dvd Fact.out]

Goal state after:
case neg.inr.refine_1
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
⊢ ¬(Nat.card G).minFac ∣ (↑P).index