mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.last.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver l.last.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
last : RelSeries.last L = { asIdeal := P, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
⊢ l.toList[0].asIdeal = comap (algebraMap R S) (RelSeries.toList L)[0].asIdeal

Tactic:
have : l.toList[0] = (PrimeSpectrum.comap (algebraMap R S)) L.toList[0] := by
        rw [List.getElem_map_rev (PrimeSpectrum.comap (algebraMap R S)),
          List.getElem_of_eq spec.symm _]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.last.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver l.last.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
last : RelSeries.last L = { asIdeal := P, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
this : l.toList[0] = PrimeSpectrum.comap (algebraMap R S) (RelSeries.toList L)[0]
⊢ l.toList[0].asIdeal = comap (algebraMap R S) (RelSeries.toList L)[0].asIdeal
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: case refine_2
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
⊢ Function.LeftInverse (fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩

Tactic:
intro d

Goal state after:
case refine_2
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
d : Derivation R A ↥I
⊢ (fun f ↦ derivationToSquareZeroOfLift I hI ↑f ⋯) ((fun d ↦ ⟨liftOfDerivationToSquareZero I hI d, ⋯⟩) d) = d
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: b : ℕ
⊢ factorizationLCMRight 0 b = 1

Tactic:
simp [factorizationLCMRight]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a : ℕ
⊢ a.factorizationLCMRight 0 = 1

Tactic:
simp [factorizationLCMRight]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ a.factorization.support
⊢ p ∈ (a.lcm b).factorization.support

Tactic:
mem_support_iff

Goal state after:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : a.factorization p ≠ 0
⊢ (a.lcm b).factorization p ≠ 0
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inl
b : ℕ
⊢ factorizationLCMRight 0 b ∣ b

Tactic:
simp [factorizationLCMRight]

Goal state after:
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : p ∈ b.factorization.support
⊢ p ∈ (a.lcm b).factorization.support

Tactic:
mem_support_iff

Goal state after:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
hp : b.factorization p ≠ 0
⊢ (a.lcm b).factorization p ≠ 0
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case pos
G : Type u
inst✝ : Monoid G
g : G
h : ExponentExists G
⊢ g ^ Nat.find h = 1

Tactic:
exact (Nat.find_spec h).2 g

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
p : ℕ
hp : Nat.Prime p
this : Fact (Nat.Prime p)
h : (exponent G).factorization p = 0
⊢ orderOf 1 = p ^ (exponent G).factorization p

Tactic:
by rw [h, pow_zero, orderOf_one]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
G : Type u_2
G' : Type u_3
a : α
inst✝³ : Group α
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : IsCyclic α
H : Subgroup α
this✝ : (a : Prop) → Decidable a
g : α
hg : ∀ (x : α), x ∈ zpowers g
hx✝ : ∃ x ∈ H, x ≠ 1
x✝¹ : α
hx₁ : x✝¹ ∈ H
hx₂ : x✝¹ ≠ 1
k✝ : ℤ
hk✝² : (fun x ↦ g ^ x) k✝ = x✝¹
hk✝¹ : g ^ k✝ = x✝¹
hex : ∃ n, 0 < n ∧ g ^ n ∈ H
x✝ : ↥H
x : α
hx : x ∈ H
k : ℤ
hk✝ : (fun x ↦ g ^ x) k = x
hk : g ^ k = x
hk₂ : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) ∈ H
hk₃ : g ^ (k % ↑(Nat.find hex)) ∈ H
hk₄ : k % ↑(Nat.find hex) = ↑(k % ↑(Nat.find hex)).natAbs
hk₅ : g ^ (k % ↑(Nat.find hex)).natAbs ∈ H
hk₆ : (k % ↑(Nat.find hex)).natAbs = 0
this : g ^ (↑(Nat.find hex) * (k / ↑(Nat.find hex))) = x
⊢ ↑((fun x ↦ ⟨g ^ Nat.find hex, ⋯⟩ ^ x) (k / ↑(Nat.find hex))) = ↑⟨x, hx⟩

Tactic:
by simpa [zpow_mul]

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Group α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : IsCyclic α
n : ℕ
hn0 : 0 < n
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ #{a | a ^ n = 1} ≤ #(↑(zpowers (g ^ (Fintype.card α / n.gcd (Fintype.card α))))).toFinset

Tactic:
gcongr
      intro x hx
      let ⟨m, hm⟩ := show x ∈ Submonoid.powers g from mem_powers_iff_mem_zpowers.2 <| hg x
      refine Set.mem_toFinset.2 ⟨(m / (Fintype.card α / Nat.gcd n (Fintype.card α)) : ℕ), ?_⟩
      dsimp only at ⊢ hm
      rw [zpow_natCast, ← pow_mul, Nat.mul_div_cancel_left', hm]
      refine Nat.dvd_of_mul_dvd_mul_right (gcd_pos_of_pos_left (Fintype.card α) hn0) ?_
      conv_lhs =>
        rw [Nat.div_mul_cancel (Nat.gcd_dvd_right _ _), ← Nat.card_eq_fintype_card,
          ← orderOf_eq_card_of_forall_mem_zpowers hg]
      exact orderOf_dvd_of_pow_eq_one <| by simpa [pow_mul, hm] using (mem_filter.1 hx).2

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝ : Group α
h : IsCyclic α
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ orderOf g = Nat.card α

Tactic:
← card_zpowers g,

Goal state after:
case h
α : Type u_1
inst✝ : Group α
h : IsCyclic α
g : α
hg : ∀ (x : α), x ∈ zpowers g
⊢ Nat.card ↥(zpowers g) = Nat.card α
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
q : ℕ
hpq : p ∣ q
hp : ∀ (g : G), ∃ k, orderOf g ∣ p ^ k
⊢ ∀ (g : G), ∃ k, orderOf g ∣ q ^ k

Tactic:
exact fun g ↦ (hp g).imp fun k hk ↦ hk.trans <| pow_dvd_pow_of_dvd hpq k

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
h : p₁.Coprime p₂
g : G
hg₁ : g ∈ H₁
hg₂ : g ∈ H₂
k₁ : ℕ
hk₁ : ⟨g, hg₁⟩ ^ p₁ ^ k₁ = 1
⊢ g = 1

Tactic:
have hg₁ := Subgroup.orderOf_mk g _ ▸ orderOf_dvd_of_pow_eq_one hk₁

Goal state after:
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ ↥H₁
hH₂ : IsPGroup p₂ ↥H₂
h : p₁.Coprime p₂
g : G
hg₁✝ : g ∈ H₁
hg₂ : g ∈ H₂
k₁ : ℕ
hk₁ : ⟨g, hg₁✝⟩ ^ p₁ ^ k₁ = 1
hg₁ : orderOf g ∣ p₁ ^ k₁
⊢ g = 1
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝¹ : Fintype ι
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
m : (i : ι) → M i
i : ι
⊢ exponent (M i) ∣ univ.lcm fun x ↦ exponent (M x)

Tactic:
exact Finset.dvd_lcm (mem_univ i)

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
z : G
hy : z * g⁻¹ * x = g⁻¹ * (x * (g * (z * g⁻¹)))
hz : z ∈ ↑↑P
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) z * x =
    x * ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) z

Tactic:
eq_inv_mul_iff_mul_eq,

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
x g : G
hx : x ∈ centralizer ↑P
h1 : ↑P ≤ centralizer ↑(zpowers x)
z : G
hy : g * (z * g⁻¹ * x) = x * (g * (z * g⁻¹))
hz : z ∈ ↑↑P
⊢ ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) z * x =
    x * ((MulDistribMulAction.toMonoidEnd (MulAut G) G) (MulAut.conj g)) z
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
⊢ IsAddCyclic A ↔ Nonempty (A ≃+o ℤ)

