awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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_1 : F
I_1 J : Ideal R
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
ι : Sort u_3
f : R →+* S
inst_5 : RingHomSurjective f
I : Ideal R
inst_6 : I.IsTwoSided
a b : S
ha : a ∈ Submodule.map f.toSemilinearMap I
⊢ a * b ∈ Submodule.map f.toSemilinearMap I
have obtain : ∀ (a : R) (ha : a ∈ (↑I : Set R)),
  HMul.hMul (α := S) ((f.toSemilinearMap : (a : R) → S) a : S) b ∈ Submodule.map f.toSemilinearMap I
Tactic: obtain ⟨a, ha, rfl⟩ := ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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_1 : F
I_1 J : Ideal R
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
ι : Sort u_3
f : R →+* S
inst_5 : RingHomSurjective f
I : Ideal R
inst_6 : I.IsTwoSided
b : S
a : R
ha : a ∈ (↑I : Set R)
⊢ HMul.hMul (α := S) ((f.toSemilinearMap : (a : R) → S) a : S) b ∈ Submodule.map f.toSemilinearMap I
have obtain : ∀ (b : R),
  HMul.hMul (α := S) (β := S) ((f.toSemilinearMap : (a : R) → S) a : S) ((f : (a : R) → S) b : S) ∈
    Submodule.map f.toSemilinearMap I
Tactic: obtain ⟨b, rfl⟩ := f.surjective b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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_1 : F
I_1 J : Ideal R
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R
inst_4 : RingHomClass F R S
ι : Sort u_3
f : R →+* S
inst_5 : RingHomSurjective f
I : Ideal R
inst_6 : I.IsTwoSided
a : R
ha : a ∈ (↑I : Set R)
b : R
⊢ HMul.hMul (α := S) (β := S) ((f.toSemilinearMap : (a : R) → S) a : S) ((f : (a : R) → S) b : S) ∈
    Submodule.map f.toSemilinearMap I
have rw : Membership.mem (α := S) (Submodule.map f.toSemilinearMap I) ((f : (a : R) → S) (a * b) : S)
Tactic: rw [RingHom.coe_toSemilinearMap, ← map_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
⊢ IsMaximal (comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I)
have refine : ∀ (J : Ideal ((i : ι) → R i)) (x : (i : ι) → R i) (le : comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I ≤ J)
  (hxI : x ∉ comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I) (hxJ : x ∈ J), 1 ∈ J
Tactic: refine isMaximal_iff.mpr ⟨I.ne_top_iff_one.mp h.ne_top, fun J x le hxI hxJ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I
hxJ : x ∈ J
⊢ 1 ∈ J
have have : ∀ (r y : R i) (hy : y ∈ I)
  (eq : HMul.hMul (β := R i) r ((Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) x : R i) + y = 1), 1 ∈ J
Tactic: have ⟨r, y, hy, eq⟩ := h.exists_inv hxI
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : HMul.hMul (β := R i) r ((Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) x : R i) + y = 1
⊢ 1 ∈ J
have h₁ : 1 = update (β := R) 0 i r * x + update (β := R) 1 i y
Tactic: convert!
    J.add_mem (J.mul_mem_left (update 0 i r) hxJ) (b := update 1 i y)
      (le <| by apply update_self i y 1 ▸ hy)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : HMul.hMul (β := R i) r ((Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) x : R i) + y = 1
⊢ 1 = update (β := R) 0 i r * x + update (β := R) 1 i y
have h₁ : ∀ (j : ι), 1 j = (update (β := R) 0 i r * x + update (β := R) 1 i y) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : HMul.hMul (β := R i) r ((Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) x : R i) + y = 1
j : ι
⊢ 1 j = (update (β := R) 0 i r * x + update (β := R) 1 i y) j
have h₁ : ∀ {I : Ideal (R j)} (h : I.IsMaximal) (le : comap (F := ((i : ι) → R i) →+* R j) (Pi.evalRingHom R j) I ≤ J)
  (hxI : x ∉ comap (F := ((i : ι) → R i) →+* R j) (Pi.evalRingHom R j) I) (r y : R j) (hy : y ∈ I)
  (eq : HMul.hMul (β := R j) r ((Pi.evalRingHom R j : (a : (i : ι) → R i) → R j) x : R j) + y = 1),
  1 j = (update (β := R) 0 j r * x + update (β := R) 1 j y) j
Tactic: obtain rfl | ne := eq_or_ne j i
Cleared hypotheses: i, I, h, le, hxI, r, y, hy, eq
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : HMul.hMul (β := R i) r ((Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) x : R i) + y = 1
j : ι
h₁ :
  ∀ {I : Ideal (R j)} (h : I.IsMaximal) (le : comap (F := ((i : ι) → R i) →+* R j) (Pi.evalRingHom R j) I ≤ J)
    (hxI : x ∉ comap (F := ((i : ι) → R i) →+* R j) (Pi.evalRingHom R j) I) (r y : R j) (hy : y ∈ I)
    (eq : HMul.hMul (β := R j) r ((Pi.evalRingHom R j : (a : (i : ι) → R i) → R j) x : R j) + y = 1),
    1 j = (update (β := R) 0 j r * x + update (β := R) 1 j y) j
⊢ 1 j = (update (β := R) 0 i r * x + update (β := R) 1 i y) j
have h₂ : ∀ (ne : j ≠ i), 1 j = (update (β := R) 0 i r * x + update (β := R) 1 i y) j
Tactic: obtain rfl | ne := eq_or_ne j i
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : HMul.hMul (β := R i) r ((Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) x : R i) + y = 1
⊢ 1 ∈ J
have h₁ : 1 = update (β := R) 0 i r * x + update (β := R) 1 i y
Tactic: classical
  convert!
    J.add_mem (J.mul_mem_left (update 0 i r) hxJ) (b := update 1 i y)
      (le <| by apply update_self i y 1 ▸ hy)
  ext j
  obtain rfl | ne := eq_or_ne j i
  · simpa [eq_comm] using eq
  · simp [update_of_ne ne]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : HMul.hMul (β := R i) r ((Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) x : R i) + y = 1
h₁ : 1 = update (β := R) 0 i r * x + update (β := R) 1 i y
⊢ 1 ∈ J
have h₂ : ∀ (j : ι), 1 j = (update (β := R) 0 i r * x + update (β := R) 1 i y) j
Tactic: classical
  convert!
    J.add_mem (J.mul_mem_left (update 0 i r) hxJ) (b := update 1 i y)
      (le <| by apply update_self i y 1 ▸ hy)
  ext j
  obtain rfl | ne := eq_or_ne j i
  · simpa [eq_comm] using eq
  · simp [update_of_ne ne]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : HMul.hMul (β := R i) r ((Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) x : R i) + y = 1
h₁ : 1 = update (β := R) 0 i r * x + update (β := R) 1 i y
h₂ : ∀ (j : ι), 1 j = (update (β := R) 0 i r * x + update (β := R) 1 i y) j
⊢ 1 ∈ J
have h₃ : ∀ (j : ι) {I : Ideal (R j)} (h : I.IsMaximal) (le : comap (F := ((i : ι) → R i) →+* R j) (Pi.evalRingHom R j) I ≤ J)
  (hxI : x ∉ comap (F := ((i : ι) → R i) →+* R j) (Pi.evalRingHom R j) I) (r y : R j) (hy : y ∈ I)
  (eq : HMul.hMul (β := R j) r ((Pi.evalRingHom R j : (a : (i : ι) → R i) → R j) x : R j) + y = 1),
  1 j = (update (β := R) 0 j r * x + update (β := R) 1 j y) j
Tactic: classical
  convert!
    J.add_mem (J.mul_mem_left (update 0 i r) hxJ) (b := update 1 i y)
      (le <| by apply update_self i y 1 ▸ hy)
  ext j
  obtain rfl | ne := eq_or_ne j i
  · simpa [eq_comm] using eq
  · simp [update_of_ne ne]
Cleared hypotheses: i, I, h, le, hxI, r, y, hy, eq
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : HMul.hMul (β := R i) r ((Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) x : R i) + y = 1
h₁ : 1 = update (β := R) 0 i r * x + update (β := R) 1 i y
h₂ : ∀ (j : ι), 1 j = (update (β := R) 0 i r * x + update (β := R) 1 i y) j
h₃ :
  ∀ (j : ι) {I : Ideal (R j)} (h : I.IsMaximal) (le : comap (F := ((i : ι) → R i) →+* R j) (Pi.evalRingHom R j) I ≤ J)
    (hxI : x ∉ comap (F := ((i : ι) → R i) →+* R j) (Pi.evalRingHom R j) I) (r y : R j) (hy : y ∈ I)
    (eq : HMul.hMul (β := R j) r ((Pi.evalRingHom R j : (a : (i : ι) → R i) → R j) x : R j) + y = 1),
    1 j = (update (β := R) 0 j r * x + update (β := R) 1 j y) j
⊢ 1 ∈ J
have h₄ : ∀ (j : ι) (ne : j ≠ i), 1 j = (update (β := R) 0 i r * x + update (β := R) 1 i y) j
Tactic: classical
  convert!
    J.add_mem (J.mul_mem_left (update 0 i r) hxJ) (b := update 1 i y)
      (le <| by apply update_self i y 1 ▸ hy)
  ext j
  obtain rfl | ne := eq_or_ne j i
  · simpa [eq_comm] using eq
  · simp [update_of_ne ne]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
⊢ map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) (pi (R := R) I) = I i
have h : ∀ (r : R i),
  Membership.mem (γ := Ideal (R i)) (map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) (pi (R := R) I)) r ↔
    r ∈ I i
Tactic: ext r
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
r : R i
⊢ Membership.mem (γ := Ideal (R i)) (map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) (pi (R := R) I)) r ↔
    r ∈ I i
have h : (∃ x ∈ pi (R := R) I, (Pi.evalRingHom R i : (a : (x : ι) → R x) → R i) x = r) ↔ r ∈ I i
Tactic: rw [mem_map_iff_of_surjective (Pi.evalRingHom R i) (Function.surjective_eval _)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
r : R i
⊢ (∃ x ∈ pi (R := R) I, (Pi.evalRingHom R i : (a : (x : ι) → R x) → R i) x = r) ↔ r ∈ I i
have h : (∃ x ∈ pi (R := R) I, (Pi.evalRingHom R i : (a : (x : ι) → R x) → R i) x = r) → r ∈ I i
Tactic: refine ⟨?_, fun hr ↦ ⟨_, single_mem_pi hr, by simp⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
r : R i
⊢ (∃ x ∈ pi (R := R) I, (Pi.evalRingHom R i : (a : (x : ι) → R x) → R i) x = r) ↔ r ∈ I i
have h : (∃ x ∈ pi (R := R) I, (Pi.evalRingHom R i : (a : (x : ι) → R x) → R i) x = r) → r ∈ I i
Tactic: classical refine ⟨?_, fun hr ↦ ⟨_, single_mem_pi hr, by simp⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R_1 : Type u
S : Type v
F : Type u_1
inst : Semiring R_1
inst_1 : Semiring S
inst_2 : FunLike F R_1 S
f : F
I_1 J : Ideal R_1
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R_1
inst_4 : RingHomClass F R_1 S
ι_1 : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst_5 : (i : ι) → Semiring (R i)
inst_6 : Finite ι
I : Ideal ((i : ι) → R i)
⊢ pi (R := R)
      ((fun (I : Ideal ((i : ι) → R i)) (i : ι) ↦
          (map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I : Ideal (R i)))
        I) =
    I
have h : ∀ (r : (i : ι) → R i),
  Membership.mem (γ := Ideal ((i : ι) → R i))
      (pi (R := R)
        ((fun (I : Ideal ((i : ι) → R i)) (i : ι) ↦
            (map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I : Ideal (R i)))
          I))
      r ↔
    r ∈ I
Tactic: ext r
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R_1 : Type u
S : Type v
F : Type u_1
inst : Semiring R_1
inst_1 : Semiring S
inst_2 : FunLike F R_1 S
f : F
I_1 J : Ideal R_1
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R_1
inst_4 : RingHomClass F R_1 S
ι_1 : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst_5 : (i : ι) → Semiring (R i)
inst_6 : Finite ι
I : Ideal ((i : ι) → R i)
r : (i : ι) → R i
⊢ Membership.mem (γ := Ideal ((i : ι) → R i))
      (pi (R := R)
        ((fun (I : Ideal ((i : ι) → R i)) (i : ι) ↦
            (map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) I : Ideal (R i)))
          I))
      r ↔
    r ∈ I
have h : (∀ (i : ι), ∃ x ∈ I, (Pi.evalRingHom R i : (a : (x : ι) → R x) → R i) x = r i) ↔ r ∈ I
Tactic: simp_rw [mem_pi, mem_map_iff_of_surjective (Pi.evalRingHom R _) (Function.surjective_eval _)]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R_1 : Type u
S : Type v
F : Type u_1
inst : Semiring R_1
inst_1 : Semiring S
inst_2 : FunLike F R_1 S
f : F
I_1 J : Ideal R_1
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R_1
inst_4 : RingHomClass F R_1 S
ι_1 : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst_5 : (i : ι) → Semiring (R i)
inst_6 : Finite ι
I : Ideal ((i : ι) → R i)
r : (i : ι) → R i
⊢ (∀ (i : ι), ∃ x ∈ I, (Pi.evalRingHom R i : (a : (x : ι) → R x) → R i) x = r i) ↔ r ∈ I
have h : (∃ (f : (x x : ι) → R x), ∀ (x : ι), f x ∈ I ∧ (Pi.evalRingHom R x : (a : (x : ι) → R x) → R x) (f x) = r x) →
  ∀ (r' : (x x : ι) → R x) (hr' : ∀ (x : ι), r' x ∈ I ∧ (Pi.evalRingHom R x : (a : (x : ι) → R x) → R x) (r' x) = r x),
    r ∈ I
Tactic: refine ⟨(fun ⟨r', hr'⟩ ↦ ?_) ∘ Classical.skolem.mp, fun hr i ↦ ⟨r, hr, rfl⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R_1 : Type u
S : Type v
F : Type u_1
inst : Semiring R_1
inst_1 : Semiring S
inst_2 : FunLike F R_1 S
f : F
I_1 J : Ideal R_1
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R_1
inst_4 : RingHomClass F R_1 S
ι_1 : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst_5 : (i : ι) → Semiring (R i)
inst_6 : Finite ι
I : Ideal ((i : ι) → R i)
r : (i : ι) → R i
h : ∃ (f : (x x : ι) → R x), ∀ (x : ι), f x ∈ I ∧ (Pi.evalRingHom R x : (a : (x : ι) → R x) → R x) (f x) = r x
r' : (x x : ι) → R x
hr' : ∀ (x : ι), r' x ∈ I ∧ (Pi.evalRingHom R x : (a : (x : ι) → R x) → R x) (r' x) = r x
⊢ r ∈ I
have h : ∀ (this : Fintype ι), r ∈ I
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R_1 : Type u
S : Type v
F : Type u_1
inst : Semiring R_1
inst_1 : Semiring S
inst_2 : FunLike F R_1 S
f : F
I_1 J : Ideal R_1
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R_1
inst_4 : RingHomClass F R_1 S
ι_1 : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst_5 : (i : ι) → Semiring (R i)
inst_6 : Finite ι
I : Ideal ((i : ι) → R i)
r : (i : ι) → R i
h : ∃ (f : (x x : ι) → R x), ∀ (x : ι), f x ∈ I ∧ (Pi.evalRingHom R x : (a : (x : ι) → R x) → R x) (f x) = r x
r' : (x x : ι) → R x
hr' : ∀ (x : ι), r' x ∈ I ∧ (Pi.evalRingHom R x : (a : (x : ι) → R x) → R x) (r' x) = r x
this : Fintype ι
i : ι
⊢ r i = (∑ i : ι, Pi.single (M := R) i 1 * r' i) i
have rw : (Pi.evalRingHom R i : (a : (x : ι) → R x) → R i) (r' i) =
  HMul.hMul (α := (j : ι) → R j) (Pi.single (M := R) i 1) (r' i) i
Tactic: rw [← (hr' _).2, Finset.sum_apply, Fintype.sum_eq_single i fun j ne ↦ by simp [ne]]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R_1 : Type u
S : Type v
F : Type u_1
inst : Semiring R_1
inst_1 : Semiring S
inst_2 : FunLike F R_1 S
f : F
I_1 J : Ideal R_1
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R_1
inst_4 : RingHomClass F R_1 S
ι_1 : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst_5 : (i : ι) → Semiring (R i)
inst_6 : Finite ι
I : Ideal ((i : ι) → R i)
r : (i : ι) → R i
h : ∃ (f : (x x : ι) → R x), ∀ (x : ι), f x ∈ I ∧ (Pi.evalRingHom R x : (a : (x : ι) → R x) → R x) (f x) = r x
r' : (x x : ι) → R x
hr' : ∀ (x : ι), r' x ∈ I ∧ (Pi.evalRingHom R x : (a : (x : ι) → R x) → R x) (r' x) = r x
this : Fintype ι
⊢ r ∈ I
have h : ∑ i : ι, Pi.single (M := R) i 1 * r' i ∈ I
Tactic: rw [show r = ∑ i, Pi.single i 1 * r' i from funext fun i ↦ by
      rw [← (hr' _).2, Finset.sum_apply, Fintype.sum_eq_single i fun j ne ↦ by simp [ne]]; simp]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R_1 : Type u
S : Type v
F : Type u_1
inst : Semiring R_1
inst_1 : Semiring S
inst_2 : FunLike F R_1 S
f : F
I_1 J : Ideal R_1
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R_1
inst_4 : RingHomClass F R_1 S
ι_1 : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst_5 : (i : ι) → Semiring (R i)
inst_6 : Finite ι
I : Ideal ((i : ι) → R i)
r : (i : ι) → R i
h : ∃ (f : (x x : ι) → R x), ∀ (x : ι), f x ∈ I ∧ (Pi.evalRingHom R x : (a : (x : ι) → R x) → R x) (f x) = r x
r' : (x x : ι) → R x
hr' : ∀ (x : ι), r' x ∈ I ∧ (Pi.evalRingHom R x : (a : (x : ι) → R x) → R x) (r' x) = r x
this : Fintype ι
⊢ r ∈ I
have h : ∑ i : ι, Pi.single (M := R) i 1 * r' i ∈ I
Tactic: classical rw [show r = ∑ i, Pi.single i 1 * r' i from funext fun i ↦ by
      rw [← (hr' _).2, Finset.sum_apply, Fintype.sum_eq_single i fun j ne ↦ by simp [ne]]; simp]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R_1 : Type u
S : Type v
F : Type u_1
inst : Semiring R_1
inst_1 : Semiring S
inst_2 : FunLike F R_1 S
f : F
I_1 J : Ideal R_1
K L : Ideal S
G : Type u_2
inst_3 : FunLike G S R_1
inst_4 : RingHomClass F R_1 S
ι_1 : Sort u_3
ι : Type u_4
R : ι → Type u_5
inst_5 : (i : ι) → Semiring (R i)
inst_6 : Finite ι
inst_7 : ∀ (i : ι), IsPrincipalIdealRing.{u_5} (R i)
I : Ideal ((i : ι) → R i)
⊢ Submodule.IsPrincipal I
have rw : Submodule.IsPrincipal (R := (i : ι) → R i) (M := (i : ι) → R i)
  ((OrderIso.symm (piOrderIso (R := R)) : (a : (i : ι) → Ideal (R i)) → Ideal ((i : ι) → R i))
    ((piOrderIso (R := R) : (a : Ideal ((i : ι) → R i)) → (i : ι) → Ideal (R i)) I))
Tactic: rw [← piOrderIso.symm_apply_apply I]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
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 : Ideal R
inst_3 : RingHomClass F R S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ comap f ⊥ ≤ I
have refine : ∀ (x : R) (hx : Membership.mem (γ := Submodule R R) (comap f ⊥) x), Membership.mem (γ := Submodule R R) ⊥ x
Tactic: refine le_trans (fun x hx => ?_) bot_le
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (hypothesis)
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 : Ideal R
inst_3 : RingHomClass F R S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : R
hx : Membership.mem (γ := Submodule R R) (comap f ⊥) x
⊢ Membership.mem (γ := Submodule R R) ⊥ x
have hx₁ : Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) 0 : S)
Tactic: rw [mem_comap, Submodule.mem_bot, ← map_zero f] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
⊢ map (R := S) (F := S →+* R) (↑f.symm : S →+* R) (map (F := R →+* S) (↑f : R →+* S) I) = I
have rw : map (R := S) f.symm.toRingHom (map (F := R →+* S) (↑f : R →+* S) I) = I
Tactic: rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, map_map,
    RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, map_id]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
rw : map (R := S) f.symm.toRingHom (map (F := R →+* S) (↑f : R →+* S) I) = I
⊢ map (R := S) (F := S →+* R) (↑f.symm : S →+* R) (map (F := R →+* S) (↑f : R →+* S) I) = I
have rw₁ : map (R := S) f.symm.toRingHom (map f.toRingHom I) = I
Tactic: rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, map_map,
    RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, map_id]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
rw : map (R := S) f.symm.toRingHom (map (F := R →+* S) (↑f : R →+* S) I) = I
rw₁ : map (R := S) f.symm.toRingHom (map f.toRingHom I) = I
⊢ map (R := S) (F := S →+* R) (↑f.symm : S →+* R) (map (F := R →+* S) (↑f : R →+* S) I) = I
have rw₂ : map (f.symm.toRingHom.comp f.toRingHom) I = I
Tactic: rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, map_map,
    RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, map_id]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
rw : map (R := S) f.symm.toRingHom (map (F := R →+* S) (↑f : R →+* S) I) = I
rw₁ : map (R := S) f.symm.toRingHom (map f.toRingHom I) = I
rw₂ : map (f.symm.toRingHom.comp f.toRingHom) I = I
⊢ map (R := S) (F := S →+* R) (↑f.symm : S →+* R) (map (F := R →+* S) (↑f : R →+* S) I) = I
have rw₃ : map (F := R →+* R) (RingHom.comp (↑f.symm : S →+* R) f.toRingHom) I = I
Tactic: rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, map_map,
    RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, map_id]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
rw : map (R := S) f.symm.toRingHom (map (F := R →+* S) (↑f : R →+* S) I) = I
rw₁ : map (R := S) f.symm.toRingHom (map f.toRingHom I) = I
rw₂ : map (f.symm.toRingHom.comp f.toRingHom) I = I
rw₃ : map (F := R →+* R) (RingHom.comp (↑f.symm : S →+* R) f.toRingHom) I = I
⊢ map (R := S) (F := S →+* R) (↑f.symm : S →+* R) (map (F := R →+* S) (↑f : R →+* S) I) = I
have rw₄ : map (F := R →+* R) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.symm : S →+* R) (↑f : R →+* S)) I = I
Tactic: rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, map_map,
    RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, map_id]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.Maps (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
rw : map (R := S) f.symm.toRingHom (map (F := R →+* S) (↑f : R →+* S) I) = I
rw₁ : map (R := S) f.symm.toRingHom (map f.toRingHom I) = I
rw₂ : map (f.symm.toRingHom.comp f.toRingHom) I = I
rw₃ : map (F := R →+* R) (RingHom.comp (↑f.symm : S →+* R) f.toRingHom) I = I
rw₄ : map (F := R →+* R) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.symm : S →+* R) (↑f : R →+* S)) I = I
⊢ map (R := S) (F := S →+* R) (↑f.symm : S →+* R) (map (F := R →+* S) (↑f : R →+* S) I) = I
have rw₅ : map (F := R →+* R) (RingHom.id R) I = I
Tactic: rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, map_map,
    RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, map_id]