awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₂ : (a : R) → R → Prop) a b
H' : Membership.mem (γ := Set R) {x : R | (t₂ : (a : R) → R → Prop) x 0} (a - b)
⊢ (t₁ : (a : R) → R → Prop) a b
have H'₁ : Membership.mem (γ := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0} (a - b)
Tactic: rw [← h] at H'
Cleared hypotheses: H'
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₂ : (a : R) → R → Prop) a b
H' :
  Membership.mem (γ := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0} (a - b)
⊢ (t₁ : (a : R) → R → Prop) a b
have h₁ : a = a - b + b
Tactic: convert! t₁.add H' (t₁.refl b) using 1
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h :
  Eq.{u_1 + 1} (α := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
    {x : R | ({ ringCon := t₂ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0}
a b : R
H : (t₂ : (a : R) → R → Prop) a b
H' :
  Membership.mem (γ := Set R) {x : R | ({ ringCon := t₁ : TwoSidedIdeal R }.ringCon : (a : R) → R → Prop) x 0} (a - b)
h₁ : a = a - b + b
⊢ (t₁ : (a : R) → R → Prop) a b
have h₂ : b = 0 + b
Tactic: convert! t₁.add H' (t₁.refl b) using 1
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ (I.ringCon : (a : R) → R → Prop) x y ↔ x - y ∈ I
have rw : (I.ringCon : (a : R) → R → Prop) x y ↔ (I.ringCon : (a : R) → R → Prop) (x - y) 0
Tactic: rw [mem_iff]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ (I.ringCon : (a : R) → R → Prop) x y ↔ (I.ringCon : (a : R) → R → Prop) (x - y) 0
have mp : (I.ringCon : (a : R) → R → Prop) x y → (I.ringCon : (a : R) → R → Prop) (x - y) 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
mp : (I.ringCon : (a : R) → R → Prop) x y → (I.ringCon : (a : R) → R → Prop) (x - y) 0
⊢ (I.ringCon : (a : R) → R → Prop) x y ↔ (I.ringCon : (a : R) → R → Prop) (x - y) 0
have mpr : (I.ringCon : (a : R) → R → Prop) (x - y) 0 → (I.ringCon : (a : R) → R → Prop) x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : (I.ringCon : (a : R) → R → Prop) x y
⊢ (I.ringCon : (a : R) → R → Prop) (x - y) 0
have h₁ : 0 = y - y
Tactic: convert! I.ringCon.sub h (I.ringCon.refl y)
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : (I.ringCon : (a : R) → R → Prop) (x - y) 0
⊢ (I.ringCon : (a : R) → R → Prop) x y
have h₁ : x = x - y + y
Tactic: convert! I.ringCon.add h (I.ringCon.refl y)
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : (I.ringCon : (a : R) → R → Prop) (x - y) 0
h₁ : x = x - y + y
⊢ (I.ringCon : (a : R) → R → Prop) x y
have h₂ : y = 0 + y
Tactic: convert! I.ringCon.add h (I.ringCon.refl y)
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I_1 I J : TwoSidedIdeal R
h : (↑I : Set R) ⊆ (↑J : Set R)
x y : R
r :
  ((({ toFun := ringCon, invFun := mk, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → RingCon R) I :
        RingCon R) :
      (a : R) → R → Prop)
    x y
⊢ ((({ toFun := ringCon, invFun := mk, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → RingCon R) J :
        RingCon R) :
      (a : R) → R → Prop)
    x y
have rw : ∀
  (r :
    Membership.mem (γ := TwoSidedIdeal R)
      {
        ringCon :=
          ({ toFun := ringCon, invFun := mk, left_inv := sorry, right_inv := sorry } : (a : TwoSidedIdeal R) → RingCon R) I }
      (x - y)),
  Membership.mem (γ := TwoSidedIdeal R)
    {
      ringCon :=
        ({ toFun := ringCon, invFun := mk, left_inv := sorry, right_inv := sorry } : (a : TwoSidedIdeal R) → RingCon R) J }
    (x - y)
Tactic: rw [rel_iff] at r ⊢
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I_1 I J : TwoSidedIdeal R
h :
  LE.le (α := RingCon R)
    (({ toFun := ringCon, invFun := mk, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → RingCon R) I :
      RingCon R)
    (({ toFun := ringCon, invFun := mk, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → RingCon R) J :
      RingCon R)
x : R
hx : x ∈ (↑I : Set R)
⊢ x ∈ (↑J : Set R)
have rw : ∀ (hx : (I.ringCon : (a : R) → R → Prop) x 0), (J.ringCon : (a : R) → R → Prop) x 0
Tactic: rw [SetLike.mem_coe, mem_iff] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ I < J ↔ (↑I : Set R) ⊂ (↑J : Set R)
have rw : (↑I : Set R) ⊆ (↑J : Set R) ∧ I ≠ J ↔ (↑I : Set R) ⊆ (↑J : Set R) ∧ (↑I : Set R) ≠ (↑J : Set R)
Tactic: rw [lt_iff_le_and_ne, Set.ssubset_iff_subset_ne, le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
a b c d : R
h1 : a - b ∈ carrier
h2 : c - d ∈ carrier
⊢ a * c - b * d = a * (c - d) + (a - b) * d
have rw : a * c - b * d = a * c - a * d + (a * d - b * d)
Tactic: rw [mul_sub, sub_mul]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
a b c d : R
h1 : a - b ∈ carrier
h2 : c - d ∈ carrier
⊢ a * c - b * d ∈ carrier
have rw : a * (c - d) + (a - b) * d ∈ carrier
Tactic: rw [show a * c - b * d = a * (c - d) + (a - b) * d by rw [mul_sub, sub_mul]; abel]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
a b c d : R
h1 : a - b ∈ carrier
h2 : c - d ∈ carrier
⊢ a + c - (b + d) ∈ carrier
have rw : a - b + (c - d) ∈ carrier
Tactic: rw [show a + c - (b + d) = (a - b) + (c - d) by abel]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Basic (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
x : R
⊢ x ∈ mk' carrier zero_mem @add_mem @neg_mem @mul_mem_left @mul_mem_right ↔ x ∈ carrier
have rw : ((mk' carrier zero_mem @add_mem @neg_mem @mul_mem_left @mul_mem_right).ringCon : (a : R) → R → Prop) x 0 ↔ x ∈ carrier
Tactic: rw [mem_iff]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.BigOperators (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ (List.map f l).sum ∈ I
have rw : (I.ringCon : (a : R) → R → Prop) (List.map f l).sum (List.sum (List.map (fun (x : ι) ↦ 0) l))
Tactic: rw [mem_iff, ← List.sum_map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.BigOperators (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ (Multiset.map f s).sum ∈ I
have rw : (I.ringCon : (a : R) → R → Prop) (Multiset.map f s).sum (Multiset.sum (Multiset.map (fun (x : ι) ↦ 0) s))
Tactic: rw [mem_iff, ← Multiset.sum_map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.BigOperators (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ s.sum f ∈ I
have rw : (I.ringCon : (a : R) → R → Prop) (s.sum f) (∑ _x ∈ s, 0)
Tactic: rw [mem_iff, ← Finset.sum_const_zero]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.BigOperators (hypothesis)
Goal:
R : Type u_1
inst : Ring R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
x : ι
l : List ι
ih : ∀ (hl : ∃ x ∈ l, f x ∈ I), (List.map f l).prod ∈ I
hl : ∃ x_1 ∈ x :: l, f x_1 ∈ I
⊢ (List.map f (x :: l)).prod ∈ I
have hl₁ : f x ∈ I ∨ ∃ a ∈ l, f a ∈ I
Tactic: simp only [List.mem_cons, exists_eq_or_imp] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.BigOperators (goal)
Goal:
R : Type u_1
inst : Ring R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
x : ι
l : List ι
ih : ∀ (hl : ∃ x ∈ l, f x ∈ I), (List.map f l).prod ∈ I
hl : f x ∈ I ∨ ∃ a ∈ l, f a ∈ I
⊢ (List.map f (x :: l)).prod ∈ I
have cons : ∀ (h : f x ∈ I), (List.map f (x :: l)).prod ∈ I
Tactic: rcases hl with h | hal
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.BigOperators (goal)
Goal:
R : Type u_1
inst : Ring R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
x : ι
l : List ι
ih : ∀ (hl : ∃ x ∈ l, f x ∈ I), (List.map f l).prod ∈ I
hl : f x ∈ I ∨ ∃ a ∈ l, f a ∈ I
cons : ∀ (h : f x ∈ I), (List.map f (x :: l)).prod ∈ I
⊢ (List.map f (x :: l)).prod ∈ I
have cons₁ : ∀ (hal : ∃ a ∈ l, f a ∈ I), (List.map f (x :: l)).prod ∈ I
Tactic: rcases hl with h | hal
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.BigOperators (goal)
Goal:
R : Type u_1
inst : Ring R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∃ x ∈ l, f x ∈ I
⊢ (List.map f l).prod ∈ I
have nil : ∀ (hl : ∃ (x : ι), Membership.mem (γ := List ι) [] x ∧ f x ∈ I), (List.map f []).prod ∈ I
Tactic: induction l with
  | nil => simp only [List.not_mem_nil, false_and, exists_false] at hl
  | cons x l ih =>
    simp only [List.mem_cons, exists_eq_or_imp] at hl
    rcases hl with h | hal
    · simpa only [List.map_cons, List.prod_cons] using I.mul_mem_right _ _ h
    · simpa only [List.map_cons, List.prod_cons] using I.mul_mem_left _ _ <| ih hal
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.BigOperators (goal)
Goal:
R : Type u_1
inst : Ring R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∃ x ∈ l, f x ∈ I
nil : ∀ (hl : ∃ (x : ι), Membership.mem (γ := List ι) [] x ∧ f x ∈ I), (List.map f []).prod ∈ I
⊢ (List.map f l).prod ∈ I
have cons : ∀ (x : ι) (l : List ι) (ih : ∀ (hl : ∃ x ∈ l, f x ∈ I), (List.map f l).prod ∈ I) (hl : ∃ x_1 ∈ x :: l, f x_1 ∈ I),
  (List.map f (x :: l)).prod ∈ I
Tactic: induction l with
  | nil => simp only [List.not_mem_nil, false_and, exists_false] at hl
  | cons x l ih =>
    simp only [List.mem_cons, exists_eq_or_imp] at hl
    rcases hl with h | hal
    · simpa only [List.map_cons, List.prod_cons] using I.mul_mem_right _ _ h
    · simpa only [List.map_cons, List.prod_cons] using I.mul_mem_left _ _ <| ih hal
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.BigOperators (goal)
Goal:
R : Type u_1
inst : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∃ x ∈ s, f x ∈ I
⊢ (Multiset.map f s).prod ∈ I
have mk : ∀ (a : List ι)
  (hs :
    ∃ (x : ι), Membership.mem (γ := Multiset ι) (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) a) x ∧ f x ∈ I),
  (Multiset.map f (Quot.mk (⇑(List.isSetoid ι) : List ι → List ι → Prop) a)).prod ∈ I
Tactic: rcases s
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.BigOperators (goal)
Goal:
R : Type u_1
inst : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∃ x ∈ s, f x ∈ I
⊢ s.prod f ∈ I
have rcases : ∀ (val : Multiset ι) (nodup : val.Nodup) (hs : ∃ x ∈ { val := val, nodup := nodup : Finset ι }, f x ∈ I),
  { val := val, nodup := nodup : Finset ι }.prod f ∈ I
Tactic: rcases s
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Kernel (goal)
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_3
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
⊢ Equivalence fun (x y : R) ↦ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
have refl : ∀ (x : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) x : S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Kernel (goal)
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_3
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
refl : ∀ (x : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) x : S)
⊢ Equivalence fun (x y : R) ↦ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
have symm : ∀ {x y : R},
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S) →
    Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) y : S) ((f : (a : R) → S) x : S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Kernel (goal)
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_3
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
refl : ∀ (x : R), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) x : S)
symm :
  ∀ {x y : R},
    Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S) →
      Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) y : S) ((f : (a : R) → S) x : S)
⊢ Equivalence fun (x y : R) ↦ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
have trans : ∀ {x y z : R},
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S) →
    Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) y : S) ((f : (a : R) → S) z : S) →
      Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) z : S)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Kernel (goal)
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_3
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
x : R
⊢ Membership.mem (γ := TwoSidedIdeal R) (ker f) x ↔ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)
have rw : (ringCon (ker f) : (a : R) → R → Prop) x 0 ↔ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)
Tactic: rw [mem_iff, ker_ringCon, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Kernel (goal)
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_3
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
x : R
rw : (ringCon (ker f) : (a : R) → R → Prop) x 0 ↔ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)
⊢ Membership.mem (γ := TwoSidedIdeal R) (ker f) x ↔ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)
have rw₁ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) 0 : S) ↔
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)
Tactic: rw [mem_iff, ker_ringCon, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Kernel (goal)
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_3
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
x : R
rw : (ringCon (ker f) : (a : R) → R → Prop) x 0 ↔ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)
rw₁ :
  Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) 0 : S) ↔
    Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)