Tactic:
refine ⟨?_, fun ⟨e⟩ ↦ e.isAddCyclic.mpr inferInstance⟩

Goal state after:
A : Type u_4
inst✝³ : AddCommGroup A
inst✝² : LinearOrder A
inst✝¹ : IsOrderedAddMonoid A
inst✝ : Nontrivial A
⊢ IsAddCyclic A → Nonempty (A ≃+o ℤ)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
f₁ f₂ : G →* G'
H : f₁ g = f₂ g
x : G
n : ℤ
hn : g ^ n = x
⊢ f₁ x = f₂ x

Tactic:
rw [← hn, map_zpow, map_zpow, H]

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : ⨆ i ∈ s, f i = ⊤
i : ι
hi : i ∈ s
h : IsAtomistic ↑(Iic (f i))
u : Set ↑(Iic (f i))
hu : ⊤ = sSup u
hu' : ∀ a ∈ u, IsAtom a
⊢ ∃ t, f i = sSup t ∧ ∀ a ∈ t, IsAtom a

Tactic:
refine ⟨(↑) '' u, ?_, ?_⟩

Goal state after:
case refine_1
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : ⨆ i ∈ s, f i = ⊤
i : ι
hi : i ∈ s
h : IsAtomistic ↑(Iic (f i))
u : Set ↑(Iic (f i))
hu : ⊤ = sSup u
hu' : ∀ a ∈ u, IsAtom a
⊢ f i = sSup (Subtype.val '' u)

