awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
pos : ∀ (has : a ∈ s), ∃ i ∈ s, I ≤ f i
neg neg₁ : ∀ (has : a ∉ s), ∃ i ∈ s, I ≤ f i
⊢ ∃ i ∈ s, I ≤ f i

Tactic:
classical
    by_cases has : a ∈ s
    · obtain ⟨t, hat, rfl⟩ : ∃ t, a ∉ t ∧ insert a t = s :=
        ⟨s.erase a, Finset.notMem_erase a s, Finset.insert_erase has⟩
      by_cases hbt : b ∈ t
      · obtain ⟨u, hbu, rfl⟩ : ∃ u, b ∉ u ∧ insert b u = t :=
          ⟨t.erase b, Finset.notMem_erase b t, Finset.insert_erase hbt⟩
        have hp' : ∀ i ∈ u, IsPrime (f i) := by
          intro i hiu
          refine hp i (Finset.mem_insert_of_mem (Finset.mem_insert_of_mem hiu)) ?_ ?_ <;>
              rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Finset.coe_insert, Set.biUnion_insert, Set.biUnion_insert, ←
          Set.union_assoc, subset_union_prime' hp'] at h
        rwa [Finset.exists_mem_insert, Finset.exists_mem_insert]
      · have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f a : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]
    · by_cases hbs : b ∈ s
      · obtain ⟨t, hbt, rfl⟩ : ∃ t, b ∉ t ∧ insert b t = s :=
          ⟨s.erase b, Finset.notMem_erase b s, Finset.insert_erase hbs⟩
        have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f b : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]
      rcases s.eq_empty_or_nonempty with rfl | hsne
      · rw [Finset.coe_empty, Set.biUnion_empty] at h
        exact (h I.zero_mem).elim
      · obtain ⟨i, his⟩ := hsne
        obtain ⟨t, _, rfl⟩ : ∃ t, i ∉ t ∧ insert i t = s :=
          ⟨s.erase i, Finset.notMem_erase i s, Finset.insert_erase his⟩
        have hp' : ∀ j ∈ t, IsPrime (f j) := by
          intro j hj
          refine hp j (Finset.mem_insert_of_mem hj) ?_ ?_ <;> rintro rfl <;>
            solve_by_elim only [Finset.mem_insert_of_mem, *]
        rw [Finset.coe_insert, Set.biUnion_insert, ← Set.union_self (f i : Set R),
          subset_union_prime' hp', ← or_assoc, or_self_iff] at h
        rwa [Finset.exists_mem_insert]

Premises used: Finset.coe_empty, or_self_iff, Set.biUnion_empty, Set.biUnion_insert, Finset.exists_mem_insert, Ideal.zero_mem, SetLike.coe, Set.union_assoc, Set.union_self, Finset.coe_insert, rfl, or_assoc, Exists.elim, Finset.eq_empty_or_nonempty
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
this : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R) → ∃ i ∈ s, I ≤ f i
⊢ ∀ (h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)), ∃ (x : ι) (_ : x ∈ s), I ≤ f x

Tactic:
have aux := fun h => (bex_def.2 <| this h)
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
this : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R) → ∃ i ∈ s, I ≤ f i
aux : ∀ (h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)), ∃ (x : ι) (_ : x ∈ s), I ≤ f x
⊢ ∀ (h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)), ∃ x ∈ s, I ≤ f x

Tactic:
simp_rw [exists_prop] at aux

Premises used: exists_prop
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
this aux : ∀ (h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)), ∃ x ∈ s, I ≤ f x
⊢ (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R) ↔ ∃ i ∈ s, I ≤ f i

Tactic:
⟨aux, fun ⟨i, his, hi⟩ ↦ Set.Subset.trans hi ?_⟩

Premises used: Set.Subset.trans, HasSubset.Subset, SetLike.coe, Iff.intro, _private.0.Ideal.subset_union_prime'.match_1, Set.iUnion
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
this aux : ∀ (h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)), ∃ x ∈ s, I ≤ f x
refine :
  (∃ i ∈ s, I ≤ f i) → ∀ (i : ι) (his : i ∈ s) (hi : I ≤ f i), (↑(f i) : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)
⊢ (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R) ↔ ∃ i ∈ s, I ≤ f i

Tactic:
refine ⟨aux, fun ⟨i, his, hi⟩ ↦ Set.Subset.trans hi ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
R : Type u
inst : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
this aux : ∀ (h : (↑I : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)), ∃ x ∈ s, I ≤ f x
h : ∃ i ∈ s, I ≤ f i
i : ι
his : i ∈ s
hi : I ≤ f i
⊢ (↑(f i) : Set R) ⊆ ⋃ i ∈ (↑s : Set ι), (↑(f i) : Set R)

Tactic:
apply Set.subset_biUnion_of_mem (show i ∈ (↑s : Set ι) from his)

Premises used: Set.subset_biUnion_of_mem
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
rcases : ∀ (t : Finset ι) (ht : ∀ (a : ι), a ∈ t ↔ a ∈ s), (↑I : Set R) ⊆ ⋃ i ∈ s, (↑(f i) : Set R) ↔ ∃ i ∈ s, I ≤ f i
⊢ (↑I : Set R) ⊆ ⋃ i ∈ s, (↑(f i) : Set R) ↔ ∃ i ∈ s, I ≤ f i

Tactic:
rcases Set.Finite.exists_finset hs with ⟨t, ht⟩

Premises used: Set.Finite.exists_finset
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
h :
  ∀ (x : R),
    Membership.mem (γ := Set R) (⋃ i ∈ s, (↑(f i) : Set R)) x ↔
      Membership.mem (γ := Set R) (⋃ i ∈ t, (↑(f i) : Set R)) x
⊢ Eq.{u_2 + 1} (α := Set R) (⋃ i ∈ s, (↑(f i) : Set R)) (⋃ i ∈ t, (↑(f i) : Set R))

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
x : R
⊢ Membership.mem (γ := Set R) (⋃ i ∈ s, (↑(f i) : Set R)) x ↔ Membership.mem (γ := Set R) (⋃ i ∈ t, (↑(f i) : Set R)) x

Tactic:
simpa using exists_congr (fun i ↦ (and_congr_left fun a ↦ ht i).symm)

Premises used: and_congr_left, exists_congr, Iff.symm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
⊢ Eq.{u_2 + 1} (α := Set R) (⋃ i ∈ s, (↑(f i) : Set R)) (⋃ i ∈ t, (↑(f i) : Set R))

Tactic:
have heq : ⋃ i ∈ s, f i = ⋃ i ∈ t, (f i : Set R) := by
    ext
    simpa using exists_congr (fun i ↦ (and_congr_left fun a ↦ ht i).symm)
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
heq : Eq.{u_2 + 1} (α := Set R) (⋃ i ∈ s, (↑(f i) : Set R)) (⋃ i ∈ t, (↑(f i) : Set R))
⊢ (↑I : Set R) ⊆ ⋃ i ∈ s, (↑(f i) : Set R) ↔ (↑I : Set R) ⊆ ⋃ i ∈ (↑t : Set ι), (↑(f i) : Set R)

Tactic:
have hmem_union : ((I : Set R) ⊆ ⋃ i ∈ s, f i) ↔ ((I : Set R) ⊆ ⋃ i ∈ (t : Set ι), f i) :=
    (congrArg _ heq).to_iff
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
heq : Eq.{u_2 + 1} (α := Set R) (⋃ i ∈ s, (↑(f i) : Set R)) (⋃ i ∈ t, (↑(f i) : Set R))
hmem_union : (↑I : Set R) ⊆ ⋃ i ∈ s, (↑(f i) : Set R) ↔ (↑I : Set R) ⊆ ⋃ i ∈ (↑t : Set ι), (↑(f i) : Set R)
rw : (∃ i ∈ t, I ≤ f i) ↔ ∃ i ∈ s, I ≤ f i
⊢ (↑I : Set R) ⊆ ⋃ i ∈ s, (↑(f i) : Set R) ↔ ∃ i ∈ s, I ≤ f i

Tactic:
rw [hmem_union, Ideal.subset_union_prime a b (fun i hin ↦ hp i ((ht i).mp hin))]

Premises used: Iff.mp, Ideal.subset_union_prime
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
heq : Eq.{u_2 + 1} (α := Set R) (⋃ i ∈ s, (↑(f i) : Set R)) (⋃ i ∈ t, (↑(f i) : Set R))
hmem_union : (↑I : Set R) ⊆ ⋃ i ∈ s, (↑(f i) : Set R) ↔ (↑I : Set R) ⊆ ⋃ i ∈ (↑t : Set ι), (↑(f i) : Set R)
⊢ (∃ i ∈ t, I ≤ f i) ↔ ∃ i ∈ s, I ≤ f i

Tactic:
exists_congr (fun i ↦ and_congr_left fun _ ↦ ht i)

Premises used: and_congr_left, exists_congr
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
ι : Type u_3
inst : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
heq : Eq.{u_2 + 1} (α := Set R) (⋃ i ∈ s, (↑(f i) : Set R)) (⋃ i ∈ t, (↑(f i) : Set R))
hmem_union : (↑I : Set R) ⊆ ⋃ i ∈ s, (↑(f i) : Set R) ↔ (↑I : Set R) ⊆ ⋃ i ∈ (↑t : Set ι), (↑(f i) : Set R)
⊢ (∃ i ∈ t, I ≤ f i) ↔ ∃ i ∈ s, I ≤ f i

Tactic:
exact exists_congr (fun i ↦ and_congr_left fun _ ↦ ht i)

Premises used: and_congr_left, exists_congr
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
n : ℕ
obtain : ∀ (y i : R) (hmem : i ∈ I) (hi : y * x + i = 1), ∃ (y : R), ∃ i ∈ I ^ n, y * x + i = 1
⊢ ∃ (y : R), ∃ i ∈ I ^ n, y * x + i = 1

Tactic:
obtain ⟨y, i, hmem, hi⟩ := Ideal.IsMaximal.exists_inv ‹_› hx

Premises used: Ideal.IsMaximal.exists_inv
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
⊢ 0 * x + HPow.hPow (β := ℕ) i 0 = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
⊢ ∃ (y : R), y * x + HPow.hPow (β := ℕ) i 0 = 1

Tactic:
exact ⟨0, by simp⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
n : ℕ
ih : ∃ (y : R), y * x + i ^ n = 1
succ : ∀ (z : R) (hz : z * x + i ^ n = 1), ∃ (y : R), y * x + i ^ (n + 1) = 1
⊢ ∃ (y : R), y * x + i ^ (n + 1) = 1

Tactic:
obtain ⟨z, hz⟩ := ih
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
n : ℕ
z : R
hz : z * x + i ^ n = 1
⊢ ∃ (y : R), y * x + i ^ (n + 1) = 1

Tactic:
⟨z * i + y, ?_⟩

Premises used: HMul.hMul, HAdd.hAdd, Exists.intro
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
n : ℕ
z : R
hz : z * x + i ^ n = 1
succ : (z * i + y) * x + i ^ (n + 1) = 1
⊢ ∃ (y : R), y * x + i ^ (n + 1) = 1

Tactic:
refine ⟨z * i + y, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
n : ℕ
z : R
hz : z * x + i ^ n = 1
trans : (z * i + y) * x + i ^ (n + 1) = z * i * x + i * i ^ n + y * x
trans₁ : z * i * x + i * i ^ n + y * x = 1
⊢ (z * i + y) * x + i ^ (n + 1) = 1

Tactic:
trans z * i * x + i * i ^ n + y * x
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
n : ℕ
z : R
hz : z * x + i ^ n = 1
⊢ (z * i + y) * x + i ^ (n + 1) = z * i * x + i * i ^ n + y * x

Tactic:
ring
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
n : ℕ
z : R
hz : z * x + i ^ n = 1
rw : y * x + i * 1 = 1
⊢ z * i * x + i * i ^ n + y * x = 1

Tactic:
rw [mul_comm z i, mul_assoc, ← mul_add, hz, add_comm]

Premises used: mul_assoc, add_comm, mul_comm, mul_add
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
y i : R
hmem : i ∈ I
hi : y * x + i = 1
n : ℕ
z : R
hz : z * x + i ^ n = 1
⊢ y * x + i * 1 = 1

Tactic:
simpa
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
n : ℕ
y i : R
hmem : i ∈ I
hi : y * x + i = 1
zero : ∃ (y : R), y * x + HPow.hPow (β := ℕ) i 0 = 1
succ : ∀ (n : ℕ) (ih : ∃ (y : R), y * x + i ^ n = 1), ∃ (y : R), y * x + i ^ (n + 1) = 1
⊢ ∃ (y : R), y * x + i ^ n = 1

Tactic:
induction n with
    | zero => exact ⟨0, by simp⟩
    | succ n ih =>
      obtain ⟨z, hz⟩ := ih
      refine ⟨z * i + y, ?_⟩
      trans z * i * x + i * i ^ n + y * x
      · ring
      · rw [mul_comm z i, mul_assoc, ← mul_add, hz, add_comm]
        simpa

Premises used: mul_assoc, add_comm, mul_add
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
n : ℕ
y i : R
hmem : i ∈ I
hi : y * x + i = 1
obtain : ∀ (y : R) (hy : y * x + i ^ n = 1), ∃ (y : R), ∃ i ∈ I ^ n, y * x + i = 1
⊢ ∃ (y : R), ∃ i ∈ I ^ n, y * x + i = 1

Tactic:
obtain ⟨y, hy⟩ : ∃ y : R, y * x + i ^ n = 1 := by
    induction n with
    | zero => exact ⟨0, by simp⟩
    | succ n ih =>
      obtain ⟨z, hz⟩ := ih
      refine ⟨z * i + y, ?_⟩
      trans z * i * x + i * i ^ n + y * x
      · ring
      · rw [mul_comm z i, mul_assoc, ← mul_add, hz, add_comm]
        simpa
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
n : ℕ
y_1 i : R
hmem : i ∈ I
hi : y_1 * x + i = 1
y : R
hy : y * x + i ^ n = 1
⊢ ∃ (y : R), ∃ i ∈ I ^ n, y * x + i = 1

Tactic:
⟨y, i ^ n, Ideal.pow_mem_pow hmem n, hy⟩

Premises used: HPow.hPow, And.intro, Exists.intro, Ideal.pow_mem_pow
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
x : R
hx : x ∉ I
n : ℕ
y_1 i : R
hmem : i ∈ I
hi : y_1 * x + i = 1
y : R
hy : y * x + i ^ n = 1
⊢ ∃ (y : R), ∃ i ∈ I ^ n, y * x + i = 1

Tactic:
exact ⟨y, i ^ n, Ideal.pow_mem_pow hmem n, hy⟩
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
rw : a ∉ I → b ∈ I ^ n
⊢ a ∈ I ∨ b ∈ I ^ n

Tactic:
rw [Classical.or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
obtain : ∀ (c i : R) (hi : i ∈ I ^ n) (hc : c * a + i = 1), b ∈ I ^ n
⊢ b ∈ I ^ n

Tactic:
obtain ⟨c, i, hi, hc⟩ := exists_inv_pow I ha n

Premises used: Ideal.IsMaximal.exists_inv_pow
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
⊢ (c * a + i) * b = 1 * b

Tactic:
obtain hb := congr($hc * b)
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
hb : (c * a + i) * b = 1 * b
⊢ (c * a + i) * b = b

Tactic:
rw [one_mul] at hb

Premises used: one_mul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
hb : (c * a + i) * b = b
rw : c * (a * b) + i * b ∈ I ^ n
⊢ b ∈ I ^ n

Tactic:
rw [← hb, add_mul, mul_assoc]

Premises used: add_mul, mul_assoc
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
hb : (c * a + i) * b = b
⊢ c * (a * b) + i * b ∈ I ^ n

Tactic:
add_mem (mul_mem_left _ _ h) (mul_mem_right _ _ hi)

Premises used: Ideal.mul_mem_right, AddMemClass.add_mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
hb : (c * a + i) * b = b
⊢ c * (a * b) + i * b ∈ I ^ n

Tactic:
exact add_mem (mul_mem_left _ _ h) (mul_mem_right _ _ hi)

Premises used: Ideal.mul_mem_right, AddMemClass.add_mem, Ideal.mul_mem_left
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ b * a ∈ I ^ n

Tactic:
rw [mul_comm] at h

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
a b : R
n : ℕ
h : b * a ∈ I ^ n
rw : b ∈ I ∨ a ∈ I ^ n
⊢ a ∈ I ^ n ∨ b ∈ I

Tactic:
rw [or_comm]

Premises used: or_comm
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
a b : R
n : ℕ
h : b * a ∈ I ^ n
⊢ b ∈ I ∨ a ∈ I ^ n

Tactic:
mul_mem_pow _ h

Premises used: Ideal.IsMaximal.mul_mem_pow
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u_2
inst : CommSemiring R
I : Ideal R
inst_1 : I.IsMaximal
a b : R
n : ℕ
h : b * a ∈ I ^ n
⊢ b ∈ I ∨ a ∈ I ^ n

Tactic:
exact mul_mem_pow _ h

Premises used: Ideal.IsMaximal.mul_mem_pow
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
⊢ I ∣ ⊥

Tactic:
dvd_zero I

Premises used: dvd_zero
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
h : I = ⊤
rw : ⊤ = I
rw₁ rw₂ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
⊢ ⊤ = I * ⊤

Tactic:
rw [mul_top, h]

Premises used: Ideal.mul_top
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
R : Type u
ι : Type u_1
inst : CommSemiring R
I J K L : Ideal R
u : (Ideal R)ˣ
rw : Eq.{u + 1} (α := Ideal R) ⊤ 1
rw₁ rw₂ : Eq.{u + 1} (α := Ideal R) ⊤ ⊤
⊢ (↑u : Ideal R) = 1

Tactic:
rw [isUnit_iff.mp u.isUnit, one_eq_top]

Premises used: Ideal.one_eq_top, Ideal.isUnit_iff, Iff.mp, Units.isUnit
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
f : Finsupp.{u_1, u_3} ι ↥I
dsimp :
  Eq.{u_2 + 1} (α := M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M)
        (Finsupp.mapRange (Subtype.val (p := fun (x : R) ↦ x ∈ I)) ⋯ f) :
      M)
    (f.sum fun (i : ι) (x : ↥I) ↦ (↑x : R) • v i : M)
⊢ Eq.{u_2 + 1} (α := M) ((finsuppTotal ι M I v : (a : ι →₀ ↥I) → M) f : M)
    (f.sum fun (i : ι) (x : ↥I) ↦ (↑x : R) • v i : M)

Tactic:
dsimp [finsuppTotal]

Premises used: Ideal.finsuppTotal
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
f : Finsupp.{u_1, u_3} ι ↥I
rw : ∀ (a : ι), HSMul.hSMul.{u_3, u_2, u_2} (α := R) 0 (v a) = 0
⊢ Eq.{u_2 + 1} (α := M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M)
        (Finsupp.mapRange (Subtype.val (p := fun (x : R) ↦ x ∈ I)) ⋯ f) :
      M)
    (f.sum fun (i : ι) (x : ↥I) ↦ (↑x : R) • v i : M)

