awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
⊢ Function.Surjective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑e : (a : R) → S)

Tactic:
EquivLike.surjective e

Premises used: EquivLike.surjective
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
inst : Mul R
inst_1 : Add R
x : R
⊢ (refl R : (a : R) → R) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_7
inst : Mul R
inst_1 : Add R
⊢ Eq (α := (a : R) → R) (⇑(refl R) : (a : R) → R) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
inst : Mul R
inst_1 : Add R
⊢ Eq (α := R ≃+ R) (↑(refl R) : R ≃+ R) (AddEquiv.refl R)

Tactic:
rfl

Premises used: AddEquiv.refl, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
inst : Mul R
inst_1 : Add R
⊢ Eq (α := R ≃* R) (↑(refl R) : R ≃* R) (MulEquiv.refl R)

Tactic:
rfl

Premises used: MulEquiv.refl, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
f : R ≃+* S
⊢ EquivLike.inv f = (⇑f.symm : (a : S) → R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
⊢ Function.Bijective (α := R ≃+* S) RingEquiv.symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, Function.bijective_iff_has_inverse, And.intro, Exists.intro, RingEquiv.symm_symm
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
f : S → R
h₁ : Function.LeftInverse (⇑e : (a : R) → S) f
h₂ : Function.RightInverse (⇑e : (a : R) → S) f
h₃ :
  ∀ (x y : S),
    { toFun := f, invFun := (⇑e : (a : R) → S), left_inv := h₁, right_inv := h₂ : S ≃ R }.toFun (x * y) =
      { toFun := f, invFun := (⇑e : (a : R) → S), left_inv := h₁, right_inv := h₂ : S ≃ R }.toFun x *
        { toFun := f, invFun := (⇑e : (a : R) → S), left_inv := h₁, right_inv := h₂ : S ≃ R }.toFun y
h₄ :
  ∀ (x y : S),
    { toFun := f, invFun := (⇑e : (a : R) → S), left_inv := h₁, right_inv := h₂ : S ≃ R }.toFun (x + y) =
      { toFun := f, invFun := (⇑e : (a : R) → S), left_inv := h₁, right_inv := h₂ : S ≃ R }.toFun x +
        { toFun := f, invFun := (⇑e : (a : R) → S), left_inv := h₁, right_inv := h₂ : S ≃ R }.toFun y
⊢ { toFun := f, invFun := (⇑e : (a : R) → S), left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ :
      S ≃+* R } =
    e.symm

Tactic:
symm_bijective.injective <| ext fun _ => rfl

Premises used: Function.Bijective.injective, RingEquiv.symm_bijective, RingEquiv.ext, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃ S
h₁ : ∀ (x y : R), e.toFun (x * y) = e.toFun x * e.toFun y
h₂ : ∀ (x y : R), e.toFun (x + y) = e.toFun x + e.toFun y
⊢ { toEquiv := e, map_mul' := h₁, map_add' := h₂ : R ≃+* S }.symm = { toEquiv := e.symm, map_mul' := ⋯, map_add' := ⋯ }

Tactic:
rfl

Premises used: Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
inst : Mul R
inst_1 : Add R
⊢ Eq (α := R ≃+* R) (RingEquiv.symm (refl R)) (refl R)

Tactic:
rfl

Premises used: RingEquiv.refl, Equiv.symm, Equiv.refl, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
⊢ (↑e.symm : S ≃ R) = (↑e : R ≃ S).symm

Tactic:
rfl

Premises used: Equiv.symm, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
⊢ Eq (α := S ≃* R) (↑e.symm : S ≃* R) (MulEquiv.symm (↑e : R ≃* S))

Tactic:
rfl

Premises used: Equiv.symm, MulEquiv.symm, MulEquivClass.toMulEquiv, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
⊢ Eq (α := S ≃+ R) (↑e.symm : S ≃+ R) (AddEquiv.symm (↑e : R ≃+ S))

Tactic:
rfl

Premises used: AddEquivClass.toAddEquiv, Equiv.symm, EquivLike.toEquiv, rfl, AddEquiv.symm
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
⊢ ∀ (x : S), (e : (a : R) → S) ((e.symm : (a : S) → R) x : R) = x

Tactic:
e.toEquiv.apply_symm_apply

Premises used: RingEquiv.toEquiv, Equiv.apply_symm_apply
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
⊢ ∀ (x : R), (e.symm : (a : S) → R) ((e : (a : R) → S) x : S) = x

Tactic:
e.toEquiv.symm_apply_apply

Premises used: RingEquiv.toEquiv, Equiv.symm_apply_apply
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
s : Set S
⊢ Eq.{u_4 + 1} (α := Set R) ((⇑e.symm : (a : S) → R) '' s) ((⇑e : (a : R) → S) ⁻¹' s)

Tactic:
e.toEquiv.image_symm_eq_preimage _

Premises used: RingEquiv.toEquiv, Equiv.image_symm_eq_preimage
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
s : Set R
⊢ Eq.{u_5 + 1} (α := Set S) ((⇑e : (a : R) → S) '' s) ((⇑e.symm : (a : S) → R) ⁻¹' s)

Tactic:
e.toEquiv.image_eq_preimage_symm _

Premises used: RingEquiv.toEquiv, Equiv.image_eq_preimage_symm
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
⊢ Eq (α := (a : S) → R) (⇑(↑e : R ≃ S).symm : (a : S) → R) (⇑e.symm : (a : S) → R)

Tactic:
rfl

Premises used: EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
⊢ Eq (α := (a : S) → R) (⇑(MulEquiv.symm (↑e : R ≃* S)) : (a : S) → R) (⇑e.symm : (a : S) → R)

Tactic:
rfl

Premises used: EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
⊢ Eq (α := (a : S) → R) (⇑(AddEquiv.symm (↑e : R ≃+ S)) : (a : S) → R) (⇑e.symm : (a : S) → R)

Tactic:
rfl

Premises used: EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
x : S
y : R
⊢ (e.symm : (a : S) → R) x = y ↔ x = (e : (a : R) → S) y

Tactic:
Equiv.symm_apply_eq _

Premises used: Equiv.symm_apply_eq
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
e : R ≃+* S
x : S
y : R
⊢ y = (e.symm : (a : S) → R) x ↔ (e : (a : R) → S) y = x

Tactic:
Equiv.eq_symm_apply _

Premises used: Equiv.eq_symm_apply
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
S' : Type u_6
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
inst_4 : Mul S'
inst_5 : Add S'
e₁ : R ≃+* S
e₂ : S ≃+* S'
⊢ Eq (α := (a : R) → S') (⇑(e₁.trans e₂) : (a : R) → S')
    (Function.comp.{u_4 + 1, u_5 + 1, u_6 + 1} (β := S) (⇑e₂ : (a : S) → S') (⇑e₁ : (a : R) → S))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
S' : Type u_6
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
inst_4 : Mul S'
inst_5 : Add S'
e₁ : R ≃+* S
e₂ : S ≃+* S'
a : R
⊢ Eq.{u_6 + 1} (α := S') ((e₁.trans e₂ : (a : R) → S') a : S') ((e₂ : (a : S) → S') ((e₁ : (a : R) → S) a : S) : S')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
S' : Type u_6
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
inst_4 : Mul S'
inst_5 : Add S'
e₁ : R ≃+* S
e₂ : S ≃+* S'
a : S'
⊢ Eq.{u_4 + 1} (α := R) (((e₁.trans e₂).symm : (a : S') → R) a : R)
    ((e₁.symm : (a : S) → R) ((e₂.symm : (a : S') → S) a : S) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
S' : Type u_6
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
inst_4 : Mul S'
inst_5 : Add S'
e₁ : R ≃+* S
e₂ : S ≃+* S'
⊢ (e₁.trans e₂).symm = e₂.symm.trans e₁.symm

Tactic:
rfl

Premises used: Equiv.trans, RingEquiv.trans, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
S' : Type u_6
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
inst_4 : Mul S'
inst_5 : Add S'
e₁ : R ≃+* S
e₂ : S ≃+* S'
⊢ Eq (α := R ≃* S') (↑(e₁.trans e₂) : R ≃* S') (MulEquiv.trans (↑e₁ : R ≃* S) (↑e₂ : S ≃* S'))

Tactic:
rfl

Premises used: Equiv.trans, MulEquiv.trans, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
S' : Type u_6
inst : Mul R
inst_1 : Mul S
inst_2 : Add R
inst_3 : Add S
inst_4 : Mul S'
inst_5 : Add S'
e₁ : R ≃+* S
e₂ : S ≃+* S'
⊢ Eq (α := R ≃+ S') (↑(e₁.trans e₂) : R ≃+ S') (AddEquiv.trans (↑e₁ : R ≃+ S) (↑e₂ : S ≃+ S'))

Tactic:
rfl

Premises used: Equiv.trans, AddEquiv.trans, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
inst : NonUnitalCommSemiring R
r : R
⊢ (toOpposite R : (a : R) → Rᵐᵒᵖ) r = op r

Tactic:
rfl

Premises used: rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
inst : NonUnitalCommSemiring R
r : Rᵐᵒᵖ
⊢ (RingEquiv.symm (toOpposite R) : (a : Rᵐᵒᵖ) → R) r = unop r

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R ≃+* S
⊢ Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) 0 : S) (0 : S)

Tactic:
map_zero f

Premises used: map_zero
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R ≃+* S
x : R
⊢ Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) ↔ x = 0

Tactic:
EmbeddingLike.map_eq_zero_iff

Premises used: EmbeddingLike.map_eq_zero_iff
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R ≃+* S
x : R
⊢ Ne.{u_5 + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) ↔ x ≠ 0

Tactic:
EmbeddingLike.map_ne_zero_iff

Premises used: EmbeddingLike.map_ne_zero_iff
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
F : Type u_1
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
hf : Function.Bijective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Eq (α := (a : R) → S) (⇑(ofBijective f hf) : (a : R) → S) (⇑f : (a : R) → S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
F : Type u_1
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
inst_2 : FunLike F R S
inst_3 : NonUnitalRingHomClass F R S
f : F
hf : Function.Bijective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : R
⊢ Eq.{u_5 + 1} (α := S) ((ofBijective f hf : (a : R) → S) x : S) ((f : (a : R) → S) x : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
hf : Function.Bijective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a :
  ∀ (x : R),
    Eq (α := R) ((NonUnitalRingHom.comp (↑(RingEquiv.symm (ofBijective f hf)) : S →ₙ+* R) f : (a : R) → R) x : R)
      ((NonUnitalRingHom.id R : (a : R) → R) x : R)
⊢ NonUnitalRingHom.comp (↑(RingEquiv.symm (ofBijective f hf)) : S →ₙ+* R) f = NonUnitalRingHom.id R

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
hf : Function.Bijective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : R
⊢ Eq (α := R) ((NonUnitalRingHom.comp (↑(RingEquiv.symm (ofBijective f hf)) : S →ₙ+* R) f : (a : R) → R) x : R)
    ((NonUnitalRingHom.id R : (a : R) → R) x : R)

Tactic:
(RingEquiv.ofBijective f hf).injective <| RingEquiv.apply_symm_apply ..

Premises used: RingEquiv.apply_symm_apply, RingEquiv.ofBijective, RingEquiv.injective
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
hf : Function.Bijective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : R
⊢ Eq (α := R) ((NonUnitalRingHom.comp (↑(RingEquiv.symm (ofBijective f hf)) : S →ₙ+* R) f : (a : R) → R) x : R)
    ((NonUnitalRingHom.id R : (a : R) → R) x : R)

Tactic:
exact (RingEquiv.ofBijective f hf).injective <| RingEquiv.apply_symm_apply ..

Premises used: RingEquiv.apply_symm_apply, RingEquiv.ofBijective, RingEquiv.injective
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
hf : Function.Bijective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
a :
  ∀ (x : S),
    Eq (α := S) ((f.comp (↑(RingEquiv.symm (ofBijective f hf)) : S →ₙ+* R) : (a : S) → S) x : S)
      ((NonUnitalRingHom.id S : (a : S) → S) x : S)
⊢ f.comp (↑(RingEquiv.symm (ofBijective f hf)) : S →ₙ+* R) = NonUnitalRingHom.id S

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
hf : Function.Bijective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : S
⊢ Eq (α := S) ((f.comp (↑(RingEquiv.symm (ofBijective f hf)) : S →ₙ+* R) : (a : S) → S) x : S)
    ((NonUnitalRingHom.id S : (a : S) → S) x : S)

Tactic:
(RingEquiv.ofBijective f hf).symm.injective <| RingEquiv.apply_symm_apply ..

Premises used: RingEquiv.apply_symm_apply, RingEquiv.ofBijective, RingEquiv.injective, RingEquiv.symm
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R →ₙ+* S
hf : Function.Bijective.{u_4 + 1, u_5 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
x : S
⊢ Eq (α := S) ((f.comp (↑(RingEquiv.symm (ofBijective f hf)) : S →ₙ+* R) : (a : S) → S) x : S)
    ((NonUnitalRingHom.id S : (a : S) → S) x : S)

Tactic:
exact (RingEquiv.ofBijective f hf).symm.injective <| RingEquiv.apply_symm_apply ..

Premises used: RingEquiv.apply_symm_apply, RingEquiv.ofBijective, RingEquiv.injective, RingEquiv.symm
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
ι : Type u_7
R : ι → Type u_8
inst : (i : ι) → NonUnitalNonAssocSemiring (R i)
⊢ Eq (α := ((i : ι) → R i) ≃+* ((i : ι) → R i)) (piCongrRight (R := R) (S := R) fun (i : ι) ↦ refl (R i))
    (refl ((i : ι) → R i))

Tactic:
rfl

Premises used: RingEquiv.refl, Equiv.refl, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
ι : Type u_7
R : ι → Type u_8
S : ι → Type u_9
inst : (i : ι) → NonUnitalNonAssocSemiring (R i)
inst_1 : (i : ι) → NonUnitalNonAssocSemiring (S i)
e : (i : ι) → RingEquiv.{u_8, u_9} (R i) (S i)
⊢ (piCongrRight (R := R) (S := S) e).symm = piCongrRight (R := S) (S := R) fun (i : ι) ↦ (e i).symm

Tactic:
rfl

Premises used: RingEquiv.piCongrRight, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
ι : Type u_7
R : ι → Type u_8
S : ι → Type u_9
T : ι → Type u_10
inst : (i : ι) → NonUnitalNonAssocSemiring (R i)
inst_1 : (i : ι) → NonUnitalNonAssocSemiring (S i)
inst_2 : (i : ι) → NonUnitalNonAssocSemiring (T i)
e : (i : ι) → RingEquiv.{u_8, u_9} (R i) (S i)
f : (i : ι) → RingEquiv.{u_9, u_10} (S i) (T i)
⊢ (piCongrRight (R := R) (S := S) e).trans (piCongrRight (R := S) (S := T) f) =
    piCongrRight (R := R) (S := T) fun (i : ι) ↦ (e i).trans (f i)

Tactic:
rfl

Premises used: Equiv.trans, RingEquiv.piCongrRight, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
α : Type u_2
β : Type u_3
R : Type u_7
inst : NonUnitalNonAssocSemiring R
e : α ≃ β
⊢ Eq (α := ((i : β) → R) ≃+* ((i : α) → R))
    (RingEquiv.symm (piCongrLeft' (fun (x : α) ↦ R) e) : ((i : β) → R) ≃+* ((i : α) → R))
    (piCongrLeft' (fun (i : β) ↦ R) e.symm : ((i : β) → R) ≃+* ((i : α) → R))

Tactic:
simp only [piCongrLeft', RingEquiv.symm, MulEquiv.symm, Equiv.piCongrLeft'_symm]

Premises used: Equiv.piCongrLeft'_symm, RingEquiv.piCongrLeft', MulEquiv.symm, RingEquiv.symm
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
R_1 : Type u_4
S_1 : Type u_5
S'_1 : Type u_6
inst : NonUnitalNonAssocSemiring R_1
inst_1 : NonUnitalNonAssocSemiring S_1
f_1 : R_1 ≃+* S_1
x : R_1
inst_2 : FunLike F R_1 S_1
R : Type u_7
R' : Type u_8
S : Type u_9
S' : Type u_10
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : NonUnitalNonAssocSemiring R'
inst_5 : NonUnitalNonAssocSemiring S
inst_6 : NonUnitalNonAssocSemiring S'
f : R ≃+* R'
g : S ≃+* S'
x_1 x_2 : R × S
⊢ ((↑f : R ≃ R').prodCongr (↑g : S ≃ S')).toFun (x_1 * x_2) =
    ((↑f : R ≃ R').prodCongr (↑g : S ≃ S')).toFun x_1 * ((↑f : R ≃ R').prodCongr (↑g : S ≃ S')).toFun x_2

Tactic:
simp only [Equiv.toFun_as_coe, Equiv.prodCongr_apply, EquivLike.coe_coe,
      Prod.map, map_mul, Prod.mk_mul_mk]

Premises used: Equiv.toFun_as_coe, Equiv.prodCongr_apply, Prod.map, map_mul, Prod.mk_mul_mk, EquivLike.coe_coe
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
F : Type u_1
α : Type u_2
β : Type u_3
R_1 : Type u_4
S_1 : Type u_5
S'_1 : Type u_6
inst : NonUnitalNonAssocSemiring R_1
inst_1 : NonUnitalNonAssocSemiring S_1
f_1 : R_1 ≃+* S_1
x : R_1
inst_2 : FunLike F R_1 S_1
R : Type u_7
R' : Type u_8
S : Type u_9
S' : Type u_10
inst_3 : NonUnitalNonAssocSemiring R
inst_4 : NonUnitalNonAssocSemiring R'
inst_5 : NonUnitalNonAssocSemiring S
inst_6 : NonUnitalNonAssocSemiring S'
f : R ≃+* R'
g : S ≃+* S'
x_1 x_2 : R × S
⊢ ((↑f : R ≃ R').prodCongr (↑g : S ≃ S')).toFun (x_1 + x_2) =
    ((↑f : R ≃ R').prodCongr (↑g : S ≃ S')).toFun x_1 + ((↑f : R ≃ R').prodCongr (↑g : S ≃ S')).toFun x_2

Tactic:
simp only [Equiv.toFun_as_coe, Equiv.prodCongr_apply, EquivLike.coe_coe,
      Prod.map, map_add, Prod.mk_add_mk]

Premises used: Prod.mk_add_mk, Equiv.toFun_as_coe, map_add, Equiv.prodCongr_apply, Prod.map, EquivLike.coe_coe
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_7
R' : Type u_8
S : Type u_9
S' : Type u_10
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring R'
inst_2 : NonUnitalNonAssocSemiring S
inst_3 : NonUnitalNonAssocSemiring S'
f : R ≃+* R'
g : S ≃+* S'
⊢ Eq (α := (a : R × S) → R' × S') (⇑(f.prodCongr g) : (a : R × S) → R' × S')
    (Prod.map (⇑f : (a : R) → R') (⇑g : (a : S) → S'))

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R ≃+* S
⊢ Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) 1 : S) (1 : S)

Tactic:
map_one f

Premises used: map_one
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R ≃+* S
x : R
⊢ Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) x : S) (1 : S) ↔ x = 1

Tactic:
EmbeddingLike.map_eq_one_iff

Premises used: EmbeddingLike.map_eq_one_iff
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
f : R ≃+* S
x : R
⊢ Ne.{u_5 + 1} (α := S) ((f : (a : R) → S) x : S) (1 : S) ↔ x ≠ 1

Tactic:
EmbeddingLike.map_ne_one_iff

Premises used: EmbeddingLike.map_ne_one_iff
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
inst : NonAssocSemiring R
⊢ Eq (α := R →* R) (↑(refl R) : R →* R) (MonoidHom.id R)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
inst : NonAssocSemiring R
⊢ Eq (α := R →+ R) (↑(refl R) : R →+ R) (AddMonoidHom.id R)

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
inst : NonAssocSemiring R
⊢ Eq (α := R →+* R) (↑(refl R) : R →+* R) (RingHom.id R)

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
S' : Type u_6
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring S'
e₁ : R ≃+* S
e₂ : S ≃+* S'
⊢ Eq (α := R →* S') (↑(e₁.trans e₂) : R →* S') (MonoidHom.comp (↑e₂ : S →* S') (↑e₁ : R →* S))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
S' : Type u_6
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonUnitalNonAssocSemiring S'
e₁ : R ≃+* S
e₂ : S ≃+* S'
⊢ Eq (α := R →+ S') (↑(e₁.trans e₂) : R →+ S') (AddMonoidHom.comp (↑e₂ : S →+ S') (↑e₁ : R →+ S))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
S' : Type u_6
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring S'
e₁ : R ≃+* S
e₂ : S ≃+* S'
⊢ Eq (α := R →+* S') (↑(e₁.trans e₂) : R →+* S') (@RingHom.comp _ _ _ _ inst_1 _ (↑e₂ : S →+* S') (↑e₁ : R →+* S))

Tactic:
rfl

Premises used: MonoidHomClass.toMonoidHom, RingHomClass.toRingHom, rfl
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
e : R ≃+* S
⊢ Eq (α := S →+* S) (@RingHom.comp _ _ _ _ inst _ (↑e : R →+* S) (↑e.symm : S →+* R)) (RingHom.id S)

Tactic:
RingHom.ext e.apply_symm_apply

Premises used: RingEquiv.apply_symm_apply, RingHom.ext
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
e : R ≃+* S
⊢ Eq (α := R →+* R) (@RingHom.comp _ _ _ _ inst_1 _ (↑e.symm : S →+* R) (↑e : R →+* S)) (RingHom.id R)

Tactic:
RingHom.ext e.symm_apply_apply

Premises used: RingEquiv.symm_apply_apply, RingHom.ext
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R ≃+* S
x : R
⊢ Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) (-x) : S) (-(f : (a : R) → S) x : S)

Tactic:
map_neg f x

Premises used: map_neg
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocRing R
inst_1 : NonUnitalNonAssocRing S
f : R ≃+* S
x y : R
⊢ (f : (a : R) → S) (x - y) = HSub.hSub (α := S) (β := S) ((f : (a : R) → S) x : S) ((f : (a : R) → S) y : S)

Tactic:
map_sub f x y

Premises used: map_sub
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R ≃+* S
⊢ Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) (-1) : S) (-1 : S)

Tactic:
f.map_one ▸ f.map_neg 1

Premises used: RingEquiv.map_neg, RingEquiv.map_one, Eq.rec, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonAssocRing R
inst_1 : NonAssocRing S
f : R ≃+* S
x : R
rw : Eq.{u_5 + 1} (α := S) (-(f : (a : R) → S) x : S) (1 : S) ↔ x = -1
rw₁ : Eq.{u_5 + 1} (α := S) (-(f : (a : R) → S) x : S) (1 : S) ↔ -x = 1
rw₂ : Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) (-x) : S) (1 : S) ↔ -x = 1
rw₃ rw₄ : -x = 1 ↔ -x = 1
⊢ Eq.{u_5 + 1} (α := S) ((f : (a : R) → S) x : S) (-1 : S) ↔ x = -1

Tactic:
rw [← neg_eq_iff_eq_neg, ← neg_eq_iff_eq_neg, ← map_neg, RingEquiv.map_eq_one_iff]

Premises used: RingEquiv.map_eq_one_iff, neg_eq_iff_eq_neg, map_neg
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
⊢ Function.Injective (α := R ≃+* S) toNonUnitalRingHom

Tactic:
fun _ _ h =>
  RingEquiv.ext (NonUnitalRingHom.ext_iff.1 h)

Premises used: NonUnitalRingHom.ext_iff, RingEquiv.ext, Iff.mp, Function.Injective
-- Module: Mathlib.Algebra.Ring.Equiv
Goal:
R : Type u_4
S : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
f : R ≃+* S
⊢ f.toNonUnitalRingHom = (↑f : R →ₙ+* S)

Tactic:
rfl

Premises used: MulHomClass.toMulHom, RingEquiv.toNonUnitalRingHom, NonUnitalRingHomClass.toNonUnitalRingHom, rfl