mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
g : G
a : A
⊢ IsCycle₁ (single g a) ↔ g • a = a

Tactic:
rw [← (MulAction.bijective g⁻¹).1.eq_iff]

Goal state after:
G : Type u_1
A : Type u_2
inst✝² : Group G
inst✝¹ : AddCommGroup A
inst✝ : DistribMulAction G A
g : G
a : A
⊢ IsCycle₁ (single g a) ↔ g⁻¹ • g • a = g⁻¹ • a
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
⊢ (inhomogeneousChains A).d 0 0 = 0

Tactic:
simp [ChainComplex.of.d]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
x : ↑A
⊢ (ConcreteCategory.hom ((inhomogeneousChains A).d 0 0)) ((ConcreteCategory.hom (chainsIso₀ A).inv) x) = 0

Tactic:
simp [ChainComplex.of.d]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R⟦X⟧
S : Set R
hXI : X ∈ I
hSI : span S = Ideal.map constantCoeff I
⊢ I ≤ span {X} ⊔ Ideal.map (C.comp constantCoeff) I

Tactic:
exact fun f hf ↦ mem_span_singleton_sup.mpr
    ⟨_, _, mem_map_of_mem _ hf, f.eq_shift_mul_X_add_const.symm⟩

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Topology

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
⊢ T2Space R ∧ CompleteSpace R ↔ CompleteSpace R ∧ T2Space R

Tactic:
and_comm

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : UniformSpace R
inst✝ : IsUniformAddGroup R
I : Ideal R
hI : IsAdic I
⊢ CompleteSpace R ∧ T2Space R ↔ CompleteSpace R ∧ T2Space R
Module: Mathlib.RingTheory.MvPowerSeries.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : ¬optionElim n y = x
h3 : n = x none
h : y = x.some
u : Option σ
⊢ (optionElim n y) u = x u

Tactic:
cases u

Goal state after:
case none
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : ¬optionElim n y = x
h3 : n = x none
h : y = x.some
⊢ (optionElim n y) none = x none

case some
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
x : Option σ →₀ ℕ
r : R
n : ℕ
y : σ →₀ ℕ
h1 : ¬optionElim n y = x
h3 : n = x none
h : y = x.some
val✝ : σ
⊢ (optionElim n y) (Option.some val✝) = x (Option.some val✝)
Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : WithIdeal R
S : Type u_2
inst✝¹ : CommRing S
inst✝ : WithIdeal S
e : R ≃+* S
h : Ideal.map e.toRingHom i = i
⊢ Ideal.map e.toRingHom i ≤ i

Tactic:
rw [h]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b c : ℕ
x : AdicCompletion I M
h : c = b + a
ha : ↑x a = 0
⊢ ∃ t, (powSMulQuotInclusion I M h ⊤) t = ↑x c

Tactic:
by
  simpa [← LinearMap.mem_range, range_powSMulQuotInclusion] using
    (val_apply_mem_smul_top_iff I (show a ≤ c by lia)).mpr ha

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
x : ↑(ModuleCat.of k (G →₀ ↑A))
x✝ : x ∈ cycles₁ A
this :
  (ConcreteCategory.hom ((mapShortComplexH1 f φ).τ₂ ≫ (shortComplexH1 B).g)) x =
    (ConcreteCategory.hom ((shortComplexH1 A).g ≫ (mapShortComplexH1 f φ).τ₃)) x
⊢ (ModuleCat.Hom.hom (chainsMap₁ f φ)) x ∈ cycles₁ B

Tactic:
simp_all [cycles₁, shortComplexH1]

Goal state after:
Module: Mathlib.RingTheory.Algebraic.Denominator

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Algebra.denominator ℤ Polynomial.X = 0

