mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
w : Word M
h : w ≠ empty
⊢ ∃ i j w', w'.toWord.toList = w.toList

Tactic:
obtain ⟨l, hnot1, hchain⟩ := w

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
l : List ((i : ι) × M i)
hnot1 : ∀ l_1 ∈ l, l_1.snd ≠ 1
hchain : List.IsChain (fun l l' ↦ l.fst ≠ l'.fst) l
h : { toList := l, ne_one := hnot1, chain_ne := hchain } ≠ empty
⊢ ∃ i j w', w'.toWord.toList = { toList := l, ne_one := hnot1, chain_ne := hchain }.toList
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
⊢ ‖g' y - g' x‖ ≤ δ

Tactic:
← dist_eq_norm

Goal state after:
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
⊢ dist (g' y) (g' x) ≤ δ
Module: Mathlib.GroupTheory.Descent

Goal state before:
pp: 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
x : G
⊢ x / qi (q x) ∈ f.range

Tactic:
exact eq_iff_div_mem.mp (Function.surjInv_eq mk_surjective _).symm

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
j : ι
w : NeWord H j j
hcard : 3 ≤ #(H j)
⊢ (lift f) w.prod ≠ 1

Tactic:
exact lift_word_prod_nontrivial_of_head_eq_last f X hXnonempty hXdisj hpp w

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

Tactic:
hy

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
t : Finset (Quotient ↑H ↑K)
ht : ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K ≠ Set.univ
x : G
hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K
y : Quotient ↑H ↑K
hy : y ∈ t
⊢ ∀ x_1 ∈ doubleCoset (out y) ↑H ↑K, ¬Quot.mk (⇑(leftRel K)) x_1 = Quot.mk (⇑(leftRel K)) x
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
t : Finset (Quotient ↑H ↑K)
ht : ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K ≠ Set.univ
x : G
hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K
y : Quotient ↑H ↑K
⊢ y ∈ t → ∀ x_1 ∈ doubleCoset (out y) ↑H ↑K, ¬Quot.mk (⇑(rightRel H)) x_1 = Quot.mk (⇑(rightRel H)) x

Tactic:
hy

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
t : Finset (Quotient ↑H ↑K)
ht : ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K ≠ Set.univ
x : G
hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) ↑H ↑K
y : Quotient ↑H ↑K
hy : y ∈ t
⊢ ∀ x_1 ∈ doubleCoset (out y) ↑H ↑K, ¬Quot.mk (⇑(rightRel H)) x_1 = Quot.mk (⇑(rightRel H)) x
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case h₁
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
⊢ (archimedeanClassOrderHom M).comp (archimedeanClassOrderHomInv M) = OrderHom.id

pp: case h₂
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
⊢ (archimedeanClassOrderHomInv M).comp (archimedeanClassOrderHom M) = OrderHom.id

Tactic:
· ext a
    induction a with | mk a
    induction a with | mk m s
    suffices ArchimedeanClass.mk (mk m 1) = ArchimedeanClass.mk (mk m s) by
      simpa [archimedeanClassOrderHom, archimedeanClassOrderHomInv]
    simp_rw [aux_archimedeanClassMk_mk]

