mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U | IsCompact ↑U}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ } = sSup Us
t : Finset ↑Us
ht : U ⊆ ⋃ i ∈ t, f '' ↑↑i
i : ↑Us
hi : i ∈ t
x : X
hx : x ∈ ↑↑i
⊢ f x ∈ U

Tactic:
have := heq ▸ mem_sSup.mpr ⟨i.1, i.2, hx⟩

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
f : X → Y
hfc : Continuous[inst✝², inst✝¹] f
h : IsOpenMap f
U : Set Y
hs : U ⊆ Set.range f
hU : IsOpen[inst✝¹] U
hc : IsCompact U
Us : Set (Opens X)
hUs : Us ⊆ {U | IsCompact ↑U}
heq : { carrier := f ⁻¹' U, is_open' := ⋯ } = sSup Us
t : Finset ↑Us
ht : U ⊆ ⋃ i ∈ t, f '' ↑↑i
i : ↑Us
hi : i ∈ t
x : X
hx : x ∈ ↑↑i
this : x ∈ { carrier := f ⁻¹' U, is_open' := ⋯ }
⊢ f x ∈ U
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : ∀ a ∈ U₁, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₁
hU₂ : ∀ a ∈ U₂, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
W₁ : Set X
hW₁ : W₁ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁
⊢ ∃ A B,
    IsClosed[inst✝¹] A ∧
      IsClosed[inst✝¹] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty

Tactic:
obtain ⟨W₂, hW₂⟩ := hU₂ x₂ hx₂.1

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : ∀ a ∈ U₁, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₁
hU₂ : ∀ a ∈ U₂, ∃ t ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U}, a ∈ t ∧ t ⊆ U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
x₁ : X
hx₁ : x₁ ∈ U₁ ∧ x₁ ∈ Z ∧ x₁ ∉ U₂
x₂ : X
hx₂ : x₂ ∈ U₂ ∧ x₂ ∈ Z ∧ x₂ ∉ U₁
W₁ : Set X
hW₁ : W₁ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₁ ∈ W₁ ∧ W₁ ⊆ U₁
W₂ : Set X
hW₂ : W₂ ∈ {U | IsOpen[inst✝¹] U ∧ IsCompact U} ∧ x₂ ∈ W₂ ∧ W₂ ⊆ U₂
⊢ ∃ A B,
    IsClosed[inst✝¹] A ∧
      IsClosed[inst✝¹] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsRetrocompact (t i)
⊢ IsRetrocompact (s.inf t)

Tactic:
exact .finsetInf ht

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
s : Finset ι
hs : s.Nonempty
t : ι → Set X
ht : ∀ i ∈ s, IsLocallyConstructible (t i)
⊢ IsLocallyConstructible (s.inf t)

Tactic:
exact .finsetInf ht

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Descent

Goal state before:
pp: A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
this : PreservesFiniteLimits (extendScalars f)
⊢ ComonadicLeftAdjoint (extendScalars f)

Tactic:
have := reflectsIsomorphisms_extendScalars_of_faithfullyFlat hf

Goal state after:
A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
this✝ : PreservesFiniteLimits (extendScalars f)
this : (extendScalars f).ReflectsIsomorphisms
⊢ ComonadicLeftAdjoint (extendScalars f)
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.head.asIdeal = under R (RelSeries.head L).asIdeal

Tactic:
← L.toList_getElem_zero_eq_head,

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
⊢ l.head.asIdeal = under R (RelSeries.toList L)[0].asIdeal
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] = (List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L))[0]

Tactic:
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
⊢ (List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L))[0] =
    (List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L))[0]
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b * a.factorizationLCMRight b = a.lcm b

Tactic:
← prod_factorization_pow_eq_self (lcm_ne_zero ha hb),

Goal state after:
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ a.factorizationLCMLeft b * a.factorizationLCMRight b = (a.lcm b).factorization.prod fun x1 x2 ↦ x1 ^ x2
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: ⊢ flat.IsStableUnderCobaseChange

