awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
inst : NonAssocSemiring M
c d : RingCon M
h : c ≤ d
x : M
⊢ Eq (α := d.Quotient)
    ((c.quotientQuotientEquivQuotient d h : (a : (ker (c.map d h)).Quotient) → d.Quotient)
        (↑(↑x : c.Quotient) : (ker (c.map d h)).Quotient) :
      d.Quotient)
    ((↑x : d.Quotient) : d.Quotient)

Tactic:
rfl

Premises used: Quotient.liftOn', RingCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
inst : NonAssocSemiring M
c d : RingCon M
h : c ≤ d
x : M
⊢ ((c.quotientQuotientEquivQuotient d h).symm : (a : d.Quotient) → (ker (c.map d h)).Quotient) ⟦x⟧ = ⟦⟦x⟧⟧

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, RingCon.toQuotient, RingCon.Quotient, Quotient, Quot.map, rfl, Quot.mapRight
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
inst : Ring M
c : RingCon M
⊢ Eq.{u_1 + 1} (α := Subring c.Quotient) (c.mk'.range (R := M)) ⊤

Tactic:
RingHom.range_eq_top.mpr (mk'_surjective _)

Premises used: Iff.mpr, RingCon.mk'_surjective, RingHom.range_eq_top
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : Ring M
inst_1 : Ring P
c : RingCon M
f : M →+* P
H : c ≤ ker f
⊢ (c.lift f H).range = RingHom.range.{u_1, u_3} (R := M) f

Tactic:
SetLike.coe_injective <| Set.range_quot_lift _

Premises used: Set.range_quot_lift, SetLike.coe_injective
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
inst : Ring M
inst_1 : Ring P
f : M →+* P
⊢ Eq.{u_3 + 1} (α := Subring P) (kerLift f).range (RingHom.range.{u_1, u_3} (R := M) f)

Tactic:
range_lift fun _ _ => id

Premises used: RingCon.kerLift, id, RingCon.range_lift
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
inst : Ring M
inst_1 : Ring N
c : RingCon M
f : N →+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ Eq.{u_1 + 1} (α := ↥(c.mk'.comp f).range)
    ((c.comapQuotientEquivRange f hcd : (a : d.Quotient) → ↥(c.mk'.comp f).range) (↑x : d.Quotient) :
      ↥(c.mk'.comp f).range)
    (Subtype.mk (p := fun (x : c.Quotient) ↦ x ∈ (c.mk'.comp f).range) (↑((f : (a : N) → M) x) : c.Quotient) ⋯ :
      ↥(c.mk'.comp f).range)

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, RingCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
inst : Ring M
inst_1 : Ring N
c : RingCon M
f : N →+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ Eq.{u_1 + 1} (α := c.Quotient)
    ((↑((c.comapQuotientEquivRange f hcd : (a : d.Quotient) → ↥(c.mk'.comp f).range) (↑x : d.Quotient)) : c.Quotient) :
      c.Quotient)
    ((↑((f : (a : N) → M) x) : c.Quotient) : c.Quotient)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, RingCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
inst : Ring M
inst_1 : Ring N
c : RingCon M
f : N →+* M
d : RingCon N
hcd : d = c.comap f
x : N
⊢ Eq.{u_2 + 1} (α := d.Quotient)
    (((c.comapQuotientEquivRange f hcd).symm : (a : ↥(c.mk'.comp f).range) → d.Quotient)
        (Subtype.mk (p := fun (x : c.Quotient) ↦ x ∈ (c.mk'.comp f).range) (↑((f : (a : N) → M) x) : c.Quotient) ⋯) :
      d.Quotient)
    ((↑x : d.Quotient) : d.Quotient)

Tactic:
simp [RingEquiv.symm_apply_eq, ← Subtype.coe_inj]

Premises used: RingEquiv.symm_apply_eq, Subtype.coe_inj
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
c d : RingCon M
h : c = d
a : M
⊢ Eq (α := d.Quotient) ((RingCon.congrₐ R h : (a : c.Quotient) → d.Quotient) (↑a : c.Quotient) : d.Quotient)
    ((↑a : d.Quotient) : d.Quotient)

Tactic:
rfl

Premises used: RingCon.toQuotient, Quot.map, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
c : RingCon M
⊢ Eq (α := Subalgebra R c.Quotient) (AlgHom.range (mkₐ R c)) ⊤

Tactic:
(AlgHom.range_eq_top _).mpr (mkₐ_surjective _)

Premises used: Iff.mpr, AlgHom.range_eq_top, RingCon.mkₐ_surjective
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
inst_3 : Semiring P
inst_4 : Algebra R P
c : RingCon M
f : M →ₐ[R] P
H : c ≤ ker f.toRingHom
⊢ (c.liftₐ f H).toRingHom = c.lift (↑f : M →+* P) H

Tactic:
rfl

Premises used: RingCon.lift, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
inst_3 : Semiring P
inst_4 : Algebra R P
c : RingCon M
f : M →ₐ[R] P
H : c ≤ ker f.toRingHom
⊢ Eq (α := (a : c.Quotient) → P) (⇑(c.liftₐ f H) : (a : c.Quotient) → P)
    (⇑(c.lift (↑f : M →+* P) H) : (a : c.Quotient) → P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
inst_3 : Semiring P
inst_4 : Algebra R P
c : RingCon M
f : M →ₐ[R] P
H : c ≤ ker f.toRingHom
x : M
⊢ Eq.{u_3 + 1} (α := P) ((c.liftₐ f H : (a : c.Quotient) → P) (↑x : c.Quotient) : P) ((f : (a : M) → P) x : P)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
inst_3 : Semiring P
inst_4 : Algebra R P
c : RingCon M
f : M →ₐ[R] P
H : c ≤ ker f.toRingHom
⊢ (c.liftₐ f H).range = f.range

Tactic:
Subalgebra.toSubsemiring_injective <| rangeS_lift H

Premises used: Subalgebra.toSubsemiring_injective, RingCon.rangeS_lift
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
inst_3 : Semiring P
inst_4 : Algebra R P
f : M →ₐ[R] P
x : M
⊢ Eq.{u_3 + 1} (α := P) ((kerLiftₐ f : (a : (ker f.toRingHom).Quotient) → P) (↑x : (ker f.toRingHom).Quotient) : P)
    ((f : (a : M) → P) x : P)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
inst_3 : Semiring P
inst_4 : Algebra R P
f : M →ₐ[R] P
⊢ Injective.{u_1 + 1, u_3 + 1} (α := (ker f.toRingHom).Quotient) (β := P)
    (⇑(kerLiftₐ f) : (a : (ker f.toRingHom).Quotient) → P)

Tactic:
kerLift_injective f.toRingHom

Premises used: RingCon.kerLift_injective, AlgHom.toRingHom
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
c d : RingCon M
h : c ≤ d
x : c.Quotient
⊢ Eq (α := d.Quotient) ((factorₐ R h : (a : c.Quotient) → d.Quotient) x : d.Quotient)
    ((c.liftₐ (mkₐ R d) ⋯ : (a : c.Quotient) → d.Quotient) x : d.Quotient)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
c d : RingCon M
h : c ≤ d
x : M
⊢ (factorₐ R h : (a : c.Quotient) → d.Quotient) ⟦x⟧ = ⟦x⟧

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, RingCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
c d : RingCon M
h : c ≤ d
⊢ Eq (α := M →ₐ[R] d.Quotient) (AlgHom.comp (factorₐ R h) (mkₐ R c)) (mkₐ R d)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, RingCon.toQuotient, RingCon.mk', RingCon.mkₐ, AlgHom.comp, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
inst_3 : Semiring P
inst_4 : Algebra R P
f : M →ₐ[R] P
⊢ (kerLiftₐ f).range = f.range

Tactic:
liftₐ_range fun _ _ => id

Premises used: id, RingCon.kerLiftₐ, RingCon.liftₐ_range
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
inst_3 : Semiring P
inst_4 : Algebra R P
f : M →ₐ[R] P
x : M
⊢ Eq.{u_3 + 1} (α := ↥f.range)
    ((quotientKerEquivRangeₐ f : (a : (ker (↑f : M →+* P)).Quotient) → ↥f.range) (↑x : (ker (↑f : M →+* P)).Quotient) :
      ↥f.range)
    (Subtype.mk (p := fun (x : P) ↦ x ∈ f.range) ((f : (a : M) → P) x) ⋯ : ↥f.range)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
P : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
inst_3 : Semiring P
inst_4 : Algebra R P
f : M →ₐ[R] P
x : M
⊢ Eq.{u_3 + 1} (α := P)
    ((↑((quotientKerEquivRangeₐ f : (a : (ker (↑f : M →+* P)).Quotient) → ↥f.range)
            (↑x : (ker (↑f : M →+* P)).Quotient)) :
        P) :
      P)
    ((f : (a : M) → P) x : P)

Tactic:
rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
inst_3 : Semiring N
inst_4 : Algebra R N
φ : M →ₐ[R] N
⊢ (↑(quotientKerEquivRangeₐ φ) : (ker (↑φ : M →+* N)).Quotient →ₐ[R] ↥φ.range).comp (mkₐ R (ker (↑φ : M →+* N))) =
    φ.rangeRestrict

Tactic:
rfl

Premises used: Quotient.liftOn', Set.Mem, AddCon.liftOn, RingHom.codRestrict, Subsemiring.copy, AlgHom.codRestrict, AlgHom.comp, AlgHom.range, rfl, RingHom.rangeS
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
inst_3 : Semiring N
inst_4 : Algebra R N
c : RingCon M
f : N →ₐ[R] M
d : RingCon N
h : d = c.comap f
x : N
⊢ Eq.{u_1 + 1} (α := ↥(AlgHom.comp (mkₐ R c) f).range)
    ((c.comapQuotientEquivRangeₐ f h : (a : d.Quotient) → ↥((mkₐ R c).comp f).range) (↑x : d.Quotient) :
      ↥(AlgHom.comp (mkₐ R c) f).range)
    (Subtype.mk (p := fun (x : c.Quotient) ↦ x ∈ (AlgHom.comp (mkₐ R c) f).range) (↑((f : (a : N) → M) x) : c.Quotient)
        ⋯ :
      ↥(AlgHom.comp (mkₐ R c) f).range)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, RingCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
inst_3 : Semiring N
inst_4 : Algebra R N
c : RingCon M
f : N →ₐ[R] M
x : N
d : RingCon N
h : d = c.comap f
⊢ Eq.{u_1 + 1} (α := c.Quotient)
    ((↑((c.comapQuotientEquivRangeₐ f h : (a : d.Quotient) → ↥((mkₐ R c).comp f).range) (↑x : d.Quotient)) :
        c.Quotient) :
      c.Quotient)
    ((↑((f : (a : N) → M) x) : c.Quotient) : c.Quotient)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, RingCon.toQuotient, rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
inst_3 : Semiring N
inst_4 : Algebra R N
c : RingCon M
f : N →ₐ[R] M
x : N
d : RingCon N
h : d = c.comap f
⊢ Eq.{u_2 + 1} (α := d.Quotient)
    (((c.comapQuotientEquivRangeₐ f h).symm : (a : ↥((mkₐ R c).comp f).range) → d.Quotient)
        (Subtype.mk (p := fun (x : c.Quotient) ↦ x ∈ (AlgHom.comp (mkₐ R c) f).range)
          (↑((f : (a : N) → M) x) : c.Quotient) ⋯) :
      d.Quotient)
    ((↑x : d.Quotient) : d.Quotient)

Tactic:
simp [AlgEquiv.symm_apply_eq, ← Subtype.coe_inj]

Premises used: AlgEquiv.symm_apply_eq, Subtype.coe_inj
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
N : Type u_2
P : Type u_3
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
inst_3 : Semiring N
inst_4 : Algebra R N
inst_5 : Semiring P
inst_6 : Algebra R P
c_1 d_1 : RingCon M
f : M →ₐ[R] P
c d : RingCon M
h : c ≤ d
x : R
⊢ (c.quotientQuotientEquivQuotient d h).toFun
      ((algebraMap R (RingCon.Quotient (ker (↑(factorₐ R h) : c.Quotient →+* d.Quotient))) :
          (a : R) → (ker (↑(factorₐ R h) : c.Quotient →+* d.Quotient)).Quotient)
        x) =
    (algebraMap R d.Quotient : (a : R) → d.Quotient) x

Tactic:
rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
c d : RingCon M
h : c ≤ d
x : M
⊢ (quotientQuotientEquivQuotientₐ R h : (a : (ker (↑(factorₐ R h) : c.Quotient →+* d.Quotient)).Quotient) → d.Quotient)
      ⟦⟦x⟧⟧ =
    ⟦x⟧

Tactic:
rfl

Premises used: Quotient.liftOn', rfl
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
c d : RingCon M
h : c ≤ d
x : M
⊢ Eq (α := d.Quotient)
    ((quotientQuotientEquivQuotientₐ R h :
          (a : (ker (↑(factorₐ R h) : c.Quotient →+* d.Quotient)).Quotient) → d.Quotient)
        (↑(↑x : c.Quotient) : (ker (↑(factorₐ R h) : c.Quotient →+* d.Quotient)).Quotient) :
      d.Quotient)
    ((↑x : d.Quotient) : d.Quotient)

Tactic:
quotientQuotientEquivQuotientₐ_mk_mk R h x

Premises used: RingCon.toQuotient, RingCon.quotientQuotientEquivQuotientₐ_mk_mk
-- Module: Mathlib.RingTheory.Congruence.Hom
Goal:
M : Type u_1
R : Type u_4
inst : CommSemiring R
inst_1 : Semiring M
inst_2 : Algebra R M
c d : RingCon M
h : c ≤ d
x : M
⊢ (AlgEquiv.symm (quotientQuotientEquivQuotientₐ R h) :
        (a : d.Quotient) → (ker (↑(factorₐ R h) : c.Quotient →+* d.Quotient)).Quotient)
      ⟦x⟧ =
    ⟦⟦x⟧⟧

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, RingCon.toQuotient, RingCon.Quotient, Quotient, Quot.map, rfl, Quot.mapRight
-- Module: Mathlib.RingTheory.Congruence.Opposite
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c : RingCon R
x y : Rᵐᵒᵖ
⊢ (c.op : (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop) x y ↔ (c : (a : R) → R → Prop) (MulOpposite.unop y) (MulOpposite.unop x)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.Congruence.Opposite
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c : RingCon Rᵐᵒᵖ
x y : R
⊢ (c.unop : (a : R) → R → Prop) x y ↔ (c : (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop) (MulOpposite.op y) (MulOpposite.op x)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.Congruence.Opposite
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
mp :
  (∀ {x y : Rᵐᵒᵖ},
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) c :
              RingCon Rᵐᵒᵖ) :
            (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
          x y →
        ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) d :
              RingCon Rᵐᵒᵖ) :
            (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
          x y) →
    ∀ {x y : R}, (c : (a : R) → R → Prop) x y → (d : (a : R) → R → Prop) x y
mpr :
  (∀ {x y : R}, (c : (a : R) → R → Prop) x y → (d : (a : R) → R → Prop) x y) →
    ∀ {x y : Rᵐᵒᵖ},
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) c :
              RingCon Rᵐᵒᵖ) :
            (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
          x y →
        ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) d :
              RingCon Rᵐᵒᵖ) :
            (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
          x y
⊢ (∀ {x y : Rᵐᵒᵖ},
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) c :
              RingCon Rᵐᵒᵖ) :
            (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
          x y →
        ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) d :
              RingCon Rᵐᵒᵖ) :
            (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
          x y) ↔
    ∀ {x y : R}, (c : (a : R) → R → Prop) x y → (d : (a : R) → R → Prop) x y

Tactic:
constructor
-- Module: Mathlib.RingTheory.Congruence.Opposite
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
h :
  ∀ {x y : Rᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) c :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) d :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y
mp : ∀ {x y : R}, (c : (a : R) → R → Prop) x y → (d : (a : R) → R → Prop) x y
⊢ ∀ {x y : R}, (c : (a : R) → R → Prop) x y → (d : (a : R) → R → Prop) x y

Tactic:
_
-- Module: Mathlib.RingTheory.Congruence.Opposite
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
h :
  ∀ {x y : Rᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) c :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) d :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y
x : R
mp : ∀ {y : R}, (c : (a : R) → R → Prop) x y → (d : (a : R) → R → Prop) x y
⊢ ∀ {y : R}, (c : (a : R) → R → Prop) x y → (d : (a : R) → R → Prop) x y

Tactic:
_
-- Module: Mathlib.RingTheory.Congruence.Opposite
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
h : ∀ {x y : R}, (c : (a : R) → R → Prop) x y → (d : (a : R) → R → Prop) x y
mpr :
  ∀ {x y : Rᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) c :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) d :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y
⊢ ∀ {x y : Rᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) c :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) d :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y

Tactic:
_
-- Module: Mathlib.RingTheory.Congruence.Opposite
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
h : ∀ {x y : R}, (c : (a : R) → R → Prop) x y → (d : (a : R) → R → Prop) x y
x : Rᵐᵒᵖ
mpr :
  ∀ {y : Rᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) c :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) d :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y
⊢ ∀ {y : Rᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) c :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) d :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y

Tactic:
_
-- Module: Mathlib.RingTheory.Congruence.Opposite
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
h :
  ∀ {x y : Rᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) c :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) d :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y
x y : R
h' : (c : (a : R) → R → Prop) x y
⊢ (d : (a : R) → R → Prop) x y

Tactic:
h h'

Premises used: MulOpposite.unop
-- Module: Mathlib.RingTheory.Congruence.Opposite
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
h :
  ∀ {x y : Rᵐᵒᵖ},
    ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) c :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y →
      ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) d :
            RingCon Rᵐᵒᵖ) :
          (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
        x y
x y : R
h' : (c : (a : R) → R → Prop) x y
⊢ (d : (a : R) → R → Prop) x y

Tactic:
exact h h'
-- Module: Mathlib.RingTheory.Congruence.Opposite
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
h : ∀ {x y : R}, (c : (a : R) → R → Prop) x y → (d : (a : R) → R → Prop) x y
x y : Rᵐᵒᵖ
h' :
  ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) c :
        RingCon Rᵐᵒᵖ) :
      (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
    x y
⊢ ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) d :
        RingCon Rᵐᵒᵖ) :
      (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
    x y

Tactic:
h h'
-- Module: Mathlib.RingTheory.Congruence.Opposite
Goal:
R : Type u_1
inst : Add R
inst_1 : Mul R
c d : RingCon R
h : ∀ {x y : R}, (c : (a : R) → R → Prop) x y → (d : (a : R) → R → Prop) x y
x y : Rᵐᵒᵖ
h' :
  ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) c :
        RingCon Rᵐᵒᵖ) :
      (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
    x y
⊢ ((({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } : (a : RingCon R) → RingCon Rᵐᵒᵖ) d :
        RingCon Rᵐᵒᵖ) :
      (a : Rᵐᵒᵖ) → Rᵐᵒᵖ → Prop)
    x y

Tactic:
exact h h'
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y : R
H_1 : IsCoprime x y
a b : R
H : a * x + b * y = 1
rw : a * x + b * y = 1
rw₁ rw₂ : Eq.{u + 1} (α := R) 1 1
⊢ b * y + a * x = 1

Tactic:
rw [add_comm, H]

Premises used: add_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x y : R
⊢ IsCoprime x y ↔ IsCoprime y x

Tactic:
⟨IsCoprime.symm, IsCoprime.symm⟩

Premises used: IsCoprime.symm, Iff.intro
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x : R
h_1 : IsCoprime x x
a b : R
h : a * x + b * x = 1
rwa : (a + b) * x = 1
rwa₁ rwa₂ rwa₃ rwa₄ : a * x + b * x = 1
⊢ x * (a + b) = 1

Tactic:
rwa [mul_comm, add_mul]

Premises used: add_mul, mul_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x : R
h : IsUnit x
b : R
hb : b * x = 1
rwa : b * x + 0 = 1
rwa₁ rwa₂ rwa₃ rwa₄ : b * x = 1
⊢ b * x + 0 * x = 1

Tactic:
rwa [zero_mul, add_zero]

Premises used: MulZeroClass.zero_mul, add_zero
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x : R
h : IsCoprime 0 x
a b : R
H : a * 0 + b * x = 1
rwa : ∀ (H : 0 + b * x = 1), x * b = 1
rwa₁ : ∀ (H : b * x = 1), x * b = 1
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (H : x * b = 1), x * b = 1
⊢ x * b = 1

Tactic:
rwa [mul_zero, zero_add, mul_comm] at H

Premises used: zero_add, MulZeroClass.mul_zero, mul_comm
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x : R
H : IsUnit x
b : R
hb : b * x = 1
rwa : 0 + b * x = 1
rwa₁ rwa₂ rwa₃ rwa₄ : b * x = 1
⊢ HMul.hMul (α := R) 1 0 + b * x = 1

Tactic:
rwa [one_mul, zero_add]

Premises used: zero_add, one_mul
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
x : R
⊢ IsCoprime x 0 ↔ IsUnit x

Tactic:
isCoprime_comm.trans isCoprime_zero_left

Premises used: isCoprime_comm, isCoprime_zero_left, Iff.trans
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ ¬IsCoprime.{u} (R := R) 0 0

Tactic:
mt isCoprime_zero_right.mp not_isUnit_zero

Premises used: mt, not_isUnit_zero, Iff.mp, isCoprime_zero_right
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
a b : ℤ
h : IsCoprime a b
rcases : ∀ (u v : ℤ) (H : u * a + v * b = 1), IsCoprime.{u_1} (R := R) (↑a : R) (↑b : R)
⊢ IsCoprime.{u_1} (R := R) (↑a : R) (↑b : R)

Tactic:
rcases h with ⟨u, v, H⟩
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
a b u v : ℤ
H : u * a + v * b = 1
h : HMul.hMul (α := R) (↑u : R) (↑a : R) + HMul.hMul (α := R) (↑v : R) (↑b : R) = 1
⊢ IsCoprime.{u_1} (R := R) (↑a : R) (↑b : R)

Tactic:
use u, v
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
a b u v : ℤ
H : u * a + v * b = 1
h : ∀ (H : u * a + v * b = 1), Eq.{u_1 + 1} (α := R) (↑1 : R) 1
⊢ HMul.hMul (α := R) (↑u : R) (↑a : R) + HMul.hMul (α := R) (↑v : R) (↑b : R) = 1

Tactic:
rw_mod_cast [H]
-- Module: Mathlib.RingTheory.Coprime.Basic
Goal:
R : Type u_1
inst : CommRing R
a b u v : ℤ
H : u * a + v * b = 1
⊢ Eq.{u_1 + 1} (α := R) (↑1 : R) 1

Tactic:
Int.cast_one

Premises used: Int.cast_one