Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2021 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.pi
! 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.Pi

/-!
# `star` on pi types

We put a `Star` structure on pi types that operates elementwise, such that it describes the
complex conjugation of vectors.
-/


universe u v w

variable {
I: Type u
I : 
Type u: Type (u+1)
Type u}

-- The indexing type
variable {
f: I β†’ Type v
f : 
I: Type u
I β†’ 
Type v: Type (v+1)
Type v}

-- The family of types already equipped with instances
namespace Pi


instance: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ Star (f i)] β†’ Star ((i : I) β†’ f i)
instance [βˆ€ 
i: ?m.17
i, 
Star: Type ?u.20 β†’ Type ?u.20
Star (
f: I β†’ Type v
f 
i: ?m.17
i)] : 
Star: Type ?u.24 β†’ Type ?u.24
Star (βˆ€ 
i: ?m.26
i, 
f: I β†’ Type v
f 
i: ?m.26
i) where star 
x: ?m.37
x 
i: ?m.40
i := 
star: {R : Type ?u.42} β†’ [self : Star R] β†’ R β†’ R
star (
x: ?m.37
x 
i: ?m.40
i)

@[simp]
theorem 
star_apply: βˆ€ {I : Type u} {f : I β†’ Type v} [inst : (i : I) β†’ Star (f i)] (x : (i : I) β†’ f i) (i : I), star x i = star (x i)
star_apply [βˆ€ 
i: ?m.177
i, 
Star: Type ?u.180 β†’ Type ?u.180
Star (
f: I β†’ Type v
f 
i: ?m.177
i)] (
x: (i : I) β†’ f i
x : βˆ€ 
i: ?m.185
i, 
f: I β†’ Type v
f 
i: ?m.185
i) (
i: I
i : 
I: Type u
I) : 
star: {R : Type ?u.193} β†’ [self : Star R] β†’ R β†’ R
star 
x: (i : I) β†’ f i
x 
i: I
i = 
star: {R : Type ?u.231} β†’ [self : Star R] β†’ R β†’ R
star (
x: (i : I) β†’ f i
x 
i: I
i) :=
  
rfl: βˆ€ {Ξ± : Sort ?u.243} {a : Ξ±}, a = a
rfl
#align pi.star_apply 
Pi.star_apply: βˆ€ {I : Type u} {f : I β†’ Type v} [inst : (i : I) β†’ Star (f i)] (x : (i : I) β†’ f i) (i : I), star x i = star (x i)
Pi.star_apply

theorem 
star_def: βˆ€ [inst : (i : I) β†’ Star (f i)] (x : (i : I) β†’ f i), star x = fun i => star (x i)
star_def [βˆ€ 
i: ?m.283
i, 
Star: Type ?u.286 β†’ Type ?u.286
Star (
f: I β†’ Type v
f 
i: ?m.283
i)] (
x: (i : I) β†’ f i
x : βˆ€ 
i: ?m.291
i, 
f: I β†’ Type v
f 
i: ?m.291
i) : 
star: {R : Type ?u.297} β†’ [self : Star R] β†’ R β†’ R
star 
x: (i : I) β†’ f i
x = fun 
i: ?m.337
i => 
star: {R : Type ?u.339} β†’ [self : Star R] β†’ R β†’ R
star (
x: (i : I) β†’ f i
x 
i: ?m.337
i) :=
  
rfl: βˆ€ {Ξ± : Sort ?u.353} {a : Ξ±}, a = a
rfl
#align pi.star_def 
Pi.star_def: βˆ€ {I : Type u} {f : I β†’ Type v} [inst : (i : I) β†’ Star (f i)] (x : (i : I) β†’ f i), star x = fun i => star (x i)
Pi.star_def


instance: βˆ€ {I : Type u} {f : I β†’ Type v} [inst : (i : I) β†’ Star (f i)] [inst_1 : βˆ€ (i : I), TrivialStar (f i)],
  TrivialStar ((i : I) β†’ f i)
