Theorem: IQPF.M.congr.coinduction (CoInd/QPF/MIdx.lean)

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₁
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

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]
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

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
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

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
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

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
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

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
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

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
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

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₀
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

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
State after:
no goals

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
State after:
no goals