Tactic:
rw [Finsupp.linearCombination_apply, Finsupp.sum_mapRange_index]

Premises used: Finsupp.linearCombination_apply, Finsupp.sum_mapRange_index
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
f : Finsupp.{u_1, u_3} ι ↥I
⊢ ∀ (a : ι), HSMul.hSMul.{u_3, u_2, u_2} (α := R) 0 (v a) = 0

Tactic:
fun _ => zero_smul _ _

Premises used: zero_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
f : Finsupp.{u_1, u_3} ι ↥I
⊢ ∀ (a : ι), HSMul.hSMul.{u_3, u_2, u_2} (α := R) 0 (v a) = 0

Tactic:
exact fun _ => zero_smul _ _

Premises used: zero_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
inst_3 : Fintype ι
f : Finsupp.{u_1, u_3} ι ↥I
h : ∀ (i : ι), HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑0 : R) (v i) = 0
⊢ Eq.{u_2 + 1} (α := M) ((finsuppTotal ι M I v : (a : ι →₀ ↥I) → M) f : M)
    (∑ i : ι, HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑((f : (a : ι) → ↥I) i) : R) (v i) : M)

Tactic:
rw [finsuppTotal_apply, Finsupp.sum_fintype]

Premises used: Ideal.finsuppTotal_apply, Finsupp.sum_fintype
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
inst_3 : Fintype ι
f : Finsupp.{u_1, u_3} ι ↥I
⊢ ∀ (i : ι), HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑0 : R) (v i) = 0

Tactic:
fun _ => zero_smul _ _

Premises used: zero_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
inst_3 : Fintype ι
f : Finsupp.{u_1, u_3} ι ↥I
⊢ ∀ (i : ι), HSMul.hSMul.{u_3, u_2, u_2} (α := R) (↑0 : R) (v i) = 0

Tactic:
exact fun _ => zero_smul _ _

Premises used: zero_smul
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
h :
  ∀ (x : M),
    Membership.mem (γ := Submodule R M) (LinearMap.range (finsuppTotal ι M I v)) x ↔
      x ∈ HSMul.hSMul (β := Submodule R M) I (Submodule.span R (Set.range v))
⊢ LinearMap.range (finsuppTotal ι M I v) = HSMul.hSMul (β := Submodule R M) I (Submodule.span R (Set.range v))

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
x : M
h :
  Membership.mem (γ := Submodule R M) (LinearMap.range (finsuppTotal ι M I v)) x ↔
    ∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
      (a.sum fun (i : ι) (c : R) ↦ c • v i) = x
⊢ Membership.mem (γ := Submodule R M) (LinearMap.range (finsuppTotal ι M I v)) x ↔
    x ∈ HSMul.hSMul (β := Submodule R M) I (Submodule.span R (Set.range v))

Tactic:
rw [Submodule.mem_ideal_smul_span_iff_exists_sum]

Premises used: Submodule.mem_ideal_smul_span_iff_exists_sum
-- Module: Mathlib.RingTheory.Ideal.Operations
Goal:
ι : Type u_1
M : Type u_2
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
I : Ideal R
v : ι → M
x : M
⊢ Membership.mem (γ := Submodule R M) (LinearMap.range (finsuppTotal ι M I v)) x ↔
    ∃ (a : ι →₀ R) (_ : ∀ (i : ι), Membership.mem (α := R) I ((a : (a : ι) → R) i : R)),
      (a.sum fun (i : ι) (c : R) ↦ c • v i) = x

Tactic:
⟨fun ⟨f, h⟩ => ⟨Finsupp.mapRange.linearMap I.subtype f, fun i => (f i).2, h⟩, ?_⟩

Premises used: Finsupp.sum, Exists, Iff.intro, Exists.intro, Submodule.subtype, Finsupp.mapRange.linearMap, HSMul.hSMul, Eq, DFunLike.coe, Subtype.property, _private.0.Ideal.range_finsuppTotal.match_1