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

Goal state before:
pp: case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ (exponent G).primeFactorsList.Subperm (orderOf t).primeFactorsList

Tactic:
rw [List.subperm_ext_iff]

Goal state after:
case h
G : Type u
inst✝ : CommMonoid G
hG : ExponentExists G
he : exponent G ≠ 0
hne : (Set.range orderOf).Nonempty
hfin : (Set.range orderOf).Finite
t : G
ht : orderOf t = sSup (Set.range orderOf)
⊢ ∀ x ∈ (exponent G).primeFactorsList,
    List.count x (exponent G).primeFactorsList ≤ List.count x (orderOf t).primeFactorsList
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
n : ℕ
hn : Nat.card G = p ^ (n + 1)
⊢ p ^ (n + 1) = p * p ^ n

Tactic:
pow_succ'

Goal state after:
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h✝ : Finite G
n : ℕ
hn : Nat.card G = p ^ (n + 1)
⊢ p * p ^ n = p * p ^ n
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ exponent G = sSup (Set.range fun g ↦ orderOf g)

Tactic:
csSup_eq_of_forall_le_of_forall_lt_exists_gt (Set.range_nonempty _)

Goal state after:
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ exponent G = ?m.48

case H
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ a ∈ Set.range fun g ↦ orderOf g, a ≤ ?m.48

case H'
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ w < ?m.48, ∃ a ∈ Set.range fun g ↦ orderOf g, w < a

G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ℕ
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p ↥H
hK : IsPGroup p ↥K
inst✝ : K.Normal
⊢ IsPGroup p ↥(H ⊔ K)

