Theorem: Color.ext_iff (Ray/Render/Color.lean)

State before:
α β : Type
x y : Color α
⊢ x = y ↔ x.r = y.r ∧ x.g = y.g ∧ x.b = y.b ∧ x.a = y.a
Tactic:
induction x
State after:
case mk
α β : Type
y : Color α
r✝ g✝ b✝ a✝ : α
⊢ { r := r✝, g := g✝, b := b✝, a := a✝ } = y ↔
    { r := r✝, g := g✝, b := b✝, a := a✝ }.r = y.r ∧
      { r := r✝, g := g✝, b := b✝, a := a✝ }.g = y.g ∧
        { r := r✝, g := g✝, b := b✝, a := a✝ }.b = y.b ∧ { r := r✝, g := g✝, b := b✝, a := a✝ }.a = y.a

State before:
case mk
α β : Type
y : Color α
r✝ g✝ b✝ a✝ : α
⊢ { r := r✝, g := g✝, b := b✝, a := a✝ } = y ↔
    { r := r✝, g := g✝, b := b✝, a := a✝ }.r = y.r ∧
      { r := r✝, g := g✝, b := b✝, a := a✝ }.g = y.g ∧
        { r := r✝, g := g✝, b := b✝, a := a✝ }.b = y.b ∧ { r := r✝, g := g✝, b := b✝, a := a✝ }.a = y.a
Tactic:
induction y
State after:
case mk.mk
α β : Type
r✝¹ g✝¹ b✝¹ a✝¹ r✝ g✝ b✝ a✝ : α
⊢ { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ } = { r := r✝, g := g✝, b := b✝, a := a✝ } ↔
    { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ }.r = { r := r✝, g := g✝, b := b✝, a := a✝ }.r ∧
      { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ }.g = { r := r✝, g := g✝, b := b✝, a := a✝ }.g ∧
        { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ }.b = { r := r✝, g := g✝, b := b✝, a := a✝ }.b ∧
          { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ }.a = { r := r✝, g := g✝, b := b✝, a := a✝ }.a

State before:
case mk.mk
α β : Type
r✝¹ g✝¹ b✝¹ a✝¹ r✝ g✝ b✝ a✝ : α
⊢ { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ } = { r := r✝, g := g✝, b := b✝, a := a✝ } ↔
    { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ }.r = { r := r✝, g := g✝, b := b✝, a := a✝ }.r ∧
      { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ }.g = { r := r✝, g := g✝, b := b✝, a := a✝ }.g ∧
        { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ }.b = { r := r✝, g := g✝, b := b✝, a := a✝ }.b ∧
          { r := r✝¹, g := g✝¹, b := b✝¹, a := a✝¹ }.a = { r := r✝, g := g✝, b := b✝, a := a✝ }.a
Tactic:
simp only [mk.injEq]
State after:
no goals