Tactic:
by_contra h
  exact Polynomial.transcendental_X ℤ
    ((Algebra.isIntegral_denominator_smul _).isAlgebraic.of_smul
      (mem_nonZeroDivisors_of_ne_zero h))

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Completeness

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
x : AdicCompletion I ↥(I ^ n • ⊤)
⊢ (ofPowSMul I M n) x ∈ (map I ((lsum R) fun i ↦ ↑i • LinearMap.id)).range

Tactic:
have : Function.Surjective ((lsum R fun i : s ↦ i.val • (LinearMap.id : M →ₗ[R] M)).codRestrict
    (I ^ n • ⊤) (fun _ ↦ by simp [← hs, span_smul_eq, smul_top_eq_range_lsum])) := by
    rw [← LinearMap.range_eq_top, LinearMap.range_codRestrict, ← hs, span_smul_eq,
      smul_top_eq_range_lsum]
    simp

Goal state after:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
s : Finset R
hs : Ideal.span ↑s = I ^ n
x : AdicCompletion I ↥(I ^ n • ⊤)
this : Function.Surjective ⇑(LinearMap.codRestrict (I ^ n • ⊤) ((lsum R) fun i ↦ ↑i • LinearMap.id) ⋯)
⊢ (ofPowSMul I M n) x ∈ (map I ((lsum R) fun i ↦ ↑i • LinearMap.id)).range
Module: Mathlib.RingTheory.Algebraic.Pi

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : CommSemiring T
inst✝¹ : Algebra R S
inst✝ : Algebra S T
z : S
⊢ (algebraMap S T) ((aeval z) 0) = 0 z

Tactic:
simp only [Pi.zero_apply, map_zero]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hc : c x • x = d • a
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ y ∈ s, y ≠ x → c y = 0
hcxa : d = c x
⊢ x = a

Tactic:
hcxa,

Goal state after:
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hc : c x • x = c x • a
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ y ∈ s, y ≠ x → c y = 0
hcxa : d = c x
⊢ x = a
Module: Mathlib.RingTheory.Coalgebra.GroupLike

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : AddCommGroup A
inst✝² : Module R A
inst✝¹ : Coalgebra R A
inst✝ : IsTorsionFree R A
a : A
s : Finset A
has : a ∉ s
ha : IsGroupLikeElem R a
hs : ∀ a ∈ s, IsGroupLikeElem R a
d : R
c : A → R
ih :
  ∀ (f g : A × A → R), ∑ x ∈ s ×ˢ s, f x • x.1 ⊗ₜ[R] x.2 = ∑ x ∈ s ×ˢ s, g x • x.1 ⊗ₜ[R] x.2 → ∀ i ∈ s ×ˢ s, f i = g i
key : ∀ i ∈ s ×ˢ s, (if i.1 = i.2 then d * c i.1 else 0) = c i.1 * c i.2
x : A
hc : c x • x = d • a
hx : x ∈ s
hcx : c x ≠ 0
hcy : ∀ y ∈ s, y ≠ x → c y = 0
hcxa : d = c x
⊢ x = a

Tactic:
rwa [hcxa, smul_right_inj hcx] at hc

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.ExtendedHom

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹² : CommRing A
inst✝¹¹ : CommRing B
inst✝¹⁰ : Algebra A B
inst✝⁹ : Module.IsTorsionFree A B
inst✝⁸ : IsDedekindDomain A
C : Type u_3
inst✝⁷ : CommRing C
inst✝⁶ : Algebra B C
inst✝⁵ : Algebra A C
inst✝⁴ : IsScalarTower A B C
inst✝³ : Module.IsTorsionFree B C
inst✝² : Module.IsTorsionFree A C
inst✝¹ : IsDedekindDomain C
inst✝ : IsDedekindDomain B
⊢ (extendedHom B C).comp (extendedHom A B) = extendedHom A C

Tactic:
ext x
  exact extendedHom_comp_apply A B C x

Goal state after:
Module: Mathlib.RingTheory.Polynomial.ContentIdeal

