awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
α : Type u_2
inst : CommSemiring α
s : Set α
n : ℕ
f : (↑s : Type u_2) →₀ α
hf : Eq (α := α) (∑ x ∈ f.support, HMul.hMul (α := α) ((f : (a : (↑s : Type u_2)) → α) x : α) (↑x : α)) 1
this_1 :
  Membership.mem (γ := Ideal α)
    (span
      ((fun (i : (↑s : Type u_2)) ↦ HMul.hMul (α := α) ((f : (a : (↑s : Type u_2)) → α) i : α) (↑i : α) ^ (n + 1)) ''
        (↑f.support : Set (↑s : Type u_2))))
    1
x : (↑s : Type u_2)
left : x ∈ (↑f.support : Set (↑s : Type u_2))
this : LE.le (α := Ideal α) (span {(↑x : α) ^ (n + 1)}) (span ((fun (x : α) ↦ x ^ (n + 1)) '' s))
succ :
  Membership.mem (γ := Submodule α α) (span {(↑x : α) ^ (n + 1)})
    (HMul.hMul (α := α) ((f : (a : (↑s : Type u_2)) → α) x : α) (↑x : α) ^ (n + 1))
⊢ HMul.hMul (α := α) ((f : (a : (↑s : Type u_2)) → α) x : α) (↑x : α) ^ (n + 1) ∈
    (↑(span ((fun (x : α) ↦ x ^ (n + 1)) '' s)) : Set α)

Tactic:
refine this ?_
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
α : Type u_2
inst : CommSemiring α
s : Set α
n : ℕ
f : (↑s : Type u_2) →₀ α
hf : Eq (α := α) (∑ x ∈ f.support, HMul.hMul (α := α) ((f : (a : (↑s : Type u_2)) → α) x : α) (↑x : α)) 1
this_1 :
  Membership.mem (γ := Ideal α)
    (span
      ((fun (i : (↑s : Type u_2)) ↦ HMul.hMul (α := α) ((f : (a : (↑s : Type u_2)) → α) i : α) (↑i : α) ^ (n + 1)) ''
        (↑f.support : Set (↑s : Type u_2))))
    1
x : (↑s : Type u_2)
left : x ∈ (↑f.support : Set (↑s : Type u_2))
this : LE.le (α := Ideal α) (span {(↑x : α) ^ (n + 1)}) (span ((fun (x : α) ↦ x ^ (n + 1)) '' s))
succ : (↑x : α) ^ (n + 1) ∣ HPow.hPow (α := α) ((f : (a : (↑s : Type u_2)) → α) x : α) (n + 1) * (↑x : α) ^ (n + 1)
⊢ Membership.mem (γ := Submodule α α) (span {(↑x : α) ^ (n + 1)})
    (HMul.hMul (α := α) ((f : (a : (↑s : Type u_2)) → α) x : α) (↑x : α) ^ (n + 1))

Tactic:
rw [mul_pow, mem_span_singleton]

Premises used: Ideal.mem_span_singleton, mul_pow
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
α : Type u_2
inst : CommSemiring α
s : Set α
n : ℕ
f : (↑s : Type u_2) →₀ α
hf : Eq (α := α) (∑ x ∈ f.support, HMul.hMul (α := α) ((f : (a : (↑s : Type u_2)) → α) x : α) (↑x : α)) 1
this_1 :
  Membership.mem (γ := Ideal α)
    (span
      ((fun (i : (↑s : Type u_2)) ↦ HMul.hMul (α := α) ((f : (a : (↑s : Type u_2)) → α) i : α) (↑i : α) ^ (n + 1)) ''
        (↑f.support : Set (↑s : Type u_2))))
    1
x : (↑s : Type u_2)
left : x ∈ (↑f.support : Set (↑s : Type u_2))
this : LE.le (α := Ideal α) (span {(↑x : α) ^ (n + 1)}) (span ((fun (x : α) ↦ x ^ (n + 1)) '' s))
⊢ (↑x : α) ^ (n + 1) ∣ HPow.hPow (α := α) ((f : (a : (↑s : Type u_2)) → α) x : α) (n + 1) * (↑x : α) ^ (n + 1)

Tactic:
⟨f x ^ (n + 1), mul_comm _ _⟩

Premises used: HPow.hPow, HAdd.hAdd, Exists.intro, mul_comm, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
α : Type u_2
inst : CommSemiring α
s : Set α
n : ℕ
f : (↑s : Type u_2) →₀ α
hf : Eq (α := α) (∑ x ∈ f.support, HMul.hMul (α := α) ((f : (a : (↑s : Type u_2)) → α) x : α) (↑x : α)) 1
this_1 :
  Membership.mem (γ := Ideal α)
    (span
      ((fun (i : (↑s : Type u_2)) ↦ HMul.hMul (α := α) ((f : (a : (↑s : Type u_2)) → α) i : α) (↑i : α) ^ (n + 1)) ''
        (↑f.support : Set (↑s : Type u_2))))
    1
x : (↑s : Type u_2)
left : x ∈ (↑f.support : Set (↑s : Type u_2))
this : LE.le (α := Ideal α) (span {(↑x : α) ^ (n + 1)}) (span ((fun (x : α) ↦ x ^ (n + 1)) '' s))
⊢ (↑x : α) ^ (n + 1) ∣ HPow.hPow (α := α) ((f : (a : (↑s : Type u_2)) → α) x : α) (n + 1) * (↑x : α) ^ (n + 1)

Tactic:
exact ⟨f x ^ (n + 1), mul_comm _ _⟩
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
α : Type u_2
inst : CommSemiring α
s : Set α
hs : Eq (α := Ideal α) (span s) ⊤
n : (↑s : Type u_2) → ℕ
have :
  ∀ (t : Finset α) (hts : (↑t : Set α) ⊆ s)
    (mem : Membership.mem (γ := Submodule α α) (Submodule.span α (↑t : Set α)) 1),
    Eq.{u_2 + 1} (α := Ideal α) (span (range fun (x : (↑s : Type u_2)) ↦ (↑x : α) ^ n x)) ⊤
⊢ Eq.{u_2 + 1} (α := Ideal α) (span (range fun (x : (↑s : Type u_2)) ↦ (↑x : α) ^ n x)) ⊤

Tactic:
have ⟨t, hts, mem⟩ := Submodule.mem_span_finite_of_mem_span ((eq_top_iff_one _).mp hs)
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
α : Type u_2
inst : CommSemiring α
s : Set α
hs : Eq (α := Ideal α) (span s) ⊤
n : (↑s : Type u_2) → ℕ
t : Finset α
hts : (↑t : Set α) ⊆ s
mem : Membership.mem (γ := Submodule α α) (Submodule.span α (↑t : Set α)) 1
⊢ Eq.{u_2 + 1} (α := Ideal α) (span (range fun (x : (↑s : Type u_2)) ↦ (↑x : α) ^ n x)) ⊤

Tactic:
top_unique ((span_pow_eq_top _ ((eq_top_iff_one _).mpr mem) <|
    t.attach.sup fun x ↦ n ⟨x, hts x.2⟩).ge.trans <| span_le.mpr ?_)

Premises used: Ideal.span_le, Iff.mpr, Eq.ge, Ideal.span_pow_eq_top, Subtype.mk, Ideal.eq_top_iff_one, top_unique, Finset.attach, Finset.sup, LE.le.trans, Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
α : Type u_2
inst : CommSemiring α
s : Set α
hs : Eq (α := Ideal α) (span s) ⊤
n : (↑s : Type u_2) → ℕ
t : Finset α
hts : (↑t : Set α) ⊆ s
mem : Membership.mem (γ := Submodule α α) (Submodule.span α (↑t : Set α)) 1
refine :
  (fun (x : α) ↦
        HPow.hPow (β := ℕ) x (t.attach.sup fun (x : ↥t) ↦ n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯))) ''
      (↑t : Set α) ⊆
    (↑(span (range fun (x : (↑s : Type u_2)) ↦ (↑x : α) ^ n x)) : Set α)
⊢ Eq.{u_2 + 1} (α := Ideal α) (span (range fun (x : (↑s : Type u_2)) ↦ (↑x : α) ^ n x)) ⊤

Tactic:
refine top_unique ((span_pow_eq_top _ ((eq_top_iff_one _).mpr mem) <|
    t.attach.sup fun x ↦ n ⟨x, hts x.2⟩).ge.trans <| span_le.mpr ?_)

Premises used: Ideal.span_le, Iff.mpr, Eq.ge, Ideal.span_pow_eq_top, Subtype.mk, Ideal.eq_top_iff_one, top_unique, Finset.attach, Finset.sup, LE.le.trans, Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
α : Type u_2
inst : CommSemiring α
s : Set α
hs : Eq (α := Ideal α) (span s) ⊤
n : (↑s : Type u_2) → ℕ
t : Finset α
hts : (↑t : Set α) ⊆ s
mem : Membership.mem (γ := Submodule α α) (Submodule.span α (↑t : Set α)) 1
x : α
hxt : x ∈ (↑t : Set α)
rw :
  (fun (x_1 : α) ↦
        x_1 ^
          ((t.attach.sup fun (x : ↥t) ↦ n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)) -
              n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hxt) : α) ⋯) +
            n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hxt) : α) ⋯)))
      x ∈
    (↑(span (range fun (x : (↑s : Type u_2)) ↦ (↑x : α) ^ n x)) : Set α)
⊢ (fun (x : α) ↦
        HPow.hPow (β := ℕ) x (t.attach.sup fun (x : ↥t) ↦ n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)))
      x ∈
    (↑(span (range fun (x : (↑s : Type u_2)) ↦ (↑x : α) ^ n x)) : Set α)

Tactic:
rw [← Nat.sub_add_cancel (Finset.le_sup <| t.mem_attach ⟨x, hxt⟩)]

Premises used: Finset.mem_attach, Subtype.mk, Nat.sub_add_cancel, Finset.le_sup
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
α : Type u_2
inst : CommSemiring α
s : Set α
hs : Eq (α := Ideal α) (span s) ⊤
n : (↑s : Type u_2) → ℕ
t : Finset α
hts : (↑t : Set α) ⊆ s
mem : Membership.mem (γ := Submodule α α) (Submodule.span α (↑t : Set α)) 1
x : α
hxt : x ∈ (↑t : Set α)
simp_rw :
  x ^
        ((t.attach.sup fun (x : ↥t) ↦ n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)) -
          n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x ⋯)) *
      x ^ n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x ⋯) ∈
    (↑(span (range fun (x : (↑s : Type u_2)) ↦ (↑x : α) ^ n x)) : Set α)
⊢ (fun (x_1 : α) ↦
        x_1 ^
          ((t.attach.sup fun (x : ↥t) ↦ n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)) -
              n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hxt) : α) ⋯) +
            n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hxt) : α) ⋯)))
      x ∈
    (↑(span (range fun (x : (↑s : Type u_2)) ↦ (↑x : α) ^ n x)) : Set α)

Tactic:
simp_rw [pow_add]

Premises used: pow_add
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
α : Type u_2
inst : CommSemiring α
s : Set α
hs : Eq (α := Ideal α) (span s) ⊤
n : (↑s : Type u_2) → ℕ
t : Finset α
hts : (↑t : Set α) ⊆ s
mem : Membership.mem (γ := Submodule α α) (Submodule.span α (↑t : Set α)) 1
x : α
hxt : x ∈ (↑t : Set α)
⊢ x ^
        ((t.attach.sup fun (x : ↥t) ↦ n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)) -
          n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x ⋯)) *
      x ^ n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x ⋯) ∈
    (↑(span (range fun (x : (↑s : Type u_2)) ↦ (↑x : α) ^ n x)) : Set α)

Tactic:
mul_mem_left _ _ (subset_span ⟨_, rfl⟩)

Premises used: Ideal.subset_span, Set.Mem, Exists.intro, Ideal.mul_mem_left, rfl
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
α : Type u_2
inst : CommSemiring α
s : Set α
hs : Eq (α := Ideal α) (span s) ⊤
n : (↑s : Type u_2) → ℕ
t : Finset α
hts : (↑t : Set α) ⊆ s
mem : Membership.mem (γ := Submodule α α) (Submodule.span α (↑t : Set α)) 1
x : α
hxt : x ∈ (↑t : Set α)
⊢ x ^
        ((t.attach.sup fun (x : ↥t) ↦ n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) ⋯)) -
          n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x ⋯)) *
      x ^ n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x ⋯) ∈
    (↑(span (range fun (x : (↑s : Type u_2)) ↦ (↑x : α) ^ n x)) : Set α)

Tactic:
exact mul_mem_left _ _ (subset_span ⟨_, rfl⟩)
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
α : Type u_2
inst : CommSemiring α
ι : Type u_5
f : ι → α
s : Finset ι
I : Ideal α
i : ι
hi : i ∈ s
hfi : f i ∈ I
rw : (∏ x ∈ s \ {i}, f x) * f i ∈ I
⊢ ∏ i ∈ s, f i ∈ I

Tactic:
rw [Finset.prod_eq_prod_diff_singleton_mul hi]

Premises used: Finset.prod_eq_prod_diff_singleton_mul
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
α : Type u_2
inst : CommSemiring α
ι : Type u_5
f : ι → α
s : Finset ι
I : Ideal α
i : ι
hi : i ∈ s
hfi : f i ∈ I
⊢ (∏ x ∈ s \ {i}, f x) * f i ∈ I

Tactic:
Ideal.mul_mem_left _ _ hfi

Premises used: Set.Mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
α : Type u_2
inst : CommSemiring α
ι : Type u_5
f : ι → α
s : Finset ι
I : Ideal α
i : ι
hi : i ∈ s
hfi : f i ∈ I
⊢ (∏ x ∈ s \ {i}, f x) * f i ∈ I

Tactic:
exact Ideal.mul_mem_left _ _ hfi

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
α : Type u_2
inst : CommSemiring α
ι : Type u_5
f : ι → α
s : Finset ι
I : Ideal α
i : ι
hi : i ∈ s
hfi : f i ∈ I
rw rw₁ rw₂ : (∏ x ∈ s \ {i}, f x) * f i ∈ I
⊢ ∏ i ∈ s, f i ∈ I

Tactic:
classical
  rw [Finset.prod_eq_prod_diff_singleton_mul hi]
  exact Ideal.mul_mem_left _ _ hfi

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
ι : Type u_5
inst : DecidableEq ι
inst_1 : Finite ι
R : ι → Type u_6
inst_2 : (i : ι) → Semiring (R i)
rw : LE.le (α := Ideal ((j : ι) → R j)) ⊤ (span (range fun (i : ι) ↦ Pi.single (M := R) i 1))
⊢ Eq (α := Ideal ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1)) ⊤

Tactic:
rw [_root_.eq_top_iff]

Premises used: eq_top_iff
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
ι : Type u_5
inst : DecidableEq ι
inst_1 : Finite ι
R : ι → Type u_6
inst_2 : (i : ι) → Semiring (R i)
⊢ Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1)) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
ι : Type u_5
inst : DecidableEq ι
inst_1 : Finite ι
R : ι → Type u_6
inst_2 : (i : ι) → Semiring (R i)
f g : (i : ι) → R i
hf :
  Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1)) f
hg :
  Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1)) g
⊢ Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1))
    (f + g)

Tactic:
Ideal.add_mem _ hf hg

Premises used: Set.Mem, Ideal.add_mem
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
ι : Type u_5
inst : DecidableEq ι
inst_1 : Finite ι
R : ι → Type u_6
inst_2 : (i : ι) → Semiring (R i)
f g : (i : ι) → R i
hf :
  Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1)) f
hg :
  Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1)) g
⊢ Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1))
    (f + g)

Tactic:
exact Ideal.add_mem _ hf hg

Premises used: Ideal.add_mem
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
ι : Type u_5
inst : DecidableEq ι
inst_1 : Finite ι
R : ι → Type u_6
inst_2 : (i : ι) → Semiring (R i)
i : ι
r : R i
⊢ Pi.single (M := R) i r = Pi.single (M := R) i r * Pi.single (M := R) i 1

Tactic:
simp [← Pi.single_mul_left]

Premises used: Pi.single_mul_left
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
ι : Type u_5
inst : DecidableEq ι
inst_1 : Finite ι
R : ι → Type u_6
inst_2 : (i : ι) → Semiring (R i)
i : ι
r : R i
single :
  Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1))
    (Pi.single (M := R) i r * Pi.single (M := R) i 1)
⊢ Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1))
    (Pi.single (M := R) i r)

Tactic:
rw [show Pi.single i r = Pi.single i r * Pi.single i 1 by simp [← Pi.single_mul_left]]
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
ι : Type u_5
inst : DecidableEq ι
inst_1 : Finite ι
R : ι → Type u_6
inst_2 : (i : ι) → Semiring (R i)
i : ι
r : R i
⊢ Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1))
    (Pi.single (M := R) i r * Pi.single (M := R) i 1)

Tactic:
Ideal.mul_mem_left _ _ (Ideal.subset_span ⟨i, rfl⟩)

Premises used: Ideal.subset_span, Set.Mem, Exists.intro, Ideal.mul_mem_left, rfl
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
ι : Type u_5
inst : DecidableEq ι
inst_1 : Finite ι
R : ι → Type u_6
inst_2 : (i : ι) → Semiring (R i)
i : ι
r : R i
⊢ Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1))
    (Pi.single (M := R) i r * Pi.single (M := R) i 1)

Tactic:
exact Ideal.mul_mem_left _ _ (Ideal.subset_span ⟨i, rfl⟩)
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
ι : Type u_5
inst : DecidableEq ι
inst_1 : Finite ι
R : ι → Type u_6
inst_2 : (i : ι) → Semiring (R i)
x : (j : ι) → R j
zero :
  Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1)) 0
add :
  ∀ (f g : (i : ι) → R i)
    (hf :
      Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j))
        (span (range fun (i : ι) ↦ Pi.single (M := R) i 1)) f)
    (hg :
      Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j))
        (span (range fun (i : ι) ↦ Pi.single (M := R) i 1)) g),
    Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1))
      (f + g)
single :
  ∀ (i : ι) (r : R i),
    Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1))
      (Pi.single (M := R) i r)
⊢ Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1)) x

Tactic:
induction x using Pi.single_induction with
  | zero => simp
  | add f g hf hg => exact Ideal.add_mem _ hf hg
  | single i r =>
      rw [show Pi.single i r = Pi.single i r * Pi.single i 1 by simp [← Pi.single_mul_left]]
      exact Ideal.mul_mem_left _ _ (Ideal.subset_span ⟨i, rfl⟩)
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst : DivisionSemiring K
I_1 I : Ideal K
inl : Eq.{u_5 + 1} (α := Ideal K) (![⊥, ⊤] ((fun (I : Ideal K) ↦ (if I = ⊥ then 0 else 1 : Fin 2)) ⊥)) ⊥
inr : Eq.{u_5 + 1} (α := Ideal K) (![⊥, ⊤] ((fun (I : Ideal K) ↦ (if I = ⊥ then 0 else 1 : Fin 2)) ⊤)) ⊤
⊢ ![⊥, ⊤] ((fun (I : Ideal K) ↦ (if I = ⊥ then 0 else 1 : Fin 2)) I) = I

Tactic:
rcases eq_bot_or_top I with rfl | rfl

Premises used: Ideal.eq_bot_or_top, rfl
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst : DivisionSemiring K
I : Ideal K
⊢ Eq.{u_5 + 1} (α := Ideal K) (![⊥, ⊤] ((fun (I : Ideal K) ↦ (if I = ⊥ then 0 else 1 : Fin 2)) ⊥)) ⊥

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst : DivisionSemiring K
I : Ideal K
⊢ Eq.{u_5 + 1} (α := Ideal K) (![⊥, ⊤] ((fun (I : Ideal K) ↦ (if I = ⊥ then 0 else 1 : Fin 2)) ⊤)) ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst : DivisionSemiring K
I : Ideal K
i : Fin 2
0 :
  Eq (α := Fin 2) ((fun (I : Ideal K) ↦ (if I = ⊥ then 0 else 1 : Fin 2)) (![⊥, ⊤] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)))
    ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
1 :
  Eq (α := Fin 2) ((fun (I : Ideal K) ↦ (if I = ⊥ then 0 else 1 : Fin 2)) (![⊥, ⊤] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)))
    ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ (fun (I : Ideal K) ↦ (if I = ⊥ then 0 else 1 : Fin 2)) (![⊥, ⊤] i) = i

Tactic:
fin_cases i
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst : DivisionSemiring K
I : Ideal K
⊢ Eq (α := Fin 2) ((fun (I : Ideal K) ↦ (if I = ⊥ then 0 else 1 : Fin 2)) (![⊥, ⊤] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)))
    ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst : DivisionSemiring K
I : Ideal K
⊢ Eq (α := Fin 2) ((fun (I : Ideal K) ↦ (if I = ⊥ then 0 else 1 : Fin 2)) (![⊥, ⊤] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)))
    ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst : DivisionSemiring K
I : Ideal K
⊢ Finite.{u_5 + 1} (Ideal K)

Tactic:
let _i := Classical.decEq (Ideal K); ⟨equivFinTwo K⟩

Premises used: Finite.intro, Ideal, Ideal.equivFinTwo, Classical.decEq
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
F : Type u_4
K : Type u_5
inst : DivisionSemiring K
I : Ideal K
⊢ IsSimpleOrder.{u_5} (Ideal K)

Tactic:
⟨eq_bot_or_top⟩

Premises used: IsSimpleOrder.mk, Ideal.eq_bot_or_top
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
hf : ¬IsField R
⊢ ¬∀ {a : R}, a ≠ 0 → ∃ (b : R), a * b = 1

Tactic:
have : ¬_ := fun h => hf ⟨exists_pair_ne R, mul_comm, h⟩
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
hf : ¬IsField R
this : ¬∀ {a : R}, a ≠ 0 → ∃ (b : R), a * b = 1
simp_rw : ∃ (x : R) (_ : x ≠ 0), ¬∃ (b : R), x * b = 1
⊢ ∃ (x : R) (_ : x ≠ 0), ¬IsUnit x

Tactic:
simp_rw [isUnit_iff_exists_inv]

Premises used: isUnit_iff_exists_inv
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
hf : ¬IsField R
this : ¬∀ {a : R}, a ≠ 0 → ∃ (b : R), a * b = 1
push : ∀ (this : ∃ (a : R), a ≠ 0 ∧ ∀ (b : R), a * b ≠ 1), ∃ (x : R) (_ : x ≠ 0), ∀ (b : R), x * b ≠ 1
⊢ ∃ (x : R) (_ : x ≠ 0), ¬∃ (b : R), x * b = 1

Tactic:
push Not at this ⊢

Premises used: Not
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
hf : ¬IsField R
this : ∃ (a : R), a ≠ 0 ∧ ∀ (b : R), a * b ≠ 1
obtain : ∀ (x : R) (hx : x ≠ 0) (not_unit : ∀ (b : R), x * b ≠ 1), ∃ (x : R) (_ : x ≠ 0), ∀ (b : R), x * b ≠ 1
⊢ ∃ (x : R) (_ : x ≠ 0), ∀ (b : R), x * b ≠ 1

Tactic:
obtain ⟨x, hx, not_unit⟩ := this
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
hf : ¬IsField R
x : R
hx : x ≠ 0
not_unit : ∀ (b : R), x * b ≠ 1
⊢ ∃ (x : R) (_ : x ≠ 0), ∀ (b : R), x * b ≠ 1

Tactic:
⟨x, hx, not_unit⟩

Premises used: Exists.intro
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
hf : ¬IsField R
x : R
hx : x ≠ 0
not_unit : ∀ (b : R), x * b ≠ 1
⊢ ∃ (x : R) (_ : x ≠ 0), ∀ (b : R), x * b ≠ 1

Tactic:
exact ⟨x, hx, not_unit⟩
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ IsField R ↔ IsMaximal.{u_5} (α := R) ⊥

Tactic:
⟨fun h ↦ let := h.toSemifield; bot_isMaximal, fun hmax ↦ ?_⟩

Premises used: IsField.toSemifield, Ideal.bot_isMaximal, Iff.intro
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
refine : ∀ (hmax : IsMaximal.{u_5} (α := R) ⊥), IsField R
⊢ IsField R ↔ IsMaximal.{u_5} (α := R) ⊥

Tactic:
refine ⟨fun h ↦ let := h.toSemifield; bot_isMaximal, fun hmax ↦ ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
hmax : IsMaximal.{u_5} (α := R) ⊥
by_contra : ∀ (hf : ¬IsField R), False
⊢ IsField R

Tactic:
by_contra hf
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
hmax : IsMaximal.{u_5} (α := R) ⊥
hf : ¬IsField R
obtain : ∀ (x : R) (hx0 : x ≠ 0) (hxu : ¬IsUnit x), False
⊢ False

Tactic:
obtain ⟨x, hx0, hxu⟩ := exists_not_isUnit_of_not_isField hf

Premises used: Ring.exists_not_isUnit_of_not_isField
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
hmax : IsMaximal.{u_5} (α := R) ⊥
hf : ¬IsField R
x : R
hx0 : x ≠ 0
hxu : ¬IsUnit x
⊢ False

Tactic:
hx0 <| span_singleton_eq_bot.mp (hmax.eq_of_le (span_singleton_ne_top hxu) bot_le).symm

Premises used: Ideal.span_singleton_eq_bot, Ideal.IsMaximal.eq_of_le, Iff.mp, Ideal.span_singleton_ne_top, Eq.symm, bot_le
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
hmax : IsMaximal.{u_5} (α := R) ⊥
hf : ¬IsField R
x : R
hx0 : x ≠ 0
hxu : ¬IsUnit x
⊢ False

Tactic:
exact hx0 <| span_singleton_eq_bot.mp (hmax.eq_of_le (span_singleton_ne_top hxu) bot_le).symm

Premises used: Ideal.span_singleton_eq_bot, Ideal.IsMaximal.eq_of_le, Iff.mp, Ideal.span_singleton_ne_top, Eq.symm, bot_le
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
h : ¬IsField R
contrapose! : ∀ (h : ∀ (p : Ideal R) (_ : p ≠ ⊥), ¬p.IsMaximal), IsField R
⊢ ∃ (p : Ideal R), p ≠ ⊥ ∧ p.IsMaximal

Tactic:
contrapose! h
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
h : ∀ (p : Ideal R) (_ : p ≠ ⊥), ¬p.IsMaximal
⊢ ∀ (p : Ideal R) (_ : ⊥ < p), ¬p.IsMaximal

Tactic:
simp only [← bot_lt_iff_ne_bot] at h

Premises used: bot_lt_iff_ne_bot
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
h : ∀ (p : Ideal R) (_ : ⊥ < p), ¬p.IsMaximal
⊢ IsField R

Tactic:
isField_iff_maximal_bot.mpr ⟨⟨bot_ne_top, Ideal.maximal_of_no_maximal h⟩⟩

Premises used: Ideal.maximal_of_no_maximal, Iff.mpr, Ideal.IsMaximal.mk, And.intro, bot_ne_top, Ring.isField_iff_maximal_bot
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
h : ∀ (p : Ideal R) (_ : ⊥ < p), ¬p.IsMaximal
⊢ IsField R

Tactic:
refine isField_iff_maximal_bot.mpr ⟨⟨bot_ne_top, Ideal.maximal_of_no_maximal h⟩⟩

Premises used: Ideal.maximal_of_no_maximal, Iff.mpr, Ideal.IsMaximal.mk, And.intro, bot_ne_top, Ring.isField_iff_maximal_bot
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
I : Ideal R
h_bot : I ≠ ⊥
h_top : I ≠ ⊤
contrapose : ∀ (h_bot : IsField R), I = ⊥
⊢ ¬IsField R

Tactic:
contrapose h_bot
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
I : Ideal R
h_top : I ≠ ⊤
h_bot : IsField R
⊢ I = ⊥

Tactic:
((isField_iff_maximal_bot.mp h_bot).eq_of_le h_top bot_le).symm

Premises used: Ideal.IsMaximal.eq_of_le, Iff.mp, Ring.isField_iff_maximal_bot, Eq.symm, bot_le
-- Module: Mathlib.RingTheory.Ideal.Basic
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
I : Ideal R
h_top : I ≠ ⊤
h_bot : IsField R
⊢ I = ⊥

Tactic:
exact ((isField_iff_maximal_bot.mp h_bot).eq_of_le h_top bot_le).symm

Premises used: Ideal.IsMaximal.eq_of_le, Iff.mp, Ring.isField_iff_maximal_bot, Eq.symm, bot_le