-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
@[simp]
lemma ideal_inf {I J : IdealSheafData X} : (I ⊓ J).ideal = I.ideal ⊓ J.ideal

Proof state:
case h.intro.intro
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
⊢ IsLocalization.mk' (↑Γ(X, X.basicOpen f)) x s ∈
      Ideal.map (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) (I.ideal U ⊓ J.ideal U) ↔
    IsLocalization.mk' (↑Γ(X, X.basicOpen f)) x s ∈
      Ideal.map (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) (I.ideal U) ⊓
        Ideal.map (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) (J.ideal U)

Tactic:
simp only [IsLocalization.mk'_mem_map_algebraMap_iff, Submonoid.mem_powers_iff, Ideal.mem_inf,
  exists_exists_eq_and]

Result:
case h.intro.intro
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
⊢ (∃ a, f ^ a * x ∈ I.ideal U ∧ f ^ a * x ∈ J.ideal U) ↔ (∃ a, f ^ a * x ∈ I.ideal U) ∧ ∃ a, f ^ a * x ∈ J.ideal U

Proof state:
case h.intro.intro.intro.intro.intro.refine_2
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ (n₁ + n₂) * x ∈ J.ideal U

Tactic:
rw [pow_add, mul_assoc]

Result:
case h.intro.intro.intro.intro.intro.refine_2
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ n₁ * (f ^ n₂ * x) ∈ J.ideal U

Proof state:
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U ⊓ J.ideal U) =
    I.ideal (X.affineBasicOpen f) ⊓ J.ideal (X.affineBasicOpen f)

Tactic:
have : (X.presheaf.map (homOfLE (X.basicOpen_le f)).op).hom = algebraMap _ _ := rfl

Result:
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U ⊓ J.ideal U) =
    I.ideal (X.affineBasicOpen f) ⊓ J.ideal (X.affineBasicOpen f)

Proof state:
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ Ideal.map (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) (I.ideal U ⊓ J.ideal U) =
    Ideal.map (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) (I.ideal U) ⊓
      Ideal.map (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) (J.ideal U)

Tactic:
ext x

Result:
case h
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, X.basicOpen f)
⊢ x ∈ Ideal.map (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) (I.ideal U ⊓ J.ideal U) ↔
    x ∈
      Ideal.map (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) (I.ideal U) ⊓
        Ideal.map (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) (J.ideal U)

Proof state:
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U ⊓ J.ideal U) =
    I.ideal (X.affineBasicOpen f) ⊓ J.ideal (X.affineBasicOpen f)

Tactic:
rw [← I.map_ideal_basicOpen U f, ← J.map_ideal_basicOpen U f, this]

Result:
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
⊢ Ideal.map (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) (I.ideal U ⊓ J.ideal U) =
    Ideal.map (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) (I.ideal U) ⊓
      Ideal.map (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) (J.ideal U)

Proof state:
case h.intro.intro
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
⊢ (∃ a, f ^ a * x ∈ I.ideal U ∧ f ^ a * x ∈ J.ideal U) ↔ (∃ a, f ^ a * x ∈ I.ideal U) ∧ ∃ a, f ^ a * x ∈ J.ideal U

Tactic:
refine ⟨fun ⟨n, h₁, h₂⟩ ↦ ⟨⟨n, h₁⟩, ⟨n, h₂⟩⟩, ?_⟩

Result:
case h.intro.intro
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
⊢ ((∃ a, f ^ a * x ∈ I.ideal U) ∧ ∃ a, f ^ a * x ∈ J.ideal U) → ∃ a, f ^ a * x ∈ I.ideal U ∧ f ^ a * x ∈ J.ideal U

Proof state:
case h.intro.intro.intro.intro.intro.refine_2
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ n₁ * (f ^ n₂ * x) ∈ J.ideal U

Tactic:
exact Ideal.mul_mem_left _ _ h₂

Result:
no goals