mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: case e'_2
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f) ≠ 0
hf' : f ⟨x, hxU⟩ ≠ 0
V₀ : Set ↥U
hV₀f : ∀ y ∈ V₀, f y ≠ 0
hV₀ : IsOpen[instTopologicalSpaceSubtype] V₀
hxV₀ : ⟨x, hxU⟩ ∈ V₀
V : Opens M := { carrier := Subtype.val '' V₀, is_open' := ⋯ }
hUV : V ≤ U
e_1✝ : Set ↥U = Set ↑↑U
y : ↥U
⊢ y ∈ V₀ ↔ y ∈ Subtype.val ⁻¹' Subtype.val '' V₀

Tactic:
Set.preimage_image_eq _ Subtype.coe_injective

Goal state after:
case e'_2
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
S : TopCat.Presheaf CommRingCat (TopCat.of M) := (smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf
U : Opens M
hxU : x ∈ U
f : C^∞⟮IM, ↥U; 𝓘(𝕜, 𝕜), 𝕜⟯
hf : (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x) ((CategoryTheory.ConcreteCategory.hom (S.germ U x hxU)) f) ≠ 0
hf' : f ⟨x, hxU⟩ ≠ 0
V₀ : Set ↥U
hV₀f : ∀ y ∈ V₀, f y ≠ 0
hV₀ : IsOpen[instTopologicalSpaceSubtype] V₀
hxV₀ : ⟨x, hxU⟩ ∈ V₀
V : Opens M := { carrier := Subtype.val '' V₀, is_open' := ⋯ }
hUV : V ≤ U
e_1✝ : Set ↥U = Set ↑↑U
y : ↥U
⊢ y ∈ V₀ ↔ y ∈ V₀
Module: Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace

Goal state before:
pp: 𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
f : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)
⊢ f ∉ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x)) ↔ IsUnit f

Tactic:
Iff.comm