instance [βˆ€ 
i: ?m.381
i, 
Star: Type ?u.384 β†’ Type ?u.384
Star (
f: I β†’ Type v
f 
i: ?m.381
i)] [βˆ€ 
i: ?m.389
i, 
TrivialStar: (R : Type ?u.392) β†’ [inst : Star R] β†’ Prop
TrivialStar (
f: I β†’ Type v
f 
i: ?m.389
i)] : 
TrivialStar: (R : Type ?u.404) β†’ [inst : Star R] β†’ Prop
TrivialStar (βˆ€ 
i: ?m.406
i, 
f: I β†’ Type v
f 
i: ?m.406
i)
    where star_trivial 
_: ?m.472
_ := 
funext: βˆ€ {Ξ± : Sort ?u.475} {Ξ² : Ξ± β†’ Sort ?u.474} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext fun 
_: ?m.489
_ => 
star_trivial: βˆ€ {R : Type ?u.491} [inst : Star R] [self : TrivialStar R] (r : R), star r = r
star_trivial 
_: ?m.492
_


instance: {I : Type u} β†’ {f : I β†’ Type v} β†’ [inst : (i : I) β†’ InvolutiveStar (f i)] β†’ InvolutiveStar ((i : I) β†’ f i)
instance [βˆ€ 
i: ?m.579
i, 
InvolutiveStar: Type ?u.582 β†’ Type ?u.582
InvolutiveStar (
f: I β†’ Type v
f 
i: ?m.579
i)] : 
InvolutiveStar: Type ?u.586 β†’ Type ?u.586
InvolutiveStar (βˆ€ 
i: ?m.588
i, 
f: I β†’ Type v
f 
i: ?m.588
i)
    where star_involutive 
_: ?m.637
_ := 
funext: βˆ€ {Ξ± : Sort ?u.640} {Ξ² : Ξ± β†’ Sort ?u.639} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext fun 
_: ?m.654
_ => 
star_star: βˆ€ {R : Type ?u.656} [inst : InvolutiveStar R] (r : R), star (star r) = r
star_star 
_: ?m.657
_


instance: {I : Type u} β†’
  {f : I β†’ Type v} β†’
    [inst : (i : I) β†’ Semigroup (f i)] β†’ [inst_1 : (i : I) β†’ StarSemigroup (f i)] β†’ StarSemigroup ((i : I) β†’ f i)
instance [βˆ€ 
i: ?m.776
i, 
Semigroup: Type ?u.779 β†’ Type ?u.779
Semigroup (
f: I β†’ Type v
f 
i: ?m.776
i)] [βˆ€ 
i: ?m.784
i, 
StarSemigroup: (R : Type ?u.787) β†’ [inst : Semigroup R] β†’ Type ?u.787
StarSemigroup (
f: I β†’ Type v
f 
i: ?m.784
i)] : 
StarSemigroup: (R : Type ?u.803) β†’ [inst : Semigroup R] β†’ Type ?u.803
StarSemigroup (βˆ€ 
i: ?m.805
i, 
f: I β†’ Type v
f 
i: ?m.805
i)
    where star_mul 
_: ?m.1997
_ 
_: ?m.2000
_ := 
funext: βˆ€ {Ξ± : Sort ?u.2003} {Ξ² : Ξ± β†’ Sort ?u.2002} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext fun 
_: ?m.2017
_ => 
star_mul: βˆ€ {R : Type ?u.2019} [inst : Semigroup R] [self : StarSemigroup R] (r s : R), star (r * s) = star s * star r
star_mul 
_: ?m.2020
_ 
_: ?m.2020
_


instance: {I : Type u} β†’
  {f : I β†’ Type v} β†’
    [inst : (i : I) β†’ AddMonoid (f i)] β†’ [inst_1 : (i : I) β†’ StarAddMonoid (f i)] β†’ StarAddMonoid ((i : I) β†’ f i)
instance [βˆ€ 
i: ?m.2213
i, 
AddMonoid: Type ?u.2216 β†’ Type ?u.2216
AddMonoid (
f: I β†’ Type v
f 
i: ?m.2213
i)] [βˆ€ 
i: ?m.2221
i, 
StarAddMonoid: (R : Type ?u.2224) β†’ [inst : AddMonoid R] β†’ Type ?u.2224
StarAddMonoid (
f: I β†’ Type v
f 
i: ?m.2221
i)] : 
StarAddMonoid: (R : Type ?u.2240) β†’ [inst : AddMonoid R] β†’ Type ?u.2240
StarAddMonoid (βˆ€ 
i: ?m.2242
i, 
f: I β†’ Type v
f 
i: ?m.2242
i)
    where star_add 
