awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
inst_5 : Algebra.HasGoingDown R S
p : Ideal R
inst_6 : p.IsPrime
P : Ideal S
inst_7 : P.IsPrime
inst_8 : P.LiesOver p
obtain :
  ∀ (lp : LTSeries (PrimeSpectrum R))
    (hlp :
      RelSeries.last (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          lp =
        { asIdeal := p, isPrime := ⋯ })
    (hlenp :
      (↑(lp.length (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})) :
          ℕ∞) =
        p.height),
    p.height +
        height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
            (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P) ≤
      P.height
⊢ p.height +
      height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P) ≤
    P.height

Tactic:
obtain ⟨lp, hlp, hlenp⟩ := p.exists_ltSeries_length_eq_height

Premises used: Ideal.exists_ltSeries_length_eq_height
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
inst_5 : Algebra.HasGoingDown R S
p : Ideal R
inst_6 : p.IsPrime
P : Ideal S
inst_7 : P.IsPrime
inst_8 : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp :
  RelSeries.last (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      lp =
    { asIdeal := p, isPrime := ⋯ }
hlenp :
  (↑(lp.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    p.height
lq : LTSeries (PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
hlq :
  RelSeries.last (r :=
      {x :
        PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
          PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) |
        match (motive :=
          PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
              PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) →
            Prop)
          x with
        | (a, b) => a < b})
      lq =
    {
      asIdeal :=
        map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P,
      isPrime := ⋯ }
hlenq :
  (↑(lq.length (r :=
          {x :
            PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
              PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) |
            match (motive :=
              PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
                  PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) →
                Prop)
              x with
            | (a, b) => a < b})) :
      ℕ∞) =
    height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (F := R →+* S) (algebraMap R S) p))) ⋯
⊢ LiesOver (B := S)
    (PrimeSpectrum.asIdeal
      (PrimeSpectrum.comap (Quotient.mk (map (F := R →+* S) (algebraMap R S) p))
        (RelSeries.head (r :=
          {x :
            PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
              PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) |
            x.1 < x.2})
          lq)))
    p

Tactic:
⟨?_⟩

Premises used: Ideal.LiesOver.mk
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
inst_5 : Algebra.HasGoingDown R S
p : Ideal R
inst_6 : p.IsPrime
P : Ideal S
inst_7 : P.IsPrime
inst_8 : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp :
  RelSeries.last (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      lp =
    { asIdeal := p, isPrime := ⋯ }
hlenp :
  (↑(lp.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    p.height
lq : LTSeries (PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
hlq :
  RelSeries.last (r :=
      {x :
        PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
          PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) |
        match (motive :=
          PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
              PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) →
            Prop)
          x with
        | (a, b) => a < b})
      lq =
    {
      asIdeal :=
        map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P,
      isPrime := ⋯ }
hlenq :
  (↑(lq.length (r :=
          {x :
            PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
              PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) |
            match (motive :=
              PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
                  PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) →
                Prop)
              x with
            | (a, b) => a < b})) :
      ℕ∞) =
    height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (F := R →+* S) (algebraMap R S) p))) ⋯
⊢ p =
    under R (B := S)
      (PrimeSpectrum.asIdeal
        (PrimeSpectrum.comap (Quotient.mk (map (F := R →+* S) (algebraMap R S) p))
          (RelSeries.head (r :=
            {x :
              PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
                PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) |
              x.1 < x.2})
            lq)))

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
inst_5 : Algebra.HasGoingDown R S
p : Ideal R
inst_6 : p.IsPrime
P : Ideal S
inst_7 : P.IsPrime
inst_8 : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp :
  RelSeries.last (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      lp =
    { asIdeal := p, isPrime := ⋯ }
hlenp :
  (↑(lp.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    p.height
lq : LTSeries (PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
hlq :
  RelSeries.last (r :=
      {x :
        PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
          PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) |
        match (motive :=
          PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
              PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) →
            Prop)
          x with
        | (a, b) => a < b})
      lq =
    {
      asIdeal :=
        map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P,
      isPrime := ⋯ }
hlenq :
  (↑(lq.length (r :=
          {x :
            PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
              PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) |
            match (motive :=
              PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
                  PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) →
                Prop)
              x with
            | (a, b) => a < b})) :
      ℕ∞) =
    height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (F := R →+* S) (algebraMap R S) p))) ⋯
