awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x r y : R
hy : y ∈ s
⊢ (fun (x1 x2 : R) ↦ x1 * x2) r y * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
exact .inr <| ⟨r * y, ⟨r, mem_univ _, y, hy, rfl⟩, x, mem_univ _, rfl⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun (x1 x2 : R) ↦ x1 * x2) ((fun (x1 x2 : R) ↦ x1 * x2) r' y) r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
.inr <| ⟨r' * y, ⟨r', mem_univ _, y, hy, rfl⟩, r * x, mem_univ _, ?_⟩

Premises used: Set.union, HMul.hMul, Set.Mem, setOf, And.intro, Exists.intro, Set.mem_univ, Or.inr, rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
refine_2 :
  (fun (x1 x2 : R) ↦ x1 * x2) (r' * y) (r * x) = (fun (x1 x2 : R) ↦ x1 * x2) ((fun (x1 x2 : R) ↦ x1 * x2) r' y) r * x
⊢ (fun (x1 x2 : R) ↦ x1 * x2) ((fun (x1 x2 : R) ↦ x1 * x2) r' y) r * x ∈ s ∪ s * univ ∪ univ * s ∪ univ * s * univ

Tactic:
refine .inr <| ⟨r' * y, ⟨r', mem_univ _, y, hy, rfl⟩, r * x, mem_univ _, ?_⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : NonUnitalRing R
s : Set R
z x r' y : R
hy : y ∈ s
r : R
⊢ (fun (x1 x2 : R) ↦ x1 * x2) (r' * y) (r * x) = (fun (x1 x2 : R) ↦ x1 * x2) ((fun (x1 x2 : R) ↦ x1 * x2) r' y) r * x

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
s : Set R
z : R
trans :
  Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔ Membership.mem (γ := TwoSidedIdeal R) (span (univ * s * univ)) z
trans₁ :
  Membership.mem (γ := TwoSidedIdeal R) (span (univ * s * univ)) z ↔
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (univ * s * univ)) z
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (univ * s * univ)) z

Tactic:
trans z ∈ span (univ * s * univ)

Premises used: HMul.hMul, Set.univ, TwoSidedIdeal.span
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
s : Set R
z : R
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔ Membership.mem (γ := TwoSidedIdeal R) (span (univ * s * univ)) z

Tactic:
⟨(span_mono (fun x hx ↦ ?_) ·), fun hz ↦ ?_⟩

Premises used: TwoSidedIdeal.span_mono, Iff.intro
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
s : Set R
z : R
refine_1 : Membership.mem (γ := TwoSidedIdeal R) (span s) z → ∀ (x : R) (hx : x ∈ s), x ∈ univ * s * univ
refine_2 :
  ∀ (hz : Membership.mem (γ := TwoSidedIdeal R) (span (univ * s * univ)) z),
    Membership.mem (γ := TwoSidedIdeal R) (span s) z
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z ↔ Membership.mem (γ := TwoSidedIdeal R) (span (univ * s * univ)) z

Tactic:
refine ⟨(span_mono (fun x hx ↦ ?_) ·), fun hz ↦ ?_⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
s : Set R
z : R
h : Membership.mem (γ := TwoSidedIdeal R) (span s) z
x : R
hx : x ∈ s
⊢ (fun (x1 x2 : R) ↦ x1 * x2) (1 * x) 1 = x

Tactic:
simp
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
s : Set R
z : R
h : Membership.mem (γ := TwoSidedIdeal R) (span s) z
x : R
hx : x ∈ s
⊢ x ∈ univ * s * univ

Tactic:
exact ⟨1 * x, ⟨1, mem_univ _, x, hx, rfl⟩, 1, mem_univ _, by simp⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
s : Set R
z : R
hz : Membership.mem (γ := TwoSidedIdeal R) (span (univ * s * univ)) z
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z

Tactic:
mem_span_iff.mp hz (span s) <| subset_mul_set (set_mul_subset subset_span _) _

Premises used: TwoSidedIdeal.span, TwoSidedIdeal.set_mul_subset, TwoSidedIdeal.subset_mul_set, TwoSidedIdeal.mem_span_iff, Iff.mp, TwoSidedIdeal.subset_span
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
s : Set R
z : R
hz : Membership.mem (γ := TwoSidedIdeal R) (span (univ * s * univ)) z
⊢ Membership.mem (γ := TwoSidedIdeal R) (span s) z

