awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
h : RingHom.ker f ≤ I
this_1 : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} J → RingHom.ker f ≤ J
j : Ideal S
hj : map f I ≤ j
hj' this : j.IsPrime
⊢ Membership.mem (γ := Set (Ideal S)) (Set.image.{u_1, u_2} (α := Ideal R) (map f) {J : Ideal R | I ≤ J ∧ J.IsPrime}) j

Tactic:
⟨comap f j, ⟨⟨map_le_iff_le_comap.1 hj, comap_isPrime f j⟩, map_comap_of_surjective f hf j⟩⟩

Premises used: Set.Mem, setOf, Ideal.map_le_iff_le_comap, And.intro, Ideal.comap, Exists.intro, Iff.mp, Ideal.comap_isPrime, Set.image, Ideal.map_comap_of_surjective
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
h : RingHom.ker f ≤ I
this_1 : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} J → RingHom.ker f ≤ J
j : Ideal S
hj : map f I ≤ j
hj' this : j.IsPrime
⊢ Membership.mem (γ := Set (Ideal S)) (Set.image.{u_1, u_2} (α := Ideal R) (map f) {J : Ideal R | I ≤ J ∧ J.IsPrime}) j

Tactic:
exact
      ⟨comap f j, ⟨⟨map_le_iff_le_comap.1 hj, comap_isPrime f j⟩, map_comap_of_surjective f hf j⟩⟩
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} J → RingHom.ker f ≤ J
j : Ideal S
J : Ideal R
hJ : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} J
hJ' : map f J = j
⊢ J.IsPrime

Tactic:
haveI : J.IsPrime := hJ.right
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
h : RingHom.ker f ≤ I
this_1 : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} J → RingHom.ker f ≤ J
j : Ideal S
J : Ideal R
hJ : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} J
hJ' : map f J = j
this : J.IsPrime
⊢ Membership.mem (γ := Set (Ideal S)) {J : Ideal S | map f I ≤ J ∧ J.IsPrime} j

Tactic:
⟨hJ' ▸ map_mono hJ.left, hJ' ▸ map_isPrime_of_surjective hf (le_trans h hJ.left)⟩

Premises used: Set.Mem, setOf, Eq.rec, And.left, And.intro, Ideal.map_isPrime_of_surjective, Ideal.map_mono, le_trans
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
I : Ideal R
h : RingHom.ker f ≤ I
this_1 : ∀ (J : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} J → RingHom.ker f ≤ J
j : Ideal S
J : Ideal R
hJ : Membership.mem (γ := Set (Ideal R)) {J : Ideal R | I ≤ J ∧ J.IsPrime} J
hJ' : map f J = j
this : J.IsPrime
⊢ Membership.mem (γ := Set (Ideal S)) {J : Ideal S | map f I ≤ J ∧ J.IsPrime} j

Tactic:
exact ⟨hJ' ▸ map_mono hJ.left, hJ' ▸ map_isPrime_of_surjective hf (le_trans h hJ.left)⟩
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
rw : Membership.mem (γ := Ideal A) (ker g) (f_inv 1 - 1)
⊢ Eq.{u_3 + 1} (α := C) ((g : (a : A) → C) (f_inv 1) : C) (1 : C)

Tactic:
rw [← map_one g, ← sub_eq_zero, ← map_sub g, ← mem_ker]

Premises used: map_sub, sub_eq_zero, RingHom.mem_ker, map_one
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
a : Membership.mem (γ := Submodule A A) (ker f) (f_inv 1 - 1)
⊢ Membership.mem (γ := Ideal A) (ker g) (f_inv 1 - 1)

Tactic:
apply hg
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
a : Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (f_inv 1) : B) (1 : B)
⊢ Membership.mem (γ := Submodule A A) (ker f) (f_inv 1 - 1)

Tactic:
rw [mem_ker, map_sub f, sub_eq_zero, map_one f]

Premises used: map_sub, sub_eq_zero, RingHom.mem_ker, map_one
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
⊢ Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (f_inv 1) : B) (1 : B)