_: ?m.2375
_ 
_: ?m.2378
_ := 
funext: βˆ€ {Ξ± : Sort ?u.2381} {Ξ² : Ξ± β†’ Sort ?u.2380} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext fun 
_: ?m.2395
_ => 
star_add: βˆ€ {R : Type ?u.2397} [inst : AddMonoid R] [self : StarAddMonoid R] (r s : R), star (r + s) = star r + star s
star_add 
_: ?m.2398
_ 
_: ?m.2398
_


instance: {I : Type u} β†’
  {f : I β†’ Type v} β†’
    [inst : (i : I) β†’ NonUnitalSemiring (f i)] β†’ [inst_1 : (i : I) β†’ StarRing (f i)] β†’ StarRing ((i : I) β†’ f i)
instance [βˆ€ 
i: ?m.2594
i, 
NonUnitalSemiring: Type ?u.2597 β†’ Type ?u.2597
NonUnitalSemiring (
f: I β†’ Type v
f 
i: ?m.2594
i)] [βˆ€ 
i: ?m.2602
i, 
StarRing: (R : Type ?u.2605) β†’ [inst : NonUnitalSemiring R] β†’ Type ?u.2605
StarRing (
f: I β†’ Type v
f 
i: ?m.2602
i)] : 
StarRing: (R : Type ?u.2619) β†’ [inst : NonUnitalSemiring R] β†’ Type ?u.2619
StarRing (βˆ€ 
i: ?m.2621
i, 
f: I β†’ Type v
f 
i: ?m.2621
i)
  where star_add 
_: ?m.2858
_ 
_: ?m.2861
_ := 
funext: βˆ€ {Ξ± : Sort ?u.2864} {Ξ² : Ξ± β†’ Sort ?u.2863} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext fun 
_: ?m.2878
_ => 
star_add: βˆ€ {R : Type ?u.2880} [inst : AddMonoid R] [self : StarAddMonoid R] (r s : R), star (r + s) = star r + star s
star_add 
_: ?m.2881
_ 
_: ?m.2881
_


instance: βˆ€ {I : Type u} {f : I β†’ Type v} {R : Type w} [inst : (i : I) β†’ SMul R (f i)] [inst_1 : Star R]
  [inst_2 : (i : I) β†’ Star (f i)] [inst_3 : βˆ€ (i : I), StarModule R (f i)], StarModule R ((i : I) β†’ f i)
instance {
R: Type w
R : 
Type w: Type (w+1)
Type w} [βˆ€ 
i: ?m.3685
i, 
SMul: Type ?u.3689 β†’ Type ?u.3688 β†’ Type (max?u.3689?u.3688)
SMul 
R: Type w
R (
f: I β†’ Type v
f 
i: ?m.3685
i)] [
Star: Type ?u.3693 β†’ Type ?u.3693
Star 
R: Type w
R] [βˆ€ 
i: ?m.3697
i, 
Star: Type ?u.3700 β†’ Type ?u.3700
Star (
f: I β†’ Type v
f 
i: ?m.3697
i)]
    [βˆ€ 
i: ?m.3705
i, 
StarModule: (R : Type ?u.3709) β†’ (A : Type ?u.3708) β†’ [inst : Star R] β†’ [inst : Star A] β†’ [inst : SMul R A] β†’ Prop
StarModule 
R: Type w
R (
f: I β†’ Type v
f 
i: ?m.3705
i)] : 
StarModule: (R : Type ?u.3742) β†’ (A : Type ?u.3741) β†’ [inst : Star R] β†’ [inst : Star A] β†’ [inst : SMul R A] β†’ Prop
StarModule 
R: Type w
R (βˆ€ 
i: ?m.3744
i, 
f: I β†’ Type v
f 
i: ?m.3744
i)
    where star_smul 