Tactic:
exact mem_span_iff.mp hz (span s) <| subset_mul_set (set_mul_subset subset_span _) _

Premises used: TwoSidedIdeal.span, TwoSidedIdeal.set_mul_subset, TwoSidedIdeal.subset_mul_set, TwoSidedIdeal.mem_span_iff, Iff.mp, TwoSidedIdeal.subset_span
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
s : Set R
z : R
⊢ Membership.mem (γ := TwoSidedIdeal R) (span (univ * s * univ)) z ↔
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (univ * s * univ)) z

Tactic:
mem_span_iff_mem_addSubgroup_closure_absorbing ?_ ?_

Premises used: TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_absorbing, Set.Mem, setOf
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
s : Set R
z : R
refine_1 : ∀ (x y : R), y ∈ univ * s * univ → x * y ∈ univ * s * univ
refine_2 : ∀ (y x : R), y ∈ univ * s * univ → y * x ∈ univ * s * univ
⊢ Membership.mem (γ := TwoSidedIdeal R) (span (univ * s * univ)) z ↔
    Membership.mem (γ := AddSubgroup R) (AddSubgroup.closure (univ * s * univ)) z

Tactic:
refine mem_span_iff_mem_addSubgroup_closure_absorbing ?_ ?_

Premises used: TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure_absorbing
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
s : Set R
z x y : R
hy : y ∈ univ * s * univ
refine_1 : ∀ (hy : y ∈ univ * (s * univ)), x * y ∈ univ * (s * univ)
⊢ x * y ∈ univ * s * univ

Tactic:
rw [mul_assoc] at hy ⊢

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
s : Set R
z x y : R
hy : y ∈ univ * (s * univ)
refine_1 : ∀ (r y : R) (hy : y ∈ s * univ), x * (fun (x1 x2 : R) ↦ x1 * x2) r y ∈ univ * (s * univ)
⊢ x * y ∈ univ * (s * univ)

Tactic:
obtain ⟨r, -, y, hy, rfl⟩ := hy

Premises used: rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
s : Set R
z x r y : R
hy : y ∈ s * univ
⊢ x * (fun (x1 x2 : R) ↦ x1 * x2) r y ∈ univ * (s * univ)

Tactic:
⟨x * r, mem_univ _, y, hy, mul_assoc ..⟩

Premises used: HMul.hMul, Set.Mem, mul_assoc, setOf, Set.image2, And.intro, Exists.intro, Set.mem_univ
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
s : Set R
z x r y : R
hy : y ∈ s * univ
⊢ x * (fun (x1 x2 : R) ↦ x1 * x2) r y ∈ univ * (s * univ)

Tactic:
exact ⟨x * r, mem_univ _, y, hy, mul_assoc ..⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
s : Set R
z x y : R
hy : y ∈ univ * s
r : R
⊢ (fun (x1 x2 : R) ↦ x1 * x2) y r * x ∈ univ * s * univ

Tactic:
⟨y, hy, r * x, mem_univ _, (mul_assoc ..).symm⟩

Premises used: HMul.hMul, Set.Mem, mul_assoc, setOf, Set.image2, And.intro, Exists.intro, Set.mem_univ, Eq.symm
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
s : Set R
z x y : R
hy : y ∈ univ * s
r : R
⊢ (fun (x1 x2 : R) ↦ x1 * x2) y r * x ∈ univ * s * univ

Tactic:
exact ⟨y, hy, r * x, mem_univ _, (mul_assoc ..).symm⟩
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : TwoSidedIdeal R
r : R
x : ↥I
⊢ r • (↑x : R) = r * (↑x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : TwoSidedIdeal R
r : Rᵐᵒᵖ
x : ↥I
⊢ r • (↑x : R) = (↑x : R) * MulOpposite.unop r

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : TwoSidedIdeal R
⊢ Function.Injective (α := ↥I) (β := R) (⇑I.subtype : (a : ↥I) → R)

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : TwoSidedIdeal R
⊢ Eq (α := (a : ↥I) → R) (⇑I.subtype : (a : ↥I) → R) (Subtype.val (p := fun (x : R) ↦ x ∈ I))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : TwoSidedIdeal R
⊢ Function.Injective (α := ↥I) (β := Rᵐᵒᵖ) (⇑I.subtypeMop : (a : ↥I) → Rᵐᵒᵖ)

Tactic:
MulOpposite.op_injective.comp Subtype.coe_injective

Premises used: MulOpposite.op_injective, Subtype.coe_injective, Function.Injective.comp, MulOpposite.op
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
x : R
⊢ Membership.mem (γ := TwoSidedIdeal R) ((fromIdeal : (a : Ideal R) → TwoSidedIdeal R) I : TwoSidedIdeal R) x ↔
    Membership.mem (γ := TwoSidedIdeal R) (span (↑I : Set R)) x

Tactic:
simp [fromIdeal]

Premises used: TwoSidedIdeal.fromIdeal
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : TwoSidedIdeal R
x : R
⊢ Membership.mem (γ := Ideal R) ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I : Ideal R) x ↔ x ∈ I