Tactic:
hf 1

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
⊢ Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) (f_inv 1) : B) (1 : B)

Tactic:
exact hf 1

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
x y : B
rw : Membership.mem (γ := Ideal A) (ker g) (f_inv (x * y) - f_inv x * f_inv y)
⊢ (g : (a : A) → C) (f_inv (x * y)) =
    HMul.hMul (α := C) (β := C) ((g : (a : A) → C) (f_inv x) : C) ((g : (a : A) → C) (f_inv y) : C)

Tactic:
rw [← map_mul g, ← sub_eq_zero, ← map_sub g, ← mem_ker]

Premises used: map_sub, sub_eq_zero, RingHom.mem_ker, map_mul
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
x y : B
a : Membership.mem (γ := Submodule A A) (ker f) (f_inv (x * y) - f_inv x * f_inv y)
⊢ Membership.mem (γ := Ideal A) (ker g) (f_inv (x * y) - f_inv x * f_inv y)

Tactic:
apply hg
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
x y : B
a :
  (f : (a : A) → B) (f_inv (x * y)) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (f_inv x) : B) ((f : (a : A) → B) (f_inv y) : B)
⊢ Membership.mem (γ := Submodule A A) (ker f) (f_inv (x * y) - f_inv x * f_inv y)

Tactic:
rw [mem_ker, map_sub f, sub_eq_zero, map_mul f]

Premises used: map_sub, sub_eq_zero, RingHom.mem_ker, map_mul
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
x y : B
⊢ (f : (a : A) → B) (f_inv (x * y)) =
    HMul.hMul (α := B) (β := B) ((f : (a : A) → B) (f_inv x) : B) ((f : (a : A) → B) (f_inv y) : B)

Tactic:
simp only [hf _]
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
a : A
⊢ Eq.{u_3 + 1} (α := C) ((f.liftOfRightInverseAux f_inv hf g hg : (a : B) → C) ((f : (a : A) → B) a : B) : C)
    ((g : (a : A) → C) a : C)

Tactic:
f.toAddMonoidHom.liftOfRightInverse_comp_apply f_inv hf ⟨g.toAddMonoidHom, hg⟩ a

Premises used: AddMonoidHom.liftOfRightInverse_comp_apply, RingHom.toAddMonoidHom, Subtype.mk
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
φ : B →+* C
x : A
hx : Membership.mem (γ := Submodule A A) (ker f) x
⊢ Eq.{u_3 + 1} (α := C) ((φ.comp f : (a : A) → C) x : C) (0 : C)

Tactic:
simp [mem_ker.mp hx]

Premises used: RingHom.mem_ker, Iff.mp
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }
a :
  ∀ (x : A),
    Eq.{u_3 + 1} (α := C)
      (((↑((fun (φ : B →+* C) ↦
                    (Subtype.mk (p := fun (g : A →+* C) ↦ LE.le (α := Ideal A) (ker f) (ker g)) (φ.comp f) ⋯ :
                      { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }))
                  ((fun (g : { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }) ↦
                      f.liftOfRightInverseAux f_inv hf (↑g : A →+* C) ⋯)
                    g)) :
              A →+* C) :
            (a : A) → C)
          x :
        C)
      (((↑g : A →+* C) : (a : A) → C) x : C)
⊢ (fun (φ : B →+* C) ↦
        (Subtype.mk (p := fun (g : A →+* C) ↦ LE.le (α := Ideal A) (ker f) (ker g)) (φ.comp f) ⋯ :
          { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }))
      ((fun (g : { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }) ↦
          f.liftOfRightInverseAux f_inv hf (↑g : A →+* C) ⋯)
        g) =
    g

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }
x : A
⊢ Eq.{u_3 + 1} (α := C)
    (((↑((fun (φ : B →+* C) ↦
                  (Subtype.mk (p := fun (g : A →+* C) ↦ LE.le (α := Ideal A) (ker f) (ker g)) (φ.comp f) ⋯ :
                    { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }))
                ((fun (g : { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }) ↦
                    f.liftOfRightInverseAux f_inv hf (↑g : A →+* C) ⋯)
                  g)) :
            A →+* C) :
          (a : A) → C)
        x :
      C)
    (((↑g : A →+* C) : (a : A) → C) x : C)

