mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Fix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
⊢ Part.fix f x = Fix.approx f (Nat.find h').succ x

Tactic:
have : p (Nat.find h') := Nat.find_spec h'

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
this : p (Nat.find h')
⊢ Part.fix f x = Fix.approx f (Nat.find h').succ x
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : bicompr F t α✝ α'✝
⊢ traverse (bitraverse (pure ∘ f✝) (pure ∘ f'✝)) x✝ = pure (bimap f✝ f'✝ x✝)

pp: case binaturality
t : Type u → Type u → Type u
inst✝⁷ : Bitraversable t
F : Type u → Type u
inst✝⁶ : Traversable F
inst✝⁵ : LawfulTraversable F
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompr F t α✝ α'✝
⊢ η✝.app (bicompr F t β✝ β'✝) (traverse (bitraverse f✝ f'✝) x✝) =
    traverse (bitraverse (η✝.app β✝ ∘ f✝) (η✝.app β'✝ ∘ f'✝)) x✝

Tactic:
·

Goal state after:
case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → β✝
f'✝ : α'✝ → β'✝
x✝ : bicompr F t α✝ α'✝
⊢ traverse (bitraverse (pure ∘ f✝) (pure ∘ f'✝)) x✝ = pure (bimap f✝ f'✝ x✝)
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: case binaturality
t : Type u → Type u → Type u
inst✝⁷ : Bitraversable t
F : Type u → Type u
inst✝⁶ : Traversable F
inst✝⁵ : LawfulTraversable F
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompr F t α✝ α'✝
⊢ η✝.app (bicompr F t β✝ β'✝) (traverse (bitraverse f✝ f'✝) x✝) =
    traverse (bitraverse (η✝.app β✝ ∘ f✝) (η✝.app β'✝ ∘ f'✝)) x✝

Tactic:
·

Goal state after:
case binaturality
t : Type u → Type u → Type u
inst✝⁷ : Bitraversable t
F : Type u → Type u
inst✝⁶ : Traversable F
inst✝⁵ : LawfulTraversable F
inst✝⁴ : LawfulBitraversable t
F✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompr F t α✝ α'✝
⊢ η✝.app (bicompr F t β✝ β'✝) (traverse (bitraverse f✝ f'✝) x✝) =
    traverse (bitraverse (η✝.app β✝ ∘ f✝) (η✝.app β'✝ ∘ f'✝)) x✝
Module: Mathlib.Control.Fix

Goal state before:
pp: case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x✝).Dom
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x : α
⊢ none = Fix.approx f 0 x

pp: case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x✝).Dom
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x : α
⊢ ¬¬p ↑z

Tactic:
·

Goal state after:
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x✝).Dom
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x : α
⊢ none = Fix.approx f 0 x
Module: Mathlib.Control.Fix

Goal state before:
pp: case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x✝).Dom
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x : α
⊢ ¬¬p ↑z

Tactic:
·

Goal state after:
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x✝ : α
h' : ∃ i, (Fix.approx f i x✝).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x✝).Dom
z : Upto p
_this : p (0 + ↑z)
hk : Nat.find h' = 0 + ↑z
x' : α
hwf✝ : WellFounded fun y x ↦ x < y
x : α
⊢ ¬¬p ↑z
Module: Mathlib.Control.Fold

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : β → α → m β
⊢ ∀ (x y : FreeMonoid α),
    op (flip (List.foldlM f) (FreeMonoid.toList (x * y))) =
      op (flip (List.foldlM f) (FreeMonoid.toList x)) * op (flip (List.foldlM f) (FreeMonoid.toList y))

Tactic:
intros
    apply unop_injective
    funext
    apply List.foldlM_append

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: case cons
α : Type u
head✝ : α
tail✝ : List α
ih : FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) = head✝ :: tail✝

Tactic:
conv_rhs => rw [← ih]

Goal state after:
case cons
α : Type u
head✝ : α
tail✝ : List α
ih : FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝) = tail✝
⊢ FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) (head✝ :: tail✝)) =
    head✝ :: FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) tail✝)
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case mp
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F α
h₂ : P u
⊢ ∃ u, q u

pp: case mpr
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ ∃ u, P u

Tactic:
·