Tactic:
simp [asIdeal]

Premises used: TwoSidedIdeal.asIdeal
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
J : TwoSidedIdeal R
h : I ≤ (asIdeal : (a : TwoSidedIdeal R) → Ideal R) J
x : R
hx : Membership.mem (γ := TwoSidedIdeal R) ((fromIdeal : (a : Ideal R) → TwoSidedIdeal R) I : TwoSidedIdeal R) x
⊢ ∀ (I_1 : TwoSidedIdeal R), (↑I : Set R) ⊆ (↑I_1 : Set R) → x ∈ I_1

Tactic:
simp only [fromIdeal, OrderHom.coe_mk, mem_span_iff] at hx

Premises used: TwoSidedIdeal.fromIdeal, OrderHom.coe_mk, TwoSidedIdeal.mem_span_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
J : TwoSidedIdeal R
h : I ≤ (asIdeal : (a : TwoSidedIdeal R) → Ideal R) J
x : R
hx : ∀ (I_1 : TwoSidedIdeal R), (↑I : Set R) ⊆ (↑I_1 : Set R) → x ∈ I_1
⊢ x ∈ J

Tactic:
hx _ h
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
J : TwoSidedIdeal R
h : I ≤ (asIdeal : (a : TwoSidedIdeal R) → Ideal R) J
x : R
hx : ∀ (I_1 : TwoSidedIdeal R), (↑I : Set R) ⊆ (↑I_1 : Set R) → x ∈ I_1
⊢ x ∈ J

Tactic:
exact hx _ h
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : TwoSidedIdeal R
⊢ (↑((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I : Ideal R) : Set R) = (↑I : Set R)

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
⊢ Eq.{u_1 + 1} (α := Ideal R) ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) ⊥) ⊥

Tactic:
rfl

Premises used: setOf, Set.singleton, rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
⊢ Eq.{u_1 + 1} (α := Ideal R) ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) ⊤) ⊤

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I_1 I : TwoSidedIdeal R
a x : R
⊢ Membership.mem (γ := Ideal R) ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I : Ideal R) a →
    Membership.mem (γ := Ideal R) ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I : Ideal R) (a * x)

Tactic:
simpa using I.mul_mem_right _ _

Premises used: TwoSidedIdeal.mul_mem_right
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I_1 I J : TwoSidedIdeal R
h : I ≤ J
x : Rᵐᵒᵖ
h' :
  Membership.mem (γ := Submodule Rᵐᵒᵖ Rᵐᵒᵖ)
    ((fun (I : TwoSidedIdeal R) ↦
        ((asIdeal : (a : TwoSidedIdeal Rᵐᵒᵖ) → Ideal Rᵐᵒᵖ) { ringCon := I.ringCon.op } : Ideal Rᵐᵒᵖ))
      I)
    x
simp :
  ∀ (h' : (I.ringCon : (a : R) → R → Prop) 0 (MulOpposite.unop x)),
    (J.ringCon : (a : R) → R → Prop) 0 (MulOpposite.unop x)
⊢ Membership.mem (γ := Submodule Rᵐᵒᵖ Rᵐᵒᵖ)
    ((fun (I : TwoSidedIdeal R) ↦
        ((asIdeal : (a : TwoSidedIdeal Rᵐᵒᵖ) → Ideal Rᵐᵒᵖ) { ringCon := I.ringCon.op } : Ideal Rᵐᵒᵖ))
      J)
    x

Tactic:
simp only [mem_asIdeal, mem_iff, RingCon.op_iff, MulOpposite.unop_zero] at h' ⊢

Premises used: RingCon.op_iff, MulOpposite.unop_zero, TwoSidedIdeal.mem_asIdeal, TwoSidedIdeal.mem_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I_1 I J : TwoSidedIdeal R
h : I ≤ J
x : Rᵐᵒᵖ
h' : (I.ringCon : (a : R) → R → Prop) 0 (MulOpposite.unop x)
⊢ (J.ringCon : (a : R) → R → Prop) 0 (MulOpposite.unop x)

Tactic:
J.rel_iff _ _ |>.2 <| h <| I.rel_iff 0 x.unop |>.1 h'

Premises used: Iff.mpr, TwoSidedIdeal.rel_iff, Iff.mp, MulOpposite.unop, OfNat.ofNat
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I_1 I J : TwoSidedIdeal R
h : I ≤ J
x : Rᵐᵒᵖ
h' : (I.ringCon : (a : R) → R → Prop) 0 (MulOpposite.unop x)
⊢ (J.ringCon : (a : R) → R → Prop) 0 (MulOpposite.unop x)

Tactic:
exact J.rel_iff _ _ |>.2 <| h <| I.rel_iff 0 x.unop |>.1 h'

Premises used: Iff.mpr, TwoSidedIdeal.rel_iff, Iff.mp, MulOpposite.unop, OfNat.ofNat
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : TwoSidedIdeal R
x : Rᵐᵒᵖ
⊢ Membership.mem (γ := Ideal Rᵐᵒᵖ) ((asIdealOpposite : (a : TwoSidedIdeal R) → Ideal Rᵐᵒᵖ) I : Ideal Rᵐᵒᵖ) x ↔
    MulOpposite.unop x ∈ I

Tactic:
simpa [asIdealOpposite, asIdeal, TwoSidedIdeal.mem_iff, RingCon.op_iff] using
    ⟨I.ringCon.symm, I.ringCon.symm⟩

Premises used: TwoSidedIdeal.asIdealOpposite, TwoSidedIdeal.asIdeal, RingCon.op_iff, TwoSidedIdeal.mem_iff
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
x : TwoSidedIdeal R
x_1 : R
⊢ (∀ (I : TwoSidedIdeal R),
      (↑((asIdeal : (a : TwoSidedIdeal R) → Ideal R) x : Ideal R) : Set R) ⊆ (↑I : Set R) → x_1 ∈ I) ↔
    x_1 ∈ x

Tactic:
aesop
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
J : Ideal R
x_1 : R
h : ∀ (I : TwoSidedIdeal R), (↑J : Set R) ⊆ (↑I : Set R) → x_1 ∈ I
x : R
⊢ x ∈ (↑J : Set R) → x ∈ (↑(mk' (↑J : Set R) ⋯ ⋯ ⋯ ⋯ ⋯) : Set R)

Tactic:
simp
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : CommRing R
J : Ideal R
x : R
⊢ x ∈ J → ∀ (I : TwoSidedIdeal R), (↑J : Set R) ⊆ (↑I : Set R) → x ∈ I

Tactic:
aesop
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
x : R
⊢ x ∈ I.toTwoSided ↔ x ∈ I

Tactic:
simp [toTwoSided]

Premises used: Ideal.toTwoSided
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
⊢ (↑I.toTwoSided : Set R) = (↑I : Set R)

Tactic:
simp [toTwoSided]

Premises used: Ideal.toTwoSided
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : TwoSidedIdeal R
h :
  ∀ (x : R),
    Membership.mem (γ := TwoSidedIdeal R) (toTwoSided ((TwoSidedIdeal.asIdeal : (a : TwoSidedIdeal R) → Ideal R) I)) x ↔
      x ∈ I
⊢ toTwoSided ((TwoSidedIdeal.asIdeal : (a : TwoSidedIdeal R) → Ideal R) I) = I

Tactic:
ext
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : TwoSidedIdeal R
x : R
⊢ Membership.mem (γ := TwoSidedIdeal R) (toTwoSided ((TwoSidedIdeal.asIdeal : (a : TwoSidedIdeal R) → Ideal R) I)) x ↔
    x ∈ I

Tactic:
simp
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
h :
  ∀ (x : R),
    Membership.mem (γ := Ideal R) ((TwoSidedIdeal.asIdeal : (a : TwoSidedIdeal R) → Ideal R) I.toTwoSided : Ideal R) x ↔
      x ∈ I
⊢ (TwoSidedIdeal.asIdeal : (a : TwoSidedIdeal R) → Ideal R) I.toTwoSided = I

Tactic:
ext
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : Ideal R
inst_1 : I.IsTwoSided
x : R
⊢ Membership.mem (γ := Ideal R) ((TwoSidedIdeal.asIdeal : (a : TwoSidedIdeal R) → Ideal R) I.toTwoSided : Ideal R) x ↔
    x ∈ I

Tactic:
simp
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
x : TwoSidedIdeal R
⊢ (fun (I : { I : Ideal R // I.IsTwoSided }) ↦
        have this := ⋯;
        (↑I : Ideal R).toTwoSided)
      ((fun (I : TwoSidedIdeal R) ↦
          (Subtype.mk (p := fun (I : Ideal R) ↦ I.IsTwoSided) ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I) ⋯ :
            { I : Ideal R // I.IsTwoSided }))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I : { I : Ideal R // I.IsTwoSided }
⊢ (fun (I : TwoSidedIdeal R) ↦
        (Subtype.mk (p := fun (I : Ideal R) ↦ I.IsTwoSided) ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I) ⋯ :
          { I : Ideal R // I.IsTwoSided }))
      ((fun (I : { I : Ideal R // I.IsTwoSided }) ↦
          have this := ⋯;
          (↑I : Ideal R).toTwoSided)
        I) =
    I

Tactic:
simp
-- Module: Mathlib.RingTheory.TwoSidedIdeal.Operations
Goal:
R : Type u_1
inst : Ring R
I I' : TwoSidedIdeal R
⊢ LE.le (α := { I : Ideal R // I.IsTwoSided })
      (({
              toFun := fun (I : TwoSidedIdeal R) ↦
                Subtype.mk (p := fun (I : Ideal R) ↦ I.IsTwoSided) ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I) ⋯,
              invFun := fun (I : { I : Ideal R // I.IsTwoSided }) ↦
                have this := ⋯;
                (↑I : Ideal R).toTwoSided,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : TwoSidedIdeal R) → { I : Ideal R // I.IsTwoSided })
          I :
        { I : Ideal R // I.IsTwoSided })
      (({
              toFun := fun (I : TwoSidedIdeal R) ↦
                Subtype.mk (p := fun (I : Ideal R) ↦ I.IsTwoSided) ((asIdeal : (a : TwoSidedIdeal R) → Ideal R) I) ⋯,
              invFun := fun (I : { I : Ideal R // I.IsTwoSided }) ↦
                have this := ⋯;
                (↑I : Ideal R).toTwoSided,
              left_inv := ⋯, right_inv := ⋯ } :
            (a : TwoSidedIdeal R) → { I : Ideal R // I.IsTwoSided })
          I' :
        { I : Ideal R // I.IsTwoSided }) ↔
    I ≤ I'

Tactic:
simp [SetLike.le_def]

Premises used: SetLike.le_def
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
h : WfDvdMonoid.{u_1} (Associates α)
⊢ WfDvdMonoid α

Tactic:
⟨(mk_surjective.wellFounded_iff mk_dvdNotUnit_mk_iff.symm).2 wellFounded_dvdNotUnit⟩

Premises used: Function.Surjective.wellFounded_iff, Iff.mpr, IsWellFounded.mk, wellFounded_dvdNotUnit, Associates.mk_surjective
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
⊢ WfDvdMonoid.{u_1} (Associates α)

Tactic:
⟨(mk_surjective.wellFounded_iff mk_dvdNotUnit_mk_iff.symm).1 wellFounded_dvdNotUnit⟩

Premises used: Function.Surjective.wellFounded_iff, IsWellFounded.mk, wellFounded_dvdNotUnit, Associates.mk_surjective, Iff.mp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : WfDvdMonoid α
⊢ WellFoundedLT.{u_1} (Associates α)

Tactic:
⟨Subrelation.wf dvdNotUnit_of_lt wellFounded_dvdNotUnit⟩

Premises used: IsWellFounded.mk, wellFounded_dvdNotUnit, Associates.dvdNotUnit_of_lt, Subrelation.wf
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
h : WellFoundedLT.{u_1} (Associates α)
⊢ WellFounded fun (x1 x2 : Associates α) ↦ x1 < x2

Tactic:
h.wf

Premises used: IsWellFounded.wf
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
h : WellFoundedLT.{u_1} (Associates α)
h₁ : ∀ (x x : Associates α), Eq.{u_1 + 1} (α := (a b : Associates α) → Prop) DvdNotUnit LT.lt
⊢ WellFounded.{u_1 + 1} (α := Associates α) DvdNotUnit

Tactic:
convert! h.wf

Premises used: IsWellFounded.wf
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
h : WellFoundedLT.{u_1} (Associates α)
x x_1 : Associates α
h₁ : ∀ (x x_2 : Associates α), DvdNotUnit x x_2 ↔ x < x_2
⊢ Eq.{u_1 + 1} (α := (a b : Associates α) → Prop) DvdNotUnit LT.lt

Tactic:
ext
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
h : WellFoundedLT.{u_1} (Associates α)
x x_1 x_2 x_3 : Associates α
⊢ DvdNotUnit x_2 x_3 ↔ x_2 < x_3

Tactic:
Associates.dvdNotUnit_iff_lt

Premises used: Associates.dvdNotUnit_iff_lt
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
h : WellFoundedLT.{u_1} (Associates α)
x x_1 x_2 x_3 : Associates α
⊢ DvdNotUnit x_2 x_3 ↔ x_2 < x_3

Tactic:
exact Associates.dvdNotUnit_iff_lt

Premises used: Associates.dvdNotUnit_iff_lt
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
⊢ WfDvdMonoid α → WellFoundedLT.{u_1} (Associates α)

Tactic:
apply WfDvdMonoid.wellFoundedLT_associates

Premises used: WfDvdMonoid.wellFoundedLT_associates
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
rw : ∀ (a : α), Irreducible a ↔ Prime a
⊢ ∀ {a : Associates α}, Irreducible a ↔ Prime a

Tactic:
rw [← Associates.irreducible_iff_prime_iff]

Premises used: Associates.irreducible_iff_prime_iff
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : UniqueFactorizationMonoid α
⊢ ∀ (a : α), Irreducible a ↔ Prime a

Tactic:
apply UniqueFactorizationMonoid.irreducible_iff_prime

Premises used: UniqueFactorizationMonoid.irreducible_iff_prime
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
g : Multiset α
empty :
  (∀ (x : α), Membership.mem (γ := Multiset α) 0 x → Prime x) →
    (∀ x ∈ g, Prime x) → Multiset.prod 0 ~ᵤ g.prod → Multiset.Rel Associated 0 g
⊢ (∀ (x : α), Membership.mem (γ := Multiset α) 0 x → Prime x) →
    (∀ x ∈ g, Prime x) → Multiset.prod 0 ~ᵤ g.prod → Multiset.Rel Associated 0 g

Tactic:
_
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
g : Multiset α
h_1 : ∀ (x : α), Membership.mem (γ := Multiset α) 0 x → Prime x
hg : ∀ x ∈ g, Prime x
h : Multiset.prod 0 ~ᵤ g.prod
x : α
hx : x ∈ g
⊢ IsUnit g.prod

Tactic:
simpa [associated_one_iff_isUnit] using h.symm

Premises used: associated_one_iff_isUnit, Associated.symm
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
g : Multiset α
h_1 : ∀ (x : α), Membership.mem (γ := Multiset α) 0 x → Prime x
hg : ∀ x ∈ g, Prime x
h : Multiset.prod 0 ~ᵤ g.prod
⊢ Multiset.Rel Associated 0 g

Tactic:
exact Multiset.rel_zero_left.2 <|
      Multiset.eq_zero_of_forall_notMem fun x hx =>
        have : IsUnit g.prod := by simpa [associated_one_iff_isUnit] using h.symm
        (hg x hx).not_unit <|
          isUnit_iff_dvd_one.2 <| (Multiset.dvd_prod hx).trans (isUnit_iff_dvd_one.1 this)

Premises used: Iff.mpr, Multiset.dvd_prod, Prime.not_unit, Iff.mp, Multiset.eq_zero_of_forall_notMem, isUnit_iff_dvd_one, Multiset.rel_zero_left, Dvd.dvd.trans
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
⊢ p ∈ p ::ₘ f

Tactic:
simp
-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
⊢ p ∣ (p ::ₘ f).prod

Tactic:
simp