Tactic:
simp only [comp_apply, liftOfRightInverseAux_comp_apply]

Premises used: RingHom.comp_apply, RingHom.liftOfRightInverseAux_comp_apply
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
φ : B →+* C
a :
  ∀ (b : B),
    Eq.{u_3 + 1} (α := C)
      (((fun (g : { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }) ↦
                f.liftOfRightInverseAux f_inv hf (↑g : A →+* C) ⋯)
              ((fun (φ : B →+* C) ↦
                  (Subtype.mk (p := fun (g : A →+* C) ↦ LE.le (α := Ideal A) (ker f) (ker g)) (φ.comp f) ⋯ :
                    { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }))
                φ) :
            (a : B) → C)
          b :
        C)
      ((φ : (a : B) → C) b : C)
⊢ (fun (g : { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }) ↦
        f.liftOfRightInverseAux f_inv hf (↑g : A →+* C) ⋯)
      ((fun (φ : B →+* C) ↦
          (Subtype.mk (p := fun (g : A →+* C) ↦ LE.le (α := Ideal A) (ker f) (ker g)) (φ.comp f) ⋯ :
            { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }))
        φ) =
    φ

Tactic:
ext b
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
φ : B →+* C
b : B
⊢ Eq.{u_3 + 1} (α := C)
    (((fun (g : { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }) ↦
              f.liftOfRightInverseAux f_inv hf (↑g : A →+* C) ⋯)
            ((fun (φ : B →+* C) ↦
                (Subtype.mk (p := fun (g : A →+* C) ↦ LE.le (α := Ideal A) (ker f) (ker g)) (φ.comp f) ⋯ :
                  { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }))
              φ) :
          (a : B) → C)
        b :
      C)
    ((φ : (a : B) → C) b : C)

Tactic:
simp [liftOfRightInverseAux, hf b]

