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

Goal state before:
pp: P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
⊢ S.Nonempty → ⊤ ∉ S → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds S

Tactic:
hS₂

Goal state after:
P : Type u_1
inst✝¹ : LE P
inst✝ : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun x1 x2 ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
⊢ ⊤ ∉ S → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds S
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case sdiff
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
P : (s : Set X) → IsConstructible s → Prop
inst✝¹ : QuasiSeparatedSpace X
ι : Type u_4
inst✝ : Nonempty ι
b : ι → Set X
basis : IsTopologicalBasis (range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
sdiff : ∀ (i : ι) (s : Set ι) (hs : s.Finite), P (b i \ ⋃ j ∈ s, b j) ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), P s hs → P t ht → P (s ∪ t) ⋯
s U : Set X
hU : U ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
V : Set X
hV : V ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
⊢ P (U \ V) ⋯

Tactic:
have := isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis _ basis isCompact_basis

Goal state after:
case sdiff
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
P : (s : Set X) → IsConstructible s → Prop
inst✝¹ : QuasiSeparatedSpace X
ι : Type u_4
inst✝ : Nonempty ι
b : ι → Set X
basis : IsTopologicalBasis (range b)
isCompact_basis : ∀ (i : ι), IsCompact (b i)
sdiff : ∀ (i : ι) (s : Set ι) (hs : s.Finite), P (b i \ ⋃ j ∈ s, b j) ⋯
union : ∀ (s : Set X) (hs : IsConstructible s) (t : Set X) (ht : IsConstructible t), P s hs → P t ht → P (s ∪ t) ⋯
s U : Set X
hU : U ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
V : Set X
hV : V ∈ {U | IsOpen[inst✝³] U ∧ IsRetrocompact U}
this : ∀ (U : Set X), IsCompact U ∧ IsOpen[inst✝³] U ↔ ∃ s, s.Finite ∧ U = ⋃ i ∈ s, b i
⊢ P (U \ V) ⋯
Module: Mathlib.RingTheory.Derivation.ToSquareZero

Goal state before:
pp: 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
hI : I ^ 2 = ⊥
f : Derivation R A ↥I
⊢ ↑(f 1) + (algebraMap A B) 1 = 1

Tactic:
map_one (algebraMap _ _),

Goal state after:
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
hI : I ^ 2 = ⊥
f : Derivation R A ↥I
⊢ ↑(f 1) + 1 = 1
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b ∣ a

Tactic:
nth_rewrite 2 [← prod_factorization_pow_eq_self ha]

Goal state after:
case inr.inr
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b ∣ a.factorization.prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))
p : Ideal S
hp : p.IsPrime
eq : p✝.asIdeal = ⊤.prod p
⊢ p✝ ∈ Set.range (comap (RingHom.fst R S))

Tactic:
· refine (hp.ne_top <| (Ideal.eq_top_iff_one _).mpr ?_).elim
    simpa [eq] using h (show (0, 1) ∈ RingHom.ker (RingHom.fst R S) by simp)

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x ↦ h ^ x) m = σ h
g : G
⊢ σ g = g ^ m

Tactic:
obtain ⟨n, rfl⟩ := hG g

Goal state after:
G : Type u_2
inst✝ : Group G
h✝ : IsCyclic G
σ : G →* G
h : G
hG : ∀ (x : G), x ∈ zpowers h
m : ℤ
hm : (fun x ↦ h ^ x) m = σ h
n : ℤ
⊢ σ ((fun x ↦ h ^ x) n) = (fun x ↦ h ^ x) n ^ m
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
ι : Type u_1
R : ι → Type u_2
inst✝ : (i : ι) → CommRing (R i)
i : ι
⊢ Continuous fun a ↦ sigmaToPi R ⟨i, a⟩

Tactic:
exact continuous_comap (Pi.evalRingHom R i)

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

Goal state before:
pp: G : Type u_2
inst✝³ : Group G
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
m : M
g : G
k : ℤ
h : (toMonoidHomZModOfIsCyclic G M hn) m = ↑k
⊢ g ^ ⋯.choose = g ^ k

Tactic:
zpow_eq_zpow_iff_modEq

