awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
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
rw : a * c - b * d = a * c - a * d + (a * d - b * d)
⊢ a * c - b * d = a * (c - d) + (a - b) * d

Tactic:
rw [mul_sub, sub_mul]

Premises used: mul_sub, sub_mul
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
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 - a * d + (a * d - b * d)

Tactic:
abel
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
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
rw : a * (c - d) + (a - b) * d ∈ carrier
⊢ a * c - b * d ∈ carrier

Tactic:
rw [show a * c - b * d = a * (c - d) + (a - b) * d by rw [mul_sub, sub_mul]; abel]
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
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 - d) + (a - b) * d ∈ carrier

Tactic:
add_mem (mul_mem_left h2) (mul_mem_right h1)
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
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 - d) + (a - b) * d ∈ carrier

Tactic:
exact add_mem (mul_mem_left h2) (mul_mem_right h1)
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
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 - b + (c - d)

Tactic:
abel
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
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
rw : a - b + (c - d) ∈ carrier
⊢ a + c - (b + d) ∈ carrier

Tactic:
rw [show a + c - (b + d) = (a - b) + (c - d) by abel]
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
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 - b + (c - d) ∈ carrier

Tactic:
add_mem h1 h2
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
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 - b + (c - d) ∈ carrier

Tactic:
exact add_mem h1 h2
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
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
rw :
  ((mk' carrier zero_mem @add_mem @neg_mem @mul_mem_left @mul_mem_right).ringCon : (a : R) → R → Prop) x 0 ↔ x ∈ carrier
⊢ x ∈ mk' carrier zero_mem @add_mem @neg_mem @mul_mem_left @mul_mem_right ↔ x ∈ carrier

Tactic:
rw [mem_iff]

Premises used: TwoSidedIdeal.mem_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
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
⊢ ((mk' carrier zero_mem @add_mem @neg_mem @mul_mem_left @mul_mem_right).ringCon : (a : R) → R → Prop) x 0 ↔ x ∈ carrier

Tactic:
simp [mk']

Premises used: TwoSidedIdeal.mk'
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
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
⊢ (↑(mk' carrier zero_mem @add_mem @neg_mem @mul_mem_left @mul_mem_right) : Set R) = carrier

Tactic:
Set.ext <| mem_mk' carrier zero_mem add_mem neg_mem mul_mem_left mul_mem_right

Premises used: Set.ext, TwoSidedIdeal.mem_mk'
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x : Rᵐᵒᵖ
⊢ x ∈ I.op ↔ unop x ∈ I

Tactic:
I.ringCon.comm'

Premises used: RingCon.toCon, Set.Mem, setOf, Con.toSetoid, TwoSidedIdeal.ringCon, MulOpposite.unop, Setoid.comm'
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
⊢ (↑I.op : Set Rᵐᵒᵖ) = unop ⁻¹' (↑I : Set R)

Tactic:
Set.ext fun _ => mem_op_iff

Premises used: Set.ext, TwoSidedIdeal.mem_op_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal Rᵐᵒᵖ
x : R
⊢ x ∈ I.unop ↔ MulOpposite.op x ∈ I

Tactic:
I.ringCon.comm'

Premises used: RingCon.toCon, Set.Mem, setOf, Con.toSetoid, TwoSidedIdeal.ringCon, Setoid.comm'
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal Rᵐᵒᵖ
⊢ (↑I.unop : Set R) = MulOpposite.op ⁻¹' (↑I : Set Rᵐᵒᵖ)

Tactic:
Set.ext fun _ => mem_unop_iff

Premises used: Set.ext, TwoSidedIdeal.mem_unop_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I I' J' : TwoSidedIdeal R
⊢ LE.le (α := TwoSidedIdeal Rᵐᵒᵖ)
      (({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → TwoSidedIdeal Rᵐᵒᵖ)
          I' :
        TwoSidedIdeal Rᵐᵒᵖ)
      (({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : TwoSidedIdeal R) → TwoSidedIdeal Rᵐᵒᵖ)
          J' :
        TwoSidedIdeal Rᵐᵒᵖ) ↔
    I' ≤ J'

Tactic:
simpa [ringCon_le_iff] using RingCon.opOrderIso.map_rel_iff

Premises used: TwoSidedIdeal.ringCon_le_iff, RelIso.map_rel_iff, RingCon.opOrderIso
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
rw : (I.ringCon : (a : R) → R → Prop) (List.map f l).sum (List.sum (List.map (fun (x : ι) ↦ 0) l))
rw₁ : Type u_2
rw₂ : List ι
⊢ (List.map f l).sum ∈ I

Tactic:
rw [mem_iff, ← List.sum_map_zero]

Premises used: List.sum_map_zero, TwoSidedIdeal.mem_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∀ x ∈ l, f x ∈ I
⊢ (I.ringCon : (a : R) → R → Prop) (List.map f l).sum (List.sum (List.map (fun (x : ι) ↦ 0) l))

Tactic:
I.ringCon.listSum l hl

Premises used: RingCon.listSum, TwoSidedIdeal.ringCon
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
rw : (I.ringCon : (a : R) → R → Prop) (Multiset.map f s).sum (Multiset.sum (Multiset.map (fun (x : ι) ↦ 0) s))
rw₁ : Type u_2
rw₂ : Multiset ι
⊢ (Multiset.map f s).sum ∈ I

Tactic:
rw [mem_iff, ← Multiset.sum_map_zero]

Premises used: Multiset.sum_map_zero, TwoSidedIdeal.mem_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ (I.ringCon : (a : R) → R → Prop) (Multiset.map f s).sum (Multiset.sum (Multiset.map (fun (x : ι) ↦ 0) s))

Tactic:
I.ringCon.multisetSum s hs

Premises used: RingCon.multisetSum, TwoSidedIdeal.ringCon
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
rw : (I.ringCon : (a : R) → R → Prop) (s.sum f) (∑ _x ∈ s, 0)
rw₁ : Type u_2
rw₂ : Finset ι
⊢ s.sum f ∈ I

Tactic:
rw [mem_iff, ← Finset.sum_const_zero]

Premises used: Finset.sum_const_zero, TwoSidedIdeal.mem_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∀ x ∈ s, f x ∈ I
⊢ (I.ringCon : (a : R) → R → Prop) (s.sum f) (∑ _x ∈ s, 0)

Tactic:
I.ringCon.finsetSum s hs

Premises used: TwoSidedIdeal.ringCon, RingCon.finsetSum
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
β : Type u_3
inst_1 : Zero β
f : ι →₀ β
g : ι → β → R
h : ∀ i ∈ f.support, g i ((f : (a : ι) → β) i) ∈ I
⊢ f.sum g ∈ I

Tactic:
finsetSum_mem _ _ _ h

Premises used: Set.Mem, setOf, Finsupp.sum, TwoSidedIdeal.finsetSum_mem
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
ι : Type u_2
β : ι → Type u_3
inst_1 : DecidableEq ι
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
g : (i : ι) → β i → R
h : ∀ i ∈ f.support (β := β), g i ((f : (a : ι) → β a) i) ∈ I
⊢ f.sum (β := β) g ∈ I

Tactic:
finsetSum_mem _ _ _ h

Premises used: Set.Mem, setOf, TwoSidedIdeal.finsetSum_mem, DFinsupp.sum
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
Goal:
R : Type u_1
inst : Ring R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
hl : ∃ (x : ι), Membership.mem (γ := List ι) [] x ∧ f x ∈ I
⊢ (List.map f []).prod ∈ I

Tactic:
simp only [List.not_mem_nil, false_and, exists_false] at hl

Premises used: false_and, exists_false, List.not_mem_nil
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
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
⊢ f x ∈ I ∨ ∃ a ∈ l, f a ∈ I

Tactic:
simp only [List.mem_cons, exists_eq_or_imp] at hl

Premises used: exists_eq_or_imp, List.mem_cons
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
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
cons₁ : ∀ (hal : ∃ a ∈ l, f a ∈ I), (List.map f (x :: l)).prod ∈ I
⊢ (List.map f (x :: l)).prod ∈ I

Tactic:
rcases hl with h | hal
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
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
h : f x ∈ I
⊢ (List.map f (x :: l)).prod ∈ I

Tactic:
simpa only [List.map_cons, List.prod_cons] using I.mul_mem_right _ _ h

Premises used: TwoSidedIdeal.mul_mem_right, List.map_cons, List.prod_cons
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
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
hal : ∃ a ∈ l, f a ∈ I
⊢ (List.map f (x :: l)).prod ∈ I

Tactic:
simpa only [List.map_cons, List.prod_cons] using I.mul_mem_left _ _ <| ih hal

Premises used: TwoSidedIdeal.mul_mem_left, List.map_cons, List.prod_cons
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
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
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
⊢ (List.map f 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

Premises used: TwoSidedIdeal.mul_mem_left, List.map_cons, false_and, exists_false, exists_eq_or_imp, List.mem_cons, List.prod_cons, List.not_mem_nil
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
Goal:
R : Type u_1
inst : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
hs : ∃ x ∈ s, f x ∈ I
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
⊢ (Multiset.map f s).prod ∈ I

Tactic:
rcases s
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
Goal:
R : Type u_1
inst : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Multiset ι
f : ι → R
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:
simpa using listProd_mem (hl := hs)

Premises used: TwoSidedIdeal.listProd_mem
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
Goal:
R : Type u_1
inst : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∃ x ∈ s, f x ∈ I
rcases :
  ∀ (val : Multiset ι) (nodup : val.Nodup) (hs : ∃ x ∈ { val := val, nodup := nodup : Finset ι }, f x ∈ I),
    { val := val, nodup := nodup : Finset ι }.prod f ∈ I
⊢ s.prod f ∈ I

Tactic:
rcases s
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
Goal:
R : Type u_1
inst : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
f : ι → R
val : Multiset ι
nodup : val.Nodup
hs : ∃ x ∈ { val := val, nodup := nodup : Finset ι }, f x ∈ I
⊢ { val := val, nodup := nodup : Finset ι }.prod f ∈ I

Tactic:
simpa using multiSetProd_mem (hs := hs)

Premises used: TwoSidedIdeal.multiSetProd_mem
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
Goal:
R : Type u_1
inst : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
β : Type u_3
M : Type u_4
inst_1 : Add M
inst_2 : CommMonoid M
inst_3 : Zero β
h : ι → β → R
f : ι →₀ β
H : ∃ i ∈ f.support, h i ((f : (a : ι) → β) i) ∈ I
⊢ f.prod h ∈ I

Tactic:
finsetProd_mem _ _ _ H

Premises used: Set.Mem, setOf, TwoSidedIdeal.finsetProd_mem, Finsupp.prod
-- Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators
Goal:
R : Type u_1
inst : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
β : ι → Type u_3
inst_1 : DecidableEq ι
inst_2 : (i : ι) → Zero (β i)
inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
g : (i : ι) → β i → R
h : ∃ i ∈ f.support (β := β), g i ((f : (a : ι) → β a) i) ∈ I
⊢ f.prod (β := β) g ∈ I

Tactic:
finsetProd_mem _ _ _ h

Premises used: Set.Mem, setOf, TwoSidedIdeal.finsetProd_mem, DFinsupp.prod
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel
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)
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)
⊢ Equivalence fun (x y : R) ↦ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)

Tactic:
constructor
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel
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), Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) x : S)

Tactic:
aesop
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel
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 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:
aesop
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel
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 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:
aesop
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel
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
w : R
⊢ ∀ {x y z : R},
    Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) w : S) ((f : (a : R) → S) x : 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) (w * y) : S) ((f : (a : R) → S) (x * z) : S)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel
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
w : R
⊢ ∀ {x y z : R},
    Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) w : S) ((f : (a : R) → S) x : 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) (w + y) : S) ((f : (a : R) → S) (x + z) : S)