r: ?m.3902
r 
x: ?m.3905
x := 
funext: βˆ€ {Ξ± : Sort ?u.3908} {Ξ² : Ξ± β†’ Sort ?u.3907} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext fun 
i: ?m.3922
i => 
star_smul: βˆ€ {R : Type ?u.3925} {A : Type ?u.3924} [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 
r: ?m.3902
r (
x: ?m.3905
x 
i: ?m.3922
i)

theorem 
single_star: βˆ€ [inst : (i : I) β†’ AddMonoid (f i)] [inst_1 : (i : I) β†’ StarAddMonoid (f i)] [inst_2 : DecidableEq I] (i : I)
  (a : f i), single i (star a) = star (single i a)
single_star [βˆ€ 
i: ?m.4058
i, 
AddMonoid: Type ?u.4061 β†’ Type ?u.4061
AddMonoid (
f: I β†’ Type v
f 
i: ?m.4058
i)] [βˆ€ 
i: ?m.4066
i, 
StarAddMonoid: (R : Type ?u.4069) β†’ [inst : AddMonoid R] β†’ Type ?u.4069
StarAddMonoid (
f: I β†’ Type v
f 
i: ?m.4066
i)] [
DecidableEq: Sort ?u.4085 β†’ Sort (max1?u.4085)
DecidableEq 
I: Type u
I] (
i: I
i : 
I: Type u
I)
    (
a: f i
a : 
f: I β†’ Type v
f 
i: I
i) : 
Pi.single: {I : Type ?u.4100} β†’
  {f : I β†’ Type ?u.4099} β†’ [inst : DecidableEq I] β†’ [inst : (i : I) β†’ Zero (f i)] β†’ (i : I) β†’ f i β†’ (j : I) β†’ f j
Pi.single 
i: I
i (
star: {R : Type ?u.4105} β†’ [self : Star R] β†’ R β†’ R
star 
a: f i
a) = 
star: {R : Type ?u.5310} β†’ [self : Star R] β†’ R β†’ R
star (
Pi.single: {I : Type ?u.5314} β†’
  {f : I β†’ Type ?u.5313} β†’ [inst : DecidableEq I] β†’ [inst : (i : I) β†’ Zero (f i)] β†’ (i : I) β†’ f i β†’ (j : I) β†’ f j
Pi.single 
i: I
i 
a: f i
a) :=
  
single_op: βˆ€ {I : Type ?u.5492} {f : I β†’ Type ?u.5491} [inst : DecidableEq I] [inst_1 : (i : I) β†’ Zero (f i)]
  {g : I β†’ Type ?u.5493} [inst_2 : (i : I) β†’ Zero (g i)] (op : (i : I) β†’ f i β†’ g i),
  (βˆ€ (i : I), op i 0 = 0) β†’ βˆ€ (i : I) (x : f i), single i (op i x) = fun j => op j (single i x j)
single_op (fun 
i: ?m.5501
i => @
star: {R : Type ?u.5503} β†’ [self : Star R] β†’ R β†’ R
star (
f: I β†’ Type v
f 
i: ?m.5501
i) _) (fun 
_: ?m.5533
_ => 
star_zero: βˆ€ (R : Type ?u.5535) [inst : AddMonoid R] [inst_1 : StarAddMonoid R], star 0 = 0
star_zero 
_: Type ?u.5535
_) 
i: I
i 
a: f i
a
#align pi.single_star 
Pi.single_star: βˆ€ {I : Type u} {f : I β†’ Type v} [inst : (i : I) β†’ AddMonoid (f i)] [inst_1 : (i : I) β†’ StarAddMonoid (f i)]
  [inst_2 : DecidableEq I] (i : I) (a : f i), single i (star a) = star (single i a)
Pi.single_star

end Pi

namespace Function

theorem 
update_star: βˆ€ [inst : (i : I) β†’ Star (f i)] [inst_1 : DecidableEq I] (h : (i : I) β†’ f i) (i : I) (a : f i),
  update (star h) i (star a) = star (update h i a)
update_star [βˆ€ 
i: ?m.6681
i, 
Star: Type ?u.6684 β†’ Type ?u.6684
Star (
f: I β†’ Type v
f 
i: ?m.6681
i)] [
DecidableEq: Sort ?u.6688 β†’ Sort (max1?u.6688)
DecidableEq 
I: Type u
I] (
h: (i : I) β†’ f i
h : βˆ€ 
i: I
i : 
I: Type u
I, 
f: I β†’ Type v
f 
i: I
i) (
i: I
i : 
I: Type u
I) (
a: f i
a : 
f: I β†’ Type v
f 
i: I
i) :
    
Function.update: {Ξ± : Sort ?u.6708} β†’ {Ξ² : Ξ± β†’ Sort ?u.6707} β†’ [inst : DecidableEq Ξ±] β†’ ((a : Ξ±) β†’ Ξ² a) β†’ (a' : Ξ±) β†’ Ξ² a' β†’ (a : Ξ±) β†’ Ξ² a
Function.update (
star: {R : Type ?u.6712} β†’ [self : Star R] β†’ R β†’ R
star 
h: (i : I) β†’ f i
h) 
i: I
i (
star: {R : Type ?u.6765} β†’ [self : Star R] β†’ R β†’ R
star 
a: f i
a) = 
star: {R : Type ?u.6820} β†’ [self : Star R] β†’ R β†’ R
star (
Function.update: {Ξ± : Sort ?u.6824} β†’ {Ξ² : Ξ± β†’ Sort ?u.6823} β†’ [inst : DecidableEq Ξ±] β†’ ((a : Ξ±) β†’ Ξ² a) β†’ (a' : Ξ±) β†’ Ξ² a' β†’ (a : Ξ±) β†’ Ξ² a
Function.update 
h: (i : I) β†’ f i
h 
i: I
i 
a: f i
a) :=
  
funext: βˆ€ {Ξ± : Sort ?u.6927} {Ξ² : Ξ± β†’ Sort ?u.6926} {f g : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), f x = g x) β†’ f = g
funext fun 
j: ?m.6941
j => (
apply_update: βˆ€ {ΞΉ : Sort ?u.6943} [inst : DecidableEq ΞΉ] {Ξ± : ΞΉ β†’ Sort ?u.6944} {Ξ² : ΞΉ β†’ Sort ?u.6945} (f : (i : ΞΉ) β†’ Ξ± i β†’ Ξ² i)
  (g : (i : ΞΉ) β†’ Ξ± i) (i : ΞΉ) (v : Ξ± i) (j : ΞΉ), f j (update g i v j) = update (fun k => f k (g k)) i (f i v) j
apply_update (fun 
_: ?m.6951
_ => 
star: {R : Type ?u.6953} β†’ [self : Star R] β†’ R β†’ R
star) 
h: (i : I) β†’ f i
h 
i: I
i 
a: f i
a 
j: ?m.6941
j).
symm: βˆ€ {Ξ± : Sort ?u.7006} {a b : Ξ±}, a = b β†’ b = a
symm
#align function.update_star 
Function.update_star: βˆ€ {I : Type u} {f : I β†’ Type v} [inst : (i : I) β†’ Star (f i)] [inst_1 : DecidableEq I] (h : (i : I) β†’ f i) (i : I)
  (a : f i), update (star h) i (star a) = star (update h i a)
Function.update_star

theorem 
star_sum_elim: βˆ€ {I : Type u_1} {J : Type u_2} {Ξ± : Type u_3} (x : I β†’ Ξ±) (y : J β†’ Ξ±) [inst : Star Ξ±],
  star (Sum.elim x y) = Sum.elim (star x) (star y)
star_sum_elim {
I: Type u_1
I 
J: Type ?u.7082
J 
Ξ±: Type u_3
Ξ± : 
Type _: Type (?u.7085+1)
Type _} (
x: I β†’ Ξ±
x : 
I: Type ?u.7079
I β†’ 
Ξ±: Type ?u.7085
Ξ±) (
y: J β†’ Ξ±
y : 
J: Type ?u.7082
J β†’ 
Ξ±: Type ?u.7085
Ξ±) [
Star: Type ?u.7096 β†’ Type ?u.7096
Star 
Ξ±: Type ?u.7085
Ξ±] :
    
star: {R : Type ?u.7100} β†’ [self : Star R] β†’ R β†’ R
star (
Sum.elim: {Ξ± : Type ?u.7105} β†’ {Ξ² : Type ?u.7104} β†’ {Ξ³ : Sort ?u.7103} β†’ (Ξ± β†’ Ξ³) β†’ (Ξ² β†’ Ξ³) β†’ Ξ± βŠ• Ξ² β†’ Ξ³
Sum.elim 
x: I β†’ Ξ±
x 
y: J β†’ Ξ±
y) = 
Sum.elim: {Ξ± : Type ?u.7155} β†’ {Ξ² : Type ?u.7154} β†’ {Ξ³ : Sort ?u.7153} β†’ (Ξ± β†’ Ξ³) β†’ (Ξ² β†’ Ξ³) β†’ Ξ± βŠ• Ξ² β†’ Ξ³
Sum.elim (
star: {R : Type ?u.7159} β†’ [self : Star R] β†’ R β†’ R
star 
x: I β†’ Ξ±
x) (
star: {R : Type ?u.7202} β†’ [self : Star R] β†’ R β†’ R
star 
y: J β†’ Ξ±
y) := 
Goals accomplished! πŸ™
I✝: Type u

f: I✝ β†’ Type v

I: Type u_1

J: Type u_2

Ξ±: Type u_3

x: I β†’ Ξ±

y: J β†’ Ξ±

inst✝: Star α

star (Sum.elim x y) = Sum.elim (star x) (star y)
I✝: Type u

f: I✝ β†’ Type v

I: Type u_1

J: Type u_2

Ξ±: Type u_3

x✝: I β†’ Ξ±

y: J β†’ Ξ±

inst✝: Star α

x: I βŠ• J

h
star (Sum.elim x✝ y) x = Sum.elim (star x✝) (star y) x
I✝: Type u

f: I✝ β†’ Type v

I: Type u_1

J: Type u_2

Ξ±: Type u_3

x✝: I β†’ Ξ±

y: J β†’ Ξ±

inst✝: Star α

x: I βŠ• J

h
star (Sum.elim x✝ y) x = Sum.elim (star x✝) (star y) x
I✝: Type u

f: I✝ β†’ Type v

I: Type u_1

J: Type u_2

Ξ±: Type u_3

x: I β†’ Ξ±

y: J β†’ Ξ±

inst✝: Star α

star (Sum.elim x y) = Sum.elim (star x) (star y)
I✝: Type u

f: I✝ β†’ Type v

I: Type u_1

J: Type u_2

Ξ±: Type u_3

x: I β†’ Ξ±

y: J β†’ Ξ±

inst✝: Star α

val✝: I

h.inl
star (Sum.elim x y) (Sum.inl val✝) = Sum.elim (star x) (star y) (Sum.inl val✝)
I✝: Type u

f: I✝ β†’ Type v

I: Type u_1

J: Type u_2

Ξ±: Type u_3

x: I β†’ Ξ±

y: J β†’ Ξ±

inst✝: Star α

val✝: J

h.inr
star (Sum.elim x y) (Sum.inr val✝) = Sum.elim (star x) (star y) (Sum.inr val✝)
I✝: Type u

f: I✝ β†’ Type v

I: Type u_1

J: Type u_2

Ξ±: Type u_3

x✝: I β†’ Ξ±

y: J β†’ Ξ±

inst✝: Star α

x: I βŠ• J

h
star (Sum.elim x✝ y) x = Sum.elim (star x✝) (star y) x
I✝: Type u

f: I✝ β†’ Type v

I: Type u_1

J: Type u_2

Ξ±: Type u_3

x: I β†’ Ξ±

y: J β†’ Ξ±

inst✝: Star α

val✝: I

h.inl
star (Sum.elim x y) (Sum.inl val✝) = Sum.elim (star x) (star y) (Sum.inl val✝)
I✝: Type u

f: I✝ β†’ Type v

I: Type u_1

J: Type u_2

Ξ±: Type u_3

x: I β†’ Ξ±

y: J β†’ Ξ±

inst✝: Star α

val✝: J

h.inr
star (Sum.elim x y) (Sum.inr val✝) = Sum.elim (star x) (star y) (Sum.inr val✝)
I✝: Type u

f: I✝ β†’ Type v

I: Type u_1

J: Type u_2

Ξ±: Type u_3

x✝: I β†’ Ξ±

y: J β†’ Ξ±

inst✝: Star α

x: I βŠ• J

h
star (Sum.elim x✝ y) x = Sum.elim (star x✝) (star y) x
Goals accomplished! πŸ™

#align function.star_sum_elim 
Function.star_sum_elim: βˆ€ {I : Type u_1} {J : Type u_2} {Ξ± : Type u_3} (x : I β†’ Ξ±) (y : J β†’ Ξ±) [inst : Star Ξ±],
  star (Sum.elim x y) = Sum.elim (star x) (star y)
Function.star_sum_elim

end Function