awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Ring.Pointwise.Set
Goal:
α : Type u_1
inst : Distrib α
s t u : Set α
⊢ (s + t) * u ⊆ s * u + t * u

Tactic:
image2_distrib_subset_right add_mul

Premises used: add_mul, Set.image2_distrib_subset_right
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : Distrib R
inst_1 : Distrib S
x x_1 x_2 : R × S
fst : (x * (x_1 + x_2)).1 = (x * x_1 + x * x_2).1
snd : (x * (x_1 + x_2)).2 = (x * x_1 + x * x_2).2
⊢ x * (x_1 + x_2) = x * x_1 + x * x_2

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : Distrib R
inst_1 : Distrib S
x x_1 x_2 : R × S
⊢ (x * (x_1 + x_2)).1 = (x * x_1 + x * x_2).1

Tactic:
left_distrib ..

Premises used: left_distrib
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : Distrib R
inst_1 : Distrib S
x x_1 x_2 : R × S
⊢ (x * (x_1 + x_2)).1 = (x * x_1 + x * x_2).1

Tactic:
exact left_distrib ..

Premises used: left_distrib
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : Distrib R
inst_1 : Distrib S
x x_1 x_2 : R × S
⊢ (x * (x_1 + x_2)).2 = (x * x_1 + x * x_2).2

Tactic:
left_distrib ..

Premises used: left_distrib
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : Distrib R
inst_1 : Distrib S
x x_1 x_2 : R × S
⊢ (x * (x_1 + x_2)).2 = (x * x_1 + x * x_2).2

Tactic:
exact left_distrib ..

Premises used: left_distrib
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : Distrib R
inst_1 : Distrib S
x x_1 x_2 : R × S
fst : ((x + x_1) * x_2).1 = (x * x_2 + x_1 * x_2).1
snd : ((x + x_1) * x_2).2 = (x * x_2 + x_1 * x_2).2
⊢ (x + x_1) * x_2 = x * x_2 + x_1 * x_2

Tactic:
ext
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : Distrib R
inst_1 : Distrib S
x x_1 x_2 : R × S
⊢ ((x + x_1) * x_2).1 = (x * x_2 + x_1 * x_2).1

Tactic:
right_distrib ..

Premises used: right_distrib
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : Distrib R
inst_1 : Distrib S
x x_1 x_2 : R × S
⊢ ((x + x_1) * x_2).1 = (x * x_2 + x_1 * x_2).1

Tactic:
exact right_distrib ..

Premises used: right_distrib
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : Distrib R
inst_1 : Distrib S
x x_1 x_2 : R × S
⊢ ((x + x_1) * x_2).2 = (x * x_2 + x_1 * x_2).2

Tactic:
right_distrib ..

Premises used: right_distrib
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : Distrib R
inst_1 : Distrib S
x x_1 x_2 : R × S
⊢ ((x + x_1) * x_2).2 = (x * x_2 + x_1 * x_2).2

Tactic:
exact right_distrib ..

Premises used: right_distrib
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
S : Type u_3
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
⊢ Eq (α := (a : R × S) → R) (⇑(fst R S) : (a : R × S) → R) Prod.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
S : Type u_3
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
⊢ Eq (α := (a : R × S) → S) (⇑(snd R S) : (a : R × S) → S) Prod.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
S : Type u_3
T : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
inst_2 : NonUnitalNonAssocSemiring T
f : R →ₙ+* S
g : R →ₙ+* T
x : R
⊢ Eq (α := S × T) ((f.prod g : (a : R) → S × T) x : S × T) (((f : (a : R) → S) x, (g : (a : R) → T) x) : S × T)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
S : Type u_3
T : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
inst_2 : NonUnitalNonAssocSemiring T
f : R →ₙ+* S
g : R →ₙ+* T
⊢ comp (fst S T) (f.prod g) = f

Tactic:
ext fun _ => rfl

Premises used: NonUnitalRingHom.ext, rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
S : Type u_3
T : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
inst_2 : NonUnitalNonAssocSemiring T
f : R →ₙ+* S
g : R →ₙ+* T
⊢ comp (snd S T) (f.prod g) = g

Tactic:
ext fun _ => rfl

Premises used: NonUnitalRingHom.ext, rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
S : Type u_3
T : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
inst_2 : NonUnitalNonAssocSemiring T
f : R →ₙ+* S × T
x : R
⊢ Eq (α := S × T) (((comp (fst S T) f).prod (comp (snd S T) f) : (a : R) → S × T) x : S × T)
    ((f : (a : R) → S × T) x : S × T)