Goal state before:
pp: R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h : p.contentIdeal = ⊤
⊢ Submodule.IsPrincipal p.contentIdeal

Tactic:
rw [h]

Goal state after:
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
h : p.contentIdeal = ⊤
⊢ Submodule.IsPrincipal ⊤
Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x✝ : Kˣ ⧸ (powMonoidHom n).range
hx : x✝ ∈ {x | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}
v : HeightOneSpectrum R
hv : v ∉ S
⊢ (v.valuationOfNeZeroMod n) x✝⁻¹ = 1

Tactic:
map_inv,

Goal state after:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v✝ : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
x✝ : Kˣ ⧸ (powMonoidHom n).range
hx : x✝ ∈ {x | ∀ v ∉ S, (v.valuationOfNeZeroMod n) x = 1}
v : HeightOneSpectrum R
hv : v ∉ S
⊢ ((v.valuationOfNeZeroMod n) x✝)⁻¹ = 1
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
⊢ {r | ∃ x, x ≠ 0 ∧ r • x = 0} = {a | ∃ x, ∃ (_ : a • x = 0), ¬x = 0}

Tactic:
exists_prop,

Goal state after:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
⊢ {r | ∃ x, x ≠ 0 ∧ r • x = 0} = {a | ∃ x, a • x = 0 ∧ ¬x = 0}
Module: Mathlib.RingTheory.Regular.IsSMulRegular

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
⊢ {r | ∃ x, x ≠ 0 ∧ r • x = 0} = {a | ∃ x, a • x = 0 ∧ ¬x = 0}

Tactic:
and_comm

Goal state after:
Module: Mathlib.RingTheory.Depth.Rees

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
Nfin : Module.Finite R ↑N
Nsupp : Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      ∀ (rs : List R),
        (∀ r ∈ rs, r ∈ I) → RingTheory.Sequence.IsRegular (↑M) rs → rs.length = n → ∀ i < n, Subsingleton (Ext N M i)
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
rs : List R
i✝ : ℕ
le_rad : I ≤ (Module.annihilator R ↑N).radical
a : R
rs' : List R
k : ℕ
hk : a ^ k ∈ Module.annihilator R ↑N
reg : IsSMulRegular (↑M) a ∧ RingTheory.Sequence.IsRegular (QuotSMulTop a ↑M) rs'
mem : a ∈ I ∧ ∀ a ∈ rs', a ∈ I
len : rs'.length = n
i : ℕ
hi : i + 1 < n + 1
g : AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₁ (i + 1)) ⟶
  AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₂ (i + 1)) :=
  AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex a).f).postcomp N ⋯)
⊢ Subsingleton (Ext N M (i + 1))

Tactic:
have mono_g : Mono g := by
          apply (Ext.covariant_sequence_exact₁' N reg.1.smulShortComplex_shortExact i (i + 1)
            rfl).mono_g ((AddCommGrpCat.isZero_of_iff_subsingleton.mpr ?_).eq_zero_of_src _)
          apply ih (ModuleCat.of R (QuotSMulTop a M)) _ rs' mem.2 reg.2 len i (by omega)
          exact (smul_top_quotSMulTop_ne_top_of_smul_top_ne_top mem.1 smul_lt.ne).lt_top

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
I : Ideal R
N : ModuleCat R
Nfin : Module.Finite R ↑N
Nsupp : Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I
n : ℕ
ih :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    I • ⊤ < ⊤ →
      ∀ (rs : List R),
        (∀ r ∈ rs, r ∈ I) → RingTheory.Sequence.IsRegular (↑M) rs → rs.length = n → ∀ i < n, Subsingleton (Ext N M i)
