awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
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 :
  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
⊢ Membership.mem (γ := Ideal α) (span ((fun (x : α) ↦ x ^ (n + 1)) '' s)) 1
have succ : (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)) ⊆
  (↑(span ((fun (x : α) ↦ x ^ (n + 1)) '' s)) : Set α)
Tactic: refine span_le.mpr ?_ this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (hypothesis)
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 :
  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
a : α
hx :
  Membership.mem (γ := Set α)
    ((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)))
    a
⊢ a ∈ (↑(span ((fun (x : α) ↦ x ^ (n + 1)) '' s)) : Set α)
have hx₁ : ∃ x ∈ (↑f.support : Set (↑s : Type u_2)),
  HMul.hMul (α := α) ((f : (a : (↑s : Type u_2)) → α) x : α) (↑x : α) ^ (n + 1) = a
Tactic: simp_rw [Set.mem_image] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
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 :
  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
a : α
hx :
  ∃ x ∈ (↑f.support : Set (↑s : Type u_2)),
    HMul.hMul (α := α) ((f : (a : (↑s : Type u_2)) → α) x : α) (↑x : α) ^ (n + 1) = a
⊢ a ∈ (↑(span ((fun (x : α) ↦ x ^ (n + 1)) '' s)) : Set α)
have succ : ∀ x ∈ (↑f.support : Set (↑s : Type u_2)),
  HMul.hMul (α := α) ((f : (a : (↑s : Type u_2)) → α) x : α) (↑x : α) ^ (n + 1) ∈
    (↑(span ((fun (x : α) ↦ x ^ (n + 1)) '' s)) : Set α)
Tactic: rcases hx with ⟨x, _, rfl⟩
Cleared hypotheses: a, hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
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 :
  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))
⊢ LE.le (α := Ideal α) (span {(↑x : α) ^ (n + 1)}) (span ((fun (x : α) ↦ x ^ (n + 1)) '' s))
have rw : (↑x : α) ^ (n + 1) ∈ (↑(span ((fun (x : α) ↦ x ^ (n + 1)) '' s)) : Set α)
Tactic: rw [span_le, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (hypothesis)
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 :
  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))
⊢ HMul.hMul (α := α) ((f : (a : (↑s : Type u_2)) → α) x : α) (↑x : α) ^ (n + 1) ∈
    (↑(span ((fun (x : α) ↦ x ^ (n + 1)) '' s)) : Set α)
have this₁ : LE.le (α := Ideal α) (span {(↑x : α) ^ (n + 1)}) (span ((fun (x : α) ↦ x ^ (n + 1)) '' s))
Tactic: have : span ({(x : α) ^ (n + 1)} : Set α) ≤ span ((fun x : α => x ^ (n + 1)) '' s) := by
    rw [span_le, Set.singleton_subset_iff]
    exact subset_span ⟨x, x.prop, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
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))
⊢ HMul.hMul (α := α) ((f : (a : (↑s : Type u_2)) → α) x : α) (↑x : α) ^ (n + 1) ∈
    (↑(span ((fun (x : α) ↦ x ^ (n + 1)) '' s)) : Set α)
have succ : Membership.mem (γ := Submodule α α) (span {(↑x : α) ^ (n + 1)})
  (HMul.hMul (α := α) ((f : (a : (↑s : Type u_2)) → α) x : α) (↑x : α) ^ (n + 1))
Tactic: refine this ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
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))
⊢ Membership.mem (γ := Submodule α α) (span {(↑x : α) ^ (n + 1)})
    (HMul.hMul (α := α) ((f : (a : (↑s : Type u_2)) → α) x : α) (↑x : α) ^ (n + 1))
have succ : (↑x : α) ^ (n + 1) ∣ HPow.hPow (α := α) ((f : (a : (↑s : Type u_2)) → α) x : α) (n + 1) * (↑x : α) ^ (n + 1)
Tactic: rw [mul_pow, mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
α : Type u_2
inst : CommSemiring α
s : Set α
hs : Eq (α := Ideal α) (span s) ⊤
n : (↑s : Type u_2) → ℕ
⊢ Eq.{u_2 + 1} (α := Ideal α) (span (range fun (x : (↑s : Type u_2)) ↦ (↑x : α) ^ n x)) ⊤
have 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)) ⊤
Tactic: have ⟨t, hts, mem⟩ := Submodule.mem_span_finite_of_mem_span ((eq_top_iff_one _).mp hs)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
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)) ⊤
have refine : (fun (x : α) ↦
      HPow.hPow (β := ℕ) x (t.attach.sup fun (x : ↥t) ↦ n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) sorry))) ''
    (↑t : Set α) ⊆
  (↑(span (range fun (x : (↑s : Type u_2)) ↦ (↑x : α) ^ n x)) : Set α)
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 ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
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 α)
⊢ (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 α)
have rw : (fun (x_1 : α) ↦
      x_1 ^
        ((t.attach.sup fun (x : ↥t) ↦ n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) sorry)) -
            n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hxt) : α) sorry) +
          n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hxt) : α) sorry)))
    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⟩)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
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 α)
⊢ (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 α)
have simp_rw : x ^
      ((t.attach.sup fun (x : ↥t) ↦ n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) (↑x : α) sorry)) -
        n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x sorry)) *
    x ^ n (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x sorry) ∈
  (↑(span (range fun (x : (↑s : Type u_2)) ↦ (↑x : α) ^ n x)) : Set α)