Tactic:
simp only [prod_apply, coe_fst, coe_snd, comp_apply]

Premises used: NonUnitalRingHom.coe_snd, NonUnitalRingHom.comp_apply, NonUnitalRingHom.coe_fst, NonUnitalRingHom.prod_apply
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
inst_2 : NonUnitalNonAssocSemiring R'
inst_3 : NonUnitalNonAssocSemiring S'
f : R →ₙ+* R'
g : S →ₙ+* S'
⊢ f.prodMap g = NonUnitalRingHom.prod (f.comp (fst R S)) (g.comp (snd R S))

Tactic:
rfl

Premises used: NonUnitalRingHom.prodMap, rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
inst_2 : NonUnitalNonAssocSemiring R'
inst_3 : NonUnitalNonAssocSemiring S'
f : R →ₙ+* R'
g : S →ₙ+* S'
⊢ Eq (α := (a : R × S) → R' × S') (⇑(f.prodMap 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.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : NonUnitalNonAssocSemiring R
inst_1 : NonUnitalNonAssocSemiring S
inst_2 : NonUnitalNonAssocSemiring R'
inst_3 : NonUnitalNonAssocSemiring S'
inst_4 : NonUnitalNonAssocSemiring T
f : T →ₙ+* R
g : T →ₙ+* S
f' : R →ₙ+* R'
g' : S →ₙ+* S'
⊢ (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

Tactic:
rfl

Premises used: NonUnitalRingHom.prod, rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R_1 : Type u_1
R' : Type u_2
S_1 : Type u_3
S' : Type u_4
T : Type u_5
inst : NonAssocSemiring R_1
inst_1 : NonAssocSemiring S_1
R : Type u_6
S : Type u_7
inst_2 : Semiring R
inst_3 : Semiring S
⊢ RingHomSurjective (R₁ := R × S) (R₂ := R) (fst R S)

Tactic:
⟨(⟨⟨·, 0⟩, rfl⟩)⟩

Premises used: Prod.mk, RingHomSurjective.mk, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R_1 : Type u_1
R' : Type u_2
S_1 : Type u_3
S' : Type u_4
T : Type u_5
inst : NonAssocSemiring R_1
inst_1 : NonAssocSemiring S_1
R : Type u_6
S : Type u_7
inst_2 : Semiring R
inst_3 : Semiring S
⊢ RingHomSurjective (R₁ := R × S) (R₂ := S) (snd R S)

Tactic:
⟨(⟨⟨0, ·⟩, rfl⟩)⟩

Premises used: Prod.mk, RingHomSurjective.mk, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
S : Type u_3
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
⊢ Eq (α := (a : R × S) → R) (⇑(fst R S) : (a : R × S) → R) Prod.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
S : Type u_3
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
⊢ Eq (α := (a : R × S) → S) (⇑(snd R S) : (a : R × S) → S) Prod.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
S : Type u_3
T : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring T
f : R →+* S
g : R →+* T
x : R
⊢ Eq (α := S × T) ((f.prod g : (a : R) → S × T) x : S × T) (((f : (a : R) → S) x, (g : (a : R) → T) x) : S × T)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
S : Type u_3
T : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring T
f : R →+* S
g : R →+* T
⊢ comp (fst S T) (f.prod g) = f

Tactic:
ext fun _ => rfl

Premises used: RingHom.ext, rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
S : Type u_3
T : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring T
f : R →+* S
g : R →+* T
⊢ comp (snd S T) (f.prod g) = g

Tactic:
ext fun _ => rfl

Premises used: RingHom.ext, rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
S : Type u_3
T : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring T
f : R →+* S × T
x : R
⊢ Eq (α := S × T) (((comp (fst S T) f).prod (comp (snd S T) f) : (a : R) → S × T) x : S × T)
    ((f : (a : R) → S × T) x : S × T)

Tactic:
simp only [prod_apply, coe_fst, coe_snd, comp_apply]

Premises used: RingHom.coe_fst, RingHom.coe_snd, RingHom.comp_apply, RingHom.prod_apply
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring R'
inst_3 : NonAssocSemiring S'
f : R →+* R'
g : S →+* S'
⊢ f.prodMap g = RingHom.prod (f.comp (fst R S)) (g.comp (snd R S))

Tactic:
rfl

Premises used: rfl, RingHom.prodMap
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring R'
inst_3 : NonAssocSemiring S'
f : R →+* R'
g : S →+* S'
⊢ Eq (α := (a : R × S) → R' × S') (⇑(f.prodMap 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.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring R'
inst_3 : NonAssocSemiring S'
inst_4 : NonAssocSemiring T
f : T →+* R
g : T →+* S
f' : R →+* R'
g' : S →+* S'
⊢ (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

Tactic:
rfl

Premises used: RingHom.prod, rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
S : Type u_3
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
⊢ Eq (α := (a : R × S) → S × R) (⇑prodComm : (a : R × S) → S × R) Prod.swap

Tactic:
rfl

Premises used: Prod.swap, rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
S : Type u_3
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
⊢ Eq (α := (a : S × R) → R × S) (⇑(RingEquiv.symm prodComm) : (a : S × R) → R × S) Prod.swap

Tactic:
rfl

Premises used: Prod.swap, rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
S : Type u_3
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
⊢ Eq (α := R × S →+* S)
    (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (RingHom.fst S R) (↑prodComm : R × S →+* S × R))
    (RingHom.snd R S)

Tactic:
RingHom.ext fun _ => rfl

Premises used: RingHom.ext, rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
S : Type u_3
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
⊢ Eq (α := R × S →+* R)
    (@RingHom.comp _ _ _ _ Prod.instNonAssocSemiring _ (RingHom.snd S R) (↑prodComm : R × S →+* S × R))
    (RingHom.fst R S)

Tactic:
RingHom.ext fun _ => rfl

Premises used: RingHom.ext, rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring R'
inst_3 : NonAssocSemiring S'
⊢ Eq (α := (R × S) × R' × S' ≃+* (R × R') × S × S') (RingEquiv.symm (prodProdProdComm R R' S S'))
    (prodProdProdComm R S R' S')

Tactic:
rfl

Premises used: RingEquiv.prodProdProdComm, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring R'
inst_3 : NonAssocSemiring S'
⊢ Eq (α := (R × R') × S × S' ≃+ (R × S) × R' × S')
    (↑(prodProdProdComm R R' S S') : (R × R') × S × S' ≃+ (R × S) × R' × S') (AddEquiv.prodProdProdComm R R' S S')

Tactic:
rfl

Premises used: AddEquiv.prodProdProdComm, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring R'
inst_3 : NonAssocSemiring S'
⊢ Eq (α := (R × R') × S × S' ≃* (R × S) × R' × S')
    (↑(prodProdProdComm R R' S S') : (R × R') × S × S' ≃* (R × S) × R' × S') (MulEquiv.prodProdProdComm R R' S S')

Tactic:
rfl

Premises used: MulEquiv.prodProdProdComm, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring R'
inst_3 : NonAssocSemiring S'
⊢ (↑(prodProdProdComm R R' S S') : (R × R') × S × S' ≃ (R × S) × R' × S') = Equiv.prodProdProdComm R R' S S'

Tactic:
rfl

Premises used: Equiv.prodProdProdComm, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring R'
inst_3 : NonAssocSemiring S'
inst_4 : Subsingleton S
x : R × S
mk : ∀ (fst : R) (snd : S), (fun (x : R) ↦ ((x, 0) : R × S)) (fst, snd).1 = (fst, snd)
⊢ (fun (x : R) ↦ ((x, 0) : R × S)) x.1 = x

Tactic:
cases x
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring R'
inst_3 : NonAssocSemiring S'
inst_4 : Subsingleton S
fst : R
snd : S
⊢ (fun (x : R) ↦ ((x, 0) : R × S)) (fst, snd).1 = (fst, snd)

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring R'
inst_3 : NonAssocSemiring S'
inst_4 : Subsingleton S
⊢ ∀ (x y : R), (x * y, 0) = HMul.hMul (α := R × S) (x, 0) (y, 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring R'
inst_3 : NonAssocSemiring S'
inst_4 : Subsingleton S
⊢ ∀ (x y : R), (x + y, 0) = HAdd.hAdd (α := R × S) (x, 0) (y, 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring R'
inst_3 : NonAssocSemiring S'
inst_4 : Subsingleton S
x : S × R
mk : ∀ (fst : S) (snd : R), (fun (x : R) ↦ ((0, x) : S × R)) (fst, snd).2 = (fst, snd)
⊢ (fun (x : R) ↦ ((0, x) : S × R)) x.2 = x

Tactic:
cases x
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring R'
inst_3 : NonAssocSemiring S'
inst_4 : Subsingleton S
fst : S
snd : R
⊢ (fun (x : R) ↦ ((0, x) : S × R)) (fst, snd).2 = (fst, snd)

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring R'
inst_3 : NonAssocSemiring S'
inst_4 : Subsingleton S
⊢ ∀ (x y : R), (0, x * y) = HMul.hMul (α := S × R) (0, x) (0, y)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst : NonAssocSemiring R
inst_1 : NonAssocSemiring S
inst_2 : NonAssocSemiring R'
inst_3 : NonAssocSemiring S'
inst_4 : Subsingleton S
⊢ ∀ (x y : R), (0, x + y) = HAdd.hAdd (α := S × R) (0, x) (0, y)

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsDomain (R × S)
inst_3 : Nontrivial R
inst_4 : Nontrivial S
⊢ HMul.hMul (α := R × S) (0, 1) (1, 0) = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsDomain (R × S)
inst_3 : Nontrivial R
inst_4 : Nontrivial S
⊢ Eq (α := R × S) (0, 1) 0 ∨ Eq (α := R × S) (1, 0) 0

Tactic:
have :=
    NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero (show ((0 : R), (1 : S)) * (1, 0) = 0 by simp)
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsDomain (R × S)
inst_3 : Nontrivial R
inst_4 : Nontrivial S
this : Eq (α := R × S) (0, 1) 0 ∨ Eq (α := R × S) (1, 0) 0
⊢ Eq.{u_6 + 1} (α := R) 0 0 ∧ Eq.{u_7 + 1} (α := S) 1 0 ∨ Eq.{u_6 + 1} (α := R) 1 0 ∧ Eq.{u_7 + 1} (α := S) 0 0

Tactic:
rw [Prod.mk_eq_zero, Prod.mk_eq_zero] at this

Premises used: Prod.mk_eq_zero
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsDomain (R × S)
inst_3 : Nontrivial R
inst_4 : Nontrivial S
this : Eq.{u_6 + 1} (α := R) 0 0 ∧ Eq.{u_7 + 1} (α := S) 1 0 ∨ Eq.{u_6 + 1} (α := R) 1 0 ∧ Eq.{u_7 + 1} (α := S) 0 0
inl : Eq.{u_6 + 1} (α := R) 0 0 → ∀ (h : Eq.{u_7 + 1} (α := S) 1 0), False
inr : ∀ (h : Eq.{u_6 + 1} (α := R) 1 0), Eq.{u_7 + 1} (α := S) 0 0 → False
⊢ False

Tactic:
rcases this with (⟨_, h⟩ | ⟨h, _⟩)
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsDomain (R × S)
inst_3 : Nontrivial R
inst_4 : Nontrivial S
left : Eq.{u_6 + 1} (α := R) 0 0
h : Eq.{u_7 + 1} (α := S) 1 0
⊢ False

Tactic:
zero_ne_one h.symm

Premises used: zero_ne_one, Eq.symm
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsDomain (R × S)
inst_3 : Nontrivial R
inst_4 : Nontrivial S
left : Eq.{u_6 + 1} (α := R) 0 0
h : Eq.{u_7 + 1} (α := S) 1 0
⊢ False

Tactic:
exact zero_ne_one h.symm

Premises used: zero_ne_one, Eq.symm
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsDomain (R × S)
inst_3 : Nontrivial R
inst_4 : Nontrivial S
h : Eq.{u_6 + 1} (α := R) 1 0
right : Eq.{u_7 + 1} (α := S) 0 0
⊢ False

Tactic:
zero_ne_one h.symm

Premises used: zero_ne_one, Eq.symm
-- Module: Mathlib.Algebra.Ring.Prod
Goal:
R : Type u_6
S : Type u_7
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsDomain (R × S)
inst_3 : Nontrivial R
inst_4 : Nontrivial S
h : Eq.{u_6 + 1} (α := R) 1 0
right : Eq.{u_7 + 1} (α := S) 0 0
⊢ False

Tactic:
exact zero_ne_one h.symm

Premises used: zero_ne_one, Eq.symm
-- Module: Mathlib.Algebra.Ring.Rat
Goal:
n : ℕ
⊢ (↑(↑(n + 1) : ℤ) : ℚ) = HAdd.hAdd (α := ℚ) (↑(↑n : ℤ) : ℚ) 1

Tactic:
simp only [intCast_eq_divInt, divInt_add_divInt _ _ Int.one_ne_zero Int.one_ne_zero,
      ← divInt_one_one, Int.natCast_add, Int.natCast_one, mul_one]

Premises used: Int.natCast_add, Rat.divInt_one_one, Int.one_ne_zero, Rat.divInt_add_divInt, Rat.intCast_eq_divInt, Int.natCast_one, mul_one
-- Module: Mathlib.Algebra.Ring.Rat
Goal:
x : ℕ
x_1 : ℚ
rw : x_1 ^ x.succ = HPow.hPow (β := ℤ) x_1 (↑x : ℤ) * x_1
rw₁ : x_1 ^ x.succ = x_1 ^ x * x_1
rw₂ rw₃ : x_1 ^ x * x_1 = x_1 ^ x * x_1
⊢ HPow.hPow (β := ℤ) x_1 (↑x.succ : ℤ) = HPow.hPow (β := ℤ) x_1 (↑x : ℤ) * x_1

Tactic:
rw [Rat.zpow_natCast, Rat.zpow_natCast, Rat.pow_succ]

Premises used: Rat.zpow_natCast, Rat.pow_succ
-- Module: Mathlib.Algebra.Ring.Rat
Goal:
⊢ IsDomain ℚ

Tactic:
NoZeroDivisors.to_isDomain _

Premises used: NoZeroDivisors.to_isDomain
-- Module: Mathlib.Algebra.Ring.Rat
Goal:
a b : ℕ
hab : Eq (α := ℚ) (↑a : ℚ) (↑b : ℚ)
⊢ a = b

Tactic:
simpa using congr_arg num hab

Premises used: Rat.num, congr_arg
-- Module: Mathlib.Algebra.Ring.Rat
Goal:
⊢ CommSemiring ℚ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Ring.Rat
Goal:
⊢ Semiring ℚ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Ring.Rat
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
rw : n /. x * (d /. x)⁻¹ = n /. d
rw₁ : n /. x * (x /. d) = n /. d
rw₂ rw₃ : n /. d = n /. d
⊢ n /. x / (d /. x) = n /. d

Tactic:
rw [div_eq_mul_inv, inv_divInt, divInt_mul_divInt_cancel hx]

Premises used: Rat.divInt_mul_divInt_cancel, Rat.inv_divInt, div_eq_mul_inv
-- Module: Mathlib.Algebra.Ring.Rat
Goal:
x : ℤ
hx : x ≠ 0
n d : ℤ
rw : x /. n * (x /. d)⁻¹ = d /. n
rw₁ : x /. n * (d /. x) = d /. n
rw₂ : d /. x * (x /. n) = d /. n
rw₃ rw₄ : d /. n = d /. n
⊢ x /. n / (x /. d) = d /. n

Tactic:
rw [div_eq_mul_inv, inv_divInt, mul_comm, divInt_mul_divInt_cancel hx]

Premises used: Rat.divInt_mul_divInt_cancel, Rat.inv_divInt, div_eq_mul_inv, mul_comm
-- Module: Mathlib.Algebra.Ring.Rat
Goal:
r : ℚ
rw : HDiv.hDiv (α := ℚ) (↑r.num : ℚ) (↑(↑r.den : ℤ) : ℚ) = r
rw₁ : r.num /. (↑r.den : ℤ) = r
rw₂ rw₃ : r = r
⊢ HDiv.hDiv (α := ℚ) (↑r.num : ℚ) (↑r.den : ℚ) = r

Tactic:
rw [← Int.cast_natCast, ← divInt_eq_div, num_divInt_den]

Premises used: Int.cast_natCast, Rat.num_divInt_den, Rat.divInt_eq_div
-- Module: Mathlib.Algebra.Ring.Rat
Goal:
num : ℕ
den : ℤ
n : ℕ
⊢ ((↑num : ℤ) /. den) ^ n = HPow.hPow (α := ℤ) (↑num : ℤ) n /. den ^ n

Tactic:
simp [divInt_eq_div, div_pow]

Premises used: Rat.divInt_eq_div, div_pow
-- Module: Mathlib.Algebra.Ring.Rat
Goal:
num den n : ℕ
rw : ((↑num : ℤ) /. (↑den : ℤ)) ^ n = mkRat (HPow.hPow (α := ℤ) (↑num : ℤ) n) (den ^ n)
rw₁ : ((↑num : ℤ) /. (↑den : ℤ)) ^ n = HPow.hPow (α := ℤ) (↑num : ℤ) n /. (↑(den ^ n) : ℤ)
rw₂ :
  HPow.hPow (α := ℤ) (↑num : ℤ) n /. HPow.hPow (α := ℤ) (↑den : ℤ) n =
    HPow.hPow (α := ℤ) (↑num : ℤ) n /. (↑(den ^ n) : ℤ)
rw₃ rw₄ :
  HPow.hPow (α := ℤ) (↑num : ℤ) n /. HPow.hPow (α := ℤ) (↑den : ℤ) n =
    HPow.hPow (α := ℤ) (↑num : ℤ) n /. HPow.hPow (α := ℤ) (↑den : ℤ) n
⊢ mkRat (↑num : ℤ) den ^ n = mkRat (HPow.hPow (α := ℤ) (↑num : ℤ) n) (den ^ n)

Tactic:
rw [mkRat_eq_divInt, mkRat_eq_divInt, divInt_pow, Int.natCast_pow]

Premises used: Int.natCast_pow, Rat.mkRat_eq_divInt, Rat.divInt_pow
-- Module: Mathlib.Algebra.Ring.Rat
Goal:
n : ℕ
rw : (↑(↑n : ℤ) : ℚ) = (↑n : ℤ) /. 1
rw₁ rw₂ : (↑n : ℤ) /. 1 = (↑n : ℤ) /. 1
⊢ (↑n : ℚ) = (↑n : ℤ) /. 1

Tactic:
rw [← Int.cast_natCast, intCast_eq_divInt]

Premises used: Int.cast_natCast, Rat.intCast_eq_divInt
-- Module: Mathlib.Algebra.Ring.Rat
Goal:
q : ℚ
this : q.num /. (↑q.den : ℤ) * ((↑q.den : ℤ) /. 1) = q.num /. 1
⊢ q * (↑q.den : ℚ) = (↑q.num : ℚ)

Tactic:
simp_all
-- Module: Mathlib.Algebra.Ring.Rat
Goal:
q : ℚ
suffices : q.num /. (↑q.den : ℤ) * ((↑q.den : ℤ) /. 1) = q.num /. 1
⊢ q * (↑q.den : ℚ) = (↑q.num : ℚ)

Tactic:
suffices (q.num /. ↑q.den) * (↑q.den /. 1) = q.num /. 1 by simp_all
-- Module: Mathlib.Algebra.Ring.Rat
Goal:
q : ℚ
⊢ Ne (α := ℤ) (↑q.den : ℤ) 0

Tactic:
have : (q.den : ℤ) ≠ 0 := mod_cast q.den_ne_zero
-- Module: Mathlib.Algebra.Ring.Rat
Goal:
q : ℚ
this : Ne (α := ℤ) (↑q.den : ℤ) 0
rw : q.num * (↑q.den : ℤ) /. HMul.hMul (α := ℤ) (↑q.den : ℤ) 1 = q.num /. 1
rw₁ : q.num * (↑q.den : ℤ) /. HMul.hMul (α := ℤ) 1 (↑q.den : ℤ) = q.num /. 1
rw₂ rw₃ : q.num /. 1 = q.num /. 1
⊢ q.num /. (↑q.den : ℤ) * ((↑q.den : ℤ) /. 1) = q.num /. 1

Tactic:
rw [divInt_mul_divInt, mul_comm (q.den : ℤ) 1, divInt_mul_right this]

Premises used: Rat.den, Rat.divInt_mul_divInt, Nat.cast, mul_comm, Rat.divInt_mul_right, OfNat.ofNat
-- Module: Mathlib.Algebra.Ring.Rat
Goal:
q : ℚ
rw : q * (↑q.den : ℚ) = (↑q.num : ℚ)
rw₁ rw₂ : Eq (α := ℚ) (↑q.num : ℚ) (↑q.num : ℚ)
⊢ (↑q.den : ℚ) * q = (↑q.num : ℚ)

Tactic:
rw [mul_comm, mul_den_eq_num]

Premises used: Rat.mul_den_eq_num, mul_comm
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), k * x = 0 → x = 0
⊢ IsLeftRegular k

Tactic:
fun x y (h' : k * x = k * y) => sub_eq_zero.mp (h _ ?_)

Premises used: sub_eq_zero, HSub.hSub, Iff.mp, Function.Injective
-- Module: Mathlib.Algebra.Ring.Regular
Goal:
α : Type u_1
inst : NonUnitalNonAssocRing α
k : α
h : ∀ (x : α), k * x = 0 → x = 0
refine : ∀ (x y : α) (h' : k * x = k * y), k * (x - y) = 0
⊢ IsLeftRegular k

Tactic:
refine fun x y (h' : k * x = k * y) => sub_eq_zero.mp (h _ ?_)

Premises used: sub_eq_zero, HSub.hSub, Iff.mp