M : ModuleCat R
inst✝ : Module.Finite R ↑M
smul_lt : I • ⊤ < ⊤
rs : List R
i✝ : ℕ
le_rad : I ≤ (Module.annihilator R ↑N).radical
a : R
rs' : List R
k : ℕ
hk : a ^ k ∈ Module.annihilator R ↑N
reg : IsSMulRegular (↑M) a ∧ RingTheory.Sequence.IsRegular (QuotSMulTop a ↑M) rs'
mem : a ∈ I ∧ ∀ a ∈ rs', a ∈ I
len : rs'.length = n
i : ℕ
hi : i + 1 < n + 1
g : AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₁ (i + 1)) ⟶
  AddCommGrpCat.of (Ext N (M.smulShortComplex a).X₂ (i + 1)) :=
  AddCommGrpCat.ofHom ((Ext.mk₀ (M.smulShortComplex a).f).postcomp N ⋯)
mono_g : Mono g
⊢ Subsingleton (Ext N M (i + 1))
Module: Mathlib.RingTheory.DividedPowerAlgebra.Init

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_4
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : f = g
x✝¹ : ℕ
x✝ : M
⊢ f (dp R x✝¹ x✝) = g (dp R x✝¹ x✝)

Tactic:
rw [h]

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case pos
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : m < n
⊢ dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y

pp: case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
⊢ dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y

Tactic:
· exact dpow_add_of_lt hn_fac hmn hx hy

Goal state after:
case neg
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : n ≤ m
⊢ dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x

Tactic:
have hk : k < n := lt_of_le_of_lt le_add_self hkm

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hkm : m + k < n
x : A
hx : x ∈ I
hm : m < n
hk : k < n
⊢ dpow I m x * dpow I k x = ↑((m + k).choose m) * dpow I (m + k) x
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
⊢ dpow I m (dpow I k x) = ↑(m.uniformBell k) * ((↑(m * k)!)⁻¹ʳ * x ^ (m * k))

Tactic:
dpow_eq_of_mem (dpow_mem hk hx)

Goal state after:
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
m k : ℕ
hk : k ≠ 0
hkm : m * k < n
x : A
hx : x ∈ I
hmn : m < n
⊢ (↑m !)⁻¹ʳ * dpow I k x ^ m = ↑(m.uniformBell k) * ((↑(m * k)!)⁻¹ʳ * x ^ (m * k))
Module: Mathlib.RingTheory.Flat.LocallyFree

Goal state before:
pp: case inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Flat R M
p : Ideal R
inst✝ : p.IsPrime
h :
  ∀ (m : Ideal R) [inst : m.IsMaximal],
    rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk M { asIdeal := p, isPrime := ⋯ }
h✝ : Subsingleton R
⊢ ∃ a ∉ p, Free (Localization.Away a) (LocalizedModule.Away a M)

pp: case inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Flat R M
p : Ideal R
inst✝ : p.IsPrime
h :
  ∀ (m : Ideal R) [inst : m.IsMaximal],
    rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk M { asIdeal := p, isPrime := ⋯ }
h✝ : Nontrivial R
⊢ ∃ a ∉ p, Free (Localization.Away a) (LocalizedModule.Away a M)

Tactic:
· use 1, Ideal.IsPrime.one_notMem ‹_›
    exact Module.Free.of_subsingleton' (Localization.Away 1) (LocalizedModule.Away 1 M)

Goal state after:
case inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
inst✝¹ : Flat R M
p : Ideal R
inst✝ : p.IsPrime
h :
  ∀ (m : Ideal R) [inst : m.IsMaximal],
    rankAtStalk M { asIdeal := m, isPrime := ⋯ } = rankAtStalk M { asIdeal := p, isPrime := ⋯ }
h✝ : Nontrivial R
⊢ ∃ a ∉ p, Free (Localization.Away a) (LocalizedModule.Away a M)
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ P.cotangentComplex ∘ₗ ↑P.h1CotangentEquivCotangent = H1Cotangent.δ R P.Ring S

