Theorem: IContainer.M.wf_destruct (CoInd/MIdx.lean)

State before:
I : Type u₀
C : IContainer I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf : WellFormed i m
⊢ ∀
    (x :
      B C (Container.M.destruct ↑{ val := m, property := wf }).fst.fst
        (Container.M.destruct ↑{ val := m, property := wf }).fst.snd),
    WellFormed
      (N C (Container.M.destruct ↑{ val := m, property := wf }).fst.fst
        (Container.M.destruct ↑{ val := m, property := wf }).fst.snd x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf }) x)
Tactic:
simp only [WellFormed, PWellFormed] at wf
State after:
I : Type u₀
C : IContainer I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf : ↑(pgfp (WellFormedF C)) ⊥ i m
⊢ ∀
    (x :
      B C (Container.M.destruct ↑{ val := m, property := wf }).fst.fst
        (Container.M.destruct ↑{ val := m, property := wf }).fst.snd),
    WellFormed
      (N C (Container.M.destruct ↑{ val := m, property := wf }).fst.fst
        (Container.M.destruct ↑{ val := m, property := wf }).fst.snd x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf }) x)

State before:
I : Type u₀
C : IContainer I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf : ↑(pgfp (WellFormedF C)) ⊥ i m
⊢ ∀
    (x :
      B C (Container.M.destruct ↑{ val := m, property := wf }).fst.fst
        (Container.M.destruct ↑{ val := m, property := wf }).fst.snd),
    WellFormed
      (N C (Container.M.destruct ↑{ val := m, property := wf }).fst.fst
        (Container.M.destruct ↑{ val := m, property := wf }).fst.snd x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf }) x)
Tactic:
rw [←pgfp.unfold] at wf
State after:
I : Type u₀
C : IContainer I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (⊥ ⊔ ↑(pgfp (WellFormedF C)) ⊥) i m
⊢ ∀
    (x :
      B C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.fst
        (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.snd),
    WellFormed
      (N C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.fst
        (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.snd x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf✝ }) x)

State before:
I : Type u₀
C : IContainer I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (⊥ ⊔ ↑(pgfp (WellFormedF C)) ⊥) i m
⊢ ∀
    (x :
      B C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.fst
        (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.snd),
    WellFormed
      (N C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.fst
        (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.snd x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf✝ }) x)
Tactic:
simp only [CompleteLattice.bot_sup] at wf
State after:
I : Type u₀
C : IContainer I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (↑(pgfp (WellFormedF C)) ⊥) i m
⊢ ∀
    (x :
      B C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.fst
        (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.snd),
    WellFormed
      (N C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.fst
        (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.snd x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf✝ }) x)

State before:
I : Type u₀
C : IContainer I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (↑(pgfp (WellFormedF C)) ⊥) i m
⊢ ∀
    (x :
      B C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.fst
        (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.snd),
    WellFormed
      (N C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.fst
        (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.snd x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf✝ }) x)
Tactic:
have ⟨_, y⟩ := wf
State after:
I : Type u₀
C : IContainer I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (↑(pgfp (WellFormedF C)) ⊥) i m
left✝ : (Container.M.destruct m).fst.fst = i
y :
  ∀ (x : B C (Container.M.destruct m).fst.fst (Container.M.destruct m).fst.snd),
    ↑(pgfp (WellFormedF C)) ⊥ (N C (Container.M.destruct m).fst.fst (Container.M.destruct m).fst.snd x)
      (PSigma.snd (Container.M.destruct m) x)
⊢ ∀
    (x :
      B C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.fst
        (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.snd),
    WellFormed
      (N C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.fst
        (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.snd x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf✝ }) x)

State before:
I : Type u₀
C : IContainer I
i : I
x✝ : M C i
m : Container.M (toContainer C)
wf✝ : ↑(pgfp (WellFormedF C)) ⊥ i m
wf : ↑(WellFormedF C) (↑(pgfp (WellFormedF C)) ⊥) i m
left✝ : (Container.M.destruct m).fst.fst = i
y :
  ∀ (x : B C (Container.M.destruct m).fst.fst (Container.M.destruct m).fst.snd),
    ↑(pgfp (WellFormedF C)) ⊥ (N C (Container.M.destruct m).fst.fst (Container.M.destruct m).fst.snd x)
      (PSigma.snd (Container.M.destruct m) x)
⊢ ∀
    (x :
      B C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.fst
        (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.snd),
    WellFormed
      (N C (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.fst
        (Container.M.destruct ↑{ val := m, property := wf✝ }).fst.snd x)
      (PSigma.snd (Container.M.destruct ↑{ val := m, property := wf✝ }) x)
Tactic:
exact y
State after:
no goals