mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Algebraic.Integral

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
alg : Algebra.IsAlgebraic R S
a : A
h : IsIntegral S a
⊢ IsAlgebraic R a

Tactic:
cases subsingleton_or_nontrivial A

Goal state after:
case inl
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
alg : Algebra.IsAlgebraic R S
a : A
h : IsIntegral S a
h✝ : Subsingleton A
⊢ IsAlgebraic R a

case inr
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Ring A
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra S A
inst✝¹ : IsScalarTower R S A
inst✝ : NoZeroDivisors S
alg : Algebra.IsAlgebraic R S
a : A
h : IsIntegral S a
h✝ : Nontrivial A
⊢ IsAlgebraic R a
Module: Mathlib.RingTheory.Localization.Integral

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁹ : CommRing R
S : Type u_2
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : IsDomain R
inst✝⁴ : Algebra R K
inst✝³ : Algebra S K
inst✝² : Module.IsTorsionFree R K
inst✝¹ : IsFractionRing S K
inst✝ : IsScalarTower R S K
⊢ (∀ (x : K), IsAlgebraic R x) → ∀ (x : S), IsAlgebraic R x

Tactic:
· intro h x
    obtain ⟨f, hf₁, hf₂⟩ := h (algebraMap S K x)
    use f, hf₁
    rw [Polynomial.aeval_algebraMap_apply] at hf₂
    exact
      (injective_iff_map_eq_zero (algebraMap S K)).1 (FaithfulSMul.algebraMap_injective _ _) _
        hf₂

Goal state after:
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
⊢ (∀ (P : Ideal S) (x : P.IsPrime), Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)) ↔
    ∀ (I : Ideal S), I ≠ ⊤ → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x

Tactic:
surjective_localRingHom_iff

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
⊢ (∀ (P : Ideal S), P.IsPrime → ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x) ↔
    ∀ (I : Ideal S), I ≠ ⊤ → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
H : ∀ (I : Ideal S) (x : I.IsMaximal), Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯)
I : Ideal S
hI : I.IsPrime
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f I) I f ⋯)

Tactic:
surjective_localRingHom_iff

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
S : Type u_2
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hI : I.IsPrime
H : ∀ (I : Ideal S), I.IsMaximal → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
⊢ ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
⊢ Function.Surjective
    ⇑(Localization.localRingHom (Ideal.comap (algebraMap S (S ⊗[R] T)) J) J (algebraMap S (S ⊗[R] T)) ⋯)

Tactic:
surjective_localRingHom_iff

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
⊢ ∀ (s : S ⊗[R] T),
    ∃ x r,
      ∃ c ∉ J, (algebraMap S (S ⊗[R] T)) r ∉ J ∧ c * (algebraMap S (S ⊗[R] T)) r * s = c * (algebraMap S (S ⊗[R] T)) x
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
J : Ideal (S ⊗[R] T)
hJ : J.IsPrime
x : S ⊗[R] T
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
⊢ 1 ⊗ₜ[R] (r • t) * (algebraMap S (S ⊗[R] T)) ((algebraMap R S) r) * x = 1 ⊗ₜ[R] (r • t) * (algebraMap S (S ⊗[R] T)) a

