mathlib-initiative/mathlib-tactics huggingface dataset:
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₁ : IsOpen[inst✝¹] U₁
hU₂ : IsOpen[inst✝¹] U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) = ∅
⊢ ∃ A B,
    IsClosed[inst✝¹] A ∧
      IsClosed[inst✝¹] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty

Tactic:
← Set.subset_empty_iff

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : PrespectralSpace X
Z U₁ U₂ : Set X
hU₁ : IsOpen[inst✝¹] U₁
hU₂ : IsOpen[inst✝¹] U₂
hU₁Z : (Z ∩ U₁).Nonempty
hU₂Z : (Z ∩ U₂).Nonempty
hU₁₂ : Z ∩ (U₁ ∩ U₂) ⊆ ∅
⊢ ∃ A B,
    IsClosed[inst✝¹] A ∧
      IsClosed[inst✝¹] B ∧ IsCompact Aᶜ ∧ IsCompact Bᶜ ∧ Z ⊆ A ∪ B ∧ (Z ∩ Aᶜ).Nonempty ∧ (Z ∩ Bᶜ).Nonempty
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝ : CompleteLattice P
I : Ideal P
α : Type u_2
f : α → P
s : Set α
hs : s.Finite
⊢ ⨆ i ∈ s, f i ∈ I ↔ ∀ i ∈ s, f i ∈ I

Tactic:
induction s, hs using Finite.induction_on with

Goal state after:
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous f
h : Function.Injective (Compacts.map f hf)
⊢ Function.Injective ((fun x ↦ {x}) ∘ f)

