/-
Copyright (c) 2022 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser

! This file was ported from Lean 3 source module algebra.star.prod
! leanprover-community/mathlib commit 9abfa6f0727d5adc99067e325e15d1a9de17fd8e
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Star.Basic
import Mathlib.Algebra.Ring.Prod
import Mathlib.Algebra.Module.Prod

/-!
# `Star` on product types

We put a `Star` structure on product types that operates elementwise.
-/


universe u v w

variable {R: Type u
R : Type u: Type (u+1)
Type u} {S: Type v
S : Type v: Type (v+1)
Type v}

namespace Prod

instance: {R : Type u} → {S : Type v} → [inst : Star R] → [inst : Star S] → Star (R × S)
instance [Star: Type ?u.10 → Type ?u.10
Star R: Type u
R] [Star: Type ?u.13 → Type ?u.13
Star S: Type v
S] : Star: Type ?u.16 → Type ?u.16
Star (R: Type u
R × S: Type v
S) where star x: ?m.26
x := (star: {R : Type ?u.34} → [self : Star R] → R → R
star x: ?m.26
x.1: {α : Type ?u.43} → {β : Type ?u.42} → α × β → α
1, star: {R : Type ?u.50} → [self : Star R] → R → R
star x: ?m.26
x.2: {α : Type ?u.59} → {β : Type ?u.58} → α × β → β
2)

@[simp]
theorem fst_star: ∀ {R : Type u} {S : Type v} [inst : Star R] [inst_1 : Star S] (x : R × S), (star x).fst = star x.fst
fst_star [Star: Type ?u.217 → Type ?u.217
Star R: Type u
R] [Star: Type ?u.220 → Type ?u.220
Star S: Type v
S] (x: R × S
x : R: Type u
R × S: Type v
S) : (star: {R : Type ?u.228} → [self : Star R] → R → R
star x: R × S
x).1: {α : Type ?u.254} → {β : Type ?u.253} → α × β → α
1 = star: {R : Type ?u.257} → [self : Star R] → R → R
star x: R × S
x.1: {α : Type ?u.261} → {β : Type ?u.260} → α × β → α
1 :=
  rfl: ∀ {α : Sort ?u.271} {a : α}, a = a
rfl
#align prod.fst_star Prod.fst_star: ∀ {R : Type u} {S : Type v} [inst : Star R] [inst_1 : Star S] (x : R × S), (star x).fst = star x.fst
Prod.fst_star

@[simp]
theorem snd_star: ∀ {R : Type u} {S : Type v} [inst : Star R] [inst_1 : Star S] (x : R × S), (star x).snd = star x.snd
snd_star [Star: Type ?u.302 → Type ?u.302
Star R: Type u
R] [Star: Type ?u.305 → Type ?u.305
Star S: Type v
S] (x: R × S
x : R: Type u
R × S: Type v
S) : (star: {R : Type ?u.313} → [self : Star R] → R → R
star x: R × S
x).2: {α : Type ?u.339} → {β : Type ?u.338} → α × β → β
2 = star: {R : Type ?u.342} → [self : Star R] → R → R
star x: R × S
x.2: {α : Type ?u.346} → {β : Type ?u.345} → α × β → β
2 :=
  rfl: ∀ {α : Sort ?u.356} {a : α}, a = a
rfl
#align prod.snd_star Prod.snd_star: ∀ {R : Type u} {S : Type v} [inst : Star R] [inst_1 : Star S] (x : R × S), (star x).snd = star x.snd
Prod.snd_star

theorem star_def: ∀ {R : Type u} {S : Type v} [inst : Star R] [inst_1 : Star S] (x : R × S), star x = (star x.fst, star x.snd)
star_def [Star: Type ?u.387 → Type ?u.387
Star R: Type u
R] [Star: Type ?u.390 → Type ?u.390
Star S: Type v
S] (x: R × S
x : R: Type u
R × S: Type v
S) : star: {R : Type ?u.398} → [self : Star R] → R → R
star x: R × S
x = (star: {R : Type ?u.427} → [self : Star R] → R → R
star x: R × S
x.1: {α : Type ?u.438} → {β : Type ?u.437} → α × β → α
1, star: {R : Type ?u.443} → [self : Star R] → R → R
star x: R × S
x.2: {α : Type ?u.454} → {β : Type ?u.453} → α × β → β
2) :=
  rfl: ∀ {α : Sort ?u.464} {a : α}, a = a