Tactic:
· simp only [tmul_smul, Algebra.TensorProduct.algebraMap_apply, Algebra.algebraMap_self,
      RingHomCompTriple.comp_apply, Algebra.smul_mul_assoc, Algebra.TensorProduct.tmul_mul_tmul,
      one_mul, mul_one, id_apply, ← e]
    rw [Algebra.algebraMap_eq_smul_one, ← smul_tmul', smul_mul_assoc]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
I✝ : Ideal R
inst✝² : I✝.IsPrime
I : Ideal A
inst✝¹ : I.IsPrime
J : Ideal B
inst✝ : J.IsPrime
f : A →ₐ[R] B
hf : I = comap f.toRingHom J
r : R
⊢ (↑↑(map I J (↑f) hf)).toFun ((algebraMap R I.ResidueField) r) = (algebraMap R J.ResidueField) r

Tactic:
by
    simp [IsScalarTower.algebraMap_apply R A I.ResidueField,
      IsScalarTower.algebraMap_apply R B J.ResidueField]

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
J : Ideal A
hJ : J ∈ Ideal.under R ⁻¹' I.minimalPrimes
⊢ Ideal.map (algebraMap R A) q ≤ J

Tactic:
← IsLocalization.under_le_under_iff q.primeCompl A,

Goal state after:
case refine_2
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this : IsLocalRing A
J : Ideal A
hJ : J ∈ Ideal.under R ⁻¹' I.minimalPrimes
⊢ Ideal.under R (Ideal.map (algebraMap R A) q) ≤ Ideal.under R J
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this✝ : IsLocalRing A
J : Ideal A
hJ : J ∈ Ideal.under R ⁻¹' I.minimalPrimes
this : J ≠ ⊤
⊢ Ideal.under R J ≤ q

Tactic:
← disjoint_under_iff q.primeCompl A J

Goal state after:
case refine_2
R : Type u_1
inst✝³ : CommSemiring R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
q : Ideal R
hqp : q.IsPrime
inst✝ : IsLocalization.AtPrime A q
I : Ideal R
hIq : q ∈ I.minimalPrimes
this✝ : IsLocalRing A
J : Ideal A
hJ : J ∈ Ideal.under R ⁻¹' I.minimalPrimes
this : Disjoint ↑q.primeCompl ↑(Ideal.under R J)
⊢ Ideal.under R J ≤ q
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
t : Set X
ht : IsLocallyClosed t
U₁ Z₁ : Set X
hU₁ : IsOpen[inst✝] U₁
hZ₁ : IsClosed[inst✝] Z₁
⊢ IsLocallyClosed (U₁ ∩ Z₁ ∩ t)

Tactic:
obtain ⟨U₂, Z₂, hU₂, hZ₂, rfl⟩ := ht

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
U₁ Z₁ : Set X
hU₁ : IsOpen[inst✝] U₁
hZ₁ : IsClosed[inst✝] Z₁
U₂ Z₂ : Set X
hU₂ : IsOpen[inst✝] U₂
hZ₂ : IsClosed[inst✝] Z₂
⊢ IsLocallyClosed (U₁ ∩ Z₁ ∩ (U₂ ∩ Z₂))
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsClosedMap f
s : Set β
t : Set ↑(f ⁻¹' s)
⊢ ∀ (u : Set α),
    IsClosed[inst✝¹] u → Subtype.val ⁻¹' u = t → ∃ v, IsClosed[inst✝] v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t

Tactic:
exact fun u hu e => ⟨f '' u, H u hu, by simp [← e, image_restrictPreimage]⟩

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
H : IsOpenMap f
s : Set β
t : Set ↑(f ⁻¹' s)
⊢ ∀ (u : Set α),
    IsOpen[inst✝¹] u → Subtype.val ⁻¹' u = t → ∃ v, IsOpen[inst✝] v ∧ Subtype.val ⁻¹' v = s.restrictPreimage f '' t

Tactic:
exact fun u hu e => ⟨f '' u, H u hu, by simp [← e, image_restrictPreimage]⟩

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case e'_3
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
H : ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f)
s : Set α
hs : IsClosed[inst✝¹] s
i : ι
e_1✝ : ↥(U i) = ↑(U i).carrier
x : β
hx : x ∈ U i
⊢ (∃ y ∈ s, f y = x) ↔ ∃ y ∈ s, f y ∈ U i ∧ f y = x

Tactic:
exact ⟨fun ⟨a, b, c⟩ => ⟨a, b, c.symm ▸ hx, c⟩, by tauto⟩

Goal state after:
Module: Mathlib.Topology.LocalAtTarget

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
h : Continuous[inst✝¹, inst✝] f
⊢ IsOpen[inst✝] (range f) ↔ ∀ (x : ι), IsOpen[instTopologicalSpaceSubtype] (range ((U x).carrier.restrictPreimage f))

Tactic:
simp_rw [range_restrictPreimage]
    exact hU.isOpen_iff_coe_preimage

Goal state after:
Module: Mathlib.Topology.Spectral.Prespectral

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U : Opens X
x : X
hxU : x ∈ U
V : Set X
h₁ : IsOpen[inst✝²] V
h₂ : IsCompact V
hxV : x ∈ V
hVU : V ⊆ ↑U
⊢ x ∈
    (fun I ↦ ⨆ U ∈ I, U.toOpens) ((fun U ↦ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ }) U)

Tactic:
simp only [Opens.mem_iSup]

Goal state after:
case a
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PrespectralSpace X
U : Opens X
x : X
hxU : x ∈ U
V : Set X
h₁ : IsOpen[inst✝²] V
h₂ : IsCompact V
hxV : x ∈ V
hVU : V ⊆ ↑U
⊢ ∃ i, ∃ (_ : i ∈ { carrier := {V | ↑V ⊆ ↑U}, lower' := ⋯, nonempty' := ⋯, directed' := ⋯ }), x ∈ i.toOpens
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: a b : ℕ
⊢ 0 < a.factorizationLCMRight b

Tactic:
apply Nat.pos_of_ne_zero
  rw [factorizationLCMRight, Finsupp.prod_ne_zero_iff]
  intro p _ H
  by_cases h : b.factorization p ≤ a.factorization p
  · simp only [h, reduceIte, reduceCtorEq] at H
  · simp only [h, ↓reduceIte, pow_eq_zero_iff', ne_eq] at H
    simpa [H.1] using H.2

Goal state after:
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : (ulift.{u₁, u₂, u_1, u_2} f).Flat
⊢ (ULift.ringEquiv.toRingHom.comp ((ulift.{u₁, u₂, u_1, u_2} f).comp ULift.ringEquiv.symm.toRingHom)).Flat

Tactic:
comp_iff_of_bijective_left (Equiv.bijective _),

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : (ulift.{u₁, u₂, u_1, u_2} f).Flat
⊢ ((ulift.{u₁, u₂, u_1, u_2} f).comp ULift.ringEquiv.symm.toRingHom).Flat
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommSemiring R
⊢ vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s} ⊆ vanishingIdeal '' {s | IsIrreducible s}

Tactic:
exact Set.image_mono fun _ ↦ And.right

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

Goal state before:
pp: case refine_2
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
x : PrimeSpectrum R
h : x ∈ {p | Disjoint ↑M ↑p.asIdeal}
⊢ x ∈ Set.range (comap (algebraMap R S))

Tactic:
use ⟨x.asIdeal.map (algebraMap R S), IsLocalization.isPrime_of_isPrime_disjoint M S _ x.2 h⟩
    ext1
    exact IsLocalization.under_map_of_isPrime_disjoint M S x.2 h

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
⊢ Set.range (comap (RingHom.fst R S)) = zeroLocus ↑(RingHom.ker (RingHom.fst R S))

Tactic:
refine Set.ext fun p ↦ ⟨?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : PrimeSpectrum (R × S)
⊢ p ∈ Set.range (comap (RingHom.fst R S)) → p ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))

case refine_2
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 ∈ Set.range (comap (RingHom.fst R S))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Set.range (comap (RingHom.snd R S)) = zeroLocus ↑(RingHom.ker (RingHom.snd R S))

Tactic:
refine Set.ext fun p ↦ ⟨?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : PrimeSpectrum (R × S)
⊢ p ∈ Set.range (comap (RingHom.snd R S)) → p ∈ zeroLocus ↑(RingHom.ker (RingHom.snd R S))

case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : PrimeSpectrum (R × S)
h : p ∈ zeroLocus ↑(RingHom.ker (RingHom.snd R S))
⊢ p ∈ Set.range (comap (RingHom.snd R S))
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case neg
G : Type u
inst✝ : Monoid G
h : ¬ExponentExists G
this : {d | 0 < d ∧ ∀ (x : G), x ^ d = 1} = ∅
⊢ exponent G = sInf {d | 0 < d ∧ ∀ (x : G), x ^ d = 1}

Tactic:
Monoid.exponent_eq_zero_iff.mpr h,

Goal state after:
case neg
G : Type u
inst✝ : Monoid G
h : ¬ExponentExists G
this : {d | 0 < d ∧ ∀ (x : G), x ^ d = 1} = ∅
⊢ 0 = sInf {d | 0 < d ∧ ∀ (x : G), x ^ d = 1}
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: G : Type u
inst✝ : Monoid G
⊢ exponent G = 0 ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1

Tactic:
exponent_eq_zero_iff,

Goal state after:
G : Type u
inst✝ : Monoid G
⊢ ¬ExponentExists G ↔ ∀ n > 0, ∃ g, g ^ n ≠ 1
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ StableUnderGeneralization {x} ↔ x.asIdeal ∈ minimalPrimes R

Tactic:
by
  simp_rw [← isMin_iff, StableUnderGeneralization, ← le_iff_specializes, Set.mem_singleton_iff,
    @forall_comm _ (_ = _), forall_eq]
  exact ⟨fun H a h ↦ (H a h).ge, fun H a h ↦ le_antisymm h (H h)⟩

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

Goal state before:
pp: case refine_2.mpr.refine_2.inr
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝¹ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this✝ : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u + v = 1
i : ι
hi : ¬i = a
this : ∀ i_1 ∈ t, i_1 ≠ i → ↑(μ i) ∈ I i_1
j : ι
hj✝ : j ∈ Finset.cons a t hat
ij : j ≠ i
hj : j ∈ t
⊢ u * ↑(μ i) ∈ I j

Tactic:
· exact mul_mem_left _ _ (this _ hj ij)

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

Goal state before:
pp: case refine_2.mpr.refine_3.e_a
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u * 1 + v = 1
⊢ ∑ x ∈ t, ↑(if hi : x = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ x), ⋯⟩) = ∑ i ∈ t, u * ↑(μ i)