Tactic:
rw [flat, RingHom.isStableUnderCobaseChange_toMorphismProperty_iff]

Goal state after:
⊢ RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] f ↦ f.Flat
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : sInf {I | I.IsMaximal} ≤ I
⊢ I.IsMaximal

Tactic:
rw [← fin.coe_toFinset, ← Finset.inf_id_eq_sInf, hI.inf_le'] at le

Goal state after:
R : Type u
inst✝ : CommSemiring R
x✝ : {I | I.IsMaximal}.Finite ∧ sInf {I | I.IsMaximal} ≤ nilradical R
fin : {I | I.IsMaximal}.Finite
I : Ideal R
hI : I.IsPrime
le : ∃ i ∈ fin.toFinset, id i ≤ I
⊢ I.IsMaximal
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst✝¹³ : CommSemiring R
inst✝¹² : CommSemiring A
inst✝¹¹ : CommSemiring B
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Module A M
inst✝⁶ : Module B M
inst✝⁵ : Module R M
D✝ D1 D2 : Derivation R A M
r✝ : R
a b : A
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module A N
inst✝² : Module R N
inst✝¹ : IsScalarTower R A M
inst✝ : IsScalarTower R A N
f : M →ₗ[A] N
e : M ≃ₗ[A] N
r : A
D : Derivation R A M
⊢ (let __LinearMap := ↑R f ∘ₗ ↑(r • D);
    { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ }) =
    (RingHom.id A) r •
      let __LinearMap := ↑R f ∘ₗ ↑D;
      { toLinearMap := __LinearMap, map_one_eq_zero' := ⋯, leibniz' := ⋯ }

Tactic:
ext; dsimp; simp only [_root_.map_smul]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : PrimeSpectrum R
⊢ ↑(Submonoid.powers r) ⊓ ↑x.asIdeal ⊆ ⊥ → r ∉ x.asIdeal

Tactic:
intro h₁ h₂

Goal state after:
case mp
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
r : R
inst✝ : IsLocalization.Away r S
x : PrimeSpectrum R
h₁ : ↑(Submonoid.powers r) ⊓ ↑x.asIdeal ⊆ ⊥
h₂ : r ∈ x.asIdeal
⊢ False
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)
inst✝ : Finite G
hGnt : Nontrivial G
k : ℕ
hk : Nat.card G = p ^ k
hk0 : k = 0
⊢ False

Tactic:
by
        rw [hk0, pow_zero] at hk; exact Finite.one_lt_card.ne' hk

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ exponent G = sSup (Set.range orderOf)

Tactic:
← iSup

Goal state after:
G : Type u
inst✝¹ : CancelCommMonoid G
inst✝ : Fintype G
⊢ exponent G = iSup orderOf
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
⊢ rank H ≤ rank G

Tactic:
obtain ⟨S, hS1, hS2⟩ := rank_spec G

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 = ⊤
⊢ rank H ≤ rank G
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
H : Subgroup G
P : Sylow p G
⊢ P ∈ fixedPoints (↥H) (Sylow p G) ↔ H ≤ normalizer ↑P

Tactic:
by
  simp_rw [SetLike.le_def, ← Sylow.smul_eq_iff_mem_normalizer]; exact Subtype.forall

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f ↑P) := ⋯.some
⊢ ∃ a, mapSurjective hf a = P

Tactic:
let Q : Subgroup G := Q₀.map (P.comap f).subtype

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : Finite G
G' : Type u_2
inst✝¹ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : Finite G'
P : Sylow p G'
Q₀ : Sylow p ↥(comap f ↑P) := ⋯.some
Q : Subgroup G := map (comap f ↑P).subtype ↑Q₀
⊢ ∃ a, mapSurjective hf a = P
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: G : Type u_2
inst✝¹ : Infinite G
inst✝ : Group G
g : G
hg : zpowers g = ⊤
⊢ (intEquivOfZPowersEqTop g hg).symm g = Multiplicative.ofAdd 1

Tactic:
by
  simp [MulEquiv.symm_apply_eq]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
Q : Sylow p G
⊢ Q = default

Tactic:
obtain ⟨x, h1⟩ := exists_smul_eq G P Q

Goal state after:
G : Type u
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : (↑P).Normal
Q : Sylow p G
x : G
h1 : x • P = Q
⊢ Q = default
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
e : X × X → X × X → Prop
h_refl : ∀ {x : X × X}, e x x
h_symm : ∀ {x y : X × X}, e x y → e y x
h_trans : ∀ {x y z : X × X}, e x y → e y z → e x z
h_rel : ∀ {x y : X}, IsMaximal x (x ⊔ y) → e (x, x ⊔ y) (x ⊓ y, y)
x y : X × X
h_iso : Iso x y
this : IsEquiv (X × X) e
⊢ e x y

Tactic:
refine Relation.EqvGen.eqvGen_le ?_ _ _ h_iso

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
e : X × X → X × X → Prop
h_refl : ∀ {x : X × X}, e x x
h_symm : ∀ {x y : X × X}, e x y → e y x
h_trans : ∀ {x y z : X × X}, e x y → e y z → e x z
h_rel : ∀ {x y : X}, IsMaximal x (x ⊔ y) → e (x, x ⊔ y) (x ⊓ y, y)
x y : X × X
h_iso : Iso x y
this : IsEquiv (X × X) e
⊢ (fun x x_1 ↦
      match x with
      | (x, xsy) =>
        match x_1 with
        | (xiy, y) => IsMaximal x xsy ∧ xsy = x ⊔ y ∧ xiy = x ⊓ y) ≤
    e
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
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : R ∙ v i ⊓ Submodule.span R (Set.range fun i_1 ↦ v ↑i_1) = ⊥
⊢ r • v i ∈ ⊥

Tactic:
← hv,

Goal state after:
ι : Type u_3
R : Type u_4
M : Type u_5
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h_ne_zero : ∀ (i : ι), torsionOf R M (v i) = ⊥
i : ι
r : R
hi : r • v i ∈ Submodule.span R (v '' (Set.univ \ {i}))
hv : R ∙ v i ⊓ Submodule.span R (Set.range fun i_1 ↦ v ↑i_1) = ⊥
⊢ r • v i ∈ R ∙ v i ⊓ Submodule.span R (Set.range fun i_1 ↦ v ↑i_1)
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : ¬(eraseLast s).last = x
imxs : IsMaximal (x ⊓ (eraseLast s).last) (eraseLast s).last
t : CompositionSeries X
htb : head t = (eraseLast s).head
htl : t.length + 1 = n
htt : last t = x ⊓ (eraseLast s).last
hteqv : Equivalent (eraseLast s) (snoc t (eraseLast s).last ⋯)
hmtx : IsMaximal (last t) x
| s

Tactic:
rw [eq_snoc_eraseLast h0s]

Goal state after:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
n : ℕ
ih :
  ∀ (s : CompositionSeries X) (x : X) (hm : IsMaximal x (last s)),
    head s ≤ x →
      s.length = n → ∃ t, head t = head s ∧ t.length + 1 = n ∧ ∃ (htx : last t = x), s.Equivalent (snoc t (last s) ⋯)