Goal state after:
G : Type u_2
inst✝³ : Group G
M : Type u_4
inst✝² : Monoid M
inst✝¹ : IsCyclic G
inst✝ : MulDistribMulAction M G
n : ℕ
hn : Nat.card G = n
m : M
g : G
k : ℤ
h : (toMonoidHomZModOfIsCyclic G M hn) m = ↑k
⊢ ⋯.choose ≡ k [ZMOD ↑(orderOf g)]
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case inr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : (I * J) ^ n ≤ 0
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)

Tactic:
have hnz : n ≠ 0 := by rintro rfl; simp at hn

Goal state after:
case inr
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
hs : IsClopen s
h✝ : Nontrivial R
I : Ideal R
hI : I.FG
J : Ideal R
hJ : J.FG
hI' : zeroLocus ↑I = sᶜ
hJ' : zeroLocus ↑J = s
this : I * J ≤ nilradical R
n : ℕ
hn : (I * J) ^ n ≤ 0
hnz : n ≠ 0
⊢ ∃ e f, e * f = 0 ∧ e + f = 1 ∧ s = ↑(basicOpen e) ∧ sᶜ = ↑(basicOpen f)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: 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)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
⊢ orderOf t / (orderOf t).gcd (p ^ k) = orderOf t / p ^ k

Tactic:
Nat.gcd_eq_right hpk

Goal state after:
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)
p : ℕ
hp : Nat.Prime p
k : ℕ := (orderOf t).factorization p
hpe : k < (exponent G).factorization p
hk : k = (orderOf t).factorization p
g : G
hg : orderOf g = p ^ (exponent G).factorization p
hpk : p ^ k ∣ orderOf t
⊢ orderOf t / p ^ k = orderOf t / p ^ k
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 : Subgroup G
inst✝ : H.FiniteIndex
⊢ ∃ n, H.index = p ^ n

Tactic:
by
  obtain ⟨n, hn⟩ := iff_card.mp (hG.to_quotient H.normalCore)
  obtain ⟨k, _, hk2⟩ :=
    (Nat.dvd_prime_pow hp.out).mp
      ((congr_arg _ (H.normalCore.index_eq_card.trans hn)).mp
        (Subgroup.index_dvd_of_le H.normalCore_le))
  exact ⟨k, hk2⟩

Goal state after:
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)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝¹ : Fintype α
this✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : card ↑(orbit G b) = p ^ k
this : k = 0
⊢ ∃ a, ∃ (_ : a ∈ Finset.univ) (_ : ↑1 ≠ 0), Quotient.mk'' ↑a = Quotient.mk'' b

Tactic:
exact
      ⟨⟨b, mem_fixedPoints_iff_card_orbit_eq_one.2 <| by rw [hk, this, pow_zero]⟩,
        Finset.mem_univ _, ne_of_eq_of_ne Nat.cast_one one_ne_zero, rfl⟩

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P Q : Sylow p G
H : ∀ {R : Sylow p G} {S : ↑(orbit G P)}, S ∈ fixedPoints ↥↑R ↑(orbit G P) ↔ ↑↑S = ↑R
this : (fixedPoints ↥↑Q ↑(orbit G P)).Nonempty
R : ↑(orbit G P)
hR : R ∈ fixedPoints ↥↑Q ↑(orbit G P)
⊢ ∃ g, g • P = Q

Tactic:
rw [← Sylow.ext (H.mp hR)]
        exact R.2

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

Goal state before:
pp: G : Type u_2
inst✝³ : Infinite G
inst✝² : CommGroup G
inst✝¹ : PartialOrder G
inst✝ : IsOrderedMonoid G
g : G
hg : zpowers g = ⊤
hg1 : 1 < g
⊢ StrictMono ⇑(intEquivOfZPowersEqTop g hg)

Tactic:
intro x y hxy
  simp only [intEquivOfZPowersEqTop, MulEquiv.ofBijective_apply, zpowersHom_apply]
  exact zpow_lt_zpow_right hg1 hxy

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p ↥N
g : G
x✝ : g ∈ ⊤
n : ↥N
hn : MulAut.conjNormal (↑n * g) • ↑P = ↑P
⊢ ↑n * g ∈ normalizer ↑(map N.subtype ↑P)

Tactic:
Subgroup.pointwise_smul_def