Tactic:
by
  rw [← QuotientGroup.ker_mk' K, ← Subgroup.comap_map_eq]
  apply (hH.map (QuotientGroup.mk' K)).comap_of_ker_isPGroup
  rwa [QuotientGroup.ker_mk']

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case pos
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : H = ⊤
h1 : Nat.card ↥H = 0
⊢ P ≤ ⊤ ∨ Disjoint ⊤ P

Tactic:
exact Or.inl le_top

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
g : G
P : Sylow p G
⊢ g • P = P ↔ g ∈ normalizer ↑P

Tactic:
eq_comm,

Goal state after:
p : ℕ
G : Type u_1
inst✝ : Group G
g : G
P : Sylow p G
⊢ P = g • P ↔ g ∈ normalizer ↑P
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : FG G
inst✝ : FG H
f : G →* H
hf : Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ rank H ≤ (Finset.image (⇑f) S).card

pp: G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : FG G
inst✝ : FG H
f : G →* H
hf : Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ (Finset.image (⇑f) S).card ≤ rank G

Tactic:
· apply rank_le
    rw [Finset.coe_image, ← MonoidHom.map_closure, hS2, Subgroup.map_top_of_surjective f hf]

Goal state after:
G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : FG G
inst✝ : FG H
f : G →* H
hf : Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ (Finset.image (⇑f) S).card ≤ rank G
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := Fintype.card α
hc0 : 0 < c
⊢ #{a | orderOf a = d} = φ d

Tactic:
apply card_orderOf_eq_totient_aux₁ hn hd

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
hd : d ∣ Fintype.card α
c : ℕ := ⋯
hc0 : 0 < c
⊢ 0 < #{a | orderOf a = d}
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ (i - ↑n * (i / ↑n)) • g = i • g

Tactic:
eq_comm,

Goal state after:
G : Type u_2
inst✝ : AddGroup G
g : G
hg : ∀ (x : G), x ∈ zmultiples g
n : ℕ
hn : Nat.card G = n
i : ℤ
⊢ i • g = (i - ↑n * (i / ↑n)) • g
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
inst✝ : Finite G
d : ℕ
h : (powMonoidHom d).ker.index ≠ 0
⊢ Nat.card G = (Nat.card G).gcd d * (Nat.card G / (Nat.card G).gcd d)

Tactic:
Nat.mul_div_cancel'

Goal state after:
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
inst✝ : Finite G
d : ℕ
h : (powMonoidHom d).ker.index ≠ 0
⊢ Nat.card G = Nat.card G

G : Type u_2
inst✝² : CommGroup G
inst✝¹ : IsCyclic G
inst✝ : Finite G
d : ℕ
h : (powMonoidHom d).ker.index ≠ 0
⊢ (Nat.card G).gcd d ∣ Nat.card G
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
x y : G
⊢ Classical.choose ⋯ ≡ Classical.choose ⋯ + Classical.choose ⋯ [ZMOD ↑(orderOf g)]

Tactic:
rw [← zpow_eq_zpow_iff_modEq, zpow_add]

Goal state after:
α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
x y : G
⊢ g ^ Classical.choose ⋯ = g ^ Classical.choose ⋯ * g ^ Classical.choose ⋯
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝ : Group G
s : Subgroup G
t : Set (G ⧸ s)
⊢ Nat.card ↑(mk ⁻¹' t) = Nat.card ↥s * Nat.card ↑t

Tactic:
← Nat.card_prod,

Goal state after:
G : Type u
inst✝ : Group G
s : Subgroup G
t : Set (G ⧸ s)
⊢ Nat.card ↑(mk ⁻¹' t) = Nat.card (↥s × ↑t)
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
this : ↥(H.subgroupOf (normalizer ↑H)) ≃ ↥H
⊢ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) * p ^ n ≡ Nat.card (G ⧸ H) * p ^ n [MOD p ^ (n + 1)]

Tactic:
pow_succ'

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
H : Subgroup G
hH : Nat.card ↥H = p ^ n
this : ↥(H.subgroupOf (normalizer ↑H)) ≃ ↥H
⊢ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) * p ^ n ≡ Nat.card (G ⧸ H) * p ^ n [MOD p * p ^ n]
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
hm' : p ∣ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H))
x : ↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer ↑H))
y : G
hy : y ∈ H
⊢ 1 = ↑⟨y, ⋯⟩

Tactic:
eq_comm,

Goal state after:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)) % p
hm' : p ∣ Nat.card (↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H))
x : ↥(normalizer ↑H) ⧸ H.subgroupOf (normalizer ↑H)
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf (normalizer ↑H))
y : G
hy : y ∈ H
⊢ ↑⟨y, ⋯⟩ = 1
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2.mp
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
⊢ ((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤

Tactic:
refine ⟨ih.mp ⟨Pi.single h.choose ⟨μ a, ?a1⟩ + fun i => ⟨μ i, ?a2⟩, ?a3⟩, fun b hb ab => ?a4⟩

Goal state after:
case a3
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
⊢ ∑ i ∈ t, ↑((Pi.single (Exists.choose h) ⟨↑(μ a), ?a1⟩ + fun i ↦ ?m.176) i) = 1

case a4
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
b : ι
hb : b ∈ ↑t
ab : a ≠ b
⊢ I a ⊔ I b = ⊤

case a1
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
⊢ ↑(μ a) ∈ ⨅ j ∈ t, ⨅ (_ : j ≠ Exists.choose h), I j

case a2
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
i : ι
⊢ ↑(μ i) ∈ ⨅ j ∈ t, ⨅ (_ : j ≠ i), I j
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x y : X
hx : x ∈ s
hy : y ∈ s
⊢ x ≤ y ∨ y ≤ x

Tactic:
rcases Set.mem_range.1 hx with ⟨i, rfl⟩
  rcases Set.mem_range.1 hy with ⟨j, rfl⟩
  rw [s.strictMono.le_iff_le, s.strictMono.le_iff_le]
  exact le_total i j

Goal state after:
Module: Mathlib.RingTheory.Coprime.Ideal

Goal state before:
pp: case refine_2.mp
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
⊢ (∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1) →
    ((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤

pp: case refine_2.mpr
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
⊢ (((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤) →
    ∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1

Tactic:
· rintro ⟨μ, hμ⟩
    rw [Finset.sum_cons] at hμ
    refine ⟨ih.mp ⟨Pi.single h.choose ⟨μ a, ?a1⟩ + fun i => ⟨μ i, ?a2⟩, ?a3⟩, fun b hb ab => ?a4⟩
    case a1 =>
      have := Submodule.coe_mem (μ a)
      rw [mem_iInf] at this ⊢
      --for some reason `simp only [mem_iInf]` times out
      intro i
      specialize this i
      rw [mem_iInf, mem_iInf] at this ⊢
      intro hi _
      apply this (Finset.subset_cons _ hi)
      rintro rfl
      exact hat hi
    case a2 =>
      have := Submodule.coe_mem (μ i)
      simp only [mem_iInf] at this ⊢
      intro j hj ij
      exact this _ (Finset.subset_cons _ hj) ij
    case a3 =>
      rw [← @if_pos _ _ h.choose_spec R (μ a) 0, ← Finset.sum_pi_single', ← Finset.sum_add_distrib]
        at hμ
      convert! hμ
      rename_i i _
      rw [Pi.add_apply, Submodule.coe_add, Submodule.coe_mk]
      by_cases hi : i = h.choose
      · rw [hi, Pi.single_eq_same, Pi.single_eq_same, Submodule.coe_mk]
      · rw [Pi.single_eq_of_ne hi, Pi.single_eq_of_ne hi, Submodule.coe_zero]
    case a4 =>
      rw [eq_top_iff_one, Submodule.mem_sup]
      rw [add_comm] at hμ
      refine ⟨_, ?_, _, ?_, hμ⟩
      · refine sum_mem _ fun x hx => ?_
        have := Submodule.coe_mem (μ x)
        simp only [mem_iInf] at this
        apply this _ (Finset.mem_cons_self _ _)
        rintro rfl
        exact hat hx
      · have := Submodule.coe_mem (μ a)
        simp only [mem_iInf] at this
        exact this _ (Finset.subset_cons _ hb) ab.symm

Goal state after:
case refine_2.mpr
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
⊢ (((↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤) ∧ ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤) →
    ∃ μ, ∑ i ∈ Finset.cons a t hat, ↑(μ i) = 1
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
⊢ Iso (((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun i.castSucc, ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun i.succ)
    (((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun (e i).castSucc, ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun (e i).succ)

Tactic:
dsimp only [e]

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x₁ x₂ y₁ y₂ : X
hsat₁ : IsMaximal (last s) x₁
hsat₂ : IsMaximal (last s) x₂
hsaty₁ : IsMaximal (snoc s x₁ hsat₁).last y₁
hsaty₂ : IsMaximal (snoc s x₂ hsat₂).last y₂
hr₁ : Iso (last s, x₁) (x₂, y₂)
hr₂ : Iso (x₁, y₁) (last s, x₂)
e : Fin (s.length + 1 + 1) ≃ Fin (s.length + 1 + 1) := Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc
h1 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ (Fin.last s.length).castSucc
h2 : ∀ {i : Fin s.length}, i.castSucc.castSucc ≠ Fin.last (s.length + 1)
i : Fin ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).length
⊢ Iso (((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun i.castSucc, ((snoc s x₁ hsat₁).snoc y₁ hsaty₁).toFun i.succ)
    (((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun
        ((Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc) i).castSucc,
      ((snoc s x₂ hsat₂).snoc y₂ hsaty₂).toFun
        ((Equiv.swap (Fin.last (s.length + 1)) (Fin.last s.length).castSucc) i).succ)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hv : iSupIndep fun i ↦ R ∙ v i
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
⊢ LinearIndependent R v

Tactic:
by
  refine linearIndependent_iff_eq_zero_of_smul_mem_span.mpr fun i r hi => ?_
  replace hv := iSupIndep_def.mp hv i
  simp only [iSup_subtype', ← Submodule.span_range_eq_iSup (ι := Subtype _), disjoint_iff] at hv
  have : r • v i ∈ (⊥ : Submodule R M) := by
    rw [← hv, Submodule.mem_inf]
    refine ⟨Submodule.mem_span_singleton.mpr ⟨r, rfl⟩, ?_⟩
    convert! hi
    ext
    simp
  rw [← Submodule.mem_bot R, ← h_ne_zero i]
  simpa using this

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
a✝ b✝ : R[X]
hf : a✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
hg : b✝ ∈ {f | ∀ (i : ℕ), f.coeff i ∈ I ^ i}
i : ℕ
⊢ a✝.coeff i + b✝.coeff i ∈ I ^ i

Tactic:
exact Ideal.add_mem _ (hf i) (hg i)

Goal state after:
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: case succ
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I ^ (n + 1)
⊢ (monomial (n + 1)) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)

Tactic:
pow_succ'

Goal state after:
case succ
R : Type u
inst✝ : CommRing R
I : Ideal R
n : ℕ
hn : ∀ {r : R}, r ∈ I ^ n → (monomial n) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
r : R
hr : r ∈ I * I ^ n
⊢ (monomial (n + 1)) r ∈ Algebra.adjoin R ↑(Submodule.map (monomial 1) I)
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
⊢ (∀ n ≥ n₀, I • F.N n = F.N (n + 1)) →
    ∀ (i : ℕ),
      single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))

Tactic:
let F' := Submodule.span (reesAlgebra I) (⋃ i ≤ n₀, single R i '' (F.N i : Set M))

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))
⊢ (∀ n ≥ n₀, I • F.N n = F.N (n + 1)) →
    ∀ (i : ℕ),
      single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case neg.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this : ∀ i ≤ n₀, single R i '' ↑(F.N i) ⊆ ↑F'
j : ℕ
hj : single R j '' ↑(F.N j) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • F.N j)
r : R
hr : r ∈ I
m' : M
hm' : m' ∈ F.N j
⊢ single R (1 + j) (r • m') ∈ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))

Tactic:
← monomial_smul_single

Goal state after:
case neg.refine_1
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this : ∀ i ≤ n₀, single R i '' ↑(F.N i) ⊆ ↑F'
j : ℕ
hj : single R j '' ↑(F.N j) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • F.N j)
r : R
hr : r ∈ I
m' : M
hm' : m' ∈ F.N j
⊢ (monomial 1) r • single R j m' ∈ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case refine_2
R : Type u
S : Type v
S' : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : CommSemiring S'
inst✝⁶ : Algebra S' R
inst✝⁵ : Algebra S S'
inst✝⁴ : IsScalarTower S S' R
I : Ideal R
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
⊢ Submodule.restrictScalars R (I₁ • ⊤) ≤
    Submodule.comap (f.toLinearMap.restrict h) (Submodule.restrictScalars R (I₂ • ⊤))

Tactic:
intro x hx
    rw [Submodule.restrictScalars_mem] at hx
    refine Submodule.smul_induction_on hx ?_ (fun _ _ ↦ add_mem)
    rintro a ha ⟨b, hb⟩ -
    simp only [SetLike.mk_smul_mk, smul_eq_mul, Submodule.mem_comap, Submodule.restrictScalars_mem]
    convert!
      (Submodule.smul_mem_smul (M := I₂) (r := f a) (n := ⟨f b, h hb⟩) (h ha)
        (Submodule.mem_top)) using 1
    ext
    exact map_mul f a b

Goal state after:
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set ↥(maximalIdeal R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span R s = ⊤
⊢ Submodule.map (maximalIdeal R).toCotangent (Submodule.span R s) = ⊤

Tactic:
hs_span,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set ↥(maximalIdeal R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span R s = ⊤
⊢ Submodule.map (maximalIdeal R).toCotangent ⊤ = ⊤
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set (CotangentSpace R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span (ResidueField R) s = ⊤
⊢ Submodule.restrictScalars R (Submodule.span (ResidueField R) s) = ⊤

Tactic:
hs_span,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set (CotangentSpace R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span (ResidueField R) s = ⊤
⊢ Submodule.restrictScalars R ⊤ = ⊤
Module: Mathlib.Algebra.Category.ModuleCat.Projective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
P : ModuleCat R
inst✝⁵ : Small.{v, u} R
inst✝⁴ : CategoryTheory.Projective P
M✝ N✝ : Type v
inst✝³ : AddCommGroup M✝
inst✝² : AddCommGroup N✝
inst✝¹ : Module R M✝
inst✝ : Module R N✝
f : M✝ →ₗ[R] N✝
g : ↑P →ₗ[R] N✝
s : Function.Surjective ⇑f
⊢ ∃ h, f ∘ₗ h = g

Tactic:
have : Epi (↟f) := (ModuleCat.epi_iff_surjective (↟f)).mpr s

Goal state after:
R : Type u
inst✝⁶ : Ring R
P : ModuleCat R
inst✝⁵ : Small.{v, u} R
inst✝⁴ : CategoryTheory.Projective P
M✝ N✝ : Type v
inst✝³ : AddCommGroup M✝
inst✝² : AddCommGroup N✝
inst✝¹ : Module R M✝
inst✝ : Module R N✝
f : M✝ →ₗ[R] N✝
g : ↑P →ₗ[R] N✝
s : Function.Surjective ⇑f
this : Epi (↟f)
⊢ ∃ h, f ∘ₗ h = g
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a₁ a₂ a₃ : A
⊢ shiftFunctorAdd C (a₁ + a₂) a₃ ≪≫
      isoWhiskerRight (shiftFunctorAdd C a₁ a₂) (shiftFunctor C a₃) ≪≫
        (shiftFunctor C a₁).associator (shiftFunctor C a₂) (shiftFunctor C a₃) =
    shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯ ≪≫ (shiftFunctor C a₁).isoWhiskerLeft (shiftFunctorAdd C a₂ a₃)

Tactic:
ext X
  simpa [shiftFunctorAdd'_eq_shiftFunctorAdd]
    using NatTrans.congr_app (congr_arg Iso.hom
      (shiftFunctorAdd'_assoc C a₁ a₂ a₃ _ _ _ rfl rfl rfl)) X

Goal state after:
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j : ι
rij rij' : c.Rel i j
⊢ eqToHom ⋯ ≫ C.d i j = C.d i j

Tactic:
simp only [eqToHom_refl, id_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
⊢ (singleObjXIsoOfEq c j A j ⋯).hom ≫ φ ≫ 𝟙 (K.X j) = (singleObjXSelf c j A).hom ≫ φ

Tactic:
comp_id

Goal state after:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
φ : A ⟶ K.X j
hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0
⊢ (singleObjXIsoOfEq c j A j ⋯).hom ≫ φ = (singleObjXSelf c j A).hom ≫ φ