internlm/Lean-Github huggingface dataset:
Theorem: IContainer.M.bisim
Proof state before:
case refl.refl.refl
I : Type u₀
C : IContainer I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
i : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i y✝
h₁✝ : R i { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy'✝ : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
k₁ : (y_1 : B C (Container.M.destruct y).fst.fst ny) → M C (N C (Container.M.destruct y).fst.fst ny y_1)
h₁ : destruct { val := x, property := wfx } = { fst := ny, snd := k₁ }
a : B C (Container.M.destruct y).fst.fst ny
wfy' : WellFormed (N C iy ny a) (ky a)
h₂ : destruct { val := y, property := wfy } = { fst := ny, snd := (destruct { val := y, property := wfy }).snd }
h₃ :
  ∀ (z : B C (Container.M.destruct y).fst.fst ny),
    R (N C (Container.M.destruct y).fst.fst ny z) (k₁ z) (Sigma.snd (destruct { val := y, property := wfy }) z)
⊢ WellFormed (N C (Container.M.destruct y).fst.fst ny a)
    ((fun x => ↑(Sigma.snd (destruct { val := y, property := wfy }) x)) a)
Tactic:
exact wfy'
Proof state after:
no goals
Theorem: IContainer.M.bisim
Proof state before:
I : Type u₀
C : IContainer I
R : (i : I) → M C i → M C i → Prop
h₀ :
  ∀ (i : I) (x y : M C i),
    R i x y →
      ∃ node k₁ k₂,
        destruct x = { fst := node, snd := k₁ } ∧
          destruct y = { fst := node, snd := k₂ } ∧ ∀ (z : B C i node), R (N C i node z) (k₁ z) (k₂ z)
i : I
x✝ : Container.M (toContainer C)
wfx✝ : WellFormed i x✝
y✝ : Container.M (toContainer C)
wfy✝ : WellFormed i y✝
h₁✝ : R i { val := x✝, property := wfx✝ } { val := y✝, property := wfy✝ }
x y : Container.M (toContainer C)
ix : I := (Container.M.destruct x).fst.fst
nx : A C (Container.M.destruct x).fst.fst := (Container.M.destruct x).fst.snd
kx : Container.B (toContainer C) (Container.M.destruct x).fst → Container.M (toContainer C) :=
  (Container.M.destruct x).snd
iy : I := (Container.M.destruct y).fst.fst
ny : A C (Container.M.destruct y).fst.fst := (Container.M.destruct y).fst.snd
ky : Container.B (toContainer C) (Container.M.destruct y).fst → Container.M (toContainer C) :=
  (Container.M.destruct y).snd
wfx' : ∀ (a : B C ix nx), WellFormed (N C ix nx a) (kx a)
wfy' : ∀ (a : B C iy ny), WellFormed (N C iy ny a) (ky a)
wfx : WellFormed (Container.M.destruct y).fst.fst x
wfy : WellFormed (Container.M.destruct y).fst.fst y
r : R (Container.M.destruct y).fst.fst { val := x, property := wfx } { val := y, property := wfy }
node : A C (Container.M.destruct y).fst.fst
k₁ k₂ : (y_1 : B C (Container.M.destruct y).fst.fst node) → M C (N C (Container.M.destruct y).fst.fst node y_1)
h₁ : destruct { val := x, property := wfx } = { fst := node, snd := k₁ }
h₂ : destruct { val := y, property := wfy } = { fst := node, snd := k₂ }
h₃ : ∀ (z : B C (Container.M.destruct y).fst.fst node), R (N C (Container.M.destruct y).fst.fst node z) (k₁ z) (k₂ z)
hix : (Container.M.destruct y).fst.fst = (Container.M.destruct x).fst.fst
a : B C (Container.M.destruct y).fst.fst node
⊢ ny = node
Tactic:
apply congrArg Sigma.fst h₂
Proof state after:
no goals
Theorem: IQPF.M.congr.coinduction
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
⊢ (∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y) → ∀ (i : I) (x y : M (C F) i), p i x y → congr F i x y
Tactic:
intro h₀ i x y h₁
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
⊢ congr F i x y
Theorem: IQPF.M.congr.coinduction
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
⊢ congr F i x y
Tactic:
simp only [congr, pcongr]
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
⊢ ↑(pgfp (precongr F)) ⊥ i x y
Theorem: IQPF.M.congr.coinduction
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
⊢ ↑(pgfp (precongr F)) ⊥ i x y
Tactic:
have := (pgfp.coinduction (precongr F) p).2
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ ↑(pgfp (precongr F)) ⊥ i x y
Theorem: IQPF.M.congr.coinduction
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ ↑(pgfp (precongr F)) ⊥ i x y
Tactic:
apply this
Proof state after:
case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)

case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p i x y
Theorem: IQPF.M.congr.coinduction
Proof state before:
case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)

case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p i x y
Tactic:
have : p ≤ p ⊔ pgfp (precongr F) p := by
  simp
Proof state after:
case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this✝ : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
this : p ≤ p ⊔ ↑(pgfp (precongr F)) p
⊢ p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)

case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p i x y
Theorem: IQPF.M.congr.coinduction
Proof state before:
case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this✝ : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
this : p ≤ p ⊔ ↑(pgfp (precongr F)) p
⊢ p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)

case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p i x y
Tactic:
have := (precongr F).2 this
Proof state after:
case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this✝¹ : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
this✝ : p ≤ p ⊔ ↑(pgfp (precongr F)) p
this : ↑(precongr F) p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)
⊢ p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)

case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p i x y
Theorem: IQPF.M.congr.coinduction
Proof state before:
case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this✝¹ : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
this✝ : p ≤ p ⊔ ↑(pgfp (precongr F)) p
this : ↑(precongr F) p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)
⊢ p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)

case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p i x y
Tactic:
apply le_trans _ this
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this✝¹ : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
this✝ : p ≤ p ⊔ ↑(pgfp (precongr F)) p
this : ↑(precongr F) p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)
⊢ p ≤ ↑(precongr F) p

case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p i x y
Theorem: IQPF.M.congr.coinduction
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this✝¹ : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
this✝ : p ≤ p ⊔ ↑(pgfp (precongr F)) p
this : ↑(precongr F) p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p)
⊢ p ≤ ↑(precongr F) p

case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p i x y
Tactic:
apply h₀
Proof state after:
case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p i x y
Theorem: IQPF.M.congr.coinduction
Proof state before:
case a
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p i x y
Tactic:
assumption
Proof state after:
no goals
Theorem: IQPF.M.congr.coinduction
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
p : (i : I) → M (C F) i → M (C F) i → Prop
h₀ : ∀ (i : I) (x y : M (C F) i), p i x y → ↑(precongr F) p i x y
i : I
x y : M (C F) i
h₁ : p i x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p ≤ p ⊔ ↑(pgfp (precongr F)) p
Tactic:
simp
Proof state after:
no goals
Theorem: IQPF.M.destruct_corec
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
α : I → Type u₁
f : (i : I) → α i → F α i
i : I
x₀ : α i
⊢ destruct (corec f x₀) = IFunctor.imap (fun i x => corec f x) (f i x₀)
Tactic:
simp only [IQPF.M.destruct, IQPF.M.corec, destruct.f, IContainer.M.destruct_corec, inst.abs_imap, inst.abs_repr]
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
α : I → Type u₁
f : (i : I) → α i → F α i
i : I
x₀ : α i
⊢ IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1)
      (IFunctor.imap (fun i => IContainer.M.corec fun i x => repr (f i x)) (f i x₀)) =
    IFunctor.imap (fun i x => Quot.mk (congr F i) (IContainer.M.corec (fun i x => repr (f i x)) x)) (f i x₀)
Theorem: IQPF.M.destruct_corec
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
α : I → Type u₁
f : (i : I) → α i → F α i
i : I
x₀ : α i
⊢ IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1)
      (IFunctor.imap (fun i => IContainer.M.corec fun i x => repr (f i x)) (f i x₀)) =
    IFunctor.imap (fun i x => Quot.mk (congr F i) (IContainer.M.corec (fun i x => repr (f i x)) x)) (f i x₀)
Tactic:
rw [←inst.abs_repr (f i x₀)]
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
α : I → Type u₁
f : (i : I) → α i → F α i
i : I
x₀ : α i
⊢ IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1)
      (IFunctor.imap (fun i => IContainer.M.corec fun i x => repr (f i x)) (abs (repr (f i x₀)))) =
    IFunctor.imap (fun i x => Quot.mk (congr F i) (IContainer.M.corec (fun i x => repr (f i x)) x))
      (abs (repr (f i x₀)))
Theorem: IQPF.M.destruct_corec
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
α : I → Type u₁
f : (i : I) → α i → F α i
i : I
x₀ : α i
⊢ IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1)
      (IFunctor.imap (fun i => IContainer.M.corec fun i x => repr (f i x)) (abs (repr (f i x₀)))) =
    IFunctor.imap (fun i x => Quot.mk (congr F i) (IContainer.M.corec (fun i x => repr (f i x)) x))
      (abs (repr (f i x₀)))
Tactic:
cases repr (f i x₀) with
| mk n k =>
  simp only [←inst.abs_imap, IContainer.Map]
Proof state after:
no goals
Theorem: IQPF.M.destruct_corec
Proof state before:
case mk
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
α : I → Type u₁
f : (i : I) → α i → F α i
i : I
x₀ : α i
n : IContainer.A (C F) i
k : (y : IContainer.B (C F) i n) → α (IContainer.N (C F) i n y)
⊢ IFunctor.imap (fun x x_1 => Quot.mk (congr F x) x_1)
      (IFunctor.imap (fun i => IContainer.M.corec fun i x => repr (f i x)) (abs { fst := n, snd := k })) =
    IFunctor.imap (fun i x => Quot.mk (congr F i) (IContainer.M.corec (fun i x => repr (f i x)) x))
      (abs { fst := n, snd := k })
Tactic:
simp only [←inst.abs_imap, IContainer.Map]
Proof state after:
no goals
Theorem: IQPF.M.imap_spec
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
i : I
α β γ : I → Type u₁
f : (i : I) → β i → γ i
g : (i : I) → α i → β i
x : F α i
⊢ IFunctor.imap (fun i => f i ∘ g i) x = IFunctor.imap f (IFunctor.imap g x)
Tactic:
conv =>
  congr
  <;> rw [←inst.abs_repr x]
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
i : I
α β γ : I → Type u₁
f : (i : I) → β i → γ i
g : (i : I) → α i → β i
x : F α i
⊢ IFunctor.imap (fun i => f i ∘ g i) (abs (repr x)) = IFunctor.imap f (IFunctor.imap g (abs (repr x)))
Theorem: IQPF.M.imap_spec
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
i : I
α β γ : I → Type u₁
f : (i : I) → β i → γ i
g : (i : I) → α i → β i
x : F α i
⊢ IFunctor.imap (fun i => f i ∘ g i) (abs (repr x)) = IFunctor.imap f (IFunctor.imap g (abs (repr x)))
Tactic:
cases repr x
Proof state after:
case mk
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
i : I
α β γ : I → Type u₁
f : (i : I) → β i → γ i
g : (i : I) → α i → β i
x : F α i
fst✝ : IContainer.A (C F) i
snd✝ : (y : IContainer.B (C F) i fst✝) → α (IContainer.N (C F) i fst✝ y)
⊢ IFunctor.imap (fun i => f i ∘ g i) (abs { fst := fst✝, snd := snd✝ }) =
    IFunctor.imap f (IFunctor.imap g (abs { fst := fst✝, snd := snd✝ }))
Theorem: IQPF.M.imap_spec
Proof state before:
case mk
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
i : I
α β γ : I → Type u₁
f : (i : I) → β i → γ i
g : (i : I) → α i → β i
x : F α i
fst✝ : IContainer.A (C F) i
snd✝ : (y : IContainer.B (C F) i fst✝) → α (IContainer.N (C F) i fst✝ y)
⊢ IFunctor.imap (fun i => f i ∘ g i) (abs { fst := fst✝, snd := snd✝ }) =
    IFunctor.imap f (IFunctor.imap g (abs { fst := fst✝, snd := snd✝ }))