Goal state after:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p ↥N
g : G
x✝ : g ∈ ⊤
n : ↥N
hn : map ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N) (MulAut.conjNormal (↑n * g))) ↑P = ↑P
⊢ ↑n * g ∈ normalizer ↑(map N.subtype ↑P)
Module: Mathlib.Order.Atoms.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
a : Bool
⊢ a = ⊥ ∨ a = ⊤

Tactic:
← Finset.mem_singleton,

Goal state after:
α : Type u_1
β : Type u_2
a : Bool
⊢ a ∈ {⊥} ∨ a = ⊤
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p ↥N
g : G
x✝ : g ∈ ⊤
n : ↥N
hn : map ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N) (MulAut.conjNormal (↑n * g))) ↑P = ↑P
this : Function.Injective ⇑(MulEquiv.toMonoidHom (MulAut.conj (↑n * g)))
⊢ ↑n * g ∈ normalizer ↑(map N.subtype ↑P)

Tactic:
refine fun x ↦ (mem_map_iff_mem this).symm.trans ?_

Goal state after:
G : Type u_1
inst✝³ : Group G
p : ℕ
inst✝² : Fact (Nat.Prime p)
N : Subgroup G
inst✝¹ : N.Normal
inst✝ : Finite (Sylow p ↥N)
P : Sylow p ↥N
g : G
x✝ : g ∈ ⊤
n : ↥N
hn : map ((MulDistribMulAction.toMonoidEnd (MulAut ↥N) ↥N) (MulAut.conjNormal (↑n * g))) ↑P = ↑P
this : Function.Injective ⇑(MulEquiv.toMonoidHom (MulAut.conj (↑n * g)))
x : G
⊢ (MulEquiv.toMonoidHom (MulAut.conj (↑n * g))) x ∈
      map (MulEquiv.toMonoidHom (MulAut.conj (↑n * g))) (map N.subtype ↑P) ↔
    ↑n * g * x * (↑n * g)⁻¹ ∈ ↑(map N.subtype ↑P)
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
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ g' ^ Classical.choose ⋯ = g' ^ 1

Tactic:
zpow_eq_zpow_iff_modEq