Tactic: simp_rw [pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
α : Type u_2
inst : CommSemiring α
ι : Type u_5
f : ι → α
s : Finset ι
I : Ideal α
i : ι
hi : i ∈ s
hfi : f i ∈ I
⊢ ∏ i ∈ s, f i ∈ I
have rw : (∏ x ∈ s \ {i}, f x) * f i ∈ I
Tactic: rw [Finset.prod_eq_prod_diff_singleton_mul hi]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
α : Type u_2
inst : CommSemiring α
ι : Type u_5
f : ι → α
s : Finset ι
I : Ideal α
i : ι
hi : i ∈ s
hfi : f i ∈ I
⊢ ∏ i ∈ s, f i ∈ I
have rw : (∏ x ∈ s \ {i}, f x) * f i ∈ I
Tactic: classical
  rw [Finset.prod_eq_prod_diff_singleton_mul hi]
  exact Ideal.mul_mem_left _ _ hfi
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
ι : Type u_5
inst : DecidableEq ι
inst_1 : Finite ι
R : ι → Type u_6
inst_2 : (i : ι) → Semiring (R i)
⊢ Eq (α := Ideal ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1)) ⊤
have rw : LE.le (α := Ideal ((j : ι) → R j)) ⊤ (span (range fun (i : ι) ↦ Pi.single (M := R) i 1))
Tactic: rw [_root_.eq_top_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
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)
have 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)
Tactic: rw [show Pi.single i r = Pi.single i r * Pi.single i 1 by simp [← Pi.single_mul_left]]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
ι : Type u_5
inst : DecidableEq ι
inst_1 : Finite ι
R : ι → Type u_6
inst_2 : (i : ι) → Semiring (R i)
x : (j : ι) → R j
⊢ Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1)) x
have zero : Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1)) 0
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⟩)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
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
⊢ Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1)) x
have 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)
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⟩)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
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)
⊢ Membership.mem (γ := Submodule ((j : ι) → R j) ((j : ι) → R j)) (span (range fun (i : ι) ↦ Pi.single (M := R) i 1)) x
have 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)
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⟩)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
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
⊢ ![⊥, ⊤] ((fun (I : Ideal K) ↦ (if I = ⊥ then 0 else 1 : Fin 2)) I) = I
have inl : Eq.{u_5 + 1} (α := Ideal K) (![⊥, ⊤] ((fun (I : Ideal K) ↦ (if I = ⊥ then 0 else 1 : Fin 2)) ⊥)) ⊥
Tactic: rcases eq_bot_or_top I with rfl | rfl
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
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)) ⊥)) ⊥
⊢ ![⊥, ⊤] ((fun (I : Ideal K) ↦ (if I = ⊥ then 0 else 1 : Fin 2)) I) = I
have inr : Eq.{u_5 + 1} (α := Ideal K) (![⊥, ⊤] ((fun (I : Ideal K) ↦ (if I = ⊥ then 0 else 1 : Fin 2)) ⊤)) ⊤
Tactic: rcases eq_bot_or_top I with rfl | rfl
Cleared hypotheses: I
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
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
⊢ (fun (I : Ideal K) ↦ (if I = ⊥ then 0 else 1 : Fin 2)) (![⊥, ⊤] i) = i
have 0 : Eq (α := Fin 2) ((fun (I : Ideal K) ↦ (if I = ⊥ then 0 else 1 : Fin 2)) (![⊥, ⊤] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)))
  ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
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, ⋯⟩)
⊢ (fun (I : Ideal K) ↦ (if I = ⊥ then 0 else 1 : Fin 2)) (![⊥, ⊤] i) = i
have 1 : Eq (α := Fin 2) ((fun (I : Ideal K) ↦ (if I = ⊥ then 0 else 1 : Fin 2)) (![⊥, ⊤] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)))
  ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (hypothesis)
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
hf : ¬IsField R
⊢ ∃ (x : R) (_ : x ≠ 0), ¬IsUnit x
have this : ¬∀ {a : R}, a ≠ 0 → ∃ (b : R), a * b = 1
Tactic: have : ¬_ := fun h => hf ⟨exists_pair_ne R, mul_comm, h⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
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
⊢ ∃ (x : R) (_ : x ≠ 0), ¬IsUnit x
have simp_rw : ∃ (x : R) (_ : x ≠ 0), ¬∃ (b : R), x * b = 1
Tactic: simp_rw [isUnit_iff_exists_inv]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
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
⊢ ∃ (x : R) (_ : x ≠ 0), ¬∃ (b : R), x * b = 1
have push : ∀ (this : ∃ (a : R), a ≠ 0 ∧ ∀ (b : R), a * b ≠ 1), ∃ (x : R) (_ : x ≠ 0), ∀ (b : R), x * b ≠ 1
Tactic: push Not at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
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
⊢ ∃ (x : R) (_ : x ≠ 0), ∀ (b : R), x * b ≠ 1
have obtain : ∀ (x : R) (hx : x ≠ 0) (not_unit : ∀ (b : R), x * b ≠ 1), ∃ (x : R) (_ : x ≠ 0), ∀ (b : R), x * b ≠ 1
Tactic: obtain ⟨x, hx, not_unit⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ IsField R ↔ IsMaximal.{u_5} (α := R) ⊥
have refine : ∀ (hmax : IsMaximal.{u_5} (α := R) ⊥), IsField R
Tactic: refine ⟨fun h ↦ let := h.toSemifield; bot_isMaximal, fun hmax ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
hmax : IsMaximal.{u_5} (α := R) ⊥
⊢ IsField R
have by_contra : ∀ (hf : ¬IsField R), False
Tactic: by_contra hf
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
hmax : IsMaximal.{u_5} (α := R) ⊥
hf : ¬IsField R
⊢ False
have obtain : ∀ (x : R) (hx0 : x ≠ 0) (hxu : ¬IsUnit x), False
Tactic: obtain ⟨x, hx0, hxu⟩ := exists_not_isUnit_of_not_isField hf
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
h : ¬IsField R
⊢ ∃ (p : Ideal R), p ≠ ⊥ ∧ p.IsMaximal
have contrapose! : ∀ (h : ∀ (p : Ideal R) (_ : p ≠ ⊥), ¬p.IsMaximal), IsField R
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (hypothesis)
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
h : ∀ (p : Ideal R) (_ : p ≠ ⊥), ¬p.IsMaximal
⊢ IsField R
have h₁ : ∀ (p : Ideal R) (_ : ⊥ < p), ¬p.IsMaximal
Tactic: simp only [← bot_lt_iff_ne_bot] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
I : Ideal R
h_bot : I ≠ ⊥
h_top : I ≠ ⊤
⊢ ¬IsField R
have contrapose : ∀ (h_bot : IsField R), I = ⊥
Tactic: contrapose h_bot
Cleared hypotheses: h_bot
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ ¬IsField R ↔ ∃ (I : Ideal R), ⊥ < I ∧ I < ⊤
have refine : ∀ (h : ¬IsField R), ∃ (I : Ideal R), ⊥ < I ∧ I < ⊤
Tactic: refine ⟨fun h ↦ ?_, fun ⟨I, h_bot, h_top⟩ ↦ not_isField_of_ne_of_ne h_bot.ne' h_top.ne⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
h : ¬IsField R
⊢ ∃ (I : Ideal R), ⊥ < I ∧ I < ⊤
have obtain : ∀ (I : Ideal R) (hI : I ≠ ⊥) (hIm : I.IsMaximal), ∃ (I : Ideal R), ⊥ < I ∧ I < ⊤
Tactic: obtain ⟨I, hI, hIm⟩ := exists_maximal_of_not_isField h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ ¬IsField R ↔ ∃ (p : Ideal R), p ≠ ⊥ ∧ p.IsPrime
have refine : ∀ (h : ¬IsField R), ∃ (p : Ideal R), p ≠ ⊥ ∧ p.IsPrime
Tactic: refine ⟨fun h ↦ ?_, fun ⟨I, h_bot, h_top⟩ ↦ not_isField_of_ne_of_ne h_bot h_top.ne_top⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
h : ¬IsField R
⊢ ∃ (p : Ideal R), p ≠ ⊥ ∧ p.IsPrime
have obtain : ∀ (I : Ideal R) (hI : I ≠ ⊥) (hIm : I.IsMaximal), ∃ (p : Ideal R), p ≠ ⊥ ∧ p.IsPrime
Tactic: obtain ⟨I, hI, hIm⟩ := exists_maximal_of_not_isField h
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
⊢ IsField R ↔ IsSimpleOrder.{u_5} (Ideal R)
have inl : Subsingleton R → (IsField R ↔ IsSimpleOrder.{u_5} (Ideal R))
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
inl : Subsingleton R → (IsField R ↔ IsSimpleOrder.{u_5} (Ideal R))
⊢ IsField R ↔ IsSimpleOrder.{u_5} (Ideal R)
have inr : Nontrivial R → (IsField R ↔ IsSimpleOrder.{u_5} (Ideal R))
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
h : Nontrivial R
⊢ IsField R ↔ IsSimpleOrder.{u_5} (Ideal R)
have inr : (∃ (I : Ideal R), ⊥ < I ∧ I < ⊤) ↔ ¬IsSimpleOrder.{u_5} (Ideal R)
Tactic: rw [← not_iff_not, Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
h : Nontrivial R
⊢ (∃ (I : Ideal R), ⊥ < I ∧ I < ⊤) ↔ ¬IsSimpleOrder.{u_5} (Ideal R)
have inr : (∀ (I : Ideal R), ¬⊥ < I ∨ ¬I < ⊤) ↔ IsSimpleOrder.{u_5} (Ideal R)
Tactic: contrapose! +distrib
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
h : Nontrivial R
⊢ (∀ (I : Ideal R), ¬⊥ < I ∨ ¬I < ⊤) ↔ IsSimpleOrder.{u_5} (Ideal R)
have inr : (∀ (I : Ideal R), I = ⊥ ∨ I = ⊤) ↔ IsSimpleOrder.{u_5} (Ideal R)
Tactic: simp_rw [not_lt_top_iff, not_bot_lt_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
inst_1 : Nontrivial R
not_field : ¬IsField R
max : Ideal.IsMaximal.{u_5} (α := R) ⊥
⊢ False
have obtain : ∀ (I : Ideal R) (hIbot : ⊥ < I) (hItop : I < ⊤), False
Tactic: obtain ⟨I, hIbot, hItop⟩ := not_isField_iff_exists_ideal_bot_lt_and_lt_top.mp not_field
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
b : Basis ι R S
x : S
hx : x ≠ 0
⊢ Eq (α := Submodule R S) (LinearMap.range (LinearMap.mulLeft R x)) (Submodule.restrictScalars R (span {x}))
have h : ∀ (x_1 : S),
  Membership.mem (γ := Submodule R S) (LinearMap.range (LinearMap.mulLeft R x)) x_1 ↔
    Membership.mem (γ := Submodule R S) (Submodule.restrictScalars R (span {x})) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Colon (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N_1 N₁ N₂ : Submodule R M
S_1 S₁ S₂ : Set M
N : Submodule R M
S : Set M
r : R
⊢ ∀ {x : R},
    Membership.mem (γ := Set R) {r : R | r • S ⊆ (↑N : Set M)} x →
      Membership.mem (γ := Set R) {r : R | r • S ⊆ (↑N : Set M)} (r • x)
have simp : ∀ {x : R}, (∀ ⦃b : M⦄, b ∈ S → x • b ∈ (↑N : Set M)) → ∀ ⦃b : M⦄, b ∈ S → r • x • b ∈ (↑N : Set M)
Tactic: simp only [Set.mem_setOf_eq, smul_eq_mul, mul_smul, Set.smul_set_subset_iff]