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

Goal state before:
pp: case inr
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : Sum.inr e ∈ T b a
⊢ (homOfPath T default ≫ Sum.recOn (↑⟨Sum.inr e, H⟩) (fun e ↦ of e) fun e ↦ inv (of e)) ≫ of e = treeHom T b

Tactic:
simp only [IsIso.inv_hom_id, Category.comp_id, Category.assoc, treeHom]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ∀ (n : ℕ), ⊤.lowerCentralSeries n = ⊥ → ∃ H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
· rintro n h
    exact ⟨lowerCentralSeries ⊤, ⟨lowerCentralSeries_isDescendingCentralSeries, 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'δ : 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
hgx : ((g x) v) v = ((g' x) w) w
hgy : ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) = ((g' y) w) w
⊢ ‖g' y - g' x‖ * (‖w‖ * ‖w‖) + ((g' x) w) w ≤ δ * (‖w‖ * ‖w‖) + ((g' x) w) w

Tactic:
gcongr

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : IsTrivialBlock B
⊢ IsBlock G B

Tactic:
by
  obtain hB | rfl := hB
  · exact .of_subsingleton hB
  · exact .univ

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
⊢ IsBlock G (orbit (↥H) a)

Tactic:
isBlock_iff_smul_eq_of_nonempty

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
H : Subgroup G
a : X
hH : stabilizer G a ≤ H
⊢ ∀ ⦃g : G⦄, (g • orbit (↥H) a ∩ orbit (↥H) a).Nonempty → g • orbit (↥H) a = orbit (↥H) a
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : Nontrivial X
a : X
⊢ Nontrivial (BlockMem G a)

Tactic:
rw [nontrivial_iff]
  use ⊥, ⊤
  intro h
  rw [← Subtype.coe_inj] at h
  simp only [coe_top, coe_bot] at h
  obtain ⟨b, hb⟩ := exists_ne a
  apply hb
  rw [← Set.mem_singleton_iff, h]
  apply Set.mem_univ

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

Goal state before:
pp: case inr
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_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
⊢ IsBlock G (⋂ k, ⋂ (_ : a ∈ k • B), k • B)

Tactic:
isBlock_iff_smul_eq_of_nonempty

Goal state after:
case inr
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_ne : B.Nonempty
hB'₀ : ∀ (k : G), a ∈ k • B → B' ⊆ k • B
hfB' : B'.Finite
hag : ∀ (g : G), a ∈ g • B' → B' ⊆ g • B'
hag' : ∀ (g : G), a ∈ g • B' → B' = g • B'
⊢ ∀ ⦃g : G⦄,
    ((g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B) ∩ ⋂ k, ⋂ (_ : a ∈ k • B), k • B).Nonempty →
      g • ⋂ k, ⋂ (_ : a ∈ k • B), k • B = ⋂ k, ⋂ (_ : a ∈ k • B), k • B
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: 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.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
this : b ∉ B
⊢ ∃ g, a ∈ g • A ∧ b ∉ g • A

Tactic:
rw [Set.mem_iInter] at this
    simpa only [Set.mem_iInter, not_forall, exists_prop] using this

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
hgx : ((g x) v) v = ((g' x) w) w
hgy : ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) = ((g' y) w) w
⊢ (1 + δ * C) * ((g' x) w) w ≤ r' ^ 2 * ((g' x) w) w

Tactic:
gcongr

Goal state after:
case ha
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 := ⋯
C : ℝ := ⋯
δ : ℝ
δ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[ℝ] ℝ := ⋯
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 := ⋯
hgx : ((g x) v) v = ((g' x) w) w
hgy : ((g y) ((trivializationAt F E x).symm y w)) ((trivializationAt F E x).symm y w) = ((g' y) w) w
⊢ 0 ≤ ((g' x) w) w
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case mp
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a✝ : IsMultiplyPretransitive G α 2
a b c : α
⊢ ∀ {d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d

Tactic:
d

Goal state after:
case mp
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a✝ : IsMultiplyPretransitive G α 2
a b c d : α
⊢ a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
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
hy :
  ‖Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
        Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ <
    2
A :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
      Trivialization.symmL ℝ (trivializationAt F E x) x =
    ContinuousLinearMap.id ℝ F
this :
  Trivialization.symmL ℝ (trivializationAt F E x) y =
    Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL ContinuousLinearMap.id ℝ F
⊢ ‖Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
          Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ *
      ‖Trivialization.symmL ℝ (trivializationAt F E x) x‖ <
    2 * (1 + ‖Trivialization.symmL ℝ (trivializationAt F E x) x‖)

Tactic:
gcongr

Goal state after:
case h₂
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
A :
  Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x ∘SL
      Trivialization.symmL ℝ (trivializationAt F E x) x =
    ContinuousLinearMap.id ℝ F
this :
  Trivialization.symmL ℝ (trivializationAt F E x) y =
    Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL ContinuousLinearMap.id ℝ F
⊢ ‖Trivialization.symmL ℝ (trivializationAt F E x) x‖ < 1 + ‖Trivialization.symmL ℝ (trivializationAt F E x) x‖
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case mpr.left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ IsMultiplyPretransitive M α 1

pp: case mpr.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ ∀ {s : Set α}, s.encard + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
· exact is_one_pretransitive_iff.mpr h.toIsPretransitive

Goal state after:
case mpr.right
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
h : IsPreprimitive M α
⊢ ∀ {s : Set α}, s.encard + 1 = ↑1 → IsPreprimitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : 2 < t.ncard
⊢ ∃ g ∈ stabilizer (↥(alternatingGroup α)) t, g • a = b

Tactic:
rw [← Set.ncard_pair hab] at ht

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : {a, b}.ncard < t.ncard
⊢ ∃ g ∈ stabilizer (↥(alternatingGroup α)) t, g • a = b
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case inr
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd✝¹ : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this✝ : ∃ s ∈ S, m ∣ s * ((m₁, s₁).1 * (m₂, s₂).1)
s : M
hs : s ∈ S
dvd✝ : m ∣ s * (m₁, s₁).1 * (m₂, s₂).1
dvd : m ∣ (m₂, s₂).1
this : f m ∣ f (m₂, s₂).1
⊢ f m ∣ n₁ ∨ f m ∣ n₂

Tactic:
rw [← eq₂, (f.map_units s₂).dvd_mul_right] at this; exact .inr this

Goal state after:
Module: Mathlib.GroupTheory.NoncommCoprod

Goal state before:
pp: case a
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ (f.noncommCoprod g comm).range ≤ f.range ⊔ g.range

pp: case a
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ f.range ⊔ g.range ≤ (f.noncommCoprod g comm).range

Tactic:
· rintro - ⟨a, rfl⟩
    exact mul_mem (mem_sup_left ⟨a.1, rfl⟩) (mem_sup_right ⟨a.2, rfl⟩)

Goal state after:
case a
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Group M
inst✝¹ : Group N
inst✝ : Group P
f : M →* P
g : N →* P
comm : ∀ (m : M) (n : N), Commute (f m) (g n)
⊢ f.range ⊔ g.range ≤ (f.noncommCoprod g comm).range
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ Nat.card { g // f ∘ ⇑g = f } = ∏ i, (Fintype.card { a // f a = i })!

Tactic:
Nat.card_congr (subtypeEquiv mk fun _ ↦ ?_),

Goal state after:
α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ Nat.card { b // ?m.28 b } = ∏ i, (Fintype.card { a // f a = i })!

α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
⊢ (Perm α)ᵈᵐᵃ → Prop

α : Type u_1
ι : Type u_2
f : α → ι
inst✝³ : Fintype α
inst✝² : DecidableEq α
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x✝ : Perm α
⊢ f ∘ ⇑x✝ = f ↔ ?m.28 (mk x✝)
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h.right.right.hf
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl ↦ pmap klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
u : List ℕ
hu : ∀ a ∈ u, a < Fintype.card α
v : List ℕ
hv : ∀ a ∈ v, a < Fintype.card α
huv : u.Disjoint v
a a' : ℕ
ha : a < Fintype.card α
ha' : a' < Fintype.card α
h : klift a ha = klift a' ha'
⊢ a = a'

Tactic:
simpa only [klift, Fin.mk_eq_mk] using h

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case mp.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
m : Multiset ℕ
g : Perm α
hg : g.cycleType = m
⊢ ∀ a ∈ m, 2 ≤ a

Tactic:
intro a
      rw [← hg]
      exact Equiv.Perm.two_le_of_mem_cycleType

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

Goal state before:
pp: case h
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
i : ↥(Finset.image f Finset.univ)
ha✝ : i ∈ Finset.univ
a : α
⊢ φ a = i ↔ f ((Equiv.refl α) a) = ↑i

Tactic:
refl_apply,

Goal state after:
case h
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f ↑(Finset.image f Finset.univ) ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
i : ↥(Finset.image f Finset.univ)
ha✝ : i ∈ Finset.univ
a : α
⊢ φ a = i ↔ f a = ↑i
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c : ↥g.cycleFactorsFinset
⊢ ∀ ⦃a₂ : ↥g.cycleFactorsFinset⦄, a c = a a₂ → c = a₂

Tactic:
d

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
c d : ↥g.cycleFactorsFinset
⊢ a c = a d → c = d
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih : ∀ {f : Equiv.Perm α}, (∀ (x : α), f x ∈ orbit (↥(closure S)) x) → (fixedBy α f)ᶜ ⊆ s → f ∈ closure S
f : Equiv.Perm α
hf : ∀ (x : α), f x ∈ orbit (↥(closure S)) x
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
⊢ (Equiv.swap (f a) a * f) b ∈ orbit (↥(closure S)) b

Tactic:
rw [Perm.mul_apply, swap_apply_def]; split_ifs with h1 h2
    · rw [← orbit_eq_iff.mpr (hf b), h1, orbit_eq_iff.mpr (hf a)]; apply mem_orbit_self
    · rw [← orbit_eq_iff.mpr (hf b), h2]; apply hf
    · exact hf b

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
c : ↥g.cycleFactorsFinset
a✝ : c ∈ ↑(↑τ).support
⊢ ∀ ⦃y : ↥g.cycleFactorsFinset⦄, y ∈ ↑(↑τ).support → c ≠ y → Function.onFun _root_.Disjoint (fun c ↦ (↑c).support) c y

Tactic:
d

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
c : ↥g.cycleFactorsFinset
a✝ : c ∈ ↑(↑τ).support
d : ↥g.cycleFactorsFinset
⊢ d ∈ ↑(↑τ).support → c ≠ d → Function.onFun _root_.Disjoint (fun c ↦ (↑c).support) c d
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ {g | (↑g).cycleType = {2, 2}}
⊢ g ^ 2 = 1

Tactic:
· convert! pow_orderOf_eq_one g
      rw [← Equiv.Perm.lcm_cycleType, hg']
      simp

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g).IsThreeCycle
⊢ g ∈ commutatorSet ↥(alternatingGroup α)

Tactic:
by
  apply mem_commutatorSet_of_isConj_sq
  apply alternatingGroup.isThreeCycle_isConj h5 hg
  simpa [sq] using hg.isThreeCycle_sq

Goal state after:
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
this : (fun i ↦ ((if i = 0 then κ else 0) a) s) = fun i ↦ if i = 0 then (κ a) s else 0
⊢ (κ a) s = ∑' (i : ℕ), if i = 0 then (κ a) s else 0

Tactic:
tsum_ite_eq

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
this : (fun i ↦ ((if i = 0 then κ else 0) a) s) = fun i ↦ if i = 0 then (κ a) s else 0
⊢ (κ a) s = (κ a) s
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
⊢ #{i | ¬f i (x i) = f i (y i)} ≤ #{i | ¬x i = y i}

Tactic:
gcongr

Goal state after:
case h₁
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
i : ι
a✝ : i ∈ univ
⊢ x i = y i → f i (x i) = f i (y i)
Module: Mathlib.InformationTheory.Hamming

Goal state before:
pp: ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
hf : ∀ (i : ι), Injective (f i)
⊢ #{i | ¬x i = y i} ≤ #{i | ¬f i (x i) = f i (y i)}

Tactic:
gcongr

Goal state after:
case h₁
ι : Type u_2
β : ι → Type u_3
inst✝² : Fintype ι
inst✝¹ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → γ i → β i
x y : (i : ι) → γ i
hf : ∀ (i : ι), Injective (f i)
i : ι
a✝ : i ∈ univ
⊢ f i (x i) = f i (y i) → x i = y i
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝ : Countable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val✝ : Fintype ι
⊢ IsSFiniteKernel (Kernel.sum κs)

Tactic:
rw [sum_fintype]

Goal state after:
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝ : Countable ι
κs : ι → Kernel α β
hκs : ∀ (n : ι), IsSFiniteKernel (κs n)
val✝ : Fintype ι
⊢ IsSFiniteKernel (∑ i, κs i)
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:
pp: case calc.step
α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
⊢ ↑{x ∈ T | x.length = s}.card * (1 / ↑(Fintype.card α)) ^ s ≤ ↑(Fintype.card α) ^ s * (1 / ↑(Fintype.card α)) ^ s

Tactic:
gcongr

Goal state after:
case hbc
α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
⊢ ↑{x ∈ T | x.length = s}.card ≤ ↑(Fintype.card α) ^ s
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsFiniteKernel η
κ : Kernel α β
inst✝ : IsFiniteKernel κ
a : α
⊢ (κ a) Set.univ * η.bound ≤ κ.bound * η.bound

Tactic:
gcongr

Goal state after:
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
inst✝¹ : IsFiniteKernel η
κ : Kernel α β
inst✝ : IsFiniteKernel κ
a : α
⊢ (κ a) Set.univ ≤ κ.bound
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
ι : Type u_5
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel γ δ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
⊢ κ ∥ₖ Kernel.sum η = Kernel.sum fun i ↦ κ ∥ₖ η i

Tactic:
by
  by_cases h : IsSFiniteKernel κ
  swap; · simp [h]
  ext x
  simp_rw [Kernel.sum_apply, parallelComp_apply, Kernel.sum_apply, Measure.prod_sum_right]

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.ParallelComp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α × γ
⊢ (κ a.1) Set.univ * (η a.2) Set.univ ≤ κ.bound * η.bound

Tactic:
gcongr

Goal state after:
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α × γ
⊢ (κ a.1) Set.univ ≤ κ.bound

case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
x : α × γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α × γ
⊢ (η a.2) Set.univ ≤ η.bound
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: β : Type u_2
mβ : MeasurableSpace β
κ : Kernel Unit β
inst✝ : IsSFiniteKernel κ
s : Set (Unit × β)
hs : MeasurableSet s
⊢ (κ ()) (Prod.mk () ⁻¹' s) = (map (Prod.mk ()) (κ ())) s

Tactic:
Measure.map_apply measurable_prodMk_left hs

Goal state after:
β : Type u_2
mβ : MeasurableSpace β
κ : Kernel Unit β
inst✝ : IsSFiniteKernel κ
s : Set (Unit × β)
hs : MeasurableSet s
⊢ (κ ()) (Prod.mk () ⁻¹' s) = (κ ()) (Prod.mk () ⁻¹' s)