Goal state after:
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
f : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)
⊢ IsUnit f ↔ f ∉ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x))
Module: Mathlib.Geometry.Manifold.VectorBundle.Tensoriality

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
H : Type u_3
inst✝¹¹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹⁰ : TopologicalSpace M
inst✝⁹ : ChartedSpace H M
F : Type u_5
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
V : M → Type u_6
inst✝⁶ : TopologicalSpace (TotalSpace F V)
inst✝⁵ : (x : M) → AddCommGroup (V x)
inst✝⁴ : (x : M) → Module 𝕜 (V x)
inst✝³ : (x : M) → TopologicalSpace (V x)
inst✝² : FiberBundle F V
A : Type u_9
inst✝¹ : AddCommGroup A
inst✝ : Module 𝕜 A
Φ : ((x : M) → V x) → A
x : M
hΦ : TensorialAt I F Φ x
σ σ' : (x : M) → V x
hσ : MDiffAt (T% σ) x
hσ' : MDiffAt (T% σ') x
hσσ' : ∀ᶠ (x' : M) in 𝓝 x, σ x' = σ' x'
ψ : M → 𝕜 := fun x' ↦ if σ x' = σ' x' then 1 else 0
hψx : ψ x = 1
this : ∀ (x' : M), (ψ • σ) x' = (ψ • σ') x'
hψ' : MDiffAt ψ x
⊢ Φ σ = Φ (ψ • σ)

Tactic:
simp [hΦ.smul hψ' hσ, hψx]

Goal state after:
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
⊢ commProb (DihedralGroup 3) * (1 / ↑(n / 2)) = 1 / ↑n

Tactic:
commProb_odd (by decide)

Goal state after:
case neg.inl
n : ℕ
h0 : ¬n = 0
h1 : ¬n = 1
h2 : Even n
⊢ (↑3 + 3) / (4 * ↑3) * (1 / ↑(n / 2)) = 1 / ↑n
Module: Mathlib.GroupTheory.CommutingProbability

Goal state before:
pp: n : ℕ
⊢ commProb (Product (reciprocalFactors n)) = 1 / ↑n

Tactic:
by_cases h0 : n = 0
  · rw [h0, reciprocalFactors_zero, commProb_cons, commProb_nil, mul_one, Nat.cast_zero, div_zero]
    apply commProb_eq_zero_of_infinite
  by_cases h1 : n = 1
  · rw [h1, reciprocalFactors_one, commProb_nil, Nat.cast_one, div_one]
  rcases Nat.even_or_odd n with h2 | h2
  · rw [reciprocalFactors_even h0 h2, commProb_cons, commProb_reciprocal (n / 2),
        commProb_odd (by decide)]
    simp [field, h2.two_dvd]
    norm_num
  · rw [reciprocalFactors_odd h1 h2, commProb_cons, commProb_reciprocal (n / 4 + 1)]
    have hn : Odd (n % 4) := by grind
    rw [commProb_odd (hn.mul h2), div_mul_div_comm, div_eq_div_iff] <;> norm_cast
    · grind [Nat.div_add_mod n 4, Odd]
    · positivity [hn.pos.ne']

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

Goal state before:
pp: B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
⊢ Subgroup.map (↑(FreeGroup.freeGroupCongr e)) (Subgroup.normalClosure M.relationsSet) =
    Subgroup.normalClosure (CoxeterMatrix.reindex e M).relationsSet

Tactic:
reindex_relationsSet,

Goal state after:
B : Type u_1
B' : Type u_2
M : CoxeterMatrix B
e : B ≃ B'
⊢ Subgroup.map (↑(FreeGroup.freeGroupCongr e)) (Subgroup.normalClosure M.relationsSet) =
    Subgroup.normalClosure (⇑(FreeGroup.freeGroupCongr e) '' M.relationsSet)
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
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
⊢ p w

Tactic:
let p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop :=
    fun w _ ↦ p w

Goal state after:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : W → Prop
w : W
one : p 1
mul_simple_left : ∀ (w : W) (i : B), p w → p (cs.simple i * w)
p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop := fun w x ↦ p w
⊢ p w
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
⊢ MonoidHom.mrange (FreeMonoid.lift fun p ↦ (f p.fst) p.snd) = ⨆ i, MonoidHom.mrange (f i)

Tactic:
FreeMonoid.mrange_lift,

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_4
inst✝ : Monoid N
f : (i : ι) → M i →* N
⊢ Submonoid.closure (range fun p ↦ (f p.fst) p.snd) = ⨆ i, MonoidHom.mrange (f i)
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: case hbc
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δ : (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[ℝ] ℝ := ⋯
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 := ⋯
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
⊢ (1 - δ * C)⁻¹ ≤ r' ^ 2

Tactic:
· exact inv_le_of_inv_le₀ (by positivity) hδ.le

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case cons
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m : M i
k : ι
g : M k
tail : Word M
h1 : tail.fstIdx ≠ some k
h2 : g ≠ 1
ih :
  ⟨i, m⟩ ∈
      (↑(consRecOn tail ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j_1 m w h1 h2 x ↦
              if ij : j = j_1 then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
              else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔
    ⟨i, m⟩ ∈ tail.toList.tail ∨ ¬i = j ∧ ∃ (h : ¬tail.toList = []), tail.toList.head h = ⟨i, m⟩
⊢ ⟨i, m⟩ ∈
      (↑(if ij : j = k then ⟨{ head := ⋯ ▸ g, tail := tail, fstIdx_ne := ⋯ }, ⋯⟩
            else ⟨{ head := 1, tail := cons g tail h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔
    ⟨i, m⟩ ∈ (cons g tail h1 h2).toList.tail ∨
      ¬i = j ∧ ∃ (h : ¬(cons g tail h1 h2).toList = []), (cons g tail h1 h2).toList.head h = ⟨i, m⟩

Tactic:
split_ifs with h

Goal state after:
case pos
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m : M i
k : ι
g : M k
tail : Word M
h1 : tail.fstIdx ≠ some k
h2 : g ≠ 1
ih :
  ⟨i, m⟩ ∈
      (↑(consRecOn tail ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j_1 m w h1 h2 x ↦
              if ij : j = j_1 then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
              else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔
    ⟨i, m⟩ ∈ tail.toList.tail ∨ ¬i = j ∧ ∃ (h : ¬tail.toList = []), tail.toList.head h = ⟨i, m⟩
h : j = k
⊢ ⟨i, m⟩ ∈ (↑⟨{ head := ⋯ ▸ g, tail := tail, fstIdx_ne := ⋯ }, ⋯⟩).tail.toList ↔
    ⟨i, m⟩ ∈ (cons g tail h1 h2).toList.tail ∨
      ¬i = j ∧ ∃ (h : ¬(cons g tail h1 h2).toList = []), (cons g tail h1 h2).toList.head h = ⟨i, m⟩

case neg
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m : M i
k : ι
g : M k
tail : Word M
h1 : tail.fstIdx ≠ some k
h2 : g ≠ 1
ih :
  ⟨i, m⟩ ∈
      (↑(consRecOn tail ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j_1 m w h1 h2 x ↦
              if ij : j = j_1 then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
              else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔
    ⟨i, m⟩ ∈ tail.toList.tail ∨ ¬i = j ∧ ∃ (h : ¬tail.toList = []), tail.toList.head h = ⟨i, m⟩
h : ¬j = k
⊢ ⟨i, m⟩ ∈ (↑⟨{ head := 1, tail := cons g tail h1 h2, fstIdx_ne := ⋯ }, ⋯⟩).tail.toList ↔
    ⟨i, m⟩ ∈ (cons g tail h1 h2).toList.tail ∨
      ¬i = j ∧ ∃ (h : ¬(cons g tail h1 h2).toList = []), (cons g tail h1 h2).toList.head h = ⟨i, m⟩
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
⊢ (m₁ = m₂ * if h : ∃ (h : ¬w.toList = []), (w.toList.head h).fst = j then ⋯ ▸ (w.toList.head ⋯).snd else 1) ↔
    (∃ m', w.toList.head? = some ⟨j, m'⟩ ∧ m₁ = m₂ * m') ∨ ¬w.fstIdx = some j ∧ m₁ = m₂

Tactic:
split_ifs with h

Goal state after:
case pos
ι : 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 : ∃ (h : ¬w.toList = []), (w.toList.head h).fst = j
⊢ m₁ = m₂ * ⋯ ▸ (w.toList.head ⋯).snd ↔
    (∃ m', w.toList.head? = some ⟨j, m'⟩ ∧ m₁ = m₂ * m') ∨ ¬w.fstIdx = some j ∧ m₁ = m₂

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 : ¬∃ (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₂
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
this : cs.lengthParity t = Multiplicative.ofAdd 1
⊢ Odd (cs.length t)

Tactic:
simpa [lengthParity_eq_ofAdd_length, ZMod.natCast_eq_one_iff_odd]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ∀ l ∈ _w₁✝.toList, l.snd ≠ 1
_w₂_ih✝ : ∀ l ∈ _w₂✝.toList, l.snd ≠ 1
⊢ ∀ l ∈ (_w₁✝.append _hne✝ _w₂✝).toList, l.snd ≠ 1

Tactic:
intro l h

Goal state after:
case append
ι : Type u_1
M : ι → Type u_2
inst✝¹ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝ : Monoid N
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
_w₁_ih✝ : ∀ l ∈ _w₁✝.toList, l.snd ≠ 1
_w₂_ih✝ : ∀ l ∈ _w₂✝.toList, l.snd ≠ 1
l : (i : ι) × M i
h : l ∈ (_w₁✝.append _hne✝ _w₂✝).toList
⊢ l.snd ≠ 1
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsAddTorsionFree M
s : ℕ+
⊢ Function.Injective fun m ↦ mk m s

Tactic:
by
  intro m n h
  simp_rw [mk_eq_mk_iff_smul_eq_smul] at h
  exact nsmul_right_injective (by simp) h

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ y * b = l * a * r * r'⁻¹

Tactic:
eq_mul_inv_iff_mul_eq

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b l : G
hl : l ∈ ↑H
r : G
hr : r ∈ ↑K
y : G
hy : y ∈ ↑H
r' : G
hr' : r' ∈ ↑K
hrx : y * b * r' = l * a * r
⊢ y * b * r' = l * a * r
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: case mp.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a✝ : Finite (Quotient ↑H ↑K)
val✝ : Fintype (Quotient ↑H ↑K)
⊢ ∃ I, ⋃ i ∈ I, quotToDoubleCoset H K i = Set.univ

Tactic:
exact ⟨Finset.univ, by simpa using! iUnion_quotToDoubleCoset _ _⟩

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
T : H.LeftTransversal
inst✝ : H.FiniteIndex
g : G
⊢ ϕ.transfer g = diff ϕ T (g • T)

Tactic:
transfer,

Goal state after:
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : ↥H →* A
T : H.LeftTransversal
inst✝ : H.FiniteIndex
g : G
⊢ { toFun := fun g ↦ diff ϕ default (g • default), map_one' := ⋯, map_mul' := ⋯ } g = diff ϕ T (g • T)
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
R S : Set G
hR : IsComplement (↑H) R
hR1 : 1 ∈ R
hS : closure S = ⊤
⊢ ↑(closure ((fun g ↦ g * (↑(hR.toRightFun g))⁻¹) '' (R * S))) * R = ⊤

Tactic:
let f : G → R := hR.toRightFun
  let U : Set G := (R * S).image fun g => g * (f g : G)⁻¹
  change (closure U : Set G) * R = ⊤
  refine top_le_iff.mp fun g _ => ?_
  refine closure_induction_right ?_ ?_ ?_ (eq_top_iff.mp hS (mem_top g))
  · exact ⟨1, (closure U).one_mem, 1, hR1, one_mul 1⟩
  · rintro - - s hs ⟨u, hu, r, hr, rfl⟩
    rw [show u * r * s = u * (r * s * (f (r * s) : G)⁻¹) * f (r * s) by group]
    refine Set.mul_mem_mul ((closure U).mul_mem hu ?_) (f (r * s)).coe_prop
    exact subset_closure ⟨r * s, Set.mul_mem_mul hr hs, rfl⟩
  · rintro - - s hs ⟨u, hu, r, hr, rfl⟩
    rw [show u * r * s⁻¹ = u * (f (r * s⁻¹) * s * r⁻¹)⁻¹ * f (r * s⁻¹) by group]
    refine Set.mul_mem_mul ((closure U).mul_mem hu ((closure U).inv_mem ?_)) (f (r * s⁻¹)).2
    refine subset_closure ⟨f (r * s⁻¹) * s, Set.mul_mem_mul (f (r * s⁻¹)).2 hs, ?_⟩
    rw [mul_right_inj, inv_inj, ← Subtype.coe_mk r hr, ← Subtype.ext_iff, Subtype.coe_mk]
    apply (isComplement_iff_existsUnique_mul_inv_mem.mp hR (f (r * s⁻¹) * s)).unique
      (hR.mul_inv_toRightFun_mem (f (r * s⁻¹) * s))
    rw [mul_assoc, ← inv_inv s, ← mul_inv_rev, inv_inv]
    exact hR.toRightFun_mul_inv_mem (r * s⁻¹)

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

Goal state before:
pp: G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type ?u.18
inst✝ : Monoid X
f : End (root' T) →* X
a : G
⊢ 1 = 𝟙 ()

Tactic:
id_as_one

Goal state after:
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type ?u.18
inst✝ : Monoid X
f : End (root' T) →* X
a : G
⊢ 1 = 1
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_1.nil
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a : WideSubquiver.toType (Symmetrify (Generators G)) T
⊢ 𝟙 (F'.obj (root' T)) = 1

Tactic:
id_as_one

Goal state after:
case refine_1.nil
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
x y : G
q : x ⟶ y
a : WideSubquiver.toType (Symmetrify (Generators G)) T
⊢ 1 = 1
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_2.e_5
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (root' T) →* X
hE : ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), E (loopOfHom T (of (↑a).hom)) = f a
x : End (root' T)
a b : Generators G
e : a ⟶ b
⊢ E (loopOfHom T (of e)) =
    if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩

Tactic:
split_ifs with h

Goal state after:
case pos
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (root' T) →* X
hE : ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), E (loopOfHom T (of (↑a).hom)) = f a
x : End (root' T)
a b : Generators G
e : a ⟶ b
h : e ∈ wideSubquiverSymmetrify T a b
⊢ E (loopOfHom T (of e)) = 1

case neg
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (root' T) →* X
hE : ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), E (loopOfHom T (of (↑a).hom)) = f a
x : End (root' T)
a b : Generators G
e : a ⟶ b
h : e ∉ wideSubquiverSymmetrify T a b
⊢ E (loopOfHom T (of e)) = f ⟨{ left := a, right := b, hom := e }, h⟩
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ center ↥(alternatingGroup α)
a : α
ha : a ∈ g.support
hab : g a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ g a
hd : d ≠ a ∧ d ≠ g a
k : Perm α := swap (g a) d * swap (g a) c
hka : k • a = a
hkga : k • g a = c
⊢ False

Tactic:
suffices k • (⟨g, hg⟩ : alternatingGroup α) • a ≠ c by
    apply this; simp [← hkga]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ center ↥(alternatingGroup α)
a : α
ha : a ∈ g.support
hab : g a ≠ a
c d : α
hcd : c ≠ d
hc : c ≠ a ∧ c ≠ g a
hd : d ≠ a ∧ d ≠ g a
k : Perm α := swap (g a) d * swap (g a) c
hka : k • a = a
hkga : k • g a = c
⊢ k • ⟨g, hg⟩ • a ≠ c
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
⊢ IsPretransitive G α

Tactic:
rw [← is_one_pretransitive_iff]

Goal state after:
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
⊢ IsMultiplyPretransitive G α 1
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ IsPretransitive G α

Tactic:
rw [← is_one_pretransitive_iff]

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
⊢ IsMultiplyPretransitive G α 1
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this✝ : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : normalClosure ↑(stabilizer G a) ≤ stabilizer G a
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
⊢ IsPretransitive ↥(stabilizer G a) ↥(ofStabilizer G a)

Tactic:
rw [← is_one_pretransitive_iff]

Goal state after:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this✝ : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : normalClosure ↑(stabilizer G a) ≤ stabilizer G a
b c : ↥(ofStabilizer G a)
hbc : b ≠ c
⊢ IsMultiplyPretransitive (↥(stabilizer G a)) (↥(ofStabilizer G a)) 1