Premises used: RingHom.liftOfRightInverseAux
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }
x : A
⊢ Eq.{u_3 + 1} (α := C)
    ((((f.liftOfRightInverse f_inv hf : (a : { g : A →+* C // ker f ≤ ker g }) → B →+* C) g : B →+* C) : (a : B) → C)
        ((f : (a : A) → B) x : B) :
      C)
    (((↑g : A →+* C) : (a : A) → C) x : C)

Tactic:
f.liftOfRightInverseAux_comp_apply f_inv hf g.1 g.2 x

Premises used: RingHom.liftOfRightInverseAux_comp_apply, Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }
⊢ comp ((f.liftOfRightInverse f_inv hf : (a : { g : A →+* C // ker f ≤ ker g }) → B →+* C) g) f = (↑g : A →+* C)

Tactic:
RingHom.ext <| f.liftOfRightInverse_comp_apply f_inv hf g

Premises used: RingHom.liftOfRightInverse_comp_apply, RingHom.ext
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
h : B →+* C
hh : h.comp f = g
simp_rw :
  h =
    (f.liftOfRightInverse f_inv hf : (a : { g : A →+* C // ker f ≤ ker g }) → B →+* C)
      (Subtype.mk (p := fun (g : A →+* C) ↦ LE.le (α := Ideal A) (ker f) (ker g)) (h.comp f) ⋯)
⊢ h =
    (f.liftOfRightInverse f_inv hf : (a : { g : A →+* C // ker f ≤ ker g }) → B →+* C)
      (Subtype.mk (p := fun (g : A →+* C) ↦ LE.le (α := Ideal A) (ker f) (ker g)) g hg)

Tactic:
simp_rw [← hh]
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
h : B →+* C
hh : h.comp f = g
⊢ h =
    (f.liftOfRightInverse f_inv hf : (a : { g : A →+* C // ker f ≤ ker g }) → B →+* C)
      (Subtype.mk (p := fun (g : A →+* C) ↦ LE.le (α := Ideal A) (ker f) (ker g)) (h.comp f) ⋯)

Tactic:
((f.liftOfRightInverse f_inv hf).apply_symm_apply _).symm

Premises used: Equiv.apply_symm_apply, RingHom.liftOfRightInverse, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
h : B →+* C
hh : h.comp f = g
⊢ h =
    (f.liftOfRightInverse f_inv hf : (a : { g : A →+* C // ker f ≤ ker g }) → B →+* C)
      (Subtype.mk (p := fun (g : A →+* C) ↦ LE.le (α := Ideal A) (ker f) (ker g)) (h.comp f) ⋯)

Tactic:
exact ((f.liftOfRightInverse f_inv hf).apply_symm_apply _).symm

Premises used: Equiv.apply_symm_apply, RingHom.liftOfRightInverse, Eq.symm
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
g : { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }
x : A
⊢ Eq.{u_3 + 1} (α := C)
    ((((f.liftOfSurjective hf : (a : { g : A →+* C // ker f ≤ ker g }) → B →+* C) g : B →+* C) : (a : B) → C)
        ((f : (a : A) → B) x : B) :
      C)
    (((↑g : A →+* C) : (a : A) → C) x : C)

Tactic:
RingHom.liftOfRightInverse_comp_apply f _ _ g x

Premises used: RingHom.liftOfRightInverse_comp_apply
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
g : { g : A →+* C // LE.le (α := Ideal A) (ker f) (ker g) }
⊢ comp ((f.liftOfSurjective hf : (a : { g : A →+* C // ker f ≤ ker g }) → B →+* C) g) f = (↑g : A →+* C)

Tactic:
RingHom.liftOfRightInverse_comp f _ _ g

Premises used: RingHom.liftOfRightInverse_comp
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Ring A
inst_1 : Ring B
inst_2 : Ring C
f : A →+* B
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
g : A →+* C
hg : LE.le (α := Ideal A) (ker f) (ker g)
h : B →+* C
hh : h.comp f = g
⊢ h =
    (f.liftOfSurjective hf : (a : { g : A →+* C // ker f ≤ ker g }) → B →+* C)
      (Subtype.mk (p := fun (g : A →+* C) ↦ LE.le (α := Ideal A) (ker f) (ker g)) g hg)

Tactic:
RingHom.eq_liftOfRightInverse f _ _ g _ _ hh

Premises used: RingHom.eq_liftOfRightInverse
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
e : R ≃+* S
⊢ ∀ {a b : Ideal S},
    LE.le.{u_1} (α := Ideal R)
        (({ toFun := fun (I : Ideal S) ↦ Ideal.comap e I, invFun := fun (I : Ideal R) ↦ Ideal.map e I, left_inv := ⋯,
                right_inv := ⋯ } :
              (a : Ideal S) → Ideal R)
            a :
          Ideal R)
        (({ toFun := fun (I : Ideal S) ↦ Ideal.comap e I, invFun := fun (I : Ideal R) ↦ Ideal.map e I, left_inv := ⋯,
                right_inv := ⋯ } :
              (a : Ideal S) → Ideal R)
            b :
          Ideal R) ↔
      a ≤ b

Tactic:
simp [← Ideal.map_le_iff_le_comap, Ideal.map_comap_of_surjective _ e.surjective]

Premises used: RingEquiv.surjective, Ideal.map_le_iff_le_comap, Ideal.map_comap_of_surjective
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
e : R ≃+* S
I : Ideal R
⊢ Eq.{u_2 + 1} (α := Ideal S) ((e.idealComapOrderIso.symm : (a : Ideal R) → Ideal S) I : Ideal S)
    (Ideal.map e I : Ideal S)

Tactic:
rfl

Premises used: Ideal.map, Submodule.span, rfl
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ Eq (α := Ideal A) (RingHom.ker f) (RingHom.ker (F := A →+* B) (↑f : A →+* B))

Tactic:
rfl

Premises used: RingHomClass.toRingHom, Ideal.comap, rfl, RingHom.ker
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
I : Ideal A
⊢ Eq.{u_3 + 1} (α := Ideal B) (Ideal.map f I) (Ideal.map (F := A →+* B) (↑f : A →+* B) I)

Tactic:
rfl

Premises used: Ideal.map, RingHomClass.toRingHom, rfl
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
C : Type u_4
inst_5 : Semiring C
inst_6 : Algebra R C
f : B →ₐ[R] C
g : A →ₐ[R] B
⊢ Eq (α := Ideal A) (Ideal.comap g (RingHom.ker f)) (RingHom.ker (f.comp g))

Tactic:
RingHom.comap_ker f.toRingHom g.toRingHom

Premises used: RingHom.comap_ker, AlgHom.toRingHom, Ideal.comap, AlgHom.comp, RingHom.ker
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : Algebra R S
I : Ideal R
x y : ↥I
a :
  (↑(((idealMap S I : LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) ↥I ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
            (a : ↥I) → ↥(Ideal.map (algebraMap R S) I))
          (x * y)) :
      S) =
    (↑(HMul.hMul (α := ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) (β :=
          ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))
          (((idealMap S I :
                  LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) ↥I ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
                (a : ↥I) → ↥(Ideal.map (algebraMap R S) I))
              x :
            ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))
          (((idealMap S I :
                  LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) ↥I ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
                (a : ↥I) → ↥(Ideal.map (algebraMap R S) I))
              y :
            ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))) :
      S)
⊢ ((idealMap S I : LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) ↥I ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
        (a : ↥I) → ↥(Ideal.map (algebraMap R S) I))
      (x * y) =
    HMul.hMul (α := ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) (β :=
      ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))
      (((idealMap S I :
              LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) ↥I ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
            (a : ↥I) → ↥(Ideal.map (algebraMap R S) I))
          x :
        ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))
      (((idealMap S I :
              LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) ↥I ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
            (a : ↥I) → ↥(Ideal.map (algebraMap R S) I))
          y :
        ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : Algebra R S
I : Ideal R
x y : ↥I
⊢ (↑(((idealMap S I : LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) ↥I ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
            (a : ↥I) → ↥(Ideal.map (algebraMap R S) I))
          (x * y)) :
      S) =
    (↑(HMul.hMul (α := ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) (β :=
          ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))
          (((idealMap S I :
                  LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) ↥I ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
                (a : ↥I) → ↥(Ideal.map (algebraMap R S) I))
              x :
            ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))
          (((idealMap S I :
                  LinearMap.{u_1, u_1, u_1, u_2} (RingHom.id R) ↥I ↥(Ideal.map (F := R →+* S) (algebraMap R S) I)) :
                (a : ↥I) → ↥(Ideal.map (algebraMap R S) I))
              y :
            ↥(Ideal.map (F := R →+* S) (algebraMap R S) I))) :
      S)

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
h :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) (RingHom.ker (F := R →+* A) (algebraMap R A)) x ↔ Membership.mem (γ := Ideal R) ⊥ x
⊢ Eq (α := Ideal R) (RingHom.ker (F := R →+* A) (algebraMap R A)) ⊥

Tactic:
ext
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
x : R
⊢ Membership.mem (γ := Ideal R) (RingHom.ker (F := R →+* A) (algebraMap R A)) x ↔ Membership.mem (γ := Ideal R) ⊥ x

Tactic:
simp
-- Module: Mathlib.RingTheory.Ideal.Maps
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
I : Ideal R
inst_2 : Submodule.IsPrincipal I
obtain :
  ∀ (x : R) [Submodule.IsPrincipal (M := R) (R ∙ x)], Submodule.IsPrincipal.{u_2, u_2} (R := S) (Ideal.map f (R ∙ x))
⊢ Submodule.IsPrincipal.{u_2, u_2} (R := S) (Ideal.map f I)

Tactic:
obtain ⟨x, rfl⟩ := Submodule.IsPrincipal.principal I

Premises used: Submodule.IsPrincipal.principal, rfl