rfl
#align prod.star_def Prod.star_def: ∀ {R : Type u} {S : Type v} [inst : Star R] [inst_1 : Star S] (x : R × S), star x = (star x.fst, star x.snd)
Prod.star_def

instance: ∀ {R : Type u} {S : Type v} [inst : Star R] [inst_1 : Star S] [inst_2 : TrivialStar R] [inst_3 : TrivialStar S],
  TrivialStar (R × S)
instance [Star: Type ?u.480 → Type ?u.480
Star R: Type u
R] [Star: Type ?u.483 → Type ?u.483
Star S: Type v
S] [TrivialStar: (R : Type ?u.486) → [inst : Star R] → Prop
TrivialStar R: Type u
R] [TrivialStar: (R : Type ?u.494) → [inst : Star R] → Prop
TrivialStar S: Type v
S] : TrivialStar: (R : Type ?u.502) → [inst : Star R] → Prop
TrivialStar (R: Type u
R × S: Type v
S)
    where star_trivial _: ?m.545
_ := Prod.ext: ∀ {α : Type ?u.547} {β : Type ?u.548} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
Prod.ext (star_trivial: ∀ {R : Type ?u.558} [inst : Star R] [self : TrivialStar R] (r : R), star r = r
star_trivial _: ?m.559
_) (star_trivial: ∀ {R : Type ?u.586} [inst : Star R] [self : TrivialStar R] (r : R), star r = r
star_trivial _: ?m.587
_)

instance: {R : Type u} → {S : Type v} → [inst : InvolutiveStar R] → [inst : InvolutiveStar S] → InvolutiveStar (R × S)
instance [InvolutiveStar: Type ?u.667 → Type ?u.667
InvolutiveStar R: Type u
R] [InvolutiveStar: Type ?u.670 → Type ?u.670
InvolutiveStar S: Type v
S] : InvolutiveStar: Type ?u.673 → Type ?u.673
InvolutiveStar (R: Type u
R × S: Type v
S)
    where star_involutive _: ?m.713
_ := Prod.ext: ∀ {α : Type ?u.715} {β : Type ?u.716} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
Prod.ext (star_star: ∀ {R : Type ?u.726} [inst : InvolutiveStar R] (r : R), star (star r) = r
star_star _: ?m.727
_) (star_star: ∀ {R : Type ?u.749} [inst : InvolutiveStar R] (r : R), star (star r) = r
star_star _: ?m.750
_)

instance: {R : Type u} →
  {S : Type v} →
    [inst : Semigroup R] →
      [inst_1 : Semigroup S] → [inst_2 : StarSemigroup R] → [inst_3 : StarSemigroup S] → StarSemigroup (R × S)
instance [Semigroup: Type ?u.847 → Type ?u.847
Semigroup R: Type u
R] [Semigroup: Type ?u.850 → Type ?u.850
Semigroup S: Type v
S] [StarSemigroup: (R : Type ?u.853) → [inst : Semigroup R] → Type ?u.853
StarSemigroup R: Type u
R] [StarSemigroup: (R : Type ?u.865) → [inst : Semigroup R] → Type ?u.865
StarSemigroup S: Type v
S] : StarSemigroup: (R : Type ?u.877) → [inst : Semigroup R] → Type ?u.877
StarSemigroup (R: Type u
R × S: Type v
S)
    where star_mul _: ?m.1967
_ _: ?m.1970
_ := Prod.ext: ∀ {α : Type ?u.1972} {β : Type ?u.1973} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
Prod.ext (star_mul: ∀ {R : Type ?u.1983} [inst : Semigroup R] [self : StarSemigroup R] (r s : R), star (r * s) = star s * star r
star_mul _: ?m.1984
_ _: ?m.1984
_) (star_mul: ∀ {R : Type ?u.2036} [inst : Semigroup R] [self : StarSemigroup R] (r s : R), star (r * s) = star s * star r
star_mul _: ?m.2037
_ _: ?m.2037
_)

instance: {R : Type u} →
  {S : Type v} →
    [inst : AddMonoid R] →
      [inst_1 : AddMonoid S] → [inst_2 : StarAddMonoid R] → [inst_3 : StarAddMonoid S] → StarAddMonoid (R × S)
instance [AddMonoid: Type ?u.2201 → Type ?u.2201
AddMonoid R: Type u
R] [AddMonoid: Type ?u.2204 → Type ?u.2204
AddMonoid S: Type v
S] [StarAddMonoid: (R : Type ?u.2207) → [inst : AddMonoid R] → Type ?u.2207
StarAddMonoid R: Type u
R] [StarAddMonoid: (R : Type ?u.2219) → [inst : AddMonoid R] → Type ?u.2219
StarAddMonoid S: Type v
S] : StarAddMonoid: (R : Type ?u.2231) → [inst : AddMonoid R] → Type ?u.2231
StarAddMonoid (R: Type u
R × S: Type v
S)
    where star_add _: ?m.2343
_ _: ?m.2346
_ := Prod.ext: ∀ {α : Type ?u.2348} {β : Type ?u.2349} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
Prod.ext (star_add: ∀ {R : Type ?u.2359} [inst : AddMonoid R] [self : StarAddMonoid R] (r s : R), star (r + s) = star r + star s
star_add _: ?m.2360
_ _: ?m.2360
_) (star_add: ∀ {R : Type ?u.2420} [inst : AddMonoid R] [self : StarAddMonoid R] (r s : R), star (r + s) = star r + star s
star_add _: ?m.2421
_ _: ?m.2421
_)

instance: {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalSemiring R] →
      [inst_1 : NonUnitalSemiring S] → [inst_2 : StarRing R] → [inst_3 : StarRing S] → StarRing (R × S)