⊢ Membership.mem (γ := TwoSidedIdeal R) (ker f) x ↔ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)
have rw₂ : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) ↔ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)
Tactic: rw [mem_iff, ker_ringCon, map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Kernel (goal)
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_3
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
⊢ Eq (α := TwoSidedIdeal R) (ker f) ⊥ ↔ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
have mp : Eq (α := TwoSidedIdeal R) (ker f) ⊥ → Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Kernel (goal)
Goal:
R : Type u_1
S : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocSemiring S
F : Type u_3
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
mp : Eq (α := TwoSidedIdeal R) (ker f) ⊥ → Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Eq (α := TwoSidedIdeal R) (ker f) ⊥ ↔ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
have mpr : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S) → Eq (α := TwoSidedIdeal R) (ker f) ⊥
Tactic: fconstructor
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ I ≤ { ringCon := I.ringCon ⊔ J.ringCon }
have rw : I.ringCon ≤ { ringCon := I.ringCon ⊔ J.ringCon }.ringCon
Tactic: rw [ringCon_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ J ≤ { ringCon := I.ringCon ⊔ J.ringCon }
have rw : J.ringCon ≤ { ringCon := I.ringCon ⊔ J.ringCon }.ringCon
Tactic: rw [ringCon_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J K : TwoSidedIdeal R
h1 : I ≤ K
h2 : J ≤ K
⊢ { ringCon := I.ringCon ⊔ J.ringCon : TwoSidedIdeal R } ≤ K
have rw : ∀ (h1 : I.ringCon ≤ K.ringCon) (h2 : J.ringCon ≤ K.ringCon),
  { ringCon := I.ringCon ⊔ J.ringCon : TwoSidedIdeal R }.ringCon ≤ K.ringCon
Tactic: rw [ringCon_le_iff] at h1 h2 ⊢
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ x ∈ I ⊔ J ↔ ∃ y ∈ I, ∃ z ∈ J, y + z = x
have mp : x ∈ I ⊔ J → ∃ y ∈ I, ∃ z ∈ J, y + z = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
mp : x ∈ I ⊔ J → ∃ y ∈ I, ∃ z ∈ J, y + z = x
⊢ x ∈ I ⊔ J ↔ ∃ y ∈ I, ∃ z ∈ J, y + z = x
have mpr : (∃ y ∈ I, ∃ z ∈ J, y + z = x) → x ∈ I ⊔ J
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
h : x ∈ I ⊔ J
⊢ ∃ y ∈ I, ∃ z ∈ J, y + z = x
have a : (∃ y ∈ I, ∃ z ∈ J, y + z = x) ↔ (s.ringCon : (a : R) → R → Prop) x 0
Tactic: convert! this h
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
h : x ∈ I ⊔ J
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) ↔ (s.ringCon : (a : R) → R → Prop) x 0
have a : (∃ y ∈ I, ∃ z ∈ J, y + z = x) ↔ Membership.mem (γ := Set R) {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} x
Tactic: rw [rel_iff, sub_zero, mem_mk']
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
⊢ x ∈ I ⊔ J → ∃ y ∈ I, ∃ z ∈ J, y + z = x
have mp : I.ringCon ⊔ J.ringCon ≤ s.ringCon
Tactic: suffices (I.ringCon ⊔ J.ringCon) ≤ s.ringCon by
      intro h; convert! this h; rw [rel_iff, sub_zero, mem_mk']; rfl
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
⊢ I.ringCon ⊔ J.ringCon ≤ s.ringCon
have mp : ∀ (x y : R) (h : (I.ringCon : (a : R) → R → Prop) x y), (s.ringCon : (a : R) → R → Prop) x y
Tactic: refine sup_le (fun x y h => ?_) (fun x y h => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
mp : ∀ (x y : R) (h : (I.ringCon : (a : R) → R → Prop) x y), (s.ringCon : (a : R) → R → Prop) x y
⊢ I.ringCon ⊔ J.ringCon ≤ s.ringCon
have mp₁ : ∀ (x y : R) (h : (J.ringCon : (a : R) → R → Prop) x y), (s.ringCon : (a : R) → R → Prop) x y
Tactic: refine sup_le (fun x y h => ?_) (fun x y h => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : (I.ringCon : (a : R) → R → Prop) x y
⊢ (s.ringCon : (a : R) → R → Prop) x y
have mp : ∀ (h : x - y ∈ I), x - y ∈ s
Tactic: rw [rel_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : (J.ringCon : (a : R) → R → Prop) x y
⊢ (s.ringCon : (a : R) → R → Prop) x y
have mp : ∀ (h : x - y ∈ J), x - y ∈ s
Tactic: rw [rel_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : x - y ∈ I
⊢ x - y ∈ s
have mp : Membership.mem (γ := Set R) {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} (x - y)
Tactic: rw [mem_mk']
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x_1 : R
s : TwoSidedIdeal R := mk' {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : x - y ∈ J
⊢ x - y ∈ s
have mp : Membership.mem (γ := Set R) {x : R | ∃ y ∈ I, ∃ z ∈ J, y + z = x} (x - y)
Tactic: rw [mem_mk']
-- Lean 4 proof step from Mathlib.RingTheory.TwoSidedIdeal.Lattice (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
⊢ { ringCon := I.ringCon ⊓ J.ringCon : TwoSidedIdeal R } ≤ I
have rw : { ringCon := I.ringCon ⊓ J.ringCon : TwoSidedIdeal R }.ringCon ≤ I.ringCon
Tactic: rw [ringCon_le_iff]