mathlib-initiative/mathlib-tactics huggingface dataset:
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:
[

Goal state after:
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 ⋯)
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfullyFlat R S
inst✝ : Flat S (S ⊗[R] M)
⊢ Flat R M

Tactic:
Module.Flat.iff_lTensor_preserves_injective_linearMap

Goal state after:
R : Type u
M : Type v
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
S : Type u_1
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FaithfullyFlat R S
inst✝ : Flat S (S ⊗[R] M)
⊢ ∀ ⦃N N' : Type (max u v)⦄ [inst : AddCommGroup N] [inst_1 : AddCommGroup N'] [inst_2 : Module R N]
    [inst_3 : Module R N'] (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case tmul
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
J : Ideal T
hJ : J.IsPrime
x₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : (algebraMap R T) s ∉ J
e : c * (algebraMap R T) s * x₂ = c * (algebraMap R T) y
⊢ ∃ t r a, r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x₁ ⊗ₜ[R] x₂ = a ⊗ₜ[R] t

Tactic:
[

Goal state after:
case tmul
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
J : Ideal T
hJ : J.IsPrime
x₁ : S
x₂ : T
y s : R
c : T
hs : c ∉ J
hc : (algebraMap R T) s ∉ J
e : c * (algebraMap R T) s * x₂ = c * (algebraMap R T) y
⊢ ∃ t r a, r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x₁ ⊗ₜ[R] x₂ = a ⊗ₜ[R] t
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: case tmul
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
J : Ideal T
hJ : J.IsPrime
x₁ : S
x₂ : T
⊢ ∃ t r a, r • t ∉ J ∧ 1 ⊗ₜ[R] (r • t) * x₁ ⊗ₜ[R] x₂ = a ⊗ₜ[R] t

Tactic:
| tmul x₁ x₂ =>

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
T : Type u_3
inst✝² : CommRing T
inst✝¹ : Algebra R T
inst✝ : Algebra R S
hf₂ : (algebraMap R T).SurjectiveOnStalks
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
⊢ (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂

Tactic:
[

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
J : Ideal T
hJ : J.IsPrime
x₁ x₂ : S ⊗[R] T
t₁ : T
r₁ : R
a₁ : S
hr₁ : r₁ • t₁ ∉ J
e₁ : 1 ⊗ₜ[R] (r₁ • t₁) * x₁ = a₁ ⊗ₜ[R] t₁
t₂ : T
r₂ : R
a₂ : S
hr₂ : r₂ • t₂ ∉ J
e₂ : 1 ⊗ₜ[R] (r₂ • t₂) * x₂ = a₂ ⊗ₜ[R] t₂
⊢ (r₁ * r₂) • (t₁ * t₂) = r₁ • t₁ * r₂ • t₂
Module: Mathlib.RingTheory.SurjectiveOnStalks

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
⊢ (algebraMap R S).SurjectiveOnStalks

Tactic:
refine surjectiveOnStalks_of_exists_div fun s ↦ ?_

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
s : S
⊢ ∃ r s_1, IsUnit ((algebraMap R S) s_1) ∧ (algebraMap R S) s_1 * s = (algebraMap R S) r
Module: Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Flat A B
h : Function.Surjective (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ }
this : m = Ideal.comap (algebraMap A B) m'.asIdeal
⊢ Submodule.restrictScalars A (Ideal.map (algebraMap A B) m) ≠ ⊤

Tactic:
this

Goal state after:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Flat A B
h : Function.Surjective (PrimeSpectrum.comap (algebraMap A B))
m : Ideal A
hm : m.IsMaximal
m' : PrimeSpectrum B
hm' : PrimeSpectrum.comap (algebraMap A B) m' = { asIdeal := m, isPrime := ⋯ }
this : m = Ideal.comap (algebraMap A B) m'.asIdeal
⊢ Submodule.restrictScalars A (Ideal.map (algebraMap A B) (Ideal.comap (algebraMap A B) m'.asIdeal)) ≠ ⊤
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ ((↑a).1 + (↑a).2 * (↑b).1) * ((↑a).2 * (↑b).2) = 0

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ ((↑a).1 + (↑a).2 * (↑b).1) * ((↑a).2 * (↑b).2) = 0
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑a).1 + (↑a).2 * (↑b).1 + (↑a).2 * (↑b).2 = 1

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑a).1 + (↑a).2 * (↑b).1 + (↑a).2 * (↑b).2 = 1
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ a ≤ ⟨((↑a).1 + (↑a).2 * (↑b).1, (↑a).2 * (↑b).2), ⋯⟩

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ a ≤ ⟨((↑a).1 + (↑a).2 * (↑b).1, (↑a).2 * (↑b).2), ⋯⟩
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ b ≤ ⟨((↑a).1 + (↑a).2 * (↑b).1, (↑a).2 * (↑b).2), ⋯⟩

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ b ≤ ⟨((↑a).1 + (↑a).2 * (↑b).1, (↑a).2 * (↑b).2), ⋯⟩
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hac : a ≤ c
hbc : b ≤ c
⊢ ⟨((↑a).1 + (↑a).2 * (↑b).1, (↑a).2 * (↑b).2), ⋯⟩ ≤ c

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hac : a ≤ c
hbc : b ≤ c
⊢ ⟨((↑a).1 + (↑a).2 * (↑b).1, (↑a).2 * (↑b).2), ⋯⟩ ≤ c
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ a

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ a
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ b

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (aᶜ ⊔ bᶜ)ᶜ ≤ b
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : a ≤ b
hac : a ≤ c
⊢ a ≤ (bᶜ ⊔ cᶜ)ᶜ

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
hab : a ≤ b
hac : a ≤ c
⊢ a ≤ (bᶜ ⊔ cᶜ)ᶜ
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
⊢ (if h : i ∈ x.support then r i * x i else 0) = (r • DFinsupp.coeFnAddMonoidHom x) i

Tactic:
[

Goal state after:
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
r : (i : ι) → R i
x : Π₀ (i : ι), R i
i : ι
⊢ (if h : i ∈ x.support then r i * x i else 0) = (r • DFinsupp.coeFnAddMonoidHom x) i
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑((a ⊔ b) ⊓ (a ⊔ c))).2 = (↑(a ⊔ b ⊓ c)).2

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b✝ a b c : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑((a ⊔ b) ⊓ (a ⊔ c))).2 = (↑(a ⊔ b ⊓ c)).2
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ KrullDimLE 0 R ↔ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
⊢ KrullDimLE 0 R ↔ ∀ (I : Ideal R), I.IsPrime → I.IsMaximal
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom;
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
I : Ideal ((i : ι) → R i)
max : I.IsMaximal
le : J ≤ I
x✝ : { asIdeal := I, isPrime := ⋯ } ∈ Set.range (sigmaToPi R)
i : ι
p : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = { asIdeal := I, isPrime := ⋯ }
this : ⇑(DFinsupp.single i 1) ∉ (sigmaToPi R ⟨i, p⟩).asIdeal
⊢ False

Tactic:
rw [eq] at this

Goal state after:
ι : Type u_3
R : ι → Type u_2
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : Infinite ι
inst✝ : ∀ (i : ι), Nontrivial (R i)
J : Ideal ((i : ι) → R i) :=
  let __spread.0 := AddMonoidHom.mrange DFinsupp.coeFnAddMonoidHom;
  { toAddSubmonoid := __spread.0, smul_mem' := ⋯ }
I : Ideal ((i : ι) → R i)
max : I.IsMaximal
le : J ≤ I
x✝ : { asIdeal := I, isPrime := ⋯ } ∈ Set.range (sigmaToPi R)
i : ι
p : PrimeSpectrum (R i)
eq : sigmaToPi R ⟨i, p⟩ = { asIdeal := I, isPrime := ⋯ }
this : ⇑(DFinsupp.single i 1) ∉ { asIdeal := I, isPrime := ⋯ }.asIdeal
⊢ False
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I.IsPrime → I ∈ minimalPrimes R ∨ I.IsMaximal
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b a : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑(a ⊓ aᶜ)).2 = 1

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b a : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ (↑(a ⊓ aᶜ)).2 = 1
Module: Mathlib.RingTheory.KrullDimension.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : ⊥.IsPrime
this : OrderBot (PrimeSpectrum R) := { bot := { asIdeal := ⊥, isPrime := inst✝ }, bot_le := ⋯ }
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal

Tactic:
[

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : ⊥.IsPrime
this : OrderBot (PrimeSpectrum R) := { bot := { asIdeal := ⊥, isPrime := inst✝ }, bot_le := ⋯ }
⊢ KrullDimLE 1 R ↔ ∀ (I : Ideal R), I ≠ ⊥ → I.IsPrime → I.IsMaximal
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
a✝ b a : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ 1 = (↑(a ⊔ aᶜ)).1

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
a✝ b a : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
⊢ 1 = (↑(a ⊔ aᶜ)).1
Module: Mathlib.RingTheory.Spectrum.Prime.RingHom

Goal state before:
pp: ι : Type u_3
R : ι → Type u_4
inst✝² : (i : ι) → CommRing (R i)
inst✝¹ : _root_.Finite ι
S : Type u_5
inst✝ : CommRing S
f : S →+* (i : ι) → R i
⊢ ⋃ i, Set.range (comap ((Pi.evalRingHom R i).comp f)) = Set.range (comap f)

Tactic:
[

Goal state after:
ι : Type u_3
R : ι → Type u_4
inst✝² : (i : ι) → CommRing (R i)
inst✝¹ : _root_.Finite ι
S : Type u_5
inst✝ : CommRing S
f : S →+* (i : ι) → R i
⊢ ⋃ i, Set.range (comap ((Pi.evalRingHom R i).comp f)) = Set.range (comap f)
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
⊢ ↑a * ↑b * ↑a = ↑a * ↑b

Tactic:
[

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
⊢ ↑a * ↑b * ↑a = ↑a * ↑b
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
⊢ ↑a * ↑b * ↑b = ↑a * ↑b

Tactic:
[

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b : { a // IsIdempotentElem a }
⊢ ↑a * ↑b * ↑b = ↑a * ↑b
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b c : { a // IsIdempotentElem a }
hab : ↑a * ↑b = ↑a
hac : ↑a * ↑c = ↑a
⊢ ↑a * (↑b * ↑c) = ↑a

Tactic:
[

Goal state after:
R : Type u_1
S : Type u_2
inst✝ : CommSemigroup S
a b c : { a // IsIdempotentElem a }
hab : ↑a * ↑b = ↑a
hac : ↑a * ↑c = ↑a
⊢ ↑a * (↑b * ↑c) = ↑a
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ ↑a * (↑a + ↑b - ↑a * ↑b) = ↑a

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ ↑a * (↑a + ↑b - ↑a * ↑b) = ↑a
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ ↑b * (↑a + ↑b - ↑a * ↑b) = ↑b

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ ↑b * (↑a + ↑b - ↑a * ↑b) = ↑b
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b c : { a // IsIdempotentElem a }
hac : a ≤ c
hbc : b ≤ c
⊢ (↑a + ↑b - ↑a * ↑b) * ↑c = ↑a + ↑b - ↑a * ↑b

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b c : { a // IsIdempotentElem a }
hac : a ≤ c
hbc : b ≤ c
⊢ (↑a + ↑b - ↑a * ↑b) * ↑c = ↑a + ↑b - ↑a * ↑b
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b c : { x // IsIdempotentElem x }
⊢ ↑(a ⊓ (b ⊔ c)) = ↑(a ⊓ b ⊔ a ⊓ c)

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b c : { x // IsIdempotentElem x }
⊢ ↑(a ⊓ (b ⊔ c)) = ↑(a ⊓ b ⊔ a ⊓ c)
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this✝ : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : ↑t * (x ^ n * ↑b) = ↑t * ↑a
this : (x * (↑t * ↑b)) ^ (n + 1) = ↑t ^ n * ↑b ^ n * x * ↑t * ↑a
⊢ (x * (↑t * ↑b)) ^ (n + 1) ∈ I

Tactic:
this

Goal state after:
case mp
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
x : R
p : Ideal R
hxp : x ∈ p
hp₃ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hp₁ : p.IsPrime
hp₂ : I ≤ p
this✝ : map (algebraMap R (Localization.AtPrime p)) p ≤ (map (algebraMap R (Localization.AtPrime p)) I).radical
n : ℕ
a : ↥I
b t : ↥p.primeCompl
ht : ↑t * (x ^ n * ↑b) = ↑t * ↑a
this : (x * (↑t * ↑b)) ^ (n + 1) = ↑t ^ n * ↑b ^ n * x * ↑t * ↑a
⊢ ↑t ^ n * ↑b ^ n * x * ↑t * ↑a ∈ I
Module: Mathlib.RingTheory.Localization.AsSubring

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ ofField K S hS = subalgebra K S hS

Tactic:
[

Goal state after:
A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S : Submonoid A
hS : S ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ ofField K S hS = subalgebra K S hS
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ ↑(a ⊔ ⟨1 - ↑a, ⋯⟩) = ↑⊤

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ ↑(a ⊔ ⟨1 - ↑a, ⋯⟩) = ↑⊤
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ 1 - ↑a * (1 - ↑b) = ↑(b ⊔ ⟨1 - ↑a, ⋯⟩)

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : { a // IsIdempotentElem a }
⊢ 1 - ↑a * (1 - ↑b) = ↑(b ⊔ ⟨1 - ↑a, ⋯⟩)
Module: Mathlib.RingTheory.Localization.AsSubring

Goal state before:
pp: A : Type u_1
K : Type u_2
inst✝³ : CommRing A
S✝ : Submonoid A
hS : S✝ ≤ A⁰
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
S : Subalgebra A K
⊢ IsFractionRing (↥S) K

Tactic:
by
  refine IsFractionRing.of_field S K fun z ↦ ?_
  rcases IsFractionRing.div_surjective A z with ⟨x, y, _, eq⟩
  exact ⟨algebraMap A S x, algebraMap A S y, eq.symm⟩

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ ↑a * (1 - ↑a) = 0

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : { a // IsIdempotentElem a }
⊢ ↑a * (1 - ↑a) = 0
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
⊢ Disjoint ↑p ↑(nonZeroDivisors R)

Tactic:
[

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
p : Ideal R
hp : p ∈ minimalPrimes R
⊢ Disjoint ↑p ↑(nonZeroDivisors R)
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mp
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
⊢ p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes → p ∈ Ideal.under R ⁻¹' J.minimalPrimes

Tactic:
intro hp

Goal state after:
case mp
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
⊢ p ∈ Ideal.under R ⁻¹' J.minimalPrimes
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Localization

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
⊢ p ∈ Ideal.under R ⁻¹' J.minimalPrimes → p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes

Tactic:
intro hp

Goal state after:
case mpr
R : Type u_1
inst✝³ : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : IsLocalization S A
J : Ideal R
p : Ideal A
hp : p ∈ Ideal.under R ⁻¹' J.minimalPrimes
⊢ p ∈ (Ideal.map (algebraMap R A) J).minimalPrimes
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.under R (Ideal.map (algebraMap R A) q) ≤ Ideal.under R J

Tactic:
AtPrime.map_eq_maximalIdeal q 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 (IsLocalRing.maximalIdeal A) ≤ Ideal.under R J
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ : α
hab : le a✝ b✝
hba : le b✝ a✝
⊢ a✝ = b✝

Tactic:
[

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ : α
hab : le a✝ b✝
hba : le b✝ a✝
⊢ a✝ = b✝
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hac : le a✝ c✝
hbc : le b✝ c✝
⊢ le (sup a✝ b✝) c✝

Tactic:
[

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hac : le a✝ c✝
hbc : le b✝ c✝
⊢ le (sup a✝ b✝) c✝
Module: Mathlib.Order.Copy

Goal state before:
pp: α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hac : le a✝ b✝
hbc : le a✝ c✝
⊢ le a✝ (inf b✝ c✝)

Tactic:
[

Goal state after:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a✝ b✝ c✝ : α
hac : le a✝ b✝
hbc : le a✝ c✝
⊢ le a✝ (inf b✝ c✝)
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Bijective ⇑f
r : R
I : MaximalSpectrum S
⊢ (Localization.localRingHom (Ideal.comap f I.asIdeal) I.asIdeal f ⋯)
      ((algebraMap R (Localization.AtPrime (Ideal.comap f I.asIdeal))) r) =
    (algebraMap S (Localization.AtPrime I.asIdeal)) (f r)

Tactic:
[

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Bijective ⇑f
r : R
I : MaximalSpectrum S
⊢ (Localization.localRingHom (Ideal.comap f I.asIdeal) I.asIdeal f ⋯)
      ((algebraMap R (Localization.AtPrime (Ideal.comap f I.asIdeal))) r) =
    (algebraMap S (Localization.AtPrime I.asIdeal)) (f r)
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ mapPiLocalization ((↑f).comp ↑f.symm) ⋯ = RingHom.id (PiLocalization S)

Tactic:
[

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ mapPiLocalization ((↑f).comp ↑f.symm) ⋯ = RingHom.id (PiLocalization S)
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ mapPiLocalization ((↑f.symm).comp ↑f) ⋯ = RingHom.id (PiLocalization R)

Tactic:
[

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f✝ : R →+* S
hf : Function.Bijective ⇑f✝
f : R ≃+* S := RingEquiv.ofBijective f✝ hf
⊢ mapPiLocalization ((↑f.symm).comp ↑f) ⋯ = RingHom.id (PiLocalization R)