Goal state after:
G : Type u_2
G' : Type u_3
inst✝¹ : Group G
inst✝ : Group G'
g : G
hg : ∀ (x : G), x ∈ zpowers g
g' : G'
hg' : orderOf g' ∣ orderOf g
⊢ Classical.choose ⋯ ≡ 1 [ZMOD ↑(orderOf g')]
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card ↥H
H' : Subgroup ↥H
H'card : Nat.card ↥H' = p ^ n
⊢ Nat.card ↥(Subgroup.map H.subtype H') = Nat.card ↥H'

Tactic:
let e : H' ≃* H'.map H.subtype := H'.equivMapOfInjective (Subgroup.subtype H) H.subtype_injective

Goal state after:
G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card ↥H
H' : Subgroup ↥H
H'card : Nat.card ↥H' = p ^ n
e : ↥H' ≃* ↥(Subgroup.map H.subtype H') := H'.equivMapOfInjective H.subtype ⋯
⊢ Nat.card ↥(Subgroup.map H.subtype H') = Nat.card ↥H'
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: case refine_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i : Fin (smash s₁ s₂ hs).length
⊢ ∀ (i : Fin s₁.length),
    Iso
      ((smash s₁ s₂ hs).toFun (Fin.castAdd s₂.length i).castSucc, (smash s₁ s₂ hs).toFun (Fin.castAdd s₂.length i).succ)
      ((smash t₁ t₂ ht).toFun (e (Fin.castAdd s₂.length i)).castSucc,
        (smash t₁ t₂ ht).toFun (e (Fin.castAdd s₂.length i)).succ)

pp: case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i : Fin (smash s₁ s₂ hs).length
⊢ ∀ (i : Fin s₂.length),
    Iso ((smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).castSucc, (smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).succ)
      ((smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).castSucc,
        (smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).succ)

Tactic:
· intro i
      simpa [e, smash_castAdd, smash_succ_castAdd] using h₁.choose_spec i

Goal state after:
case refine_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ t₁ t₂ : CompositionSeries X
hs : last s₁ = head s₂
ht : last t₁ = head t₂
h₁ : s₁.Equivalent t₁
h₂ : s₂.Equivalent t₂
e : Fin (s₁.length + s₂.length) ≃ Fin (t₁.length + t₂.length) :=
  Trans.trans (Trans.trans finSumFinEquiv.symm ((Exists.choose h₁).sumCongr (Exists.choose h₂))) finSumFinEquiv
i : Fin (smash s₁ s₂ hs).length
⊢ ∀ (i : Fin s₂.length),
    Iso ((smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).castSucc, (smash s₁ s₂ hs).toFun (Fin.natAdd s₁.length i).succ)
      ((smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).castSucc,
        (smash t₁ t₂ ht).toFun (e (Fin.natAdd s₁.length i)).succ)
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
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
f : Bool → Submodule R M := fun t ↦ Bool.rec q p t
⊢ IsSemisimpleModule R ↥(⨆ i ∈ Set.univ, f i)

Tactic:
exact isSemisimpleModule_biSup_of_isSemisimpleModule_submodule
    (by rintro (_ | _) _ <;> assumption)

Goal state after:
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ J.jacobson
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
s : R
hs : s * r - 1 ∈ J
⊢ n = 1 • n - s • r • n

Tactic:
hr.2 n hn,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : N.FG
hIN : N ≤ I • N
hIjac : I ≤ J.jacobson
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
s : R
hs : s * r - 1 ∈ J
⊢ n = 1 • n - s • 0
Module: Mathlib.RingTheory.Nakayama

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
N N' P : Submodule R M
hN' : N'.FG
hN'le : N' ≤ P
hNN' : P ≤ N ⊔ I • N'
⊢ N ⊔ I • N' ≤ N ⊔ N'

Tactic:
by simpa using le_trans smul_le_right le_sup_right

Goal state after:
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
x : M
N : Submodule R M := ⋯
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
⊢ (∃ r, ↑r • x = x) → x ∈ ⨅ i, I ^ i • ⊤

Tactic:
· rintro ⟨r, eq⟩
    rw [Submodule.mem_iInf]
    intro i
    induction i with
    | zero => simp
    | succ i hi =>
      rw [add_comm, pow_add, ← smul_smul, pow_one, ← eq]
      exact Submodule.smul_mem_smul r.prop hi

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ (∃ a, ⊤ = ResidueField R ∙ a) ↔ Submodule.IsPrincipal (maximalIdeal R)

Tactic:
(maximalIdeal R).toCotangent_surjective.exists,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ (∃ x, ⊤ = ResidueField R ∙ (maximalIdeal R).toCotangent x) ↔ Submodule.IsPrincipal (maximalIdeal R)
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
m n n' : M
g : n ⟶ n'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.map g).app ((F.obj m).obj X) ≫ (μ F m n').app X = (μ F m n).app X ≫ (F.map (m ◁ g)).app X

Tactic:
rw [← id_tensorHom, ← μ_naturality₂ F (𝟙 m) g X]

Goal state after:
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
m n n' : M
g : n ⟶ n'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.map g).app ((F.obj m).obj X) ≫ (μ F m n').app X =
    (F.map g).app ((F.obj m).obj X) ≫ (F.obj n').map ((F.map (𝟙 m)).app X) ≫ (μ F m n').app X
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: β : Type
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : HasZeroMorphisms C
X Y : GradedObject β C
f g : X ⟶ Y
w : (total β C).map f = (total β C).map g
i : β
⊢ f i = g i

Tactic:
replace w := Sigma.ι (fun i : β => X i) i ≫= w

Goal state after:
β : Type
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : HasZeroMorphisms C
X Y : GradedObject β C
f g : X ⟶ Y
i : β
w : Sigma.ι (fun i ↦ X i) i ≫ (total β C).map f = Sigma.ι (fun i ↦ X i) i ≫ (total β C).map g
⊢ f i = g i
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
F : A → C ⥤ C
zero : F 0 ≅ 𝟭 C
add : (n m : A) → F (n + m) ≅ F n ⋙ F m
m₁ m₂ m₃ : A
X : C
⊢ (F (m₁ + m₂ + m₃)).obj X = (F (m₁ + (m₂ + m₃))).obj X

Tactic:
rw [add_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ (h.F (m₁ + (m₂ + m₃))).obj X = (h.F (m₁ + m₂ + m₃)).obj X

Tactic:
rw [add_assoc]

Goal state after:
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
⊢ shiftFunctorAdd' C a 0 a ⋯ =
    (shiftFunctor C a).rightUnitor.symm ≪≫ (shiftFunctor C a).isoWhiskerLeft (shiftFunctorZero C A).symm

Tactic:
by
  ext
  dsimp [shiftFunctorAdd', shiftFunctorZero, shiftFunctor]
  simp only [eqToHom_app, ε_app_obj, Discrete.addMonoidal_rightUnitor, eqToIso.inv,
    eqToHom_map, Category.id_comp]
  rfl

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
i k : ι
hik : c.Rel i k
⊢ (if hi : i = j then (singleObjXIsoOfEq c j A i hi).hom ≫ φ ≫ (K.XIsoOfEq hi).inv else 0) ≫ K.d i k =
    ((single V c j).obj A).d i k ≫
      if hi : k = j then (singleObjXIsoOfEq c j A k hi).hom ≫ φ ≫ (K.XIsoOfEq hi).inv else 0

Tactic:
dsimp
    rw [zero_comp]
    split_ifs with hi
    · subst hi
      simp only [XIsoOfEq_rfl, Iso.refl_inv, comp_id, assoc, hφ k hik, comp_zero]
    · apply (isZero_single_obj_X c j A i hi).eq_of_src

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

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Submodule.restrictScalars S (ideal R S) ≤
    Submodule.restrictScalars S (Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1))

Tactic:
rw [← KaehlerDifferential.submodule_span_range_eq_ideal, Ideal.span]

Goal state after:
case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ≤
    Submodule.restrictScalars S (Submodule.span (S ⊗[R] S) (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1))
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
| Submodule.restrictScalars S (Submodule.span (S ⊗[R] S) (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1))

Tactic:
← Submodule.span_span_of_tower S

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
| Submodule.restrictScalars S (Submodule.span (S ⊗[R] S) ↑(Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)))
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
⊢ (DLinearMap R S) 1 = 0

Tactic:
by
      dsimp [KaehlerDifferential.DLinearMap_apply, Ideal.toCotangent_apply]
      congr
      rw [sub_self]

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 : ι
inst✝⁵ : HasZeroObject W₁
inst✝⁴ : HasZeroObject W₂
W : Type u_5
inst✝³ : Category.{v_4, u_5} W
inst✝² : Preadditive W
inst✝¹ : HasZeroObject W
inst✝ : DecidableEq ι
j : ι
x✝¹ x✝ : W
f g : x✝¹ ⟶ x✝
⊢ (single W c j).map (f + g) = (single W c j).map f + (single W c j).map g

Tactic:
by ext; simp [single]

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
P Q : ChainComplex V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' f'' ≫ Q.d (n + 2) (n + 1) = P.d (n + 2) (n + 1) ≫ p.snd.fst
n m : ℕ
⊢ (ComplexShape.down ℕ).Rel n m →
    (P.mkHomAux Q zero one one_zero_comm succ n).fst ≫ Q.d n m =
      P.d n m ≫ (P.mkHomAux Q zero one one_zero_comm succ m).fst

Tactic:
by
    rintro (rfl : m + 1 = n)
    exact (mkHomAux P Q zero one one_zero_comm succ m).2.2

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

Goal state before:
pp: case pos
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : DecidableEq ι
i j : ι
I : C
inst✝ : Injective I
hij : j = i
⊢ Injective (((single C c i).obj I).X j)

Tactic:
subst hij
    simp only [single_obj_X_self]
    infer_instance

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

Goal state before:
pp: case pos
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : DecidableEq ι
i j : ι
P : C
inst✝ : Projective P
hij : j = i
⊢ Projective (((single C c i).obj P).X j)

Tactic:
subst hij
    simp only [single_obj_X_self]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map ((add hF s i a b).hom.app X) =
    (i (a + b)).hom.app X ≫
      (shiftFunctorAdd D a b).hom.app (F.obj X) ≫ (shiftFunctor D b).map ((i a).inv.app X) ≫ (i b).inv.app ((s a).obj X)

Tactic:
dsimp [add]
  simp

Goal state after: