awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
P : Ideal S
inst_3 : P.IsPrime
hx : ¬conductor R x ≤ P
s : Subalgebra R S
hs : s = R[x]
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
a : S
ha : Membership.mem (γ := Ideal S) (conductor R x) a
haP : a ∉ P
⊢ ∀ (b : S), a * b ∈ s

Tactic:
replace ha (b : _) : a * b ∈ s := by simpa [hs] using ha b
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
P : Ideal S
inst_3 : P.IsPrime
hx : ¬conductor R x ≤ P
s : Subalgebra R S
hs : s = R[x]
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
a : S
haP : a ∉ P
ha : ∀ (b : S), a * b ∈ s
y : S
h : Membership.mem (γ := Subalgebra R S) ⊤ y
⊢ a ∈ (↑s.toSubmonoid : Set S)

Tactic:
simpa using ha 1

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.Conductor
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
P : Ideal S
inst_3 : P.IsPrime
hx : ¬conductor R x ≤ P
s : Subalgebra R S
hs : s = R[x]
p : Ideal ↥s
inst_4 : p.IsPrime
inst_5 : P.LiesOver p
a : S
haP : a ∉ P
ha : ∀ (b : S), a * b ∈ s
⊢ Function.Bijective (α := Localization.AtPrime p) (β := Localization.AtPrime P)
    (⇑(localRingHom p P (algebraMap (↥s) S) ⋯) : (a : Localization.AtPrime p) → Localization.AtPrime P)

Tactic:
exact Localization.localRingHom_bijective_of_saturated_inf_eq_top _
    (top_le_iff.mp fun y _ ↦ ⟨a, ⟨haP, by simpa using ha 1⟩, ha _⟩) _

Premises used: And.intro, top_le_iff, Exists.intro, Iff.mp, Localization.localRingHom_bijective_of_saturated_inf_eq_top
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
α : Type u_1
R : Type u_3
inst : Add R
inst_1 : MulOneClass R
inst_2 : SMul α R
inst_3 : IsScalarTower α R R
c : RingCon R
a : α
x : R
⊢ (↑(a • x) : c.Quotient) = HSMul.hSMul (β := c.Quotient) a (↑x : c.Quotient)

Tactic:
rfl

Premises used: RingCon.toQuotient, Quot.map, Quotient.map', rfl
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : Add R
inst_1 : MulOneClass R
inst_2 : SMul α R
inst_3 : IsScalarTower α R R
inst_4 : SMul β R
inst_5 : IsScalarTower β R R
c : RingCon R
inst_6 : SMulCommClass α β R
⊢ SMulCommClass.{u_1, u_2, u_3} α β c.Quotient

Tactic:
inferInstanceAs (SMulCommClass α β c.toCon.Quotient)

Premises used: _private.0.RingCon.instSMulCommClassQuotient._proof_1
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : Add R
inst_1 : MulOneClass R
inst_2 : SMul α R
inst_3 : IsScalarTower α R R
inst_4 : SMul β R
inst_5 : IsScalarTower β R R
c : RingCon R
inst_6 : SMul α β
inst_7 : IsScalarTower α β R
⊢ IsScalarTower.{u_1, u_2, u_3} α β c.Quotient

Tactic:
inferInstanceAs (IsScalarTower α β c.toCon.Quotient)

Premises used: _private.0.RingCon.instIsScalarTowerQuotient._proof_1
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : Add R
inst_1 : MulOneClass R
inst_2 : SMul α R
inst_3 : IsScalarTower α R R
inst_4 : SMul β R
inst_5 : IsScalarTower β R R
c : RingCon R
inst_6 : SMul.{u_1, u_3} αᵐᵒᵖ R
inst_7 : IsCentralScalar α R
⊢ IsCentralScalar.{u_1, u_3} α c.Quotient

Tactic:
inferInstanceAs (IsCentralScalar α c.toCon.Quotient)

Premises used: _private.0.RingCon.instIsCentralScalarQuotient._proof_1
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : Add R
inst_1 : MulOneClass R
inst_2 : SMul α R
inst_3 : IsScalarTower α R R
inst_4 : SMulCommClass R α R
c : RingCon R
⊢ SMulCommClass.{u_3, u_1, u_3} c.Quotient α c.Quotient

Tactic:
haveI := SMulCommClass.symm R α R
  SMulCommClass.symm _ _ _

Premises used: RingCon.Quotient, SMulCommClass.symm
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c d : RingCon R
⊢ c ≤ d ↔ ∀ {x y : R}, (c : (a : R) → R → Prop) x y → (d : (a : R) → R → Prop) x y

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
R' : Type u_4
inst_2 : Add R'
inst_3 : Mul R'
F : Type u_5
inst_4 : FunLike F R R'
inst_5 : AddHomClass F R R'
inst_6 : MulHomClass F R R'
J J' : RingCon R'
f : F
h : J ≤ J'
⊢ LE.le (α := RingCon R) (J.comap f) (J'.comap f)

Tactic:
fun _ _ h₁ ↦ h h₁
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
x y : R
h : ((sInf S).toSetoid : R → R → Prop) x y
r : Setoid R
h_1 : Membership.mem (γ := Set (Setoid R)) ((fun (x : RingCon R) ↦ x.toSetoid) '' S) r
c : RingCon R
hS : c ∈ S
hr : (fun (x : RingCon R) ↦ x.toSetoid) c = r
rw : ((fun (x : RingCon R) ↦ x.toSetoid) c : R → R → Prop) x y
⊢ (r : R → R → Prop) x y

Tactic:
rw [← hr]
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
x y : R
h : ((sInf S).toSetoid : R → R → Prop) x y
r : Setoid R
h_1 : Membership.mem (γ := Set (Setoid R)) ((fun (x : RingCon R) ↦ x.toSetoid) '' S) r
c : RingCon R
hS : c ∈ S
hr : (fun (x : RingCon R) ↦ x.toSetoid) c = r
⊢ ((fun (x : RingCon R) ↦ x.toSetoid) c : R → R → Prop) x y

Tactic:
h c hS
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
x y : R
h : ((sInf S).toSetoid : R → R → Prop) x y
r : Setoid R
h_1 : Membership.mem (γ := Set (Setoid R)) ((fun (x : RingCon R) ↦ x.toSetoid) '' S) r
c : RingCon R
hS : c ∈ S
hr : (fun (x : RingCon R) ↦ x.toSetoid) c = r
⊢ ((fun (x : RingCon R) ↦ x.toSetoid) c : R → R → Prop) x y

Tactic:
exact h c hS
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
h : ∀ (x x_1 : R), (sInf S : (a : R) → R → Prop) x x_1 ↔ sInf (DFunLike.coe (β := fun (x : R) ↦ R → Prop) '' S) x x_1
⊢ Eq (α := (a : R) → R → Prop) (⇑(sInf S) : (a : R) → R → Prop) (sInf (DFunLike.coe (β := fun (x : R) ↦ R → Prop) '' S))

Tactic:
ext
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
x x_1 : R
h : (sInf S : (a : R) → R → Prop) x x_1 ↔ ∀ (i : RingCon R) (i_1 : i ∈ S), (i : (a : R) → R → Prop) x x_1
⊢ (sInf S : (a : R) → R → Prop) x x_1 ↔ sInf (DFunLike.coe (β := fun (x : R) ↦ R → Prop) '' S) x x_1

Tactic:
simp only [sInf_image, iInf_apply, iInf_Prop_eq]

Premises used: iInf_apply, sInf_image, iInf_Prop_eq
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
x x_1 : R
⊢ (sInf S : (a : R) → R → Prop) x x_1 ↔ ∀ (i : RingCon R) (i_1 : i ∈ S), (i : (a : R) → R → Prop) x x_1

Tactic:
rfl
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
ι : Sort u_4
f : ι → RingCon R
rw :
  Eq (α := (a : R) → R → Prop) (⇑(sInf (Set.range f)) : (a : R) → R → Prop) (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
rw₁ :
  Eq (α := (a : R) → R → Prop) (sInf (DFunLike.coe (β := fun (x : R) ↦ R → Prop) '' Set.range f))
    (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
rw₂ :
  Eq (α := (a : R) → R → Prop) (sInf (Set.range (DFunLike.coe (β := fun (x : R) ↦ R → Prop) ∘ f)))
    (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
rw₃ :
  Eq (α := (a : R) → R → Prop) (iInf (DFunLike.coe (β := fun (x : R) ↦ R → Prop) ∘ f))
    (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
rw₄ rw₅ :
  Eq.{u_3 + 1} (α := (a : R) → R → Prop) (⨅ (x : ι), (⇑(f x) : (a : R) → R → Prop))
    (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))
⊢ Eq (α := (a : R) → R → Prop) (⇑(iInf f) : (a : R) → R → Prop) (⨅ (i : ι), (⇑(f i) : (a : R) → R → Prop))

Tactic:
rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]

Premises used: Set.range_comp, iInf, Function.comp_def, RingCon.coe_sInf, sInf_range
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
⊢ Eq.{u_3 + 1} (α := (a : R) → R → Prop) (⇑⊤ : (a : R) → R → Prop) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
⊢ Eq.{u_3 + 1} (α := (a : R) → R → Prop) (⇑⊥ : (a : R) → R → Prop) Eq

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
⊢ Eq.{u_3 + 1} (α := Con R) (toCon ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
⊢ Eq.{u_3 + 1} (α := Con R) (toCon ⊥) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c : RingCon R
rw : c.toCon = toCon ⊤ ↔ c = ⊤
rw₁ rw₂ : c = ⊤ ↔ c = ⊤
⊢ c.toCon = ⊤ ↔ c = ⊤

Tactic:
rw [← toCon_top, toCon_inj]

Premises used: RingCon.toCon_inj, RingCon.toCon_top
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c : RingCon R
rw : c.toCon = toCon ⊥ ↔ c = ⊥
rw₁ rw₂ : c = ⊥ ↔ c = ⊥
⊢ c.toCon = ⊥ ↔ c = ⊥

Tactic:
rw [← toCon_bot, toCon_inj]

Premises used: RingCon.toCon_inj, RingCon.toCon_bot
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c : RingCon R
⊢ Subsingleton.{u_3 + 1} c.Quotient ↔ c = ⊤

Tactic:
simp [RingCon.Quotient]

Premises used: RingCon.Quotient
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c : RingCon R
⊢ Nontrivial.{u_3} c.Quotient ↔ c ≠ ⊤

Tactic:
simp [← not_subsingleton_iff_nontrivial]

Premises used: not_subsingleton_iff_nontrivial
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c d : RingCon R
⊢ Eq (α := (a : R) → R → Prop) (⇑(c ⊓ d) : (a : R) → R → Prop) ((⇑c : (a : R) → R → Prop) ⊓ (⇑d : (a : R) → R → Prop))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c d : RingCon R
x y : R
⊢ (c ⊓ d : (a : R) → R → Prop) x y ↔ (c : (a : R) → R → Prop) x y ∧ (d : (a : R) → R → Prop) x y

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : Add R
inst_1 : Mul R
c d : RingCon R
inst_2 : Nontrivial R
x y : R
ne : x ≠ y
⊢ Ne (α := Prop) ((fun (x_1 : RingCon R) ↦ ((x_1 : (a : R) → R → Prop) x y : Prop)) ⊥)
    ((fun (x_1 : RingCon R) ↦ ((x_1 : (a : R) → R → Prop) x y : Prop)) ⊤)

Tactic:
simp [ne]
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
α : Type u_1
β : Type u_2
R : Type u_3
inst : Add R
inst_1 : Mul R
c_1 d : RingCon R
inst_2 : Subsingleton R
c c' : RingCon R
r r' : R
simp_rw : (c : (a : R) → R → Prop) r r ↔ (c' : (a : R) → R → Prop) r r
simp_rw₁ : True ↔ (c' : (a : R) → R → Prop) r r
⊢ (c : (a : R) → R → Prop) r r' ↔ (c' : (a : R) → R → Prop) r r'

Tactic:
simp_rw [Subsingleton.elim r' r, c.refl, c'.refl]

Premises used: RingCon.refl, Subsingleton.elim
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
inl : Subsingleton R → (Nontrivial.{u_3} (RingCon R) ↔ Nontrivial R)
inr : Nontrivial R → (Nontrivial.{u_3} (RingCon R) ↔ Nontrivial R)
⊢ Nontrivial.{u_3} (RingCon R) ↔ Nontrivial R

Tactic:
cases subsingleton_or_nontrivial R

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
h : Subsingleton R
inl : Subsingleton.{u_3 + 1} (RingCon R) ↔ Subsingleton R
⊢ Nontrivial.{u_3} (RingCon R) ↔ Nontrivial R

Tactic:
simp_rw [← not_subsingleton_iff_nontrivial, not_iff_not]

Premises used: not_iff_not, not_subsingleton_iff_nontrivial
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
h : Subsingleton R
inl : Subsingleton.{u_3 + 1} (RingCon R) ↔ Subsingleton R
⊢ Nontrivial.{u_3} (RingCon R) ↔ Nontrivial R

Tactic:
on_goal 1 => simp_rw [← not_subsingleton_iff_nontrivial, not_iff_not]

Premises used: not_iff_not, not_subsingleton_iff_nontrivial
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
h : Subsingleton R
⊢ Subsingleton.{u_3 + 1} (RingCon R) ↔ Subsingleton R

Tactic:
iff_of_true inferInstance ‹_›

Premises used: inferInstance, iff_of_true
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
h : Subsingleton R
⊢ Subsingleton.{u_3 + 1} (RingCon R) ↔ Subsingleton R

Tactic:
exact iff_of_true inferInstance ‹_›
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
h : Nontrivial R
⊢ Nontrivial.{u_3} (RingCon R) ↔ Nontrivial R

Tactic:
iff_of_true inferInstance ‹_›

Premises used: inferInstance, iff_of_true
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
h : Nontrivial R
⊢ Nontrivial.{u_3} (RingCon R) ↔ Nontrivial R

Tactic:
exact iff_of_true inferInstance ‹_›
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
simp_rw : ¬Nontrivial.{u_3} (RingCon R) ↔ ¬Nontrivial R
⊢ Subsingleton.{u_3 + 1} (RingCon R) ↔ Subsingleton R

Tactic:
simp_rw [← not_nontrivial_iff_subsingleton, nontrivial_iff]

Premises used: not_nontrivial_iff_subsingleton, RingCon.nontrivial_iff
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
r : R → R → Prop
⊢ Eq (α := RingCon R) (ringConGen r) (sInf {s : RingCon R | ∀ (x y : R), r x y → (s : (a : R) → R → Prop) x y})

Tactic:
le_antisymm
    (fun _x _y H =>
      RingConGen.Rel.recOn H (fun _ _ h _ hs => hs _ _ h) (RingCon.refl _)
        (fun _ => RingCon.symm _) (fun _ _ => RingCon.trans _)
        (fun _ _ h1 h2 c hc => c.add (h1 c hc) <| h2 c hc)
        (fun _ _ h1 h2 c hc => c.mul (h1 c hc) <| h2 c hc))
    (sInf_le fun _ _ => RingConGen.Rel.of _ _)

Premises used: le_antisymm, RingConGen.Rel.of, sInf_le
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
r : R → R → Prop
c : RingCon R
h : ∀ (x y : R), r x y → (c : (a : R) → R → Prop) x y
rw : sInf {s : RingCon R | ∀ (x y : R), r x y → (s : (a : R) → R → Prop) x y} ≤ c
⊢ ringConGen r ≤ c

Tactic:
rw [ringConGen_eq]

Premises used: RingCon.ringConGen_eq
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
r : R → R → Prop
c : RingCon R
h : ∀ (x y : R), r x y → (c : (a : R) → R → Prop) x y
⊢ sInf {s : RingCon R | ∀ (x y : R), r x y → (s : (a : R) → R → Prop) x y} ≤ c

Tactic:
sInf_le h

Premises used: sInf_le
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
r : R → R → Prop
c : RingCon R
h : ∀ (x y : R), r x y → (c : (a : R) → R → Prop) x y
⊢ sInf {s : RingCon R | ∀ (x y : R), r x y → (s : (a : R) → R → Prop) x y} ≤ c

Tactic:
exact sInf_le h
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
r s : R → R → Prop
h : ∀ (x y : R), r x y → s x y
⊢ LE.le (α := RingCon R) (ringConGen r) (ringConGen s)

Tactic:
ringConGen_le fun x y hr => RingConGen.Rel.of _ _ <| h x y hr

Premises used: RingConGen.Rel.of, RingCon.ringConGen_le
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c : RingCon R
rw : sInf {s : RingCon R | ∀ (x y : R), (c : (a : R) → R → Prop) x y → (s : (a : R) → R → Prop) x y} ≤ c
⊢ ringConGen (⇑c : (a : R) → R → Prop) ≤ c

Tactic:
rw [ringConGen_eq]

Premises used: RingCon.ringConGen_eq
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c : RingCon R
⊢ sInf {s : RingCon R | ∀ (x y : R), (c : (a : R) → R → Prop) x y → (s : (a : R) → R → Prop) x y} ≤ c

Tactic:
sInf_le fun _ _ => id

Premises used: id, sInf_le
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c : RingCon R
⊢ sInf {s : RingCon R | ∀ (x y : R), (c : (a : R) → R → Prop) x y → (s : (a : R) → R → Prop) x y} ≤ c

Tactic:
exact sInf_le fun _ _ => id
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
r : R → R → Prop
⊢ Eq (α := RingCon R) (ringConGen (⇑(ringConGen r) : (a : R) → R → Prop)) (ringConGen r)

Tactic:
ringConGen_of_ringCon _

Premises used: RingCon.ringConGen_of_ringCon
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c d : RingCon R
rw :
  c ⊔ d =
    sInf
      {s : RingCon R |
        ∀ (x y : R), (c : (a : R) → R → Prop) x y ∨ (d : (a : R) → R → Prop) x y → (s : (a : R) → R → Prop) x y}
⊢ c ⊔ d = ringConGen fun (x y : R) ↦ (c : (a : R) → R → Prop) x y ∨ (d : (a : R) → R → Prop) x y

Tactic:
rw [ringConGen_eq]

Premises used: RingCon.ringConGen_eq
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c d : RingCon R
apply :
  Eq.{u_3 + 1} (α := Set (RingCon R)) {x : RingCon R | c ≤ x ∧ d ≤ x}
    {s : RingCon R |
      ∀ (x y : R), (c : (a : R) → R → Prop) x y ∨ (d : (a : R) → R → Prop) x y → (s : (a : R) → R → Prop) x y}
⊢ c ⊔ d =
    sInf
      {s : RingCon R |
        ∀ (x y : R), (c : (a : R) → R → Prop) x y ∨ (d : (a : R) → R → Prop) x y → (s : (a : R) → R → Prop) x y}

Tactic:
apply congr_arg sInf

Premises used: congr_arg, InfSet.sInf
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c d : RingCon R
⊢ Eq.{u_3 + 1} (α := Set (RingCon R)) {x : RingCon R | c ≤ x ∧ d ≤ x}
    {s : RingCon R |
      ∀ (x y : R), (c : (a : R) → R → Prop) x y ∨ (d : (a : R) → R → Prop) x y → (s : (a : R) → R → Prop) x y}

Tactic:
simp only [le_def, or_imp, ← forall_and]

Premises used: or_imp, RingCon.le_def, forall_and
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c d : RingCon R
rw :
  Eq (α := RingCon R) (ringConGen fun (x y : R) ↦ (c : (a : R) → R → Prop) x y ∨ (d : (a : R) → R → Prop) x y)
    (ringConGen ((⇑c : (a : R) → R → Prop) ⊔ (⇑d : (a : R) → R → Prop)))
⊢ c ⊔ d = ringConGen ((⇑c : (a : R) → R → Prop) ⊔ (⇑d : (a : R) → R → Prop))

Tactic:
rw [sup_eq_ringConGen]

Premises used: RingCon.sup_eq_ringConGen
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
c d : RingCon R
⊢ Eq (α := RingCon R) (ringConGen fun (x y : R) ↦ (c : (a : R) → R → Prop) x y ∨ (d : (a : R) → R → Prop) x y)
    (ringConGen ((⇑c : (a : R) → R → Prop) ⊔ (⇑d : (a : R) → R → Prop)))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
rw : sSup S = sInf {s : RingCon R | ∀ (x y : R), (∃ c ∈ S, (c : (a : R) → R → Prop) x y) → (s : (a : R) → R → Prop) x y}
⊢ sSup S = ringConGen fun (x y : R) ↦ ∃ c ∈ S, (c : (a : R) → R → Prop) x y

Tactic:
rw [ringConGen_eq]

Premises used: RingCon.ringConGen_eq
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
apply :
  upperBounds S = {s : RingCon R | ∀ (x y : R), (∃ c ∈ S, (c : (a : R) → R → Prop) x y) → (s : (a : R) → R → Prop) x y}
⊢ sSup S = sInf {s : RingCon R | ∀ (x y : R), (∃ c ∈ S, (c : (a : R) → R → Prop) x y) → (s : (a : R) → R → Prop) x y}

Tactic:
apply congr_arg sInf

Premises used: congr_arg, InfSet.sInf
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
h :
  ∀ (x : RingCon R),
    x ∈ upperBounds S ↔
      Membership.mem (γ := Set (RingCon R))
        {s : RingCon R | ∀ (x y : R), (∃ c ∈ S, (c : (a : R) → R → Prop) x y) → (s : (a : R) → R → Prop) x y} x
⊢ upperBounds S = {s : RingCon R | ∀ (x y : R), (∃ c ∈ S, (c : (a : R) → R → Prop) x y) → (s : (a : R) → R → Prop) x y}

Tactic:
ext
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
x : RingCon R
⊢ x ∈ upperBounds S ↔
    Membership.mem (γ := Set (RingCon R))
      {s : RingCon R | ∀ (x y : R), (∃ c ∈ S, (c : (a : R) → R → Prop) x y) → (s : (a : R) → R → Prop) x y} x

Tactic:
⟨fun h _ _ ⟨r, hr⟩ => h hr.1 hr.2, fun h r hS _ _ hr => h _ _ ⟨r, hS, hr⟩⟩

Premises used: _private.0.RingCon.sSup_eq_ringConGen.match_1, And.right, And.left, And.intro, Iff.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
x : RingCon R
⊢ x ∈ upperBounds S ↔
    Membership.mem (γ := Set (RingCon R))
      {s : RingCon R | ∀ (x y : R), (∃ c ∈ S, (c : (a : R) → R → Prop) x y) → (s : (a : R) → R → Prop) x y} x

Tactic:
exact ⟨fun h _ _ ⟨r, hr⟩ => h hr.1 hr.2, fun h r hS _ _ hr => h _ _ ⟨r, hS, hr⟩⟩
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
rw :
  Eq.{u_3 + 1} (α := RingCon R) (ringConGen fun (x y : R) ↦ ∃ c ∈ S, (c : (a : R) → R → Prop) x y)
    (ringConGen (⨆ a ∈ S, (⇑a : (a : R) → R → Prop)))
⊢ sSup S = ringConGen (sSup (DFunLike.coe (β := fun (x : R) ↦ R → Prop) '' S))

Tactic:
rw [sSup_eq_ringConGen, sSup_image]

Premises used: RingCon.sSup_eq_ringConGen, sSup_image
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
e_r : ∀ (x y : R), (∃ c ∈ S, (c : (a : R) → R → Prop) x y) ↔ (⨆ a ∈ S, (⇑a : (a : R) → R → Prop)) x y
⊢ Eq.{u_3 + 1} (α := RingCon R) (ringConGen fun (x y : R) ↦ ∃ c ∈ S, (c : (a : R) → R → Prop) x y)
    (ringConGen (⨆ a ∈ S, (⇑a : (a : R) → R → Prop)))

Tactic:
congr with (x y)
-- Module: Mathlib.RingTheory.Congruence.Basic
Goal:
R : Type u_3
inst : Add R
inst_1 : Mul R
S : Set (RingCon R)
x y : R
⊢ (∃ c ∈ S, (c : (a : R) → R → Prop) x y) ↔ (⨆ a ∈ S, (⇑a : (a : R) → R → Prop)) x y

Tactic:
simp only [iSup_apply, iSup_Prop_eq, exists_prop]

Premises used: exists_prop, iSup_Prop_eq, iSup_apply
-- Module: Mathlib.RingTheory.Congruence.BigOperators
Goal:
ι : Type u_1
S : Type u_2
inst : Add S
inst_1 : Monoid S
t : RingCon S
l : List ι
f g : ι → S
h : ∀ i ∈ l, (t : (a : S) → S → Prop) (f i) (g i)
⊢ (t : (a : S) → S → Prop) (List.map f l).prod (List.map g l).prod

Tactic:
t.toCon.list_prod h

Premises used: RingCon.toCon, Con.list_prod
-- Module: Mathlib.RingTheory.Congruence.BigOperators
Goal:
ι : Type u_1
S : Type u_2
inst : AddMonoid S
inst_1 : Mul S
t : RingCon S
l : List ι
f g : ι → S
h : ∀ i ∈ l, (t : (a : S) → S → Prop) (f i) (g i)
⊢ (t : (a : S) → S → Prop) (List.map f l).sum (List.map g l).sum

Tactic:
t.toAddCon.list_sum h

Premises used: RingCon.toAddCon, AddCon.list_sum
-- Module: Mathlib.RingTheory.Congruence.BigOperators
Goal:
ι : Type u_1
S : Type u_2
inst : Add S
inst_1 : CommMonoid S
t : RingCon S
s : Multiset ι
f g : ι → S
h : ∀ i ∈ s, (t : (a : S) → S → Prop) (f i) (g i)
⊢ (t : (a : S) → S → Prop) (Multiset.map f s).prod (Multiset.map g s).prod

Tactic:
t.toCon.multiset_prod h

Premises used: RingCon.toCon, Con.multiset_prod
-- Module: Mathlib.RingTheory.Congruence.BigOperators
Goal:
ι : Type u_1
S : Type u_2
inst : AddCommMonoid S
inst_1 : Mul S
t : RingCon S
s : Multiset ι
f g : ι → S
h : ∀ i ∈ s, (t : (a : S) → S → Prop) (f i) (g i)
⊢ (t : (a : S) → S → Prop) (Multiset.map f s).sum (Multiset.map g s).sum

Tactic:
t.toAddCon.multiset_sum h

Premises used: RingCon.toAddCon, AddCon.multiset_sum
-- Module: Mathlib.RingTheory.Congruence.BigOperators
Goal:
ι : Type u_1
S : Type u_2
inst : Add S
inst_1 : CommMonoid S
t : RingCon S
s : Finset ι
f g : ι → S
h : ∀ i ∈ s, (t : (a : S) → S → Prop) (f i) (g i)
⊢ (t : (a : S) → S → Prop) (s.prod f) (s.prod g)

Tactic:
t.toCon.finsetProd s h

Premises used: RingCon.toCon, Con.finsetProd
-- Module: Mathlib.RingTheory.Congruence.BigOperators
Goal:
ι : Type u_1
S : Type u_2
inst : AddCommMonoid S
inst_1 : Mul S
t : RingCon S
s : Finset ι
f g : ι → S
h : ∀ i ∈ s, (t : (a : S) → S → Prop) (f i) (g i)
⊢ (t : (a : S) → S → Prop) (s.sum f) (s.sum g)

Tactic:
t.toAddCon.finsetSum s h

Premises used: RingCon.toAddCon, AddCon.finsetSum
-- Module: Mathlib.RingTheory.Congruence.BigOperators
Goal:
ι : Type u_1
β : Type u_2
M : Type u_3
inst : Add M
inst_1 : CommMonoid M
inst_2 : Zero β
c : RingCon M
h h' : ι → β → M
f g : ι →₀ β
hf : ∀ (i : ι), (c : (a : M) → M → Prop) (h i 0) 1
hf' : ∀ (i : ι), (c : (a : M) → M → Prop) (h' i 0) 1
H : ∀ (i : ι), (c : (a : M) → M → Prop) (h i ((f : (a : ι) → β) i)) (h' i ((g : (a : ι) → β) i))
⊢ (c : (a : M) → M → Prop) (f.prod h) (g.prod h')

Tactic:
c.toCon.finsuppProd h h' hf hf' H

Premises used: RingCon.toCon, Con.finsuppProd