s : CompositionSeries X
x : X
hm : IsMaximal x (last s)
hb : head s ≤ x
hn : s.length = n + 1
h0s : 0 < s.length
hetx : ¬(eraseLast s).last = x
imxs : IsMaximal (x ⊓ (eraseLast s).last) (eraseLast s).last
t : CompositionSeries X
htb : head t = (eraseLast s).head
htl : t.length + 1 = n
htt : last t = x ⊓ (eraseLast s).last
hteqv : Equivalent (eraseLast s) (snoc t (eraseLast s).last ⋯)
hmtx : IsMaximal (last t) x
| (eraseLast s).snoc (last s) ⋯
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
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ 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
r : R
hr1 : r - 1 ∈ I
hrn : N ≤ comap ((LinearMap.lsmul R M) r) (I • (R ∙ i) ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s

Tactic:
specialize hrn hs.1

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
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ 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
r : R
hr1 : r - 1 ∈ I
hrn : i ∈ comap ((LinearMap.lsmul R M) r) (I • (R ∙ i) ⊔ I • span R s)
hs : i ∈ ↑N ∧ s ⊆ ↑N
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case mp
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M ↥(Submonoid.powers p)
x : M
a : R
n : ℕ
hn : p ^ n = a
hx : ⟨a, ⋯⟩ • x = 0
⊢ ∃ n, p ^ n • x = 0

Tactic:
use n

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
p : R
h : IsTorsion' M ↥(Submonoid.powers p)
x : M
a : R
n : ℕ
hn : p ^ n = a
hx : ⟨a, ⋯⟩ • x = 0
⊢ p ^ n • x = 0
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: 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
⊢ (R ⧸ I ^ 2) ⧸ I.cotangentIdeal ≃+* R ⧸ I

Tactic:
refine (Ideal.quotEquivOfEq (Ideal.map_eq_submodule_map _ _).symm).trans ?_
  refine (DoubleQuot.quotQuotEquivQuotSup _ _).trans ?_
  exact Ideal.quotEquivOfEq (sup_eq_right.mpr <| Ideal.pow_le_self two_ne_zero)

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
I : Ideal R
⊢ IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤

Tactic:
by
  constructor
  · intro H
    by_cases I = ⊤; · exact Or.inr ‹_›
    refine Or.inl (eq_bot_iff.mpr ?_)
    rw [← Ideal.iInf_pow_eq_bot_of_isLocalRing I ‹_›]
    apply le_iInf
    rintro (_ | n) <;> simp [H.pow_succ_eq]
  · rintro (rfl | rfl) <;> simp [IsIdempotentElem]

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
j : ι
hj : ∀ (k : ι), ¬c.Rel j k
⊢ ¬∃ j_1, c.Rel j j_1

Tactic:
simpa using hj

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M M₁ M₂ : PresheafOfModules R
a✝ b✝ : M₁ ⟶ M₂
X✝ : Cᵒᵖ
⊢ a✝.app X✝ + b✝.app X✝ = b✝.app X✝ + a✝.app X✝

Tactic:
apply add_comm

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: I : Type u_1
J : Type u_2
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
X : GradedObject I C
p : I → J
inst✝ : X.HasMap p
A : C
j : J
φ : (i : I) → p i = j → (X i ⟶ A)
i : I
hi : p i = j
⊢ X.ιMapObj p i j hi ≫ X.descMapObj p φ = φ i hi

Tactic:
apply Cofan.IsColimit.fac

Goal state after:
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
D : Derivation R S M
x y : S ⊗[R] S
⊢ D.tensorProductTo (x * y) =
    (TensorProduct.lmul' R) x • D.tensorProductTo y + (TensorProduct.lmul' R) y • D.tensorProductTo x

Tactic:
by
  refine TensorProduct.induction_on x ?_ ?_ ?_
  · rw [zero_mul, map_zero, map_zero, zero_smul, smul_zero, add_zero]
  swap
  · intro x₁ y₁ h₁ h₂
    rw [add_mul, map_add, map_add, map_add, add_smul, smul_add, h₁, h₂, add_add_add_comm]
  intro x₁ x₂
  refine TensorProduct.induction_on y ?_ ?_ ?_
  · rw [mul_zero, map_zero, map_zero, zero_smul, smul_zero, add_zero]
  swap
  · intro x₁ y₁ h₁ h₂
    rw [mul_add, map_add, map_add, map_add, add_smul, smul_add, h₁, h₂, add_add_add_comm]
  intro x y
  simp only [TensorProduct.tmul_mul_tmul, Derivation.tensorProductTo,
    TensorProduct.AlgebraTensorModule.lift_apply,
    TensorProduct.lmul'_apply_tmul]
  dsimp
  rw [D.leibniz]
  simp only [smul_smul, smul_add, mul_comm (x * y) x₁, mul_right_comm x₁ x₂, ← mul_assoc]

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

Goal state before:
pp: case mp
C : Type u_1
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (HomologicalComplex C c)
⊢ S.ShortExact → ∀ (i : ι), (S.map (eval C c i)).ShortExact

Tactic:
intro hS i
    have := hS.mono_f
    have := hS.epi_g
    exact hS.map (eval C c i)

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
K L : CochainComplex C ℕ
φ : K ⟶ L
inst✝¹ : HomologicalComplex.HasHomology K 0
inst✝ : HomologicalComplex.HasHomology L 0
⊢ HomologicalComplex.homologyMap φ 0 ≫ L.isoHomologyπ₀.inv = K.isoHomologyπ₀.inv ≫ HomologicalComplex.cyclesMap φ 0

Tactic:
by
  simp only [← cancel_epi (K.homologyπ 0), HomologicalComplex.homologyπ_naturality_assoc,
    HomologicalComplex.isoHomologyπ_hom_inv_id, comp_id,
    HomologicalComplex.isoHomologyπ_hom_inv_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: J : Type w
C : J → Type u
D : J → Type u'
inst✝¹ : (j : J) → Category.{v, u} (C j)
inst✝ : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty (C j)
F : (j : J) → C j ⥤ D j
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X✝ Y✝ : (j : J) → C j
f : X✝ ⟶ Y✝
hf : MorphismProperty.pi W f
⊢ IsIso ((Functor.pi F).map f)

Tactic:
isIso_pi_iff

Goal state after:
J : Type w
C : J → Type u
D : J → Type u'
inst✝¹ : (j : J) → Category.{v, u} (C j)
inst✝ : (j : J) → Category.{v', u'} (D j)
W : (j : J) → MorphismProperty (C j)
F : (j : J) → C j ⥤ D j
hF : ∀ (j : J), (W j).IsInvertedBy (F j)
X✝ Y✝ : (j : J) → C j
f : X✝ ⟶ Y✝
hf : MorphismProperty.pi W f
⊢ ∀ (i : J), IsIso ((Functor.pi F).map f i)
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a.convert_2.inr
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
⊢ (fun x ↦ single ((algebraMap A B) x) 1) x ∈
    ↑(Submodule.comap (linearCombination B ⇑(D R B)) (mapBaseChange R A B).range)

Tactic:
use 1 ⊗ₜ D _ _ x

Goal state after:
case h
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : A
⊢ (mapBaseChange R A B) (1 ⊗ₜ[A] (D R A) x) = (linearCombination B ⇑(D R B)) ((fun x ↦ single ((algebraMap A B) x) 1) x)
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
e f : C ⟶ D
h : Homotopy e f
g : D ⟶ E
i : ι
⊢ ((dNext i) h.hom + (prevD i) h.hom) ≫ g.f i + f.f i ≫ g.f i =
    (dNext i) h.hom ≫ g.f i + (prevD i) h.hom ≫ g.f i + f.f i ≫ g.f i

Tactic:
Preadditive.add_comp

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
e f : C ⟶ D
h : Homotopy e f
g : D ⟶ E
i : ι
⊢ (dNext i) h.hom ≫ g.f i + (prevD i) h.hom ≫ g.f i + f.f i ≫ g.f i =
    (dNext i) h.hom ≫ g.f i + (prevD i) h.hom ≫ g.f i + f.f i ≫ g.f i