case refine_2
ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h' : ⨆ i ∈ s, f i = ⊤
i : ι
hi : i ∈ s
h : IsAtomistic ↑(Iic (f i))
u : Set ↑(Iic (f i))
hu : ⊤ = sSup u
hu' : ∀ a ∈ u, IsAtom a
⊢ ∀ a ∈ Subtype.val '' u, IsAtom a
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := (Nat.card G).primeFactors
P : (p : ℕ) → Sylow p G := default
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ ∏ p, Nat.card ↥↑(P ↑p) = ∏ p, ↑p ^ (Nat.card G).factorization ↑p

Tactic:
congr 1 with ⟨p, hp⟩
        exact @card_eq_multiplicity _ _ _ p ⟨Nat.prime_of_mem_primeFactors hp⟩ (P p)

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsSemisimpleModule R ↥N
⊢ Subsingleton (Submodule R ↥N) ∨ ∃ m ≤ N, IsSimpleModule R ↥m

Tactic:
← subsingleton_iff_bot_eq_top

Goal state after:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsSemisimpleModule R ↥N
⊢ ⊥ = ⊤ ∨ ∃ m ≤ N, IsSimpleModule R ↥m
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : iSupIndep Subtype.val
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ iSup Subtype.val = SupSet.sSup s

Tactic:
sSup_eq_iSup'

Goal state after:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
s : Set (Submodule R M)
ind : iSupIndep Subtype.val
sSup : SupSet.sSup s = ⊤
simple : ∀ m ∈ s, IsSimpleModule R ↥m
⊢ iSup Subtype.val = ⨆ a, ↑a
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Ring S
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hS : IsSemisimpleRing S
this✝ : Module (R × S) R := Module.compHom R (RingHom.fst R S)
hR : IsSemisimpleModule (R × S) R
this : Module (R × S) S := Module.compHom S (RingHom.snd R S)
_e₁ : R →ₛₗ[RingHom.fst R S] R :=
  let __src := AddMonoidHom.id R;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
_e₂ : S →ₛₗ[RingHom.snd R S] S :=
  let __src := AddMonoidHom.id S;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleRing (R × S)

Tactic:
rw [IsSemisimpleRing, ← _e₂.isSemisimpleModule_iff_of_bijective Function.bijective_id] at hS

Goal state after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Ring S
M : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module R M
m : Submodule R M
N : Type u_5
inst✝¹ : AddCommGroup N
inst✝ : Module R N
this✝ : Module (R × S) R := Module.compHom R (RingHom.fst R S)
hR : IsSemisimpleModule (R × S) R
this : Module (R × S) S := Module.compHom S (RingHom.snd R S)
hS : IsSemisimpleModule (R × S) S
_e₁ : R →ₛₗ[RingHom.fst R S] R :=
  let __src := AddMonoidHom.id R;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
_e₂ : S →ₛₗ[RingHom.snd R S] S :=
  let __src := AddMonoidHom.id S;
  { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ }
⊢ IsSemisimpleRing (R × S)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case succ
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r •
        (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
          (single R j m) =
      single R (n + j) (r • m)
r : R
j : ℕ
m : M
⊢ r •
      (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
        ((↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)) (single R j m)) =
    r •
      (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
        (single R (1 + j) m)

Tactic:
congr 2

Goal state after:
case succ.e_a.e_a
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r •
        (⇑(↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)))^[n]
          (single R j m) =
      single R (n + j) (r • m)
r : R
j : ℕ
m : M
⊢ (↑(coeffLinearEquiv R R).symm ∘ₗ Finsupp.lmapDomain M R Nat.succ ∘ₗ ↑(coeffLinearEquiv R R)) (single R j m) =
    single R (1 + j) m
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ N ≤ comap ((LinearMap.lsmul R M) 1) (I • span R s)

Tactic:
rw [hs]
      intro n hn
      rw [mem_comap]
      change (1 : R) • n ∈ I • N
      rw [one_smul]
      exact hin hn

Goal state after:
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0

Tactic:
have H : ∃ r : R, r - 1 ∈ I ∧ N ≤ (I • span R s).comap (LinearMap.lsmul R M r) ∧ s ⊆ N := by
    refine ⟨1, ?_, ?_, ?_⟩
    · rw [sub_self]
      exact I.zero_mem
    · rw [hs]
      intro n hn
      rw [mem_comap]
      change (1 : R) • n ∈ I • N
      rw [one_smul]
      exact hin hn
    · rw [← span_le, hs]

Goal state after:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hin : N ≤ I • N
s : Set M
hfs : s.Finite
hs : span R s = N
H : ∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N
⊢ ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
q : PolynomialModule R M
r : R
⊢ (eval r) (p • q) = Polynomial.eval r p • (eval r) q

Tactic:
by
  induction q using induction_linear with
  | zero => rw [smul_zero, map_zero, smul_zero]
  | add f g e₁ e₂ => rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
  | single i m =>
    induction p using Polynomial.induction_on' with
    | add _ _ e₁ e₂ => rw [add_smul, map_add, Polynomial.eval_add, e₁, e₂, add_smul]
    | monomial => simp only [monomial_smul_single, Polynomial.eval_monomial, eval_single]; module

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ↑(∏ x ∈ S, ⋯.choose) ∈ ↑⊤.annihilator

Tactic:
rw [Submonoid.coe_finsetProd, SetLike.mem_coe, ← hS, mem_annihilator_span]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
hM : IsTorsion R M
S : Finset M
hS : span R ↑S = ⊤
⊢ ∀ (n : ↑↑S), (∏ i ∈ S, ↑⋯.choose) • ↑n = 0
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
⊢ x ∈ ↑(torsion R M) ↔ x ∈ {x | ∃ x_1, (∀ n ∈ R ∙ x, x_1 • n = 0) ∧ x_1 ≠ 0}

Tactic:
mem_span_singleton

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : M
⊢ x ∈ ↑(torsion R M) ↔ x ∈ {x | ∃ x_1, (∀ (n : M), (∃ a, a • x = n) → x_1 • n = 0) ∧ x_1 ≠ 0}
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: 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₀ : ℕ
H :
  ∀ (i : ℕ), single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l : ↑(⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)) →₀ ↥(reesAlgebra I)
