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

State before:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
⊢ (∀ (x y : M (C F)), p x y → ↑(precongr F) p x y) → ∀ (x y : M (C F)), p x y → congr F x y
Tactic:
intro h₀ x y h₁
State after:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
⊢ congr F x y

State before:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
⊢ congr F x y
Tactic:
simp only [congr, pcongr]
State after:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
⊢ ↑(pgfp (precongr F)) ⊥ x y

State before:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
⊢ ↑(pgfp (precongr F)) ⊥ x y
Tactic:
have := (pgfp.coinduction (precongr F) p).2
State after:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ ↑(pgfp (precongr F)) ⊥ x y

State before:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ ↑(pgfp (precongr F)) ⊥ x y
Tactic:
apply this
State after:
case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p 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
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y

State before:
case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p 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
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y
Tactic:
have : p ≤ p ⊔ pgfp (precongr F) p := by
  simp
State after:
case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p 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
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y

State before:
case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p 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
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y
Tactic:
have := (precongr F).2 this
State after:
case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p 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
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y

State before:
case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p 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
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y
Tactic:
apply le_trans _ this
State after:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p 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
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y

State before:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p 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
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y
Tactic:
apply h₀
State after:
case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y

State before:
case a
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p x y
this : p ≤ ↑(precongr F) (p ⊔ ↑(pgfp (precongr F)) p) → p ≤ ↑(pgfp (precongr F)) ⊥
⊢ p x y
Tactic:
assumption
State after:
no goals

State before:
F✝ : Type u₁ → Type u₁
inst✝ : QPF F✝
F : Type u₁ → Type u₁
inst : QPF F
p : M (C F) → M (C F) → Prop
h₀ : ∀ (x y : M (C F)), p x y → ↑(precongr F) p x y
x y : M (C F)
h₁ : p 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