Tactic:
Function.comp_def,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous f
h : Function.Injective (Compacts.map f hf)
⊢ Function.Injective fun x ↦ {f x}
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
K : NonemptyCompacts α
⊢ NonemptyCompacts.map id ⋯ K = K

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → γ
g : α → β
hf : Continuous f
hg : Continuous g
K : NonemptyCompacts α
⊢ NonemptyCompacts.map (f ∘ g) ⋯ K = NonemptyCompacts.map f hf (NonemptyCompacts.map g hg K)

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.Topology.Sets.Compacts

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : Continuous f
x : α
⊢ NonemptyCompacts.map f hf {x} = {f x}

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set Y
hf : IsClosedEmbedding f
hf' : IsCompact (range f)ᶜ
hs : IsRetrocompact s
⊢ IsRetrocompact (f ⁻¹' s)

Tactic:
by
  rintro U hUcomp hUopen
  have hfUopen : IsOpen (f '' U ∪ (range f)ᶜ) := by
    simpa [← range_sdiff_image hf.injective, sdiff_eq, compl_inter, union_comm]
      using (hf.isClosedMap _ hUopen.isClosed_compl).isOpen_compl
  have hfUcomp : IsCompact (f '' U ∪ (range f)ᶜ) := (hUcomp.image hf.continuous).union hf'
  simpa [inter_union_distrib_left, inter_left_comm, inter_eq_right.2 (image_subset_range ..),
    hf.isCompact_iff, image_preimage_inter] using (hs hfUcomp hfUopen).inter_left hf.isClosed_range

Goal state after:
Module: Mathlib.Topology.Sober

Goal state before:
pp: case h.a
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : R1Space α
S✝ : Set α
h : IsIrreducible S✝
hs : IsClosed S✝
x : α
hx : x ∈ S✝
⊢ closure {x} ⊆ closure S✝

Tactic:
exact closure_mono (singleton_subset_iff.mpr hx)

Goal state after:
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
f₁ f₂ : A →ₐ[R] B
e : (Ideal.Quotient.mkₐ R I).comp f₁ = (Ideal.Quotient.mkₐ R I).comp f₂
x : A
⊢ (f₁.toLinearMap - f₂.toLinearMap) x ∈ Submodule.restrictScalars R I

Tactic:
by simpa [Ideal.Quotient.eq] using congr($e x)

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ ∀ A ⊆ Set.range zeroLocus, ⋂₀ A ∈ Set.range zeroLocus

Tactic:
by
      intro Zs h
      rw [Set.sInter_eq_iInter]
      choose f hf using fun i : Zs => h i.prop
      simp only [← hf]
      exact ⟨_, zeroLocus_iUnion _⟩

Goal state after:
Module: Mathlib.Data.ZMod.QuotientGroup

Goal state before:
pp: G : Type u_3
inst✝² : Group G
H : Subgroup G
g : G
inst✝¹ : Finite (G ⧸ H)
inst✝ : Fintype (Quotient (orbitRel (↥(zpowers g)) (G ⧸ H)))
⊢ H.index = ∑ q, minimalPeriod (fun x ↦ g • x) q.out

Tactic:
have : Fintype (G ⧸ H) := Fintype.ofFinite _
  have (q : Quotient (MulAction.orbitRel (zpowers g) (G ⧸ H))) :
      Fintype (MulAction.orbit (zpowers g) q.out) := Fintype.ofFinite _
  simp only [MulAction.minimalPeriod_eq_card, index_eq_card, Nat.card_eq_fintype_card]
  rw [← Fintype.card_sigma]
  exact Fintype.card_congr (MulAction.selfEquivSigmaOrbits (zpowers g) (G ⧸ H))

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : exponent (M j) = 0
⊢ exponent ((i : ι) → M i) = 0

Tactic:
@exponent_eq_zero_iff,

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
j : ι
hj : ¬ExponentExists (M j)
⊢ ¬ExponentExists ((i : ι) → M i)
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f : R
⊢ IsRetrocompact ↑(basicOpen f)

Tactic:
by
  simpa using isRetrocompact_zeroLocus_compl (Set.finite_singleton f)

Goal state after:
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

Tactic:
apply rank_le

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 = ⊤
⊢ Subgroup.closure ↑(Finset.image (⇑f) S) = ⊤
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 α
⊢ #{a | orderOf a = d} = φ d

Tactic:
let c := Fintype.card α
  have hc0 : 0 < c := Fintype.card_pos_iff.2 ⟨1⟩
  apply card_orderOf_eq_totient_aux₁ hn hd
  by_contra h0
  -- Must qualify `Finset.card_eq_zero` because of https://github.com/leanprover/lean4/issues/2849
  simp_rw [not_lt, Nat.le_zero, Finset.card_eq_zero] at h0
  apply lt_irrefl c
  calc
    c = ∑ m ∈ c.divisors, #{a : α | orderOf a = m} := by
      simp only [sum_card_orderOf_eq_card_pow_eq_one hc0.ne']
      apply congr_arg card
      simp [c]
    _ = ∑ m ∈ c.divisors.erase d, #{a : α | orderOf a = m} := by
      rw [eq_comm]
      refine sum_subset (erase_subset _ _) fun m hm₁ hm₂ => ?_
      have : m = d := by
        contrapose! hm₂
        exact mem_erase_of_ne_of_mem hm₂ hm₁
      simp [this, h0]
    _ ≤ ∑ m ∈ c.divisors.erase d, φ m := by
      gcongr with m hm
      have hmc : m ∣ c := by
        simp only [mem_erase, mem_divisors] at hm
        tauto
      obtain h1 | h1 := (#{a : α | orderOf a = m}).eq_zero_or_pos
      · simp [h1]
      · simp [card_orderOf_eq_totient_aux₁ hn hmc h1]
    _ < ∑ m ∈ c.divisors, φ m :=
      sum_erase_lt_of_pos (mem_divisors.2 ⟨hd, hc0.ne'⟩) (totient_pos.2 (pos_of_dvd_of_pos hd hc0))
    _ = c := sum_totient _

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
⊢ ∀ m < orderOf g, m ≠ 0 → (orderOf g).Coprime m

Tactic:
· intro n hn hn0
    exact ((h n).resolve_left (Nat.not_dvd_of_pos_of_lt (Nat.pos_iff_ne_zero.mpr hn0) hn)).symm

Goal state after:
Module: Mathlib.Order.Atoms.Finite

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b : α
hab : a < b
⊢ b ∈ LocallyFiniteOrder.finsetIoc a b

Tactic:
simpa [LocallyFiniteOrder.finset_mem_Ioc]

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

Goal state before:
pp: case add
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f✝ : M →ₗ[R] M'
p : R[X]
f g : PolynomialModule R M
e₁ : (map R' f✝) (p • f) = Polynomial.map (algebraMap R R') p • (map R' f✝) f
e₂ : (map R' f✝) (p • g) = Polynomial.map (algebraMap R R') p • (map R' f✝) g
⊢ (map R' f✝) (p • f) + (map R' f✝) (p • g) = Polynomial.map (algebraMap R R') p • (map R' f✝) (f + g)

Tactic:
e₁,

Goal state after:
case add
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f✝ : M →ₗ[R] M'
p : R[X]
f g : PolynomialModule R M
e₁ : (map R' f✝) (p • f) = Polynomial.map (algebraMap R R') p • (map R' f✝) f
e₂ : (map R' f✝) (p • g) = Polynomial.map (algebraMap R R') p • (map R' f✝) g
⊢ Polynomial.map (algebraMap R R') p • (map R' f✝) f + (map R' f✝) (p • g) =
    Polynomial.map (algebraMap R R') p • (map R' f✝) (f + g)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single.add
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
i : ℕ
m : M
p✝ q✝ : R[X]
e₁ : (map R' f) (p✝ • single R i m) = Polynomial.map (algebraMap R R') p✝ • (map R' f) (single R i m)
e₂ : (map R' f) (q✝ • single R i m) = Polynomial.map (algebraMap R R') q✝ • (map R' f) (single R i m)
⊢ (map R' f) (p✝ • single R i m) + (map R' f) (q✝ • single R i m) =
    Polynomial.map (algebraMap R R') (p✝ + q✝) • (map R' f) (single R i m)

Tactic:
e₁,

Goal state after:
case single.add
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
i : ℕ
m : M
p✝ q✝ : R[X]
e₁ : (map R' f) (p✝ • single R i m) = Polynomial.map (algebraMap R R') p✝ • (map R' f) (single R i m)
e₂ : (map R' f) (q✝ • single R i m) = Polynomial.map (algebraMap R R') q✝ • (map R' f) (single R i m)
⊢ Polynomial.map (algebraMap R R') p✝ • (map R' f) (single R i m) + (map R' f) (q✝ • single R i m) =
    Polynomial.map (algebraMap R R') (p✝ + q✝) • (map R' f) (single R i m)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case add
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
f g : PolynomialModule R M
e₁ : (eval r) (p • f) = Polynomial.eval r p • (eval r) f
e₂ : (eval r) (p • g) = Polynomial.eval r p • (eval r) g
⊢ (eval r) (p • f) + (eval r) (p • g) = Polynomial.eval r p • (eval r) (f + g)

Tactic:
e₁,

Goal state after:
case add
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
f g : PolynomialModule R M
e₁ : (eval r) (p • f) = Polynomial.eval r p • (eval r) f
e₂ : (eval r) (p • g) = Polynomial.eval r p • (eval r) g
⊢ Polynomial.eval r p • (eval r) f + (eval r) (p • g) = Polynomial.eval r p • (eval r) (f + g)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single.add
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
i : ℕ
m : M
p✝ q✝ : R[X]
e₁ : (eval r) (p✝ • single R i m) = Polynomial.eval r p✝ • (eval r) (single R i m)
e₂ : (eval r) (q✝ • single R i m) = Polynomial.eval r q✝ • (eval r) (single R i m)
⊢ (eval r) (p✝ • single R i m) + (eval r) (q✝ • single R i m) =
    (Polynomial.eval r p✝ + Polynomial.eval r q✝) • (eval r) (single R i m)

Tactic:
e₁,

Goal state after:
case single.add
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : R
i : ℕ
m : M
p✝ q✝ : R[X]
e₁ : (eval r) (p✝ • single R i m) = Polynomial.eval r p✝ • (eval r) (single R i m)
e₂ : (eval r) (q✝ • single R i m) = Polynomial.eval r q✝ • (eval r) (single R i m)
⊢ Polynomial.eval r p✝ • (eval r) (single R i m) + (eval r) (q✝ • single R i m) =
    (Polynomial.eval r p✝ + Polynomial.eval r q✝) • (eval r) (single R i m)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case add
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f✝ : M →ₗ[R] M'
r : R
f g : PolynomialModule R M
e₁ : (eval ((algebraMap R R') r)) ((map R' f✝) f) = f✝ ((eval r) f)
e₂ : (eval ((algebraMap R R') r)) ((map R' f✝) g) = f✝ ((eval r) g)
⊢ (eval ((algebraMap R R') r)) ((map R' f✝) f) + (eval ((algebraMap R R') r)) ((map R' f✝) g) =
    f✝ ((eval r) f) + f✝ ((eval r) g)

Tactic:
e₁,

Goal state after:
case add
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f✝ : M →ₗ[R] M'
r : R
f g : PolynomialModule R M
e₁ : (eval ((algebraMap R R') r)) ((map R' f✝) f) = f✝ ((eval r) f)
e₂ : (eval ((algebraMap R R') r)) ((map R' f✝) g) = f✝ ((eval r) g)
⊢ f✝ ((eval r) f) + (eval ((algebraMap R R') r)) ((map R' f✝) g) = f✝ ((eval r) f) + f✝ ((eval r) g)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case add
R : Type u_2
inst✝² : CommRing R
S : Type u_8
inst✝¹ : CommRing S
inst✝ : Algebra S R
x : R
f g : PolynomialModule S S
e₁ : (aeval x) (equivPolynomial f) = (eval x) ((map R (Algebra.linearMap S R)) f)
e₂ : (aeval x) (equivPolynomial g) = (eval x) ((map R (Algebra.linearMap S R)) g)
⊢ (aeval x) (equivPolynomial f) + (aeval x) (equivPolynomial g) =
    (eval x) ((map R (Algebra.linearMap S R)) f) + (eval x) ((map R (Algebra.linearMap S R)) g)

Tactic:
e₁,

Goal state after:
case add
R : Type u_2
inst✝² : CommRing R
S : Type u_8
inst✝¹ : CommRing S
inst✝ : Algebra S R
x : R
f g : PolynomialModule S S
e₁ : (aeval x) (equivPolynomial f) = (eval x) ((map R (Algebra.linearMap S R)) f)
e₂ : (aeval x) (equivPolynomial g) = (eval x) ((map R (Algebra.linearMap S R)) g)
⊢ (eval x) ((map R (Algebra.linearMap S R)) f) + (aeval x) (equivPolynomial g) =
    (eval x) ((map R (Algebra.linearMap S R)) f) + (eval x) ((map R (Algebra.linearMap S R)) g)
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case add
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
x✝ y✝ : PolynomialModule R M
e₁ : (eval r ∘ₗ comp p) x✝ = (eval (Polynomial.eval r p)) x✝
e₂ : (eval r ∘ₗ comp p) y✝ = (eval (Polynomial.eval r p)) y✝
⊢ (eval r ∘ₗ comp p) x✝ + (eval r ∘ₗ comp p) y✝ = (eval (Polynomial.eval r p)) x✝ + (eval (Polynomial.eval r p)) y✝

Tactic:
e₁,

Goal state after:
case add
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
x✝ y✝ : PolynomialModule R M
e₁ : (eval r ∘ₗ comp p) x✝ = (eval (Polynomial.eval r p)) x✝
e₂ : (eval r ∘ₗ comp p) y✝ = (eval (Polynomial.eval r p)) y✝
⊢ (eval (Polynomial.eval r p)) x✝ + (eval r ∘ₗ comp p) y✝ =
    (eval (Polynomial.eval r p)) x✝ + (eval (Polynomial.eval r p)) y✝
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₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
⊢ ∃ n₀, ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀

Tactic:
use n₀

Goal state after:
case h
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₀ : ℕ
hn : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
⊢ ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : IsAddTorsionFree M
x y : M
h : y ≠ 0
r s : ℕ
hrs : ↑r • y = s • y
⊢ r = s

Tactic:
← natCast_zsmul

Goal state after:
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : IsAddTorsionFree M
x y : M
h : y ≠ 0
r s : ℕ
hrs : ↑r • y = ↑s • y
⊢ r = s
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
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
⊢ ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀

Tactic:
use n₀

Goal state after:
case h
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
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
⊢ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀
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 F' : I.Filtration M
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
⊢ ∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n

Tactic:
use n₀

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : I.Filtration M
e : F.N 0 ≤ F'.N 0
n₀ : ℕ
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
⊢ ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case a
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
⊢ AddSubmonoid.closure (⋃ i, single R i '' ↑(F.N i)) ≤ F.submodule.toAddSubmonoid

Tactic:
rw [AddSubmonoid.closure_le, Set.iUnion_subset_iff]

Goal state after:
case a
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
⊢ ∀ (i : ℕ), single R i '' ↑(F.N i) ⊆ ↑F.submodule.toAddSubmonoid
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.Stable
F' : I.Filtration M
hf : F' ≤ F
⊢ F'.Stable

Tactic:
← submodule_fg_iff_stable

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
⊢ F'.submodule.FG

case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
⊢ ∀ (i : ℕ), (F'.N i).FG

case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.Stable
F' : I.Filtration M
hf : F' ≤ F
⊢ ∀ (i : ℕ), (F.N i).FG
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 := ⨅ i, I ^ i • ⊤
hN : ∀ (k : ℕ), (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N
r : ↥I
eq : ↑r • x = x
i : ℕ
⊢ x ∈ I ^ i • ⊤

Tactic:
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.Algebra.Homology.ComplexShape

Goal state before:
pp: α : Type u_1
inst✝² : AddRightCancelSemigroup α
inst✝¹ : DecidableEq α
inst✝ : One α
⊢ DecidableRel (up α).Rel

Tactic:
dsimp [ComplexShape.up]

Goal state after:
α : Type u_1
inst✝² : AddRightCancelSemigroup α
inst✝¹ : DecidableEq α
inst✝ : One α
⊢ DecidableRel (up' 1).Rel
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
M : PresheafOfModules R
f : unit R ⟶ M
X✝ Y✝ : Cᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom (f.app Y✝)) ((ConcreteCategory.hom ((unit R).map f✝)) 1) = (ConcreteCategory.hom (f.app Y✝)) 1

Tactic:
unit_map_one

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : PresheafOfModules R
f : unit R ⟶ M
X✝ Y✝ : Cᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ (ConcreteCategory.hom (f.app Y✝)) 1 = (ConcreteCategory.hom (f.app Y✝)) 1
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
I : Type u_1
x x' : GradedObject I C
h : x = x'
i : I
⊢ eqToHom h i = eqToHom ⋯

Tactic:
subst h
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
β : Type w
X Y : β → C
h : X = Y
b : β
⊢ eqToHom h b = eqToHom ⋯

Tactic:
subst h
  rfl

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 Y : GradedObject I C
p : I → J
inst✝¹ : X.HasMap p
inst✝ : Y.HasMap p
φ₁ φ₂ : X ⟶ Y
h : φ₁ = φ₂
⊢ mapMap φ₁ p = mapMap φ₂ p

Tactic:
subst h
  rfl

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₁ C₂ : HomologicalComplex V c
h : C₁ = C₂
n : ι
⊢ (eqToHom h).f n = eqToHom ⋯

Tactic:
subst h
  rfl

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
⊢ Submodule.span S (Set.range ⇑(D R S)) = ⊤

Tactic:
_root_.eq_top_iff

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ ⊤ ≤ Submodule.span S (Set.range ⇑(D R S))
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₁ C₂ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
i : ι
⊢ isoApp (isoOfComponents f hf) i = f i

Tactic:
by
  ext
  simp

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✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ p' + m = n'

Tactic:
rw [← add_left_inj n, hn, add_assoc, h, hp]

Goal state after: