mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂) →
    ∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y

pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y) →
    ∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂

Tactic:
·

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂) →
    ∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ 1 ∣ p ^ b.factorization p

pp: case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬b.factorization p ≤ a.factorization p
⊢ p ^ (a.lcm b).factorization p ∣ p ^ b.factorization p

Tactic:
·

Goal state after:
case pos
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : b.factorization p ≤ a.factorization p
⊢ 1 ∣ p ^ b.factorization p
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y) →
    ∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂

Tactic:
·

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y) →
    ∀ (z₁ z₂ : Set (PrimeSpectrum R)),
      (∃ I, z₁ = zeroLocus ↑I) →
        (∃ I, z₂ = zeroLocus ↑I) → zeroLocus ↑I ⊆ z₁ ∪ z₂ → zeroLocus ↑I ⊆ z₁ ∨ zeroLocus ↑I ⊆ z₂
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬b.factorization p ≤ a.factorization p
⊢ p ^ (a.lcm b).factorization p ∣ p ^ b.factorization p

Tactic:
·

Goal state after:
case neg
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
p : ℕ
le : ¬b.factorization p ≤ a.factorization p
⊢ p ^ (a.lcm b).factorization p ∣ p ^ b.factorization p
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y) ↔
    ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
·

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R),
      zeroLocus ↑I ⊆ zeroLocus ↑x ∪ zeroLocus ↑y → zeroLocus ↑I ⊆ zeroLocus ↑x ∨ zeroLocus ↑I ⊆ zeroLocus ↑y) ↔
    ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
Module: Mathlib.Data.Nat.Factorization.LCM

Goal state before:
pp: case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ b.factorization.support ⊆ (a.lcm b).factorization.support

pp: case inr.inr.h
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ ∀ i ∈ (a.lcm b).factorization.support, i ^ 0 = 1

Tactic:
·

Goal state after:
case inr.inr.hs
a b : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ b.factorization.support ⊆ (a.lcm b).factorization.support
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) → ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I

pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I

Tactic:
·

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I) → ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I

Tactic:
·

Goal state after:
case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsRadical
⊢ (∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I) → ∀ (x y : Ideal R), x ⊓ y ≤ I → x ≤ I ∨ y ≤ I
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}

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

Tactic:
·

Goal state after:
case refine_1
R : Type u
inst✝ : CommSemiring R
⊢ vanishingIdeal '' {s | IsClosed s ∧ IsIrreducible s} ⊆ vanishingIdeal '' {s | IsIrreducible s}
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case succ.inl
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
ihn : D (a ^ 0) = 0 • a ^ (0 - 1) • D a
⊢ D (a ^ (0 + 1)) = (0 + 1) • a ^ (0 + 1 - 1) • D a

pp: case succ.inr
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
hpos : 0 < n
⊢ D (a ^ (n + 1)) = (n + 1) • a ^ (n + 1 - 1) • D a

Tactic:
·

Goal state after:
case succ.inl
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
ihn : D (a ^ 0) = 0 • a ^ (0 - 1) • D a
⊢ D (a ^ (0 + 1)) = (0 + 1) • a ^ (0 + 1 - 1) • D a
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case succ.inr
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
hpos : 0 < n
⊢ D (a ^ (n + 1)) = (n + 1) • a ^ (n + 1 - 1) • D a

Tactic:
·

Goal state after:
case succ.inr
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a : A
n : ℕ
ihn : D (a ^ n) = n • a ^ (n - 1) • D a
hpos : 0 < n
⊢ D (a ^ (n + 1)) = (n + 1) • a ^ (n + 1 - 1) • D a
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case C
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
x : A
a✝ : R
⊢ D ((aeval x) (C a✝)) = (aeval x) (derivative (C a✝)) • D x

pp: case add
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
x : A
p✝ q✝ : R[X]
a✝¹ : D ((aeval x) p✝) = (aeval x) (derivative p✝) • D x
a✝ : D ((aeval x) q✝) = (aeval x) (derivative q✝) • D x
⊢ D ((aeval x) (p✝ + q✝)) = (aeval x) (derivative (p✝ + q✝)) • D x

pp: case monomial
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
x : A
n✝ : ℕ
a✝¹ : R
a✝ : D ((aeval x) (C a✝¹ * X ^ n✝)) = (aeval x) (derivative (C a✝¹ * X ^ n✝)) • D x
⊢ D ((aeval x) (C a✝¹ * X ^ (n✝ + 1))) = (aeval x) (derivative (C a✝¹ * X ^ (n✝ + 1))) • D x

Tactic:
·

Goal state after:
case C
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
x : A
a✝ : R
⊢ D ((aeval x) (C a✝)) = (aeval x) (derivative (C a✝)) • D x
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case add
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
x : A
p✝ q✝ : R[X]
a✝¹ : D ((aeval x) p✝) = (aeval x) (derivative p✝) • D x
a✝ : D ((aeval x) q✝) = (aeval x) (derivative q✝) • D x
⊢ D ((aeval x) (p✝ + q✝)) = (aeval x) (derivative (p✝ + q✝)) • D x

pp: case monomial
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
x : A
n✝ : ℕ
a✝¹ : R
a✝ : D ((aeval x) (C a✝¹ * X ^ n✝)) = (aeval x) (derivative (C a✝¹ * X ^ n✝)) • D x
⊢ D ((aeval x) (C a✝¹ * X ^ (n✝ + 1))) = (aeval x) (derivative (C a✝¹ * X ^ (n✝ + 1))) • D x

Tactic:
·

Goal state after:
case add
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
x : A
p✝ q✝ : R[X]
a✝¹ : D ((aeval x) p✝) = (aeval x) (derivative p✝) • D x
a✝ : D ((aeval x) q✝) = (aeval x) (derivative q✝) • D x
⊢ D ((aeval x) (p✝ + q✝)) = (aeval x) (derivative (p✝ + q✝)) • D x
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case monomial
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
x : A
n✝ : ℕ
a✝¹ : R
a✝ : D ((aeval x) (C a✝¹ * X ^ n✝)) = (aeval x) (derivative (C a✝¹ * X ^ n✝)) • D x
⊢ D ((aeval x) (C a✝¹ * X ^ (n✝ + 1))) = (aeval x) (derivative (C a✝¹ * X ^ (n✝ + 1))) • D x

Tactic:
·

Goal state after:
case monomial
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
x : A
n✝ : ℕ
a✝¹ : R
a✝ : D ((aeval x) (C a✝¹ * X ^ n✝)) = (aeval x) (derivative (C a✝¹ * X ^ n✝)) • D x
⊢ D ((aeval x) (C a✝¹ * X ^ (n✝ + 1))) = (aeval x) (derivative (C a✝¹ * X ^ (n✝ + 1))) • D x
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
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
⊢ x ∈ Set.range (comap (algebraMap R S)) → x ∈ {p | Disjoint ↑M ↑p.asIdeal}

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:
·

Goal state after:
case refine_1
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
⊢ x ∈ Set.range (comap (algebraMap R S)) → x ∈ {p | Disjoint ↑M ↑p.asIdeal}
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:
·

Goal state after:
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))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mp
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
Z : Set (PrimeSpectrum S)
⊢ (∃ s, zeroLocus s = Z) → ∃ a, zeroLocus (⇑(algebraMap R S) '' a) = Z

pp: case mpr
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
Z : Set (PrimeSpectrum S)
⊢ (∃ a, zeroLocus (⇑(algebraMap R S) '' a) = Z) → ∃ s, zeroLocus s = Z

Tactic:
·

Goal state after:
case mp
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
Z : Set (PrimeSpectrum S)
⊢ (∃ s, zeroLocus s = Z) → ∃ a, zeroLocus (⇑(algebraMap R S) '' a) = Z
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case mpr
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
Z : Set (PrimeSpectrum S)
⊢ (∃ a, zeroLocus (⇑(algebraMap R S) '' a) = Z) → ∃ s, zeroLocus s = Z

Tactic:
·

Goal state after:
case mpr
R : Type u
S : Type v
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M : Submonoid R
inst✝ : IsLocalization M S
Z : Set (PrimeSpectrum S)
⊢ (∃ a, zeroLocus (⇑(algebraMap R S) '' a) = Z) → ∃ s, zeroLocus s = Z
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: 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))

pp: 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))

Tactic:
·

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))
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
D : Derivation R A M
a : A
⊢ ((↑e.symm).compDer ((↑e).compDer.toFun D)) a = D a

Tactic:
exact e.symm_apply_apply (D a)

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

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

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

Tactic:
·

Goal state after:
case refine_2.inl
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.fst R S))
p : Ideal R
hp : p.IsPrime
eq : p✝.asIdeal = p.prod ⊤
⊢ p✝ ∈ Set.range (comap (RingHom.fst R S))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
·

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommRing A
inst✝⁴ : CommRing M
inst✝³ : Algebra R A
inst✝² : Algebra R M
F : Type u_4
inst✝¹ : FunLike F A M
inst✝ : AlgHomClass F R A M
f : F
f_inv : M → A
hf : Function.RightInverse f_inv ⇑f
d : Derivation R A A
hd : ∀ (x : A), f x = 0 → f (d x) = 0
x y : M
⊢ f (d (f_inv (x + y))) = f (d (f_inv x)) + f (d (f_inv y))