Tactic:
simp_all
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel
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 y : R
⊢ (ringCon (ker f) : (a : R) → R → Prop) x y ↔ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel
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)
rw₂ 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)
⊢ Membership.mem (γ := TwoSidedIdeal R) (ker f) x ↔ Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S)

Tactic:
rw [mem_iff, ker_ringCon, map_zero]

Premises used: TwoSidedIdeal.ker_ringCon, map_zero, TwoSidedIdeal.mem_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel
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)
mpr : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S) → Eq (α := TwoSidedIdeal R) (ker f) ⊥
⊢ Eq (α := TwoSidedIdeal R) (ker f) ⊥ ↔ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)

Tactic:
fconstructor
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel
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
h : Eq (α := TwoSidedIdeal R) (ker f) ⊥
x y : R
hxy : Eq.{u_2 + 1} (α := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)
⊢ x = y

Tactic:
simpa [h, rel_iff, mem_bot, sub_eq_zero] using show (ker f).ringCon x y from hxy

Premises used: sub_eq_zero, TwoSidedIdeal.rel_iff, TwoSidedIdeal.mem_bot
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel
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
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S) → Eq (α := TwoSidedIdeal R) (ker f) ⊥

Tactic:
fun h ↦ eq_bot_iff.2 fun x hx => h hx

Premises used: Iff.mpr, eq_bot_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel
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
⊢ Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S) → Eq (α := TwoSidedIdeal R) (ker f) ⊥

Tactic:
exact fun h ↦ eq_bot_iff.2 fun x hx => h hx

Premises used: Iff.mpr, eq_bot_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel
Goal:
R : Type u_4
inst : NonAssocRing R
I : TwoSidedIdeal R
x : R
h :
  Membership.mem (γ := TwoSidedIdeal R)
    (ker (F := R →+* I.ringCon.Quotient) (RingCon.mk'.{u_4} (R := R) I.ringCon : R →+* I.ringCon.Quotient)) x
⊢ x ∈ I

Tactic:
simpa using I.rel_iff _ _ |>.1 (Quotient.eq'.1 h)

Premises used: Quotient.eq', TwoSidedIdeal.rel_iff, Iff.mp
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel
Goal:
R : Type u_4
inst : NonAssocRing R
I : TwoSidedIdeal R
x : R
h : x ∈ I
⊢ x - 0 ∈ I

Tactic:
simpa using h