Goal state after:
case mp
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F α
h₂ : P u
⊢ ∃ u, q u
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case mpr
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ ∃ u, P u

Tactic:
·

Goal state after:
case mpr
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
u : F β
h₂ : q u
⊢ ∃ u, P u
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ f P n α ⊚ g P n α = TypeVec.id

pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ ∀ (u : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }),
    (fun i ↦ Subtype.val) <$$> u = x ↔ (fun i ↦ Subtype.val) <$$> f P n α <$$> u = x

Tactic:
·

Goal state after:
case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ f P n α ⊚ g P n α = TypeVec.id
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ ∀ (u : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }),
    (fun i ↦ Subtype.val) <$$> u = x ↔ (fun i ↦ Subtype.val) <$$> f P n α <$$> u = x

Tactic:
·

Goal state after:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ ∀ (u : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }),
    (fun i ↦ Subtype.val) <$$> u = x ↔ (fun i ↦ Subtype.val) <$$> f P n α <$$> u = x
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
⊢ f' rr n α ⊚ g' rr n α = TypeVec.id

pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
⊢ ∀ (u : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }),
    (fun i t ↦ (↑t).1) <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> u = y ↔
      (fun i t ↦ (↑t).1) <$$> f' rr n α <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> f' rr n α <$$> u = y

Tactic:
·

Goal state after:
case h₀
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
⊢ f' rr n α ⊚ g' rr n α = TypeVec.id
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
⊢ ∀ (u : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }),
    (fun i t ↦ (↑t).1) <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> u = y ↔
      (fun i t ↦ (↑t).1) <$$> f' rr n α <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> f' rr n α <$$> u = y

Tactic:
·

Goal state after:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
⊢ ∀ (u : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }),
    (fun i t ↦ (↑t).1) <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> u = y ↔
      (fun i t ↦ (↑t).1) <$$> f' rr n α <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> f' rr n α <$$> u = y
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case succ.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
j : ℕ
ih : j + 1 ≤ j → approx (⇑f) (j + 1) ≤ approx (⇑f) j
⊢ approx (⇑f) (j + 1) ≤ approx (⇑f) (j + 1)

pp: case succ.step
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
ih : i ≤ j → approx (⇑f) i ≤ approx (⇑f) j
a✝ : i.le j
⊢ approx (⇑f) i ≤ approx (⇑f) (j + 1)

Tactic:
·

Goal state after:
case succ.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
j : ℕ
ih : j + 1 ≤ j → approx (⇑f) (j + 1) ≤ approx (⇑f) j
⊢ approx (⇑f) (j + 1) ≤ approx (⇑f) (j + 1)
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ approx (⇑f) i a

pp: case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ¬∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ approx (⇑f) i a

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ approx (⇑f) i a
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mp
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : b ∈ approx (⇑f) (Nat.find h₀).succ a
⊢ ∃ i, b ∈ approx (⇑f) i a

pp: case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : ∃ i, b ∈ approx (⇑f) i a
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a

Tactic:
·

Goal state after:
case pos.mp
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
hh : b ∈ approx (⇑f) (Nat.find h₀).succ a
⊢ ∃ i, b ∈ approx (⇑f) i a
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr.inr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
⊢ y = b

pp: α✝ : Type u_1
β✝ : α✝ → Type u_2
f✝ : ((a : α✝) → Part (β✝ a)) →o (a : α✝) → Part (β✝ a)
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
case : i ≤ j
⊢ y = b

Tactic:
·

Goal state after:
case pos.mpr.inr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
⊢ y = b
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
⊢ f Fin2.fz = g Fin2.fz

pp: case fs
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
a✝ : Fin2 n
⊢ f a✝.fs = g a✝.fs

Tactic:
·

Goal state after:
case fz
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
⊢ f Fin2.fz = g Fin2.fz
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fs
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
a✝ : Fin2 n
⊢ f a✝.fs = g a✝.fs

Tactic:
·

Goal state after:
case fs
n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
a✝ : Fin2 n
⊢ f a✝.fs = g a✝.fs
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ¬∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ approx (⇑f) i a

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ¬∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ approx (⇑f) i a
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case refine_1
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
x✝ : ¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
h₁ : ¬(π x).2 = none
h₂ : ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
⊢ ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i

pp: case refine_2
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
hn' : (π x).2 = ↑n
⊢ ¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x

Tactic:
·

Goal state after:
case refine_1
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
x✝ : ¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
h₁ : ¬(π x).2 = none
h₂ : ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
⊢ ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case refine_2
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
hn' : (π x).2 = ↑n
⊢ ¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x

Tactic:
·

Goal state after:
case refine_2
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
hn' : (π x).2 = ↑n
⊢ ¬(π x).2 = none ∧ ∀ (x_1 : X) (x_2 : S), ¬σ (Option.some x_1) x_2 = x
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∃ i b, b ∈ approx (⇑f) i x
⊢ ∃ i, Part.fix (⇑f) x ≤ approx (⇑f) i x

pp: case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (i : ℕ) (b : β x), b ∉ approx (⇑f) i x
⊢ ∃ i, Part.fix (⇑f) x ≤ approx (⇑f) i x

Tactic:
·

Goal state after:
case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∃ i b, b ∈ approx (⇑f) i x
⊢ ∃ i, Part.fix (⇑f) x ≤ approx (⇑f) i x
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (i : ℕ) (b : β x), b ∉ approx (⇑f) i x
⊢ ∃ i, Part.fix (⇑f) x ≤ approx (⇑f) i x

Tactic:
·

Goal state after:
case neg
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
hh : ∀ (i : ℕ) (b : β x), b ∉ approx (⇑f) i x
⊢ ∃ i, Part.fix (⇑f) x ≤ approx (⇑f) i x
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ Part.fix ⇑f ≤ ωSup (approxChain f)

pp: case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ωSup (approxChain f) ≤ Part.fix ⇑f

Tactic:
·

Goal state after:
case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ Part.fix ⇑f ≤ ωSup (approxChain f)
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ approx (⇑f) i.succ x

pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ approx (⇑f) i.succ x ≤ ωSup (approxChain f) x

Tactic:
·

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ approx (⇑f) i.succ x
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ ?m.39

pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ ?m.39 ≤ approx (⇑f) i.succ x

pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ Part (β x)

Tactic:
·

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ Part.fix (⇑f) x ≤ ?m.39
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case refine_1
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
i : X
⊢ IsOpen (Set.range (σ (Option.some i)))ᶜ

pp: case refine_2
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
i : X
⊢ IsOpen (Prod.snd ∘ π ⁻¹' {↑i})

Tactic:
·

Goal state after:
case refine_1
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
i : X
⊢ IsOpen (Set.range (σ (Option.some i)))ᶜ
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ approx (⇑f) i x ≤ approx (⇑f) i.succ x

Tactic:
·

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
i : ℕ
hx : Part.fix (⇑f) x ≤ approx (⇑f) i x
⊢ approx (⇑f) i x ≤ approx (⇑f) i.succ x
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case refine_2
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
i : X
⊢ IsOpen (Prod.snd ∘ π ⁻¹' {↑i})

Tactic:
·

Goal state after:
case refine_2
S : Type u_1
T : Type u_2
X : Type u_3
inst✝⁵ : TopologicalSpace S
inst✝⁴ : TopologicalSpace T
inst✝³ : TopologicalSpace X
inst✝² : DiscreteTopology X
inst✝¹ : T2Space T
inst✝ : CompactSpace S
π : T → S × OnePoint X
hπ : Continuous π
σ : Option X → S → T
hσ : ∀ (x : Option X), Continuous (σ x)
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
i : X
⊢ IsOpen (Prod.snd ∘ π ⁻¹' {↑i})
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ωSup (approxChain f) ≤ Part.fix ⇑f

Tactic:
·

Goal state after:
case a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ωSup (approxChain f) ≤ Part.fix ⇑f
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: case none
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
⊢ ∃ a, (fun x ↦ π ↑x) a = (s, none)

pp: case some
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
x : X
⊢ ∃ a, (fun x ↦ π ↑x) a = (s, Option.some x)

Tactic:
·

Goal state after:
case none
S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
hπ : Function.Surjective π
σ : Option X → S → T
hσ : ∀ (x : Option X) (s : S), (π (σ x s)).1 = s
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
s : S
⊢ ∃ a, (fun x ↦ π ↑x) a = (s, none)