⊢ map (R := S) (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) (map (F := R →+* S) (algebraMap R S) p) ≤
    (RelSeries.head (r :=
        {x :
          PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
            PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) |
          x.1 < x.2})
        lq).asIdeal

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
inst_5 : Algebra.HasGoingDown R S
p : Ideal R
inst_6 : p.IsPrime
P : Ideal S
inst_7 : P.IsPrime
inst_8 : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp :
  RelSeries.last (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      lp =
    { asIdeal := p, isPrime := ⋯ }
hlenp :
  (↑(lp.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    p.height
lq : LTSeries (PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)))
hlq :
  RelSeries.last (r :=
      {x :
        PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
          PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) |
        match (motive :=
          PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
              PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) →
            Prop)
          x with
        | (a, b) => a < b})
      lq =
    {
      asIdeal :=
        map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P,
      isPrime := ⋯ }
hlenq :
  (↑(lq.length (r :=
          {x :
            PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
              PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) |
            match (motive :=
              PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
                  PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) →
                Prop)
              x with
            | (a, b) => a < b})) :
      ℕ∞) =
    height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
      (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (F := R →+* S) (algebraMap R S) p))) ⋯
rw : comap (F := R →+* S) (algebraMap R S) P
| p

Tactic:
rw [LiesOver.over (p := p) (P := P), under_def]

Premises used: Ideal.under_def, Ideal.LiesOver.over
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
⊢ ringKrullDim R ≤ (↑(Submodule.spanFinrank (IsLocalRing.maximalIdeal R)) : WithBot ℕ∞)

Tactic:
le_of_eq_of_le IsLocalRing.maximalIdeal_height_eq_ringKrullDim.symm
    (WithBot.coe_le_coe.mpr (Ideal.height_le_spanFinrank (IsLocalRing.maximalIdeal R)
      Ideal.IsPrime.ne_top'))

Premises used: Iff.mpr, Ideal.height_le_spanFinrank, IsLocalRing.maximalIdeal, WithBot.coe_le_coe, le_of_eq_of_le, IsLocalRing.maximalIdeal_height_eq_ringKrullDim, Ideal.IsPrime.ne_top', Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
α : Type u
β : Type v
F : Type w
inst : Semiring α
I : Ideal α
a b a_1 x : α
h : Membership.mem (γ := Ideal α) ⊥ a_1
rw : Membership.mem (γ := Ideal α) ⊥ 0
⊢ Membership.mem (γ := Ideal α) ⊥ (a_1 * x)

Tactic:
rw [h, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
α : Type u
β : Type v
F : Type w
inst : Semiring α
I : Ideal α
a b a_1 x : α
h : Membership.mem (γ := Ideal α) ⊥ a_1
⊢ Membership.mem (γ := Ideal α) ⊥ 0

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
α : Type u
β : Type v
F : Type w
inst : Semiring α
I : Ideal α
a b a_1 x : α
h : Membership.mem (γ := Ideal α) ⊥ a_1
⊢ Membership.mem (γ := Ideal α) ⊥ 0

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
α : Type u
β : Type v
F : Type w
inst : Semiring α
I : Ideal α
a b : α
⊢ IsTwoSided.{u} (α := α) ⊤

Tactic:
⟨fun _ _ ↦ trivial⟩

Premises used: trivial, Ideal.IsTwoSided.mk
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
α : Type u
β : Type v
F : Type w
inst : Semiring α
I_1 : Ideal α
a b : α
ι : Sort u_1
I : ι → Ideal α
inst_1 : ∀ (i : ι), (I i).IsTwoSided
⊢ IsTwoSided.{u} (α := α) (⨅ (i : ι), I i)

Tactic:
⟨fun _ h ↦ (Submodule.mem_iInf _).mpr (mul_mem_right _ _ <| (Submodule.mem_iInf _).mp h ·)⟩

Premises used: Iff.mpr, Submodule.mem_iInf, Ideal.mul_mem_right, Iff.mp, Ideal.IsTwoSided.mk
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
α : Type u
inst : Semiring α
I : Ideal α
x y : α
hx : x ∈ I
h : y * x = 1
z : α
h_1 : Membership.mem (γ := Submodule α α) ⊤ z
rw : z * 1 = z
rw₁ rw₂ : z = z
⊢ z * (y * x) = z

Tactic:
rw [h, mul_one]

Premises used: mul_one
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
α : Type u
inst : Semiring α
I : Ideal α
x : α
hx : x ∈ I
h : IsUnit x
⊢ I = ⊤

Tactic:
let ⟨y, hy⟩ := h.exists_left_inv
  eq_top_of_unit_mem I x y hx hy

Premises used: Ideal.eq_top_of_unit_mem, IsUnit.exists_left_inv, _private.0.Ideal.eq_top_of_isUnit_mem.match_1, Top.top, Eq
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
α : Type u
inst : Semiring α
⊢ Membership.mem (γ := Ideal α) ⊤ 1

Tactic:
trivial
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
α : Type u
inst : Semiring α
I : Ideal α
h : 1 ∈ I
⊢ HMul.hMul (α := α) 1 1 = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
α : Type u
inst : Semiring α
I : Ideal α
⊢ I ≠ ⊤ ↔ 1 ∉ I

Tactic:
not_congr I.eq_top_iff_one

Premises used: Ideal.eq_top_iff_one, not_congr
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
R : Type u
inst : Semiring R
S T : Ideal R
⊢ ∀ {x : R}, x ∈ S → x ∈ S ⊔ T

Tactic:
@le_sup_left _ _ S T

Premises used: le_sup_left, Set.Mem
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
R : Type u
inst : Semiring R
S T : Ideal R
⊢ ∀ {x : R}, x ∈ T → x ∈ S ⊔ T

Tactic:
@le_sup_right _ _ S T

Premises used: Set.Mem, le_sup_right
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
R : Type u
inst : Semiring R
ι : Sort u_1
S : ι → Ideal R
i : ι
⊢ ∀ {x : R}, x ∈ S i → x ∈ iSup S

Tactic:
@le_iSup _ _ _ S _

Premises used: Set.Mem, le_iSup
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
R : Type u
inst : Semiring R
S : Set (Ideal R)
s : Ideal R
hs : s ∈ S
⊢ ∀ {x : R}, x ∈ s → x ∈ sSup S

Tactic:
@le_sSup _ _ _ _ hs

Premises used: Set.Mem, le_sSup
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
R : Type u
inst : Semiring R
s : Set (Ideal R)
x : R
⊢ x ∈ sInf s ↔ ∀ ⦃I : Ideal R⦄, I ∈ s → x ∈ I

Tactic:
⟨fun hx I his => hx I ⟨I, iInf_pos his⟩, fun H _I ⟨_J, hij⟩ => hij ▸ fun _S ⟨hj, hS⟩ => hS ▸ H hj⟩

Premises used: Membership.mem, Eq.rec, _private.0.Ideal.mem_sInf.match_1, SetLike.coe, Iff.intro, Exists.intro, iInf_pos, _private.0.Ideal.mem_sInf.match_2
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
R : Type u
inst : Semiring R
I J : Ideal R
x : R
⊢ x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
R : Type u
inst : Semiring R
ι : Sort u_1
I : ι → Ideal R
x : R
⊢ x ∈ iInf I ↔ ∀ (i : ι), x ∈ I i

Tactic:
Submodule.mem_iInf _

Premises used: Submodule.mem_iInf, Set.Mem
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
R : Type u
inst : Semiring R
x : R
⊢ Membership.mem (γ := Ideal R) ⊥ x ↔ x = 0

Tactic:
Submodule.mem_bot _

Premises used: Set.Mem, Submodule.mem_bot
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
K : Type u
inst : DivisionSemiring K
I : Ideal K
rw : ¬I = ⊤ → I = ⊥
⊢ I = ⊥ ∨ I = ⊤

Tactic:
rw [or_iff_not_imp_right]

Premises used: Classical.or_iff_not_imp_right
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
K : Type u
inst : DivisionSemiring K
I : Ideal K
rw : 1 ∉ I → I = ⊥
⊢ I ≠ ⊤ → I = ⊥

Tactic:
rw [Ideal.ne_top_iff_one]

Premises used: Ideal.ne_top_iff_one
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
K : Type u
inst : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
rw : I ≤ ⊥
⊢ I = ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
K : Type u
inst : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
pos : ∀ (H : r = 0), Membership.mem (γ := Submodule K K) ⊥ r
neg : ∀ (H : ¬r = 0), Membership.mem (γ := Submodule K K) ⊥ r
⊢ Membership.mem (γ := Submodule K K) ⊥ r

Tactic:
by_cases H : r = 0
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
K : Type u
inst : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
H : r = 0
⊢ Membership.mem (γ := Submodule K K) ⊥ r

Tactic:
simpa
-- Module: Mathlib.RingTheory.Ideal.Lattice
Goal:
K : Type u
inst : DivisionSemiring K
I : Ideal K
h1 : 1 ∉ I
r : K
hr : r ∈ I
H : ¬r = 0
⊢ Membership.mem (γ := Submodule K K) ⊥ r

Tactic:
simpa [H, h1] using I.mul_mem_left r⁻¹ hr

Premises used: Inv.inv, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I_1 J : Ideal R
K L : Ideal S
inst_3 : RingHomClass F R S
I : Ideal S
x y : R
hx : Membership.mem (γ := Set R) ((⇑f : (a : R) → S) ⁻¹' (↑I : Set S)) x
hy : Membership.mem (γ := Set R) ((⇑f : (a : R) → S) ⁻¹' (↑I : Set S)) y
simp :
  ∀ (hx : Membership.mem (α := S) I ((f : (a : R) → S) x : S))
    (hy : Membership.mem (α := S) I ((f : (a : R) → S) y : S)),
    HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S) ∈ I
⊢ Membership.mem (γ := Set R) ((⇑f : (a : R) → S) ⁻¹' (↑I : Set S)) (x + y)

Tactic:
simp only [Set.mem_preimage, SetLike.mem_coe, map_add f] at hx hy ⊢

Premises used: map_add, SetLike.mem_coe, Set.mem_preimage
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I_1 J : Ideal R
K L : Ideal S
inst_3 : RingHomClass F R S
I : Ideal S
x y : R
hx : Membership.mem (α := S) I ((f : (a : R) → S) x : S)
hy : Membership.mem (α := S) I ((f : (a : R) → S) y : S)
⊢ HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S) ∈ I

Tactic:
add_mem hx hy

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I_1 J : Ideal R
K L : Ideal S
inst_3 : RingHomClass F R S
I : Ideal S
x y : R
hx : Membership.mem (α := S) I ((f : (a : R) → S) x : S)
hy : Membership.mem (α := S) I ((f : (a : R) → S) y : S)
⊢ HAdd.hAdd (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S) ∈ I

Tactic:
exact add_mem hx hy

Premises used: AddMemClass.add_mem
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I_1 J : Ideal R
K L : Ideal S
inst_3 : RingHomClass F R S
I : Ideal S
⊢ Membership.mem (γ := Set R) ((⇑f : (a : R) → S) ⁻¹' (↑I : Set S)) 0

Tactic:
simp only [Set.mem_preimage, map_zero, SetLike.mem_coe, Submodule.zero_mem]

Premises used: map_zero, Submodule.zero_mem, SetLike.mem_coe, Set.mem_preimage
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I_1 J : Ideal R
K L : Ideal S
inst_3 : RingHomClass F R S
I : Ideal S
c x : R
hx : Membership.mem (γ := Set R) ((⇑f : (a : R) → S) ⁻¹' (↑I : Set S)) x
simp :
  ∀ (hx : Membership.mem (α := S) I ((f : (a : R) → S) x : S)),
    HMul.hMul (α := S) (β := S) ((f : (a : R) → S) c : S) ((f : (a : R) → S) x : S) ∈ I
⊢ Membership.mem (γ := Set R) ((⇑f : (a : R) → S) ⁻¹' (↑I : Set S)) (c • x)

Tactic:
simp only [smul_eq_mul, Set.mem_preimage, map_mul, SetLike.mem_coe] at *

Premises used: map_mul, SetLike.mem_coe, smul_eq_mul, Set.mem_preimage
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I_1 J : Ideal R
K L : Ideal S
inst_3 : RingHomClass F R S
I : Ideal S
c x : R
hx : Membership.mem (α := S) I ((f : (a : R) → S) x : S)
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) c : S) ((f : (a : R) → S) x : S) ∈ I

Tactic:
mul_mem_left I _ hx

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I_1 J : Ideal R
K L : Ideal S
inst_3 : RingHomClass F R S
I : Ideal S
c x : R
hx : Membership.mem (α := S) I ((f : (a : R) → S) x : S)
⊢ HMul.hMul (α := S) (β := S) ((f : (a : R) → S) c : S) ((f : (a : R) → S) x : S) ∈ I

Tactic:
exact mul_mem_left I _ hx

Premises used: Ideal.mul_mem_left