Tactic:
simp [←inst.abs_imap, IContainer.Map]
Proof state after:
no goals
Theorem: IContainer.Map_spec
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
i : I
α β γ : I → Type u₁
f : (i : I) → β i → γ i
g : (i : I) → α i → β i
x : Obj (IQPF.C F) α i
⊢ Map (fun i => f i ∘ g i) x = Map f (Map g x)
Tactic:
cases x
Proof state after:
case mk
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
i : I
α β γ : I → Type u₁
f : (i : I) → β i → γ i
g : (i : I) → α i → β i
fst✝ : A (IQPF.C F) i
snd✝ : (y : B (IQPF.C F) i fst✝) → α (N (IQPF.C F) i fst✝ y)
⊢ Map (fun i => f i ∘ g i) { fst := fst✝, snd := snd✝ } = Map f (Map g { fst := fst✝, snd := snd✝ })
Theorem: IContainer.Map_spec
Proof state before:
case mk
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
i : I
α β γ : I → Type u₁
f : (i : I) → β i → γ i
g : (i : I) → α i → β i
fst✝ : A (IQPF.C F) i
snd✝ : (y : B (IQPF.C F) i fst✝) → α (N (IQPF.C F) i fst✝ y)
⊢ Map (fun i => f i ∘ g i) { fst := fst✝, snd := snd✝ } = Map f (Map g { fst := fst✝, snd := snd✝ })
Tactic:
simp [IContainer.Map]
Proof state after:
no goals
Theorem: IQPF.M.bisim_lemma
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
⊢ ∀ (i : I) (x y : M F i), r i x y → x = y
Tactic:
intro i x
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i : I
x : M F i
⊢ ∀ (y : M F i), r i x y → x = y
Theorem: IQPF.M.bisim_lemma
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i : I
x : M F i
⊢ ∀ (y : M F i), r i x y → x = y
Tactic:
apply Quot.inductionOn (motive := _) x
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i : I
x : M F i
⊢ ∀ (a : IContainer.M (C F) i) (y : M F i), r i (Quot.mk (congr F i) a) y → Quot.mk (congr F i) a = y
Theorem: IQPF.M.bisim_lemma
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i : I
x : M F i
⊢ ∀ (a : IContainer.M (C F) i) (y : M F i), r i (Quot.mk (congr F i) a) y → Quot.mk (congr F i) a = y
Tactic:
clear x
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i : I
⊢ ∀ (a : IContainer.M (C F) i) (y : M F i), r i (Quot.mk (congr F i) a) y → Quot.mk (congr F i) a = y
Theorem: IQPF.M.bisim_lemma
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i : I
⊢ ∀ (a : IContainer.M (C F) i) (y : M F i), r i (Quot.mk (congr F i) a) y → Quot.mk (congr F i) a = y
Tactic:
intro x y
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i : I
x : IContainer.M (C F) i
y : M F i
⊢ r i (Quot.mk (congr F i) x) y → Quot.mk (congr F i) x = y
Theorem: IQPF.M.bisim_lemma
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i : I
x : IContainer.M (C F) i
y : M F i
⊢ r i (Quot.mk (congr F i) x) y → Quot.mk (congr F i) x = y
Tactic:
apply Quot.inductionOn (motive := _) y
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i : I
x : IContainer.M (C F) i
y : M F i
⊢ ∀ (a : IContainer.M (C F) i),
    r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) a) → Quot.mk (congr F i) x = Quot.mk (congr F i) a
Theorem: IQPF.M.bisim_lemma
Proof state before:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i : I
x : IContainer.M (C F) i
y : M F i
⊢ ∀ (a : IContainer.M (C F) i),
    r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) a) → Quot.mk (congr F i) x = Quot.mk (congr F i) a
Tactic:
clear y
Proof state after:
I : Type u₁
F : (I → Type u₁) → I → Type u₁
inst : IQPF F
r : (i : I) → M F i → M F i → Prop
h₀ : ∀ (i : I) (x : M F i), r i x x
h₁ :
  ∀ (i : I) (x y : M F i),
    r i x y → IFunctor.imap (fun i => Quot.mk (r i)) (destruct x) = IFunctor.imap (fun i => Quot.mk (r i)) (destruct y)
i : I
x : IContainer.M (C F) i
⊢ ∀ (a : IContainer.M (C F) i),
    r i (Quot.mk (congr F i) x) (Quot.mk (congr F i) a) → Quot.mk (congr F i) x = Quot.mk (congr F i) a