Tactic:
suffices f (d (f_inv (x + y) - (f_inv x + f_inv y))) = 0 by simpa [sub_eq_zero]
    apply hd
    simp [hf _]

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

Goal state before:
pp: 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))

pp: 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))

Tactic:
·

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))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_2.inl
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 : Ideal R
hp : p.IsPrime
eq : p✝.asIdeal = p.prod ⊤
⊢ p✝ ∈ Set.range (comap (RingHom.snd R S))

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

Tactic:
·

Goal state after:
case refine_2.inl
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 : Ideal R
hp : p.IsPrime
eq : p✝.asIdeal = p.prod ⊤
⊢ p✝ ∈ Set.range (comap (RingHom.snd R S))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

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

Tactic:
·

Goal state after:
case refine_2.inr
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : PrimeSpectrum (R × S)
h : p✝ ∈ zeroLocus ↑(RingHom.ker (RingHom.snd R S))
p : Ideal S
hp : p.IsPrime
eq : p✝.asIdeal = ⊤.prod p
⊢ p✝ ∈ Set.range (comap (RingHom.snd R S))
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Continuous ⇑(primeSpectrumProd R S).symm

pp: case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ IsClosedMap ⇑(primeSpectrumProd R S).symm

Tactic:
·

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ Continuous ⇑(primeSpectrumProd R S).symm
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
⊢ IsClosedMap ⇑(primeSpectrumProd R S).symm

Tactic:
·

Goal state after:
case refine_2
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
⊢ IsClosedMap ⇑(primeSpectrumProd R S).symm
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
⊢ D 0⁻¹ = -0⁻¹ ^ 2 • D 0

pp: case inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
ha : a ≠ 0
⊢ D a⁻¹ = -a⁻¹ ^ 2 • D a

Tactic:
·

Goal state after:
case inl
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
⊢ D 0⁻¹ = -0⁻¹ ^ 2 • D 0
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
ha : a ≠ 0
⊢ D a⁻¹ = -a⁻¹ ^ 2 • D a

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
ha : a ≠ 0
⊢ D a⁻¹ = -a⁻¹ ^ 2 • D a
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case h_open
R : Type u
inst✝ : CommSemiring R
⊢ ∀ u ∈ Set.range fun r ↦ ↑(basicOpen r), IsOpen u

pp: case h_nhds
R : Type u
inst✝ : CommSemiring R
⊢ ∀ (a : PrimeSpectrum R) (u : Set (PrimeSpectrum R)),
    a ∈ u → IsOpen u → ∃ v ∈ Set.range fun r ↦ ↑(basicOpen r), a ∈ v ∧ v ⊆ u

Tactic:
·

Goal state after:
case h_open
R : Type u
inst✝ : CommSemiring R
⊢ ∀ u ∈ Set.range fun r ↦ ↑(basicOpen r), IsOpen u
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: case h_nhds
R : Type u
inst✝ : CommSemiring R
⊢ ∀ (a : PrimeSpectrum R) (u : Set (PrimeSpectrum R)),
    a ∈ u → IsOpen u → ∃ v ∈ Set.range fun r ↦ ↑(basicOpen r), a ∈ v ∧ v ⊆ u

Tactic:
·

Goal state after:
case h_nhds
R : Type u
inst✝ : CommSemiring R
⊢ ∀ (a : PrimeSpectrum R) (u : Set (PrimeSpectrum R)),
    a ∈ u → IsOpen u → ∃ v ∈ Set.range fun r ↦ ↑(basicOpen r), a ∈ v ∧ v ⊆ u
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : n = 0
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

pp: case neg
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : n = 0
⊢ D (a ^ n) = n • a ^ (n - 1) • D a
Module: Mathlib.RingTheory.Derivation.Basic

Goal state before:
pp: case pos
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : a = 0
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

pp: case neg
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : ¬a = 0
⊢ D (a ^ n) = n • a ^ (n - 1) • D a

Tactic:
·

Goal state after:
case pos
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
K : Type u_4
inst✝² : Field K
inst✝¹ : Module K M
inst✝ : Algebra R K
D : Derivation R K M
a : K
n : ℤ
hn : ¬n = 0
ha : a = 0
⊢ D (a ^ n) = n • a ^ (n - 1) • D a