hl : ((Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l).coeff (n + 1) = x
⊢ ∀ c ∈ l.support, (fun a₁ b ↦ (b • ↑a₁).coeff (n + 1)) c (l c) ∈ I • F.N n

Tactic:
rintro ⟨_, _, ⟨n', rfl⟩, _, ⟨hn', rfl⟩, m, hm, rfl⟩ -

Goal state after:
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₀ : ℕ
H :
  ∀ (i : ℕ), single R i '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l : ↑(⋃ i, ⋃ (_ : i ≤ n₀), single R i '' ↑(F.N i)) →₀ ↥(reesAlgebra I)
hl : ((Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l).coeff (n + 1) = x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(F.N n')
⊢ (fun a₁ b ↦ (b • ↑a₁).coeff (n + 1)) ⟨single R n' m, ⋯⟩ (l ⟨single R n' m, ⋯⟩) ∈ I • F.N n
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj n).map ((η F).app X) = (μ F (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X

Tactic:
rw [← cancel_mono ((F.obj n).map ((ε F).app X)), ← Functor.map_comp]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u_1
D : Type u_2
J : Type u_4
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : C ⥤ D
j : J
⊢ F.map (e.hom j) ≫ F.map (e.inv j) = 𝟙 (F.obj (X j))

Tactic:
← F.map_comp,

Goal state after:
C : Type u_1
D : Type u_2
J : Type u_4
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : C ⥤ D
j : J
⊢ F.map (e.hom j ≫ e.inv j) = 𝟙 (F.obj (X j))
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u_1
D : Type u_2
J : Type u_4
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : C ⥤ D
j : J
⊢ F.map (e.inv j) ≫ F.map (e.hom j) = 𝟙 (F.obj (Y j))

Tactic:
← F.map_comp,

Goal state after:
C : Type u_1
D : Type u_2
J : Type u_4
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : C ⥤ D
j : J
⊢ F.map (e.inv j ≫ e.hom j) = 𝟙 (F.obj (Y j))
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
X Y✝ : GradedObject J C
e : X ≅ Y✝
F : C ⥤ D ⥤ E
j : J
Y : D
⊢ (F.map (e.hom j) ≫ F.map (e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)

Tactic:
← F.map_comp,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
X Y✝ : GradedObject J C
e : X ≅ Y✝
F : C ⥤ D ⥤ E
j : J
Y : D
⊢ (F.map (e.hom j ≫ e.inv j)).app Y = 𝟙 ((F.obj (X j)).obj Y)
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
X Y✝ : GradedObject J C
e : X ≅ Y✝
F : C ⥤ D ⥤ E
j : J
Y : D
⊢ (F.map (e.inv j) ≫ F.map (e.hom j)).app Y = 𝟙 ((F.obj (Y✝ j)).obj Y)

Tactic:
← F.map_comp,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
J : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
X Y✝ : GradedObject J C
e : X ≅ Y✝
F : C ⥤ D ⥤ E
j : J
Y : D
⊢ (F.map (e.inv j ≫ e.hom j)).app Y = 𝟙 ((F.obj (Y✝ j)).obj Y)
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 : ι
r : c.Rel i j
⊢ C.dTo j = (C.xPrevIso r).hom ≫ C.d i j

Tactic:
by
  obtain rfl := c.prev_eq' r
  exact (Category.id_comp _).symm

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : Preadditive V
W : Type u_2
inst✝⁶ : Category.{v_1, u_2} W
inst✝⁵ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁴ : Category.{v_2, u_3} W₁
inst✝³ : Category.{v_3, u_4} W₂
inst✝² : HasZeroMorphisms W₁
inst✝¹ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C✝ D : HomologicalComplex V c✝
f : C✝ ⟶ D
i✝ : ι
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
c : ComplexShape ι
C : HomologicalComplex W₁ c
i j k : ι
x✝¹ : c.Rel i j
x✝ : c.Rel j k
⊢ F.map (C.d i j) ≫ F.map (C.d j k) = 0

Tactic:
← F.map_comp,

Goal state after:
ι : Type u_1
V : Type u
inst✝⁸ : Category.{v, u} V
inst✝⁷ : Preadditive V
W : Type u_2
inst✝⁶ : Category.{v_1, u_2} W
inst✝⁵ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁴ : Category.{v_2, u_3} W₁
inst✝³ : Category.{v_3, u_4} W₂
inst✝² : HasZeroMorphisms W₁
inst✝¹ : HasZeroMorphisms W₂
c✝ : ComplexShape ι
C✝ D : HomologicalComplex V c✝
f : C✝ ⟶ D
i✝ : ι
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
c : ComplexShape ι
C : HomologicalComplex W₁ c
i j k : ι
x✝¹ : c.Rel i j
x✝ : c.Rel j k
⊢ F.map (C.d i j ≫ C.d j k) = 0