awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
hf : Function.Surjective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
H : I.IsMaximal
⊢ Eq.{v + 1} (α := Ideal S) (map f I) ⊤ ∨ IsMaximal.{v} (α := S) (map f I)

Tactic:
or_iff_not_imp_left.2 fun ne_top ↦ ⟨⟨ne_top, fun _J hJ ↦ comap_injective_of_surjective f hf <|
    H.1.2 _ (le_comap_map.trans_lt <| (orderEmbeddingOfSurjective f hf).strictMono hJ)⟩⟩

Premises used: Iff.mpr, Ideal.orderEmbeddingOfSurjective, OrderEmbedding.strictMono, Ideal.IsMaximal.mk, And.right, Ideal.IsMaximal.out, Classical.or_iff_not_imp_left, And.intro, Ideal.le_comap_map, Ideal.comap, LE.le.trans_lt, Ideal.comap_injective_of_surjective
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
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
⊢ map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) (pi (R := R) I) = I i

Tactic:
ext r
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
r : R i
h : (∃ x ∈ pi (R := R) I, (Pi.evalRingHom R i : (a : (x : ι) → R x) → R i) x = r) ↔ r ∈ I 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:
rw [mem_map_iff_of_surjective (Pi.evalRingHom R i) (Function.surjective_eval _)]

Premises used: Function.surjective_eval, Pi.evalRingHom, Ideal.mem_map_iff_of_surjective
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
r : R i
hr : r ∈ I i
⊢ (Pi.evalRingHom R i : (a : (x : ι) → R x) → R i) (Pi.single (M := R) i r) = r

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
r : R i
h : (∃ x ∈ pi (R := R) I, (Pi.evalRingHom R i : (a : (x : ι) → R x) → R i) x = r) → r ∈ I i
⊢ (∃ 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⟩⟩
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
r : R i
h : (∃ x ∈ pi (R := R) I, (Pi.evalRingHom R i : (a : (x : ι) → R x) → R i) x = r) → r ∈ I i
⊢ (∃ 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⟩⟩
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
r : (x : ι) → R x
hr : r ∈ pi (R := R) I
⊢ Membership.mem (α := R i) (I i) ((Pi.evalRingHom R i : (a : (x : ι) → R x) → R i) r : R i)

Tactic:
hr i

Premises used: Set.Mem
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
ι : Type u_4
R : ι → Type u_5
inst : (i : ι) → Semiring (R i)
I : (i : ι) → Ideal (R i)
i : ι
r : (x : ι) → R x
hr : r ∈ pi (R := R) I
⊢ Membership.mem (α := R i) (I i) ((Pi.evalRingHom R i : (a : (x : ι) → R x) → R i) r : R i)

Tactic:
exact hr i
-- Module: Mathlib.RingTheory.Ideal.Maps
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)
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
⊢ 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

Tactic:
ext r
-- Module: Mathlib.RingTheory.Ideal.Maps
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 : (∀ (i : ι), ∃ x ∈ I, (Pi.evalRingHom R i : (a : (x : ι) → R x) → R i) x = 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:
simp_rw [mem_pi, mem_map_iff_of_surjective (Pi.evalRingHom R _) (Function.surjective_eval _)]

Premises used: Function.surjective_eval, Pi.evalRingHom, Ideal.mem_map_iff_of_surjective, Ideal.mem_pi
-- Module: Mathlib.RingTheory.Ideal.Maps
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

Tactic:
⟨(fun ⟨r', hr'⟩ ↦ ?_) ∘ Classical.skolem.mp, fun hr i ↦ ⟨r, hr, rfl⟩⟩

Premises used: Classical.skolem, Function.comp, And.intro, Iff.intro, Exists.intro, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Ideal.Maps
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
⊢ (∀ (i : ι), ∃ x ∈ I, (Pi.evalRingHom R i : (a : (x : ι) → R x) → R i) x = r i) ↔ r ∈ I

Tactic:
refine ⟨(fun ⟨r', hr'⟩ ↦ ?_) ∘ Classical.skolem.mp, fun hr i ↦ ⟨r, hr, rfl⟩⟩
-- Module: Mathlib.RingTheory.Ideal.Maps
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_1 : ∃ (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
h : ∀ (this : Fintype ι), r ∈ I
⊢ r ∈ I

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.RingTheory.Ideal.Maps
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 j : ι
ne : j ≠ i
⊢ HMul.hMul (α := (j : ι) → R j) (Pi.single (M := R) j 1) (r' j) i = 0

Tactic:
simp [ne]
-- Module: Mathlib.RingTheory.Ideal.Maps
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 : ι
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
⊢ r i = (∑ i : ι, 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]]

Premises used: Finset.sum_apply, And.right, Fintype.sum_eq_single
-- Module: Mathlib.RingTheory.Ideal.Maps
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 : ι
⊢ (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:
simp
-- Module: Mathlib.RingTheory.Ideal.Maps
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_1 : ∃ (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 ι
h : ∑ i : ι, Pi.single (M := R) i 1 * r' i ∈ I
⊢ r ∈ 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]

Premises used: funext
-- Module: Mathlib.RingTheory.Ideal.Maps
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_1 : ∃ (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 ι
h : ∑ i : ι, Pi.single (M := R) i 1 * r' i ∈ I
⊢ r ∈ 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]

Premises used: funext
-- Module: Mathlib.RingTheory.Ideal.Maps
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 : ι, Pi.single (M := R) i 1 * r' i ∈ I

Tactic:
sum_mem fun i _ ↦ I.mul_mem_left _ (hr' i).1

Premises used: Pi.single, And.left, Ideal.mul_mem_left, OfNat.ofNat, sum_mem
-- Module: Mathlib.RingTheory.Ideal.Maps
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 : ι, Pi.single (M := R) i 1 * r' i ∈ I

Tactic:
exact sum_mem fun i _ ↦ I.mul_mem_left _ (hr' i).1

Premises used: And.left, Ideal.mul_mem_left, sum_mem
-- Module: Mathlib.RingTheory.Ideal.Maps
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)
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))
⊢ Submodule.IsPrincipal I

Tactic:
rw [← piOrderIso.symm_apply_apply I]

Premises used: OrderIso.symm_apply_apply, Ideal.piOrderIso
-- Module: Mathlib.RingTheory.Ideal.Maps
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 (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:
⟨_, congr(pi $(funext fun i ↦
      (Submodule.IsPrincipal.span_singleton_generator _).symm)).trans pi_span⟩

Premises used: congrArg, id, Ideal.pi_span, funext, Submodule.IsPrincipal.mk, Ideal.pi, Exists.intro, Submodule.IsPrincipal.span_singleton_generator, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.Ideal.Maps
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 (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:
exact ⟨_, congr(pi $(funext fun i ↦
      (Submodule.IsPrincipal.span_singleton_generator _).symm)).trans pi_span⟩
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I : Ideal R
inst_3 : RingHomClass F R S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ comap f ⊥ ≤ I

Tactic:
le_trans (fun x hx => ?_) bot_le

Premises used: bot_le, le_trans
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I : Ideal R
inst_3 : RingHomClass F R S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
refine : ∀ (x : R) (hx : Membership.mem (γ := Submodule R R) (comap f ⊥) x), Membership.mem (γ := Submodule R R) ⊥ x
⊢ comap f ⊥ ≤ I

Tactic:
refine le_trans (fun x hx => ?_) bot_le

Premises used: bot_le, le_trans
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I : 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
⊢ 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

Premises used: Submodule.mem_bot, map_zero, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I : Ideal R
inst_3 : RingHomClass F R S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : R
hx : Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) 0 : S)
⊢ Membership.mem (γ := Submodule R R) ⊥ x

Tactic:
Eq.symm (hf hx) ▸ Submodule.zero_mem ⊥

Premises used: Eq.rec, Bot.bot, Submodule.zero_mem, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
I : Ideal R
inst_3 : RingHomClass F R S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : R
hx : Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) 0 : S)
⊢ Membership.mem (γ := Submodule R R) ⊥ x

Tactic:
exact Eq.symm (hf hx) ▸ Submodule.zero_mem ⊥
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
F : Type u_1
inst : Semiring R
inst_1 : Semiring S
inst_2 : FunLike F R S
f : F
inst_3 : RingHomClass F R S
hf : Function.Injective.{u + 1, v + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Eq (α := Ideal R) (comap f ⊥) ⊥

Tactic:
le_bot_iff.mp (Ideal.comap_bot_le_of_injective f hf)

Premises used: le_bot_iff, Ideal.comap_bot_le_of_injective, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Maps
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
rw₅ : map (F := R →+* R) (RingHom.id R) I = I
rw₆ rw₇ : I = I
⊢ map (R := S) (F := S →+* R) (↑f.symm : S →+* R) (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]

Premises used: Ideal.map_id, Ideal.map_map, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
rw : comap f.toRingHom (comap (F := S →+* R) (↑f.symm : S →+* R) I) = I
rw₁ : comap f.toRingHom (comap f.symm.toRingHom I) = I
rw₂ : comap (f.symm.toRingHom.comp f.toRingHom) I = I
rw₃ : comap (F := R →+* R) (RingHom.comp (↑f.symm : S →+* R) f.toRingHom) I = I
rw₄ :
  comap (F := R →+* R) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑f.symm : S →+* R) (↑f : R →+* S)) I = I
rw₅ : comap (F := R →+* R) (RingHom.id R) I = I
rw₆ rw₇ : I = I
⊢ comap (F := R →+* S) (↑f : R →+* S) (comap (F := S →+* R) (↑f.symm : S →+* R) I) = I

Tactic:
rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, comap_comap,
    RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, comap_id]

Premises used: RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, Ideal.comap_id, Ideal.comap_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
⊢ Eq (α := Ideal S) (map (F := R →+* S) (↑f : R →+* S) I) (comap f.symm I)

Tactic:
le_antisymm (Ideal.map_le_comap_of_inverse _ _ _ (Equiv.left_inv' _))
    (Ideal.comap_le_map_of_inverse _ _ _ (Equiv.right_inv' _))

Premises used: Equiv.left_inv', Ideal.comap_le_map_of_inverse, Equiv.right_inv', Ideal.map_le_comap_of_inverse, le_antisymm
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
⊢ Eq (α := Ideal S) (comap f.symm I) (map f I)

Tactic:
(map_comap_of_equiv f).symm

Premises used: Ideal.map, RingHomClass.toRingHom, Ideal.map_comap_of_equiv, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal S
f : R ≃+* S
⊢ Eq (α := Ideal R) (map f.symm I) (comap f I)

Tactic:
map_comap_of_equiv (RingEquiv.symm f)

Premises used: Ideal.map, Ideal.map_comap_of_equiv, Equiv.symm, RingEquiv.symm
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
y : S
rw : Membership.mem (α := R) I ((f.symm : (a : S) → R) y : R) ↔ Membership.mem (γ := Ideal S) (comap f.symm I) y
rw₁ rw₂ :
  Membership.mem (α := R) I ((f.symm : (a : S) → R) y : R) ↔ Membership.mem (α := R) I ((f.symm : (a : S) → R) y : R)
⊢ Membership.mem (α := R) I ((f.symm : (a : S) → R) y : R) ↔ Membership.mem (γ := Ideal S) (map f I) y

Tactic:
rw [← comap_symm, mem_comap]

Premises used: Ideal.comap_symm, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
I : Ideal R
f : R ≃+* S
x : R
rw : Membership.mem (α := S) (γ := Ideal S) (comap f.symm I) ((f : (a : R) → S) x : S) ↔ x ∈ I
rw₁ : Membership.mem (α := R) I ((f.symm : (a : S) → R) ((f : (a : R) → S) x : S) : R) ↔ x ∈ I
rw₂ rw₃ : x ∈ I ↔ x ∈ I
⊢ Membership.mem.{v, v} (α := S) (γ := Ideal S) (map f I) ((f : (a : R) → S) x : S) ↔ x ∈ I

Tactic:
rw [← comap_symm, Ideal.mem_comap, f.symm_apply_apply]

Premises used: Ideal.comap_symm, RingEquiv.symm_apply_apply, Ideal.mem_comap
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
E : Type u_4
inst_2 : EquivLike E R S
inst_3 : RingEquivClass E R S
e : E
I : Ideal R
y : S
mp : Membership.mem (γ := Ideal S) (map e I) y → ∃ x ∈ I, (e : (a : R) → S) x = y
mpr : (∃ x ∈ I, (e : (a : R) → S) x = y) → Membership.mem (γ := Ideal S) (map e I) y
⊢ Membership.mem (γ := Ideal S) (map e I) y ↔ ∃ x ∈ I, (e : (a : R) → S) x = y

Tactic:
constructor
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
E : Type u_4
inst_2 : EquivLike E R S
inst_3 : RingEquivClass E R S
e : E
I : Ideal R
y : S
h : Membership.mem (γ := Ideal S) (map e I) y
⊢ Membership.mem (γ := Ideal S) (comap (F := S ≃+* R) (RingEquiv.symm (↑e : R ≃+* S)) I) y

Tactic:
simp_rw [show map e I = _ from map_comap_of_equiv (RingEquivClass.toRingEquiv e : R ≃+* S)] at h

Premises used: RingEquivClass.toRingEquiv, Ideal.map_comap_of_equiv
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
E : Type u_4
inst_2 : EquivLike E R S
inst_3 : RingEquivClass E R S
e : E
I : Ideal R
y : S
h : Membership.mem (γ := Ideal S) (comap (F := S ≃+* R) (RingEquiv.symm (↑e : R ≃+* S)) I) y
⊢ ∃ x ∈ I, (e : (a : R) → S) x = y

Tactic:
⟨(EquivLike.toEquiv e).symm y, h, (EquivLike.toEquiv e).apply_symm_apply y⟩

Premises used: Equiv.apply_symm_apply, And.intro, Exists.intro, Equiv.symm, DFunLike.coe, EquivLike.toEquiv