Goal state after:
case h₂
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
⊢ (archimedeanClassOrderHomInv M).comp (archimedeanClassOrderHom M) = OrderHom.id
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
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
g g' : G
⊢ (∀ (φ : G →* Mˣ), φ g = φ g') ↔ g = g'

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
  simpa [← not_forall, not_imp_not, mul_inv_eq_one, h] using
    exists_apply_ne_one_of_hasEnoughRootsOfUnity G M (a := g * g'⁻¹)

Goal state after:
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: case a
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ _root_.commutator G ⊓ ↑P ≤ (↑P).focalSubgroup

Tactic:
apply le_trans ?_ (ker_transferFocal_inf_eq_focalSubgroup P).le

Goal state after:
G : Type u_1
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : (↑P).FiniteIndex
⊢ _root_.commutator G ⊓ ↑P ≤ (↑P).transferFocal.ker ⊓ ↑P
Module: Mathlib.Order.Radical

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
q : a ⊔ radical α ≤ m
⊢ a = ⊤

Tactic:
rw [h, top_le_iff] at q

Goal state after:
case inr
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : IsCoatomic α
a : α
h : a ⊔ radical α = ⊤
m : α
c : IsCoatom m
le : a ≤ m
q : m = ⊤
⊢ a = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x y : G
hx : x * y⁻¹ * (x⁻¹ * y) ∈ N
⊢ x⁻¹ * y * (x * y⁻¹) ∈ N

Tactic:
exact Subgroup.Normal.mem_comm inferInstance hx

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

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l✝ : List (α × Bool) := g.toWord
h : ⟨g, hg⟩ = ⟨mk g.toWord, ⋯⟩
a b : α × Bool
l : List (α × Bool)
hl : a :: b :: l = g.toWord
ha : a = w
h1 : (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: l)
⊢ (mk [w])⁻¹ • (fun m ↦ m • x) ⟨g, hg⟩ ∈ MulAction.orbit (↑(startsWith b)) x

Tactic:
simp_rw [h, ← hl, ha, ← List.singleton_append (l := b :: l), ← mul_mk, startsWith.smul_def,
        mul_smul, inv_smul_smul]

Goal state after:
α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l✝ : List (α × Bool) := g.toWord
h : ⟨g, hg⟩ = ⟨mk g.toWord, ⋯⟩
a b : α × Bool
l : List (α × Bool)
hl : a :: b :: l = g.toWord
ha : a = w
h1 : (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: l)
⊢ mk (b :: l) • x ∈ MulAction.orbit (↑(startsWith b)) x
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
x y : G × H
hx : x ∈ I
hy : y ∈ I
this✝ : I.goursatFst.Normal
this : I.goursatSnd.Normal
⊢ (y.1 / x.1, 1) ∈ I ↔ (1, x.2 / y.2) ∈ I

Tactic:
constructor <;> intro h

Goal state after:
case mp
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
x y : G × H
hx : x ∈ I
hy : y ∈ I
this✝ : I.goursatFst.Normal
this : I.goursatSnd.Normal
h : (y.1 / x.1, 1) ∈ I
⊢ (1, x.2 / y.2) ∈ I

case mpr
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
hI₁ : Surjective (Prod.fst ∘ ⇑I.subtype)
hI₂ : Surjective (Prod.snd ∘ ⇑I.subtype)
x y : G × H
hx : x ∈ I
hy : y ∈ I
this✝ : I.goursatFst.Normal
this : I.goursatSnd.Normal
h : (1, x.2 / y.2) ∈ I
⊢ (y.1 / x.1, 1) ∈ I
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
⊢ ∃ G' H' M N,
    ∃ (x : M.Normal) (x_1 : N.Normal),
      ∃ e,
        I =
          map (G'.subtype.prodMap H'.subtype)
            (comap ((QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)) e.toMonoidHom.graph)

Tactic:
let P : I →* G' := (MonoidHom.fst ..).subgroupMap I

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
⊢ ∃ G' H' M N,
    ∃ (x : M.Normal) (x_1 : N.Normal),
      ∃ e,
        I =
          map (G'.subtype.prodMap H'.subtype)
            (comap ((QuotientGroup.mk' M).prodMap (QuotientGroup.mk' N)) e.toMonoidHom.graph)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ center G = ⊤ ↔ IsMulCommutative G

Tactic:
exact Subgroup.center_eq_top_iff

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ h • a = y

Tactic:
hy

Goal state after:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
hG : ∀ (x : X), ∃ g, g • a = x
x y : X
g : G
hx : g • a = x
h : G
hy : h • a = y
⊢ y = y
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inl
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
a : X
hfB : B.Finite
B' : Set X := ⋂ k, ⋂ (_ : a ∈ k • B), k • B
hfB_e : B = ∅
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

Tactic:
simp [hfB_e]

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

Goal state before:
pp: case mpr.inr
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
h : B = Set.univ
⊢ B = ↑⊥ ∨ B = ↑⊤

Tactic:
simp [BlockMem.coe_top, h]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: case left
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x : α
hx : x ∈ ofStabilizer G a
y : α
hy : y ∈ ofStabilizer G a
hxy : (conjMap hg) ⟨x, hx⟩ = (conjMap hg) ⟨y, hy⟩
⊢ x = y

Tactic:
apply (MulAction.injective g)

Goal state after:
case left
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
g : G
a b : α
hg : b = g • a
x : α
hx : x ∈ ofStabilizer G a
y : α
hy : y ∈ ofStabilizer G a
hxy : (conjMap hg) ⟨x, hx⟩ = (conjMap hg) ⟨y, hy⟩
⊢ (fun x ↦ g • x) x = (fun x ↦ g • x) y
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case inr
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
x : X
hx : x ∈ A
⊢ ∃ g, a ∈ g • A

Tactic:
obtain ⟨g, hg⟩ := MulAction.exists_smul_eq G x a

Goal state after:
case inr
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
hyp : B = Set.univ
x : X
hx : x ∈ A
g : G
hg : g • x = a
⊢ ∃ g, a ∈ g • A
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case a.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg3 : g ∈ {σ | σ.IsThreeCycle}
a : α
ha : a ∈ g.support
h_support : g.support = {a, g a, g (g a)}
h_nodup : [a, g a, g (g a)].Nodup
this : 1 < g.supportᶜ.card
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
H : g = swap a (g a) * swap b c * (swap b c * swap (g a) (g (g a)))
⊢ swap a (g a) * swap b c ∈ closure {g | g.cycleType = {2, 2}}

Tactic:
· apply Subgroup.subset_closure
      exact cycleType_swap_mul_swap_of_nodup (by grind [Finset.mem_compl])

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

Goal state before:
pp: case a.a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : Perm α
hg3 : g ∈ {σ | σ.IsThreeCycle}
a : α
ha : a ∈ g.support
h_support : g.support = {a, g a, g (g a)}
h_nodup : [a, g a, g (g a)].Nodup
this : 1 < g.supportᶜ.card
b c : α
hb : b ∈ g.supportᶜ
hc : c ∈ g.supportᶜ
hbc : b ≠ c
H : g = swap a (g a) * swap b c * (swap b c * swap (g a) (g (g a)))
⊢ swap b c * swap (g a) (g (g a)) ∈ closure {g | g.cycleType = {2, 2}}

Tactic:
· apply Subgroup.subset_closure
      exact cycleType_swap_mul_swap_of_nodup (by grind [Finset.mem_compl])

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 y : B
⊢ ‖Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
          Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ <
      2 →
    ‖Trivialization.symmL ℝ (trivializationAt F E x) y‖ < 2 * (1 + ‖Trivialization.symmL ℝ (trivializationAt F E x) x‖)

Tactic:
hy

Goal state after:
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 y : B
hy :
  ‖Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ <
    2
⊢ ‖Trivialization.symmL ℝ (trivializationAt F E x) y‖ < 2 * (1 + ‖Trivialization.symmL ℝ (trivializationAt F E x) x‖)
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
inst✝ : IsMultiplyPretransitive G α n
hmn : m ≤ n
hα : ↑n ≤ ENat.card α
⊢ IsMultiplyPretransitive G α m

Tactic:
by
  obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hmn
  exact IsPretransitive.of_surjective_map
    (f := embMap G α (castAddEmb p))
    (Fin.Embedding.restrictSurjective_of_add_le_ENatCard hα) inferInstance

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
hk : ∀ y ∈ t, k • y = y
y : α
⊢ y ∈ s → (MulAut.conj g) k • y = y

Tactic:
hy

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hg : g • t = s
k : M
hk : ∀ y ∈ t, k • y = y
y : α
hy : y ∈ s
⊢ (MulAut.conj g) k • y = y
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
g : M
hg : g • t = s
x✝ : ↥(ofFixingSubgroup M t)
x : α
hx : x ∈ ofFixingSubgroup M t
⊢ g • x ∈ ofFixingSubgroup M s

Tactic:
intro hgxt

Goal state after:
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
g : M
hg : g • t = s
x✝ : ↥(ofFixingSubgroup M t)
x : α
hx : x ∈ ofFixingSubgroup M t
hgxt : g • x ∈ s
⊢ False
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
m n : ℕ
inst✝¹ : IsMultiplyPreprimitive M α n
s : Set α
inst✝ : Finite ↑s
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ s.encard + t'.encard + 1 = ↑n

Tactic:
rw [Subtype.coe_injective.encard_image, add_assoc, ht,
        ← hs, Nat.cast_add, Set.Finite.cast_ncard_eq]
      exact Set.toFinite s

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
G : Subgroup (Perm α)
this✝ : Fintype α
hmt : IsMultiplyPretransitive (↥G) α (Fintype.card α - 1)
j✝ : Fin (Fintype.card α - 1) ↪ Fin (Fintype.card α) := castLEEmb ⋯
k : Perm α
a✝ : k ∈ ⊤
x : Fin (Fintype.card α) ↪ α := (Fintype.equivFinOfCardEq ⋯).symm.toEmbedding
x' : Fin (Fintype.card α - 1) ↪ α := j✝.trans x
g : ↥G
hg' : g • x' = k • x'
hx : ∀ (x : Fin (Fintype.card α) ↪ α), Function.Surjective x.toFun
hgk' : ∀ (i : Fin (Fintype.card α)), ↑i < Fintype.card α - 1 → (g • x) i = (k • x) i
i : Fin (Fintype.card α)
hi : ↑i = Fintype.card α - 1
j : Fin (Fintype.card α)
hxj : (k • x) j = (g • x) i
hj : ↑i < ↑i
this : i = j
⊢ (g • x) i = (k • x) i

Tactic:
exact (lt_irrefl _ hj).elim

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: case w
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ ofFixingSubgroup M (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ ofFixingSubgroup M s
hg'a : g⁻¹ • a ∈ ofFixingSubgroup M s
k : M
hk✝ : k ∈ fixingSubgroup M s
hk : ∀ y ∈ s, k • y = y
hkax : ⟨k, hk✝⟩ • ⟨g⁻¹ • a, hg'a⟩ = ⟨g⁻¹ • x, hg'x⟩
y : α
⊢ y ∈ s ∩ g • s → (g * k * g⁻¹) • y = y

Tactic:
hy

Goal state after:
case w
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx✝ : x ∈ ofFixingSubgroup M (s ∩ g • s)
hx : x ∉ g • s
hg'x : g⁻¹ • x ∈ ofFixingSubgroup M s
hg'a : g⁻¹ • a ∈ ofFixingSubgroup M s
k : M
hk✝ : k ∈ fixingSubgroup M s
hk : ∀ y ∈ s, k • y = y
hkax : ⟨k, hk✝⟩ • ⟨g⁻¹ • a, hg'a⟩ = ⟨g⁻¹ • x, hg'x⟩
y : α
hy : y ∈ s ∩ g • s
⊢ (g * k * g⁻¹) • y = y
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
x✝ : ↥(fixingSubgroup M s)
g : M
hg : ∀ y ∈ s, g • y = y
y : β
⊢ y ∈ t → φ g • y = y

Tactic:
hy

Goal state after:
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
x✝ : ↥(fixingSubgroup M s)
g : M
hg : ∀ y ∈ s, g • y = y
y : β
hy : y ∈ t
⊢ φ g • y = y
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hM : stabilizer M s ≠ ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∉ s
⊢ ∃ g, g • a = x

Tactic:
rw [← Set.mem_compl_iff] at hx

Goal state after:
case neg
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hM : stabilizer M s ≠ ⊤
a b : α
g : M
ha : a ∈ s
hb : b ∈ sᶜ
hgab : g • a = b
x : α
hx : x ∈ sᶜ
⊢ ∃ g, g • a = x
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : ∀ a ∈ s, ∀ b ∈ s, ∃ g, g • a = b
hs' : ∀ a ∈ sᶜ, ∀ b ∈ sᶜ, ∃ g, g • a = b
hM : ∀ (a b : α) (g : M), a ∈ s → b ∈ sᶜ → g • a ≠ b
g : M
a✝ : g ∈ ⊤
b a : α
ha : a ∈ s
hgab : (fun x ↦ g • x) a = b
hb : b ∉ s
⊢ False

Tactic:
exact hM a b g ha (Set.mem_compl hb) hgab

Goal state after:
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
g : Perm ↑s
g' : α
⊢ g' ∈ ofSubtype g • s ↔ g' ∈ s

Tactic:
simp_rw [mem_smul_set, Perm.smul_def]

Goal state after:
α : Type u_2
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
g : Perm ↑s
g' : α
⊢ (∃ y ∈ s, (ofSubtype g) y = g') ↔ g' ∈ s
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case right.hφ
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨g, hg⟩ => ⟨φ g, ⋯⟩
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := { toFun := fun x ↦ ⟨f ↑x, ⋯⟩, map_smul' := ⋯ }
k : M
hk : ∀ y ∈ ⇑f '' s, φ k • y = y
y : α
⊢ y ∈ s → k • y = y

Tactic:
hy

Goal state after:
case right.hφ
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨g, hg⟩ => ⟨φ g, ⋯⟩
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := { toFun := fun x ↦ ⟨f ↑x, ⋯⟩, map_smul' := ⋯ }
k : M
hk : ∀ y ∈ ⇑f '' s, φ k • y = y
y : α
hy : y ∈ s
⊢ k • y = y