Tactic:
apply Finset.sum_congr rfl

Goal state after:
case refine_2.mpr.refine_3.e_a
ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
hs : (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
Hb : ∀ b ∈ ↑t, a ≠ b → I a ⊔ I b = ⊤
μ : (i : ι) → ↥(⨅ j ∈ t, ⨅ (_ : j ≠ i), I j)
hμ : ∑ i ∈ t, ↑(μ i) = 1
u : R
hu : u ∈ I a
v : R
hv : v ∈ ⨅ i ∈ t, I i
huv : u * 1 + v = 1
⊢ ∀ x ∈ t, ↑(if hi : x = a then ⟨v, ⋯⟩ else ⟨u * ↑(μ x), ⋯⟩) = u * ↑(μ x)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
⊢ b • 0 + a • b • y = 0

Tactic:
hy,

Goal state after:
case h
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
x y : M
a : S
hx : a • x = 0
b : S
hy : b • y = 0
⊢ b • 0 + a • 0 = 0
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 : 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

Tactic:
rw [mem_comap, mem_sup] at hrn

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 : ∃ y ∈ I • (R ∙ i), ∃ z ∈ I • span R s, y + z = ((LinearMap.lsmul R M) r) i
hs : i ∈ ↑N ∧ s ⊆ ↑N
⊢ ∃ c, c - 1 ∈ I ∧ c • i ∈ I • span R s
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case insert.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
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
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hrn : n ∈ comap ((LinearMap.lsmul R M) r) (I • (R ∙ i) ⊔ I • span R s)
hn : n ∈ N
⊢ n ∈ comap ((LinearMap.lsmul R M) (c * r)) (I • span R s)

Tactic:
rw [mem_comap, mem_sup] at hrn

Goal state after:
case insert.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
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
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hrn : ∃ y ∈ I • (R ∙ i), ∃ z ∈ I • span R s, y + z = ((LinearMap.lsmul R M) r) n
hn : n ∈ N
⊢ n ∈ comap ((LinearMap.lsmul R M) (c * r)) (I • span 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 F' : I✝.Filtration M
I : Ideal R
N : Submodule R M
i : ℕ
⊢ I • I ^ i • N ≤ I ^ (i + 1) • N

Tactic:
rw [add_comm, pow_add, mul_smul, pow_one]

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
n : ℕ
a✝ : n ≥ 0
⊢ I • I ^ n • N = I ^ (n + 1) • N

Tactic:
rw [add_comm, pow_add, mul_smul, pow_one]

Goal state after:
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: case smul₀
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'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
x p : M
hp : p ∈ P
⊢ r • p ∈ N

Tactic:
rw [← Submodule.Quotient.mk_eq_zero, Quotient.mk_smul]

Goal state after:
case smul₀
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'
hNN'' : P ≤ N ⊔ N'
h1 : map N.mkQ P = map N.mkQ N'
h2 : map N.mkQ P = map N.mkQ (I • N')
hle : map N.mkQ P ≤ I • map N.mkQ P
r : R
hmem : r - 1 ∈ I
hr : ∀ n ∈ map N.mkQ P, r • n = 0
x p : M
hp : p ∈ P
⊢ r • Quotient.mk p = 0
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
s : Set ↥(maximalIdeal R)
⊢ Submodule.span (ResidueField R) (⇑(maximalIdeal R).toCotangent '' s) = ⊤ ↔ Submodule.span R s = ⊤

Tactic:
by
  rw [← map_eq_top_iff, ← (Submodule.restrictScalars_injective R ..).eq_iff,
    Submodule.restrictScalars_span]
  · simp
  · exact Ideal.Quotient.mk_surjective

Goal state after:
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₁ m₂ : M
X : C
inst✝ : F.Monoidal
⊢ (μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫
      (μ F m₁ (𝟙_ M ⊗ m₂)).app X ≫ (F.map (α_ m₁ (𝟙_ M) m₂).inv).app X ≫ (δ F (m₁ ⊗ 𝟙_ M) m₂).app X =
    (μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫
      (F.map (λ_ m₂).hom).app ((F.obj m₁).obj X) ≫ (F.obj m₂).map ((F.map (ρ_ m₁).inv).app X)

Tactic:
rw [← obj_η_app_assoc, ← Functor.map_comp]

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₁ m₂ : M
X : C
inst✝ : F.Monoidal
⊢ (μ F (𝟙_ M) m₂).app ((F.obj m₁).obj X) ≫
      (μ F m₁ (𝟙_ M ⊗ m₂)).app X ≫ (F.map (α_ m₁ (𝟙_ M) m₂).inv).app X ≫ (δ F (m₁ ⊗ 𝟙_ M) m₂).app X =
    (F.obj m₂).map ((η F).app ((F.obj m₁).obj X) ≫ (F.map (ρ_ m₁).inv).app X)
Module: Mathlib.CategoryTheory.GradedObject

Goal state before:
pp: I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst✝² : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst✝¹ : X.HasMap p
inst✝ : Y.HasMap p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
i : I
c : (j : J) → q j = q (p i) → X.CofanMapObjFun p j
hc : (j : J) → (hj : q j = q (p i)) → IsColimit (c j hj)
c' : Cofan fun j ↦ (c ↑j ⋯).pt
hc' : IsColimit c'
s : Cofan (X.mapObjFun r (q (p i)))
m : (X.cofanMapObjComp p q r hpqr (q (p i)) c c').pt ⟶ s.pt
hm : ∀ (j : ↑(r ⁻¹' {q (p i)})), Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c') j ≫ m = s.inj j
⊢ Cofan.inj (c (p i) ⋯) ⟨i, ⋯⟩ ≫ c'.inj ⟨p i, ⋯⟩ ≫ m = s.inj ⟨↑⟨i, ⋯⟩, ⋯⟩

Tactic:
← hm

Goal state after:
I : Type u_1
J : Type u_2
K : Type u_3
C : Type u_4
inst✝² : Category.{v_1, u_4} C
X Y Z : GradedObject I C
φ : X ⟶ Y
e : X ≅ Y
ψ : Y ⟶ Z
p : I → J
j : J
inst✝¹ : X.HasMap p
inst✝ : Y.HasMap p
q : J → K
r : I → K
hpqr : ∀ (i : I), q (p i) = r i
i : I
c : (j : J) → q j = q (p i) → X.CofanMapObjFun p j
hc : (j : J) → (hj : q j = q (p i)) → IsColimit (c j hj)
c' : Cofan fun j ↦ (c ↑j ⋯).pt
hc' : IsColimit c'
s : Cofan (X.mapObjFun r (q (p i)))
m : (X.cofanMapObjComp p q r hpqr (q (p i)) c c').pt ⟶ s.pt
hm : ∀ (j : ↑(r ⁻¹' {q (p i)})), Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c') j ≫ m = s.inj j
⊢ Cofan.inj (c (p i) ⋯) ⟨i, ⋯⟩ ≫ c'.inj ⟨p i, ⋯⟩ ≫ m =
    Cofan.inj (X.cofanMapObjComp p q r hpqr (q (p i)) c c') ⟨↑⟨i, ⋯⟩, ⋯⟩ ≫ m