instance [NonUnitalSemiring: Type ?u.2593 → Type ?u.2593
NonUnitalSemiring R: Type u
R] [NonUnitalSemiring: Type ?u.2596 → Type ?u.2596
NonUnitalSemiring S: Type v
S] [StarRing: (R : Type ?u.2599) → [inst : NonUnitalSemiring R] → Type ?u.2599
StarRing R: Type u
R] [StarRing: (R : Type ?u.2609) → [inst : NonUnitalSemiring R] → Type ?u.2609
StarRing S: Type v
S] : StarRing: (R : Type ?u.2619) → [inst : NonUnitalSemiring R] → Type ?u.2619
StarRing (R: Type u
R × S: Type v
S) :=
  { inferInstanceAs (StarAddMonoid (R × S)),
    inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757
{ inferInstanceAs: (α : Sort ?u.2652) → [i : α] → α
inferInstanceAs{ inferInstanceAs (StarAddMonoid (R × S)),
    inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757
 (StarAddMonoid: (R : Type ?u.2653) → [inst : AddMonoid R] → Type ?u.2653
StarAddMonoid{ inferInstanceAs (StarAddMonoid (R × S)),
    inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757
 (R: Type u
R{ inferInstanceAs (StarAddMonoid (R × S)),
    inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757
 × S: Type v
S{ inferInstanceAs (StarAddMonoid (R × S)),
    inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757)),
    inferInstanceAs: (α : Sort ?u.3651) → [i : α] → α
inferInstanceAs{ inferInstanceAs (StarAddMonoid (R × S)),
    inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757
 (StarSemigroup: (R : Type ?u.3652) → [inst : Semigroup R] → Type ?u.3652
StarSemigroup{ inferInstanceAs (StarAddMonoid (R × S)),
    inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757
 (R: Type u
R{ inferInstanceAs (StarAddMonoid (R × S)),
    inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757
 × S: Type v
S{ inferInstanceAs (StarAddMonoid (R × S)),
    inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757
)) { inferInstanceAs (StarAddMonoid (R × S)),
    inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757
with{ inferInstanceAs (StarAddMonoid (R × S)),
    inferInstanceAs (StarSemigroup (R × S)) with }: StarRing ?m.3757
 }

instance: ∀ {R : Type u} {S : Type v} {α : Type w} [inst : SMul α R] [inst_1 : SMul α S] [inst_2 : Star α] [inst_3 : Star R]
  [inst_4 : Star S] [inst_5 : StarModule α R] [inst_6 : StarModule α S], StarModule α (R × S)
instance {α: Type w
α : Type w: Type (w+1)
Type w} [SMul: Type ?u.4779 → Type ?u.4778 → Type (max?u.4779?u.4778)
SMul α: Type w
α R: Type u
R] [SMul: Type ?u.4783 → Type ?u.4782 → Type (max?u.4783?u.4782)
SMul α: Type w
α S: Type v
S] [Star: Type ?u.4786 → Type ?u.4786
Star α: Type w
α] [Star: Type ?u.4789 → Type ?u.4789
Star R: Type u
R] [Star: Type ?u.4792 → Type ?u.4792
Star S: Type v
S]
    [StarModule: (R : Type ?u.4796) → (A : Type ?u.4795) → [inst : Star R] → [inst : Star A] → [inst : SMul R A] → Prop
StarModule α: Type w
α R: Type u
R] [StarModule: (R : Type ?u.4821) → (A : Type ?u.4820) → [inst : Star R] → [inst : Star A] → [inst : SMul R A] → Prop
StarModule α: Type w
α S: Type v
S] : StarModule: (R : Type ?u.4844) → (A : Type ?u.4843) → [inst : Star R] → [inst : Star A] → [inst : SMul R A] → Prop
StarModule α: Type w
α (R: Type u
R × S: Type v
S)
    where star_smul _: ?m.4964
_ _: ?m.4967
_ := Prod.ext: ∀ {α : Type ?u.4969} {β : Type ?u.4970} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
Prod.ext (star_smul: ∀ {R : Type ?u.4981} {A : Type ?u.4980} [inst : Star R] [inst_1 : Star A] [inst_2 : SMul R A] [self : StarModule R A]
  (r : R) (a : A), star (r • a) = star r • star a
star_smul _: ?m.4982
_ _: ?m.4983
_) (star_smul: ∀ {R : Type ?u.5088} {A : Type ?u.5087} [inst : Star R] [inst_1 : Star A] [inst_2 : SMul R A] [self : StarModule R A]
  (r : R) (a : A), star (r • a) = star r • star a
star_smul _: ?m.5089
_ _: ?m.5090
_)

end Prod

--Porting note: removing @[simp], `simp` simplifies LHS
theorem Units.embed_product_star: ∀ [inst : Monoid R] [inst_1 : StarSemigroup R] (u : Rˣ), ↑(embedProduct R) (star u) = star (↑(embedProduct R) u)
Units.embed_product_star [Monoid: Type ?u.5284 → Type ?u.5284
Monoid R: Type u
R] [StarSemigroup: (R : Type ?u.5287) → [inst : Semigroup R] → Type ?u.5287
StarSemigroup R: Type u
R] (u: Rˣ
u : R: Type u
Rˣ) :
    Units.embedProduct: (α : Type ?u.5618) → [inst : Monoid α] → αˣ →* α × αᵐᵒᵖ
Units.embedProduct R: Type u
R (star: {R : Type ?u.6176} → [self : Star R] → R → R
star u: Rˣ
u) = star: {R : Type ?u.6763} → [self : Star R] → R → R
star (Units.embedProduct: (α : Type ?u.6766) → [inst : Monoid α] → αˣ →* α × αᵐᵒᵖ
Units.embedProduct R: Type u
R u: Rˣ
u) :=
  rfl: ∀ {α : Sort ?u.7794} {a : α}, a = a
rfl
#align units.embed_product_star Units.embed_product_star: ∀ {R : Type u} [inst : Monoid R] [inst_1 : StarSemigroup R] (u : Rˣ),
  ↑(Units.embedProduct R) (star u) = star (↑(Units.embedProduct R) u)
Units.embed_product_star