Theorem: Reactor.ext_obj? (ReactorModel/Objects/Reactor/Theorems/Proper.lean)

State before:
α : Type
rtr₂ : α
inst✝ : Proper α
rtr₁ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
⊢ rtr₁ = rtr₂
Tactic:
induction rtr₁ using WellFounded.induction generalizing rtr₂
State after:
case nested
α : Type
inst✝ : Proper α
rtr✝ : α
a✝ :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr✝{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr✝ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr✝[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
⊢ rtr✝ = rtr₂

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
⊢ rtr₁ = rtr₂
Tactic:
case nested rtr₁ hi =>
  ext1; funext cpt i
  case _ =>
    cases hc₁ : rtr₁{cpt}{i}
    case none => simp [Equivalent.get?_none_iff e |>.mp hc₁]
    case some n₁ =>
      have ⟨n₂, hc₂⟩ := Equivalent.get?_some_iff e |>.mp ⟨_, hc₁⟩ 
      simp [hc₂]
      cases cpt
      case rcn => exact Equivalent.get?_rcn_some_eq e hc₁ hc₂
      case rtr =>
        apply hi n₁ ⟨_, hc₁⟩ $ Equivalent.get?_rtr_some_equiv e hc₁ hc₂
        intro c _ _ _ ho₁ ho₂
        exact h (obj?_some_nested hc₁ ho₁) (obj?_some_nested hc₂ ho₂)
      all_goals 
        have ho₁ := get?_some_to_obj?_some hc₁
        have ho₂ := get?_some_to_obj?_some hc₂
        exact h ho₁ ho₂
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
⊢ rtr₁ = rtr₂
Tactic:
ext1
State after:
case a
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
⊢ get? rtr₁ = get? rtr₂

State before:
case a
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
⊢ get? rtr₁ = get? rtr₂
Tactic:
funext cpt i
State after:
case a.h.h
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
cpt : Component
i : ID
⊢ rtr₁{cpt}{i} = rtr₂{cpt}{i}

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
cpt : Component
i : ID
⊢ rtr₁{cpt}{i} = rtr₂{cpt}{i}
Tactic:
case _ =>
  cases hc₁ : rtr₁{cpt}{i}
  case none => simp [Equivalent.get?_none_iff e |>.mp hc₁]
  case some n₁ =>
    have ⟨n₂, hc₂⟩ := Equivalent.get?_some_iff e |>.mp ⟨_, hc₁⟩ 
    simp [hc₂]
    cases cpt
    case rcn => exact Equivalent.get?_rcn_some_eq e hc₁ hc₂
    case rtr =>
      apply hi n₁ ⟨_, hc₁⟩ $ Equivalent.get?_rtr_some_equiv e hc₁ hc₂
      intro c _ _ _ ho₁ ho₂
      exact h (obj?_some_nested hc₁ ho₁) (obj?_some_nested hc₂ ho₂)
    all_goals 
      have ho₁ := get?_some_to_obj?_some hc₁
      have ho₂ := get?_some_to_obj?_some hc₂
      exact h ho₁ ho₂
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
cpt : Component
i : ID
⊢ rtr₁{cpt}{i} = rtr₂{cpt}{i}
Tactic:
cases hc₁ : rtr₁{cpt}{i}
State after:
case none
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
cpt : Component
i : ID
hc₁ : rtr₁{cpt}{i} = none
⊢ none = rtr₂{cpt}{i}

case some
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
cpt : Component
i : ID
val✝ : Component.type α cpt
hc₁ : rtr₁{cpt}{i} = some val✝
⊢ some val✝ = rtr₂{cpt}{i}

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
cpt : Component
i : ID
hc₁ : rtr₁{cpt}{i} = none
⊢ none = rtr₂{cpt}{i}
Tactic:
case none => simp [Equivalent.get?_none_iff e |>.mp hc₁]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
cpt : Component
i : ID
n₁ : Component.type α cpt
hc₁ : rtr₁{cpt}{i} = some n₁
⊢ some n₁ = rtr₂{cpt}{i}
Tactic:
case some n₁ =>
  have ⟨n₂, hc₂⟩ := Equivalent.get?_some_iff e |>.mp ⟨_, hc₁⟩ 
  simp [hc₂]
  cases cpt
  case rcn => exact Equivalent.get?_rcn_some_eq e hc₁ hc₂
  case rtr =>
    apply hi n₁ ⟨_, hc₁⟩ $ Equivalent.get?_rtr_some_equiv e hc₁ hc₂
    intro c _ _ _ ho₁ ho₂
    exact h (obj?_some_nested hc₁ ho₁) (obj?_some_nested hc₂ ho₂)
  all_goals 
    have ho₁ := get?_some_to_obj?_some hc₁
    have ho₂ := get?_some_to_obj?_some hc₂
    exact h ho₁ ho₂
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
cpt : Component
i : ID
hc₁ : rtr₁{cpt}{i} = none
⊢ none = rtr₂{cpt}{i}
Tactic:
simp [Equivalent.get?_none_iff e |>.mp hc₁]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
cpt : Component
i : ID
n₁ : Component.type α cpt
hc₁ : rtr₁{cpt}{i} = some n₁
⊢ some n₁ = rtr₂{cpt}{i}
Tactic:
have ⟨n₂, hc₂⟩ := Equivalent.get?_some_iff e |>.mp ⟨_, hc₁⟩
State after:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
cpt : Component
i : ID
n₁ : Component.type α cpt
hc₁ : rtr₁{cpt}{i} = some n₁
n₂ : Component.type α cpt
hc₂ : rtr₂{cpt}{i} = some n₂
⊢ some n₁ = rtr₂{cpt}{i}

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
cpt : Component
i : ID
n₁ : Component.type α cpt
hc₁ : rtr₁{cpt}{i} = some n₁
n₂ : Component.type α cpt
hc₂ : rtr₂{cpt}{i} = some n₂
⊢ some n₁ = rtr₂{cpt}{i}
Tactic:
simp [hc₂]
State after:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
cpt : Component
i : ID
n₁ : Component.type α cpt
hc₁ : rtr₁{cpt}{i} = some n₁
n₂ : Component.type α cpt
hc₂ : rtr₂{cpt}{i} = some n₂
⊢ n₁ = n₂

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
cpt : Component
i : ID
n₁ : Component.type α cpt
hc₁ : rtr₁{cpt}{i} = some n₁
n₂ : Component.type α cpt
hc₂ : rtr₂{cpt}{i} = some n₂
⊢ n₁ = n₂
Tactic:
cases cpt
State after:
case val
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
i : ID
v✝ : Component.Valued
n₁ : Component.type α (Component.val v✝)
hc₁ : rtr₁{Component.val v✝}{i} = some n₁
n₂ : Component.type α (Component.val v✝)
hc₂ : rtr₂{Component.val v✝}{i} = some n₂
⊢ n₁ = n₂

case rtr
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
i : ID
n₁ : Component.type α Component.rtr
hc₁ : rtr₁{Component.rtr}{i} = some n₁
n₂ : Component.type α Component.rtr
hc₂ : rtr₂{Component.rtr}{i} = some n₂
⊢ n₁ = n₂

case rcn
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
i : ID
n₁ : Component.type α Component.rcn
hc₁ : rtr₁{Component.rcn}{i} = some n₁
n₂ : Component.type α Component.rcn
hc₂ : rtr₂{Component.rcn}{i} = some n₂
⊢ n₁ = n₂

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
i : ID
n₁ : Component.type α Component.rcn
hc₁ : rtr₁{Component.rcn}{i} = some n₁
n₂ : Component.type α Component.rcn
hc₂ : rtr₂{Component.rcn}{i} = some n₂
⊢ n₁ = n₂
Tactic:
case rcn => exact Equivalent.get?_rcn_some_eq e hc₁ hc₂
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
i : ID
n₁ : Component.type α Component.rtr
hc₁ : rtr₁{Component.rtr}{i} = some n₁
n₂ : Component.type α Component.rtr
hc₂ : rtr₂{Component.rtr}{i} = some n₂
⊢ n₁ = n₂
Tactic:
case rtr =>
  apply hi n₁ ⟨_, hc₁⟩ $ Equivalent.get?_rtr_some_equiv e hc₁ hc₂
  intro c _ _ _ ho₁ ho₂
  exact h (obj?_some_nested hc₁ ho₁) (obj?_some_nested hc₂ ho₂)
State after:
no goals

State before:
case val
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
i : ID
v✝ : Component.Valued
n₁ : Component.type α (Component.val v✝)
hc₁ : rtr₁{Component.val v✝}{i} = some n₁
n₂ : Component.type α (Component.val v✝)
hc₂ : rtr₂{Component.val v✝}{i} = some n₂
⊢ n₁ = n₂
Tactic:
all_goals 
  have ho₁ := get?_some_to_obj?_some hc₁
  have ho₂ := get?_some_to_obj?_some hc₂
  exact h ho₁ ho₂
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
i : ID
n₁ : Component.type α Component.rcn
hc₁ : rtr₁{Component.rcn}{i} = some n₁
n₂ : Component.type α Component.rcn
hc₂ : rtr₂{Component.rcn}{i} = some n₂
⊢ n₁ = n₂
Tactic:
exact Equivalent.get?_rcn_some_eq e hc₁ hc₂
State after:
no goals

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
i : ID
n₁ : Component.type α Component.rtr
hc₁ : rtr₁{Component.rtr}{i} = some n₁
n₂ : Component.type α Component.rtr
hc₂ : rtr₂{Component.rtr}{i} = some n₂
⊢ n₁ = n₂
Tactic:
apply hi n₁ ⟨_, hc₁⟩ $ Equivalent.get?_rtr_some_equiv e hc₁ hc₂
State after:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
i : ID
n₁ : Component.type α Component.rtr
hc₁ : rtr₁{Component.rtr}{i} = some n₁
n₂ : Component.type α Component.rtr
hc₂ : rtr₂{Component.rtr}{i} = some n₂
⊢ ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    n₁[Component.val c][i] = some o₁ → n₂[Component.val c][i] = some o₂ → o₁ = o₂

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
i : ID
n₁ : Component.type α Component.rtr
hc₁ : rtr₁{Component.rtr}{i} = some n₁
n₂ : Component.type α Component.rtr
hc₂ : rtr₂{Component.rtr}{i} = some n₂
⊢ ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    n₁[Component.val c][i] = some o₁ → n₂[Component.val c][i] = some o₂ → o₁ = o₂
Tactic:
intro c _ _ _ ho₁ ho₂
State after:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
i : ID
n₁ : Component.type α Component.rtr
hc₁ : rtr₁{Component.rtr}{i} = some n₁
n₂ : Component.type α Component.rtr
hc₂ : rtr₂{Component.rtr}{i} = some n₂
c : Component.Valued
i✝ : Component.idType (Component.val c)
o₁✝ o₂✝ : Component.type α (Component.val c)
ho₁ : n₁[Component.val c][i✝] = some o₁✝
ho₂ : n₂[Component.val c][i✝] = some o₂✝
⊢ o₁✝ = o₂✝

State before:
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
i : ID
n₁ : Component.type α Component.rtr
hc₁ : rtr₁{Component.rtr}{i} = some n₁
n₂ : Component.type α Component.rtr
hc₂ : rtr₂{Component.rtr}{i} = some n₂
c : Component.Valued
i✝ : Component.idType (Component.val c)
o₁✝ o₂✝ : Component.type α (Component.val c)
ho₁ : n₁[Component.val c][i✝] = some o₁✝
ho₂ : n₂[Component.val c][i✝] = some o₂✝
⊢ o₁✝ = o₂✝
Tactic:
exact h (obj?_some_nested hc₁ ho₁) (obj?_some_nested hc₂ ho₂)
State after:
no goals

State before:
case val
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
i : ID
v✝ : Component.Valued
n₁ : Component.type α (Component.val v✝)
hc₁ : rtr₁{Component.val v✝}{i} = some n₁
n₂ : Component.type α (Component.val v✝)
hc₂ : rtr₂{Component.val v✝}{i} = some n₂
⊢ n₁ = n₂
Tactic:
have ho₁ := get?_some_to_obj?_some hc₁
State after:
case val
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
i : ID
v✝ : Component.Valued
n₁ : Component.type α (Component.val v✝)
hc₁ : rtr₁{Component.val v✝}{i} = some n₁
n₂ : Component.type α (Component.val v✝)
hc₂ : rtr₂{Component.val v✝}{i} = some n₂
ho₁ :
  rtr₁[Component.val v✝][match Component.val v✝ with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some n₁
⊢ n₁ = n₂

State before:
case val
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
i : ID
v✝ : Component.Valued
n₁ : Component.type α (Component.val v✝)
hc₁ : rtr₁{Component.val v✝}{i} = some n₁
n₂ : Component.type α (Component.val v✝)
hc₂ : rtr₂{Component.val v✝}{i} = some n₂
ho₁ :
  rtr₁[Component.val v✝][match Component.val v✝ with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some n₁
⊢ n₁ = n₂
Tactic:
have ho₂ := get?_some_to_obj?_some hc₂
State after:
case val
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
i : ID
v✝ : Component.Valued
n₁ : Component.type α (Component.val v✝)
hc₁ : rtr₁{Component.val v✝}{i} = some n₁
n₂ : Component.type α (Component.val v✝)
hc₂ : rtr₂{Component.val v✝}{i} = some n₂
ho₁ :
  rtr₁[Component.val v✝][match Component.val v✝ with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some n₁
ho₂ :
  rtr₂[Component.val v✝][match Component.val v✝ with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some n₂
⊢ n₁ = n₂

State before:
case val
α : Type
inst✝ : Proper α
rtr₁ : α
hi :
  ∀ (n : Component.type α Component.rtr),
    (∃ i, rtr₁{Component.rtr}{i} = some n) →
      ∀ {rtr₂ : α},
        n ≈ rtr₂ →
          (∀ {c : Component.Valued} {i : Component.idType (Component.val c)}
              {o₁ o₂ : Component.type α (Component.val c)},
              n[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂) →
            n = rtr₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
h :
  ∀ {c : Component.Valued} {i : Component.idType (Component.val c)} {o₁ o₂ : Component.type α (Component.val c)},
    rtr₁[Component.val c][i] = some o₁ → rtr₂[Component.val c][i] = some o₂ → o₁ = o₂
i : ID
v✝ : Component.Valued
n₁ : Component.type α (Component.val v✝)
hc₁ : rtr₁{Component.val v✝}{i} = some n₁
n₂ : Component.type α (Component.val v✝)
hc₂ : rtr₂{Component.val v✝}{i} = some n₂
ho₁ :
  rtr₁[Component.val v✝][match Component.val v✝ with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some n₁
ho₂ :
  rtr₂[Component.val v✝][match Component.val v✝ with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some n₂
⊢ n₁ = n₂
Tactic:
exact h ho₁ ho₂
State after:
no goals