Tactic:
rw [h1CotangentEquivCotangent, LinearEquiv.coe_trans, LinearEquiv.coe_trans,
    h1CotangentEquivOfSurjective_toLinearMap, ← LinearMap.comp_assoc, ← LinearMap.comp_assoc,
    LinearEquiv.comp_toLinearMap_symm_eq, LinearMap.comp_assoc,
    h1CotangentExtendScalarsEquiv_toLinearMap]
  ext ⟨x, _⟩
  obtain ⟨⟨x : P.Ring, x_in : x ∈ P.ker⟩, rfl⟩ := Cotangent.mk_surjective x
  trans 1 ⊗ₜ[P.Ring] D R P.Ring x; · exact cotangentComplex_mk P ⟨x, x_in⟩
  let u : (Generators.self P.Ring S).toExtension.ker :=
    ⟨algebraMap P.Ring (Generators.self P.Ring S).toExtension.Ring x, by
      rwa [← Ideal.mem_comap, RingHom.comap_ker, ← IsScalarTower.algebraMap_eq]⟩
  rw [← Generators.H1Cotangent.δ_C _ _ u.prop]
  congr

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal := ⋯
⊢ span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ ⨅ s ∈ insert ⊤ {J | S ⊆ ↑J.carrier}, s.carrier

Tactic:
rw [le_iInf₂_iff]

Goal state after:
case a
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
J : hI.SubDPIdeal :=
  { carrier := span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}, isSubideal := ⋯, dpow_mem := ⋯ }
⊢ ∀ i ∈ insert ⊤ {J | S ⊆ ↑J.carrier}, span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x} ≤ i.carrier
Module: Mathlib.RingTheory.Grassmannian

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
k : ℕ
A✝ : Type w
inst✝⁵ : CommRing A✝
inst✝⁴ : Algebra R A✝
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A✝ →ₐ[R] B
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g : B →ₐ[R] C
A : CommAlgCat R
⊢ ↾map (CommAlgCat.Hom.hom (𝟙 A)) = 𝟙 G(k, ↑A ⊗[R] M; ↑A)

Tactic:
ext N : 1

Goal state after:
R : Type u
inst✝⁸ : CommRing R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
k : ℕ
A✝ : Type w
inst✝⁵ : CommRing A✝
inst✝⁴ : Algebra R A✝
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
f : A✝ →ₐ[R] B
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g : B →ₐ[R] C
A : CommAlgCat R
N : G(k, ↑A ⊗[R] M; ↑A)
⊢ (ConcreteCategory.hom (↾map (CommAlgCat.Hom.hom (𝟙 A)))) N = (ConcreteCategory.hom (𝟙 G(k, ↑A ⊗[R] M; ↑A))) N
Module: Mathlib.RingTheory.Grassmannian

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
k : ℕ
A : Type w
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
f✝ : A →ₐ[R] B
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g✝ : B →ₐ[R] C
X✝ Y✝ Z✝ : CommAlgCat R
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ↾map (CommAlgCat.Hom.hom (f ≫ g)) = ↾map (CommAlgCat.Hom.hom f) ≫ ↾map (CommAlgCat.Hom.hom g)

Tactic:
ext N : 1

Goal state after:
R : Type u
inst✝⁸ : CommRing R
M : Type v
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
k : ℕ
A : Type w
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B : Type w
inst✝³ : CommRing B
inst✝² : Algebra R B
f✝ : A →ₐ[R] B
C : Type w
inst✝¹ : CommRing C
inst✝ : Algebra R C
g✝ : B →ₐ[R] C
X✝ Y✝ Z✝ : CommAlgCat R
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
N : G(k, ↑X✝ ⊗[R] M; ↑X✝)
⊢ (ConcreteCategory.hom (↾map (CommAlgCat.Hom.hom (f ≫ g)))) N =
    (ConcreteCategory.hom (↾map (CommAlgCat.Hom.hom f) ≫ ↾map (CommAlgCat.Hom.hom g))) N
Module: Mathlib.RingTheory.HahnSeries.Binomial

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k n : ℕ
hn : n ≠ k
⊢ ((binomialFamily (1 + (single g) r) s) n).coeff (k • g) = 0

Tactic:
rw [binomialFamily_apply, add_sub_cancel_left, coeff_smul, single_pow, coeff_single_of_ne,
    smul_zero]

Goal state after:
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k n : ℕ
hn : n ≠ k
⊢ k • g ≠ n • g

case hx
Γ : Type u_1
R : Type u_2
inst✝⁴ : LinearOrder Γ
inst✝³ : AddCommMonoid Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : CommRing R
inst✝ : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k n : ℕ
hn : n ≠ k
⊢ 0 < (1 + (single g) r - 1).orderTop
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
x y : SummableFamily Γ R α
⊢ ⋃ a, ((⇑x + ⇑y) a).support ⊆ (⋃ a, (x a).support) ∪ ⋃ a, (y a).support

Tactic:
by
            rw [← Set.iUnion_union_distrib]
            exact Set.iUnion_mono fun a => support_add_subset ..

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.PowerSeries

Goal state before:
pp: Γ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring Γ
inst✝¹ : PartialOrder Γ
inst✝ : IsStrictOrderedRing Γ
r : R
⊢ (ofPowerSeries Γ R) (PowerSeries.C r) = C r

Tactic:
by
  ext n
  simp only [ofPowerSeries_apply, C, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    coeff_single]
  split_ifs with hn
  · subst hn
    convert! embDomain_coeff (a := 0) <;> simp
  · rw [embDomain_notin_image_support]
    simp only [not_exists, Set.mem_image, toPowerSeries_symm_apply_coeff, mem_support,
      PowerSeries.coeff_C]
    intro
    simp +contextual [Ne.symm hn]

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
tfae_3_to_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀) →
    ∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
tfae_2_to_1 :
  (∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R),
          (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀) →
    HenselianLocalRing R
hR : HenselianLocalRing R
K : Type u
_K : Field K
φ : R →+* K
hφ : Surjective ⇑φ
f : R[X]
hf : f.Monic
a₀ : R
H : φ (Polynomial.eval a₀ f) = 0 → IsUnit (Polynomial.eval a₀ (derivative f)) → ∃ a, f.IsRoot a ∧ φ (a - a₀) = 0
h₁ : φ (Polynomial.eval a₀ f) = 0
h₂ : φ (Polynomial.eval a₀ (derivative f)) ≠ 0
a : R
ha₁ : f.IsRoot a
ha₂ : φ (a - a₀) = 0
⊢ φ a = φ a₀

Tactic:
φ.map_sub,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
tfae_3_to_2 :
  (∀ {K : Type u} [inst : Field K] (φ : R →+* K),
      Surjective ⇑φ →
        ∀ (f : R[X]),
          f.Monic → ∀ (a₀ : K), eval₂ φ a₀ f = 0 → eval₂ φ a₀ (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀) →
    ∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R), (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀
tfae_2_to_1 :
  (∀ (f : R[X]),
      f.Monic →
        ∀ (a₀ : ResidueField R),
          (aeval a₀) f = 0 → (aeval a₀) (derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (residue R) a = a₀) →
    HenselianLocalRing R
hR : HenselianLocalRing R
K : Type u
_K : Field K
φ : R →+* K
hφ : Surjective ⇑φ
f : R[X]
hf : f.Monic
a₀ : R
H : φ (Polynomial.eval a₀ f) = 0 → IsUnit (Polynomial.eval a₀ (derivative f)) → ∃ a, f.IsRoot a ∧ φ (a - a₀) = 0
h₁ : φ (Polynomial.eval a₀ f) = 0
h₂ : φ (Polynomial.eval a₀ (derivative f)) ≠ 0
a : R
ha₁ : f.IsRoot a
ha₂ : φ a - φ a₀ = 0
⊢ φ a = φ a₀