mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: case zero
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : a.coeff 0 ≠ 0
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung)^[n] b ≠ 0
ha0 : (⇑verschiebung)^[0] a ≠ 0
hab : ↑p = (⇑verschiebung)^[0] a * (⇑verschiebung)^[n] b
⊢ IsUnit ((⇑verschiebung)^[0] a) ∨ IsUnit ((⇑verschiebung)^[n] b)

pp: case succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : a.coeff 0 ≠ 0
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung)^[n] b ≠ 0
n✝ : ℕ
ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0
hab : ↑p = (⇑verschiebung)^[n✝ + 1] a * (⇑verschiebung)^[n] b
⊢ IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n] b)

Tactic:
;

Goal state after:
case zero
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : a.coeff 0 ≠ 0
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung)^[n] b ≠ 0
ha0 : (⇑verschiebung)^[0] a ≠ 0
hab : ↑p = (⇑verschiebung)^[0] a * (⇑verschiebung)^[n] b
⊢ IsUnit ((⇑verschiebung)^[0] a) ∨ IsUnit ((⇑verschiebung)^[n] b)

case succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : a.coeff 0 ≠ 0
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung)^[n] b ≠ 0
n✝ : ℕ
ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0
hab : ↑p = (⇑verschiebung)^[n✝ + 1] a * (⇑verschiebung)^[n] b
⊢ IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n] b)
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: case succ.zero
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n✝ : ℕ
ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0
hb0 : (⇑verschiebung)^[0] b ≠ 0
hab : ↑p = (⇑verschiebung)^[n✝ + 1] a * (⇑verschiebung)^[0] b
⊢ IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[0] b)

pp: case succ.succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n✝ : ℕ
ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0
n : ℕ
hb0 : (⇑verschiebung)^[n + 1] b ≠ 0
hab : ↑p = (⇑verschiebung)^[n✝ + 1] a * (⇑verschiebung)^[n + 1] b
⊢ IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n + 1] b)

Tactic:
;

Goal state after:
case succ.zero
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n✝ : ℕ
ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0
hb0 : (⇑verschiebung)^[0] b ≠ 0
hab : ↑p = (⇑verschiebung)^[n✝ + 1] a * (⇑verschiebung)^[0] b
⊢ IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[0] b)

case succ.succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n✝ : ℕ
ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0
n : ℕ
hb0 : (⇑verschiebung)^[n + 1] b ≠ 0
hab : ↑p = (⇑verschiebung)^[n✝ + 1] a * (⇑verschiebung)^[n + 1] b
⊢ IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n + 1] b)
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
x : 𝕎 k
⊢ verschiebung (frobenius x) = (⇑verschiebung ∘ ⇑frobenius) x

Tactic:
;

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
x : 𝕎 k
⊢ verschiebung (frobenius x) = (⇑verschiebung ∘ ⇑frobenius) x
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: case e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
this :
  succNthVal p n a₁ a₂ (fun i ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) +
        a₁.coeff (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun v ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p) (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun i ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
        a₂.coeff (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (fun i ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑i) (truncateFun (n + 1) a₂)
⊢ truncateFun (n + 1) (frobenius (mk p (frobeniusRotationCoeff p ha₁ ha₂))) = fun v ↦
    frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p

Tactic:
;

Goal state after:
case e'_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
n : ℕ
this :
  succNthVal p n a₁ a₂ (fun i ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) +
        a₁.coeff (n + 1) * (solution p a₁ a₂ ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun v ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p) (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ (fun i ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑i) ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
        a₂.coeff (n + 1) * solution p a₁ a₂ ^ p ^ (n + 1) +
      nthRemainder p n (fun i ↦ frobeniusRotationCoeff p ha₁ ha₂ ↑i) (truncateFun (n + 1) a₂)
⊢ truncateFun (n + 1) (frobenius (mk p (frobeniusRotationCoeff p ha₁ ha₂))) = fun v ↦
    frobeniusRotationCoeff p ha₁ ha₂ ↑v ^ p
Module: Mathlib.RingTheory.ZMod.Torsion

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
this : 2 ≤ p
⊢ p - 1 ≠ 0

Tactic:
;

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : 2 ≤ p
⊢ p - 1 ≠ 0
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (↑p ^ (n + 1) *
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars ⊆
    univ ×ˢ range (n + 1)

Tactic:
;

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (↑p ^ (n + 1) *
        (wittMul p (n + 1) + ↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1) -
            X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars ⊆
    univ ×ˢ range (n + 1)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inl
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h✝ : IsEmpty α
⊢ IsClub (⋂₀ s)

pp: case inr
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
⊢ IsClub (⋂₀ s)

Tactic:
;

Goal state after:
case inl
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h✝ : IsEmpty α
⊢ IsClub (⋂₀ s)

case inr
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
⊢ IsClub (⋂₀ s)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inl
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : IsEmpty α
⊢ IsClub (⋂₀ s)

pp: case inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
⊢ IsClub (⋂₀ s)

Tactic:
;

Goal state after:
case inl
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : IsEmpty α
⊢ IsClub (⋂₀ s)

case inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
⊢ IsClub (⋂₀ s)
Module: Mathlib.SetTheory.Cardinal.EventuallyConst

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
hf : Monotone f
hα : lift.{u, v} #β < lift.{v, u} (cof α)
this : IsEmpty α
⊢ False

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
hf : Monotone f
hα : lift.{u, v} #β < lift.{v, u} (cof α)
this : IsEmpty α
⊢ False
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hs : ∀ x ∈ s, IsClub x
hα : cof α < ℵ₀
⊢ cof α ≤ 1

Tactic:
← cof_lt_aleph0_iff

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hs : ∀ x ∈ s, IsClub x
hα : cof α < ℵ₀
⊢ cof α < ℵ₀
Module: Mathlib.SetTheory.Cardinal.EventuallyConst

Goal state before:
pp: β : Type v
inst✝¹ : PartialOrder β
f : Cardinal.{v} → β
inst✝ : Small.{v, v} β
hf : Monotone f
⊢ EventuallyConst f atTop

Tactic:
refine .of_monotone_of_lt_cof hf ?_
  simpa [← small_iff_lift_mk_lt_univ]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.EventuallyConst

Goal state before:
pp: β : Type v
inst✝¹ : PartialOrder β
f : Ordinal.{v} → β
inst✝ : Small.{v, v} β
hf : Monotone f
⊢ EventuallyConst f atTop

Tactic:
refine .of_monotone_of_lt_cof hf ?_
  simpa [← small_iff_lift_mk_lt_univ]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.UnivLE

Goal state before:
pp: case refine_2.mk
h✝ : univ.{v, u + 1} < univ.{u, v + 1}
w✝ : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent) α)
⊢ ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α

Tactic:
;

Goal state after:
case refine_2.mk
h✝ : univ.{v, u + 1} < univ.{u, v + 1}
w✝ : Cardinal.{u}
α : Type u
h : univ.{v, u + 1} = lift.{max (u + 1) (v + 1), u} (Quot.mk (⇑isEquivalent) α)
⊢ ∃ α, univ.{v, max u (v + 1)} ≤ lift.{v + 1, u} #α
Module: Mathlib.SetTheory.Cardinal.UnivLE

Goal state before:
pp: ⊢ univ.{u, v + 1} ≤ univ.{v, u + 1} ∨ univ.{v, u + 1} ≤ univ.{u, v + 1}

Tactic:
;

Goal state after:
⊢ univ.{u, v + 1} ≤ univ.{v, u + 1} ∨ univ.{v, u + 1} ≤ univ.{u, v + 1}
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
S : Set (Set (List A))
hS : S ⊆ {T | ∀ ⦃x : List A⦄ ⦃a : A⦄, x ++ [a] ∈ T → x ∈ T}
x : List A
a : A
t : Set (List A)
ht : t ∈ S
hx : x ++ [a] ∈ t
⊢ x ∈ sSup S

Tactic:
;

Goal state after:
A : Type u_1
S : Set (Set (List A))
hS : S ⊆ {T | ∀ ⦃x : List A⦄ ⦃a : A⦄, x ++ [a] ∈ T → x ∈ T}
x : List A
a : A
t : Set (List A)
ht : t ∈ S
hx : x ++ [a] ∈ t
⊢ x ∈ sSup S
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
S : Set (Set (List A))
hS : S ⊆ {T | ∀ ⦃x : List A⦄ ⦃a : A⦄, x ++ [a] ∈ T → x ∈ T}
x : List A
a : A
h : x ++ [a] ∈ sInf S
T : Set (List A)
hT : T ∈ S
⊢ x ∈ T

Tactic:
;

Goal state after:
A : Type u_1
S : Set (Set (List A))
hS : S ⊆ {T | ∀ ⦃x : List A⦄ ⦃a : A⦄, x ++ [a] ∈ T → x ∈ T}
x : List A
a : A
h : x ++ [a] ∈ sInf S
T : Set (List A)
hT : T ∈ S
⊢ x ∈ T
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x w✝ : List A
h : x ++ w✝ ∈ T
⊢ x ∈ T

Tactic:
;

Goal state after:
A : Type u_1
T : ↥(tree A)
x w✝ : List A
h : x ++ w✝ ∈ T
⊢ x ∈ T
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
⊢ [] ∉ ⊥

Tactic:
;

Goal state after:
A : Type u_1
⊢ [] ∉ ⊥
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
h : [] ∉ T
x : List A
⊢ x ∈ T ↔ x ∈ ⊥

Tactic:
;

Goal state after:
A : Type u_1
T : ↥(tree A)
h : [] ∉ T
x : List A
⊢ x ∈ T ↔ x ∈ ⊥
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inl
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : IsEmpty α
⊢ IsClub (Function.fixedPoints f)

pp: case inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
⊢ IsClub (Function.fixedPoints f)

Tactic:
;

Goal state after:
case inl
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : IsEmpty α
⊢ IsClub (Function.fixedPoints f)

case inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
⊢ IsClub (Function.fixedPoints f)
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x y x✝ : List A
⊢ x✝ ∈ subAt (subAt T x) y ↔ x✝ ∈ subAt T (x ++ y)

Tactic:
;

Goal state after:
A : Type u_1
T : ↥(tree A)
x y x✝ : List A
⊢ x✝ ∈ subAt (subAt T x) y ↔ x✝ ∈ subAt T (x ++ y)
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x y : List A
hl : x.length ≤ y.length
h1 : List.take x.length y <+: x
h2 : List.drop x.length y ∈ T
⊢ ∃ z ∈ T, y = x ++ z

Tactic:
;

Goal state after:
A : Type u_1
T : ↥(tree A)
x y : List A
hl : x.length ≤ y.length
h1 : List.take x.length y <+: x
h2 : List.drop x.length y ∈ T
⊢ ∃ z ∈ T, y = x ++ z
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case h
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
a : α
val✝ : OrderTop α
⊢ ⊤ ∈ Function.fixedPoints f ∧ a ≤ ⊤

Tactic:
;

Goal state after:
case h
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
a : α
val✝ : OrderTop α
⊢ ⊤ ∈ Function.fixedPoints f ∧ a ≤ ⊤
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x y : List A
h : y ∈ pullSub (subAt T x) x
⊢ y ∈ ↑T

Tactic:
;

Goal state after:
A : Type u_1
T : ↥(tree A)
x y : List A
h : y ∈ pullSub (subAt T x) x
⊢ y ∈ ↑T
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case inl
A : Type u_1
T : ↥(tree A)
x y : List A
h : y <+: x ∧ [] ∈ subAt T x
h' : y.length ≤ x.length
⊢ y ∈ ↑T

Tactic:
;

Goal state after:
case inl
A : Type u_1
T : ↥(tree A)
x y : List A
h : y <+: x ∧ [] ∈ subAt T x
h' : y.length ≤ x.length
⊢ y ∈ ↑T
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case inr
A : Type u_1
T : ↥(tree A)
x y : List A
h : ∃ z ∈ subAt T x, y = x ++ z
h' : x.length ≤ y.length
⊢ y ∈ ↑T

Tactic:
;

Goal state after:
case inr
A : Type u_1
T : ↥(tree A)
x y : List A
h : ∃ z ∈ subAt T x, y = x ++ z
h' : x.length ≤ y.length
⊢ y ∈ ↑T
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case inr
A : Type u_1
T : ↥(tree A)
x w✝ : List A
h : w✝ ∈ subAt T x
h' : x.length ≤ (x ++ w✝).length
⊢ x ++ w✝ ∈ ↑T

Tactic:
;

Goal state after:
case inr
A : Type u_1
T : ↥(tree A)
x w✝ : List A
h : w✝ ∈ subAt T x
h' : x.length ≤ (x ++ w✝).length
⊢ x ++ w✝ ∈ ↑T
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x y : List A
⊢ y ∈ subAt (pullSub T x) x ↔ y ∈ T

Tactic:
;

Goal state after:
A : Type u_1
T : ↥(tree A)
x y : List A
⊢ y ∈ subAt (pullSub T x) x ↔ y ∈ T
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
S T : ↥(tree A)
x : List A
x✝ : pullSub S x ≤ T
⊢ subAt (pullSub S x) x ≤ subAt T x

Tactic:
;

Goal state after:
A : Type u_1
S T : ↥(tree A)
x : List A
x✝ : pullSub S x ≤ T
⊢ subAt (pullSub S x) x ≤ subAt T x
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x y z : List A
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)

Tactic:
;

Goal state after:
A : Type u_1
T : ↥(tree A)
x y z : List A
⊢ z ∈ pullSub (pullSub T y) x ↔ z ∈ pullSub T (x ++ y)
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
h : List.take (x ++ y).length z <+: x ++ y
right✝ : List.drop (x ++ y).length z ∈ T
⊢ ?m.103

Tactic:
simpa [List.take_take] using h.take x.length

Goal state after:
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x y z : List A
hl : z.length ≤ x.length
⊢ z.length ≤ x.length + y.length

Tactic:
;

Goal state after:
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : z.length ≤ x.length
⊢ z.length ≤ x.length + y.length
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inl
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hα : cof α < ℵ₀
⊢ cof α ≤ 1

Tactic:
← cof_lt_aleph0_iff

Goal state after:
case inl
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : s.Countable
hα : cof α < ℵ₀
⊢ cof α < ℵ₀
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case cons.mk
α : Type u_1
l₁ l₂ : Lists' α true
a' a'✝ : Lists α
l✝ : Lists' α true
e : a' ~ a'✝
m : a'✝ ∈ l₂.toList
s : l✝.Subset l₂
fst✝ : Bool
snd✝ : Lists' α fst✝
h' : cons ⟨fst✝, snd✝⟩ l₁ = cons a' l✝
⊢ ⟨fst✝, snd✝⟩ ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
;

Goal state after:
case cons.mk
α : Type u_1
l₁ l₂ : Lists' α true
a' a'✝ : Lists α
l✝ : Lists' α true
e : a' ~ a'✝
m : a'✝ ∈ l₂.toList
s : l✝.Subset l₂
fst✝ : Bool
snd✝ : Lists' α fst✝
h' : cons ⟨fst✝, snd✝⟩ l₁ = cons a' l✝
⊢ ⟨fst✝, snd✝⟩ ∈ l₂ ∧ l₁ ⊆ l₂
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case cons.mk.mk
α : Type u_1
l₁ l₂ : Lists' α true
a'✝ : Lists α
l✝ : Lists' α true
m : a'✝ ∈ l₂.toList
s : l✝.Subset l₂
fst✝¹ : Bool
snd✝¹ : Lists' α fst✝¹
fst✝ : Bool
snd✝ : Lists' α fst✝
e : ⟨fst✝, snd✝⟩ ~ a'✝
h' : cons ⟨fst✝¹, snd✝¹⟩ l₁ = cons ⟨fst✝, snd✝⟩ l✝
⊢ ⟨fst✝¹, snd✝¹⟩ ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
;

Goal state after:
case cons.mk.mk
α : Type u_1
l₁ l₂ : Lists' α true
a'✝ : Lists α
l✝ : Lists' α true
m : a'✝ ∈ l₂.toList
s : l✝.Subset l₂
fst✝¹ : Bool
snd✝¹ : Lists' α fst✝¹
fst✝ : Bool
snd✝ : Lists' α fst✝
e : ⟨fst✝, snd✝⟩ ~ a'✝
h' : cons ⟨fst✝¹, snd✝¹⟩ l₁ = cons ⟨fst✝, snd✝⟩ l✝
⊢ ⟨fst✝¹, snd✝¹⟩ ∈ l₂ ∧ l₁ ⊆ l₂
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case cons.mk.mk.refl
α : Type u_1
l₁ l₂ : Lists' α true
a'✝ : Lists α
m : a'✝ ∈ l₂.toList
fst✝ : Bool
snd✝ : Lists' α fst✝
e : ⟨fst✝, snd✝⟩ ~ a'✝
s : l₁.Subset l₂
⊢ ⟨fst✝, snd✝⟩ ∈ l₂ ∧ l₁ ⊆ l₂

Tactic:
;

Goal state after:
case cons.mk.mk.refl
α : Type u_1
l₁ l₂ : Lists' α true
a'✝ : Lists α
m : a'✝ ∈ l₂.toList
fst✝ : Bool
snd✝ : Lists' α fst✝
e : ⟨fst✝, snd✝⟩ ~ a'✝
s : l₁.Subset l₂
⊢ ⟨fst✝, snd✝⟩ ∈ l₂ ∧ l₁ ⊆ l₂
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case cons
α : Type u_1
l₂ : List (Lists α)
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ ∈ l₂ ∧ tail✝ ⊆ l₂
⊢ head✝ ∈ (ofList l₂).toList

Tactic:
;

Goal state after:
case cons
α : Type u_1
l₂ : List (Lists α)
head✝ : Lists α
tail✝ : List (Lists α)
l₁_ih : tail✝ ⊆ l₂ → ofList tail✝ ⊆ ofList l₂
h : head✝ ∈ l₂ ∧ tail✝ ⊆ l₂
⊢ head✝ ∈ (ofList l₂).toList
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l : Lists' α true
⊢ ofList l.toList ⊆ ofList l.toList

Tactic:
;

Goal state after:
α : Type u_1
l : Lists' α true
⊢ ofList l.toList ⊆ ofList l.toList
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case refl
α : Type u_1
a : α
⊢ atom a = atom a

Tactic:
;

Goal state after:
case refl
α : Type u_1
a : α
⊢ atom a = atom a
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C0
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (a : α), trans (atom a)

pp: case C1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (l : Lists' α true), (∀ (l' : Lists α), l' ∈ l.toList → trans l') → trans (of' l)

pp: case D0
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (l' : Lists α), l' ∈ Lists'.nil.toList → trans l'

pp: case D1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (a : Lists α) (l : Lists' α true),
    trans a → (∀ (l' : Lists α), l' ∈ l.toList → trans l') → ∀ (l' : Lists α), l' ∈ (Lists'.cons a l).toList → trans l'

Tactic:
· intro a l₂ l₃ h₁ h₂
    rwa [← equiv_atom.1 h₁] at h₂

Goal state after:
case C1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (l : Lists' α true), (∀ (l' : Lists α), l' ∈ l.toList → trans l') → trans (of' l)

case D0
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (l' : Lists α), l' ∈ Lists'.nil.toList → trans l'

case D1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (a : Lists α) (l : Lists' α true),
    trans a → (∀ (l' : Lists α), l' ∈ l.toList → trans l') → ∀ (l' : Lists α), l' ∈ (Lists'.cons a l).toList → trans l'
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1.antisymm.antisymm
α : Type u_1
trans : Lists α → Prop := ⋯
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
⊢ l₁ ⊆ l₂✝ ∧ l₂✝ ⊆ l₁

Tactic:
;

Goal state after:
case C1.antisymm.antisymm
α : Type u_1
trans : Lists α → Prop := ⋯
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
⊢ l₁ ⊆ l₂✝ ∧ l₂✝ ⊆ l₁
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ↑a < (succ #α).ord ∧ ∃ b < (succ #α).ord, ↑a ≠ b ∧ lfpApprox f x ↑a = lfpApprox f x b

Tactic:
;

Goal state after:
case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ↑a < (succ #α).ord ∧ ∃ b < (succ #α).ord, ↑a ≠ b ∧ lfpApprox f x ↑a = lfpApprox f x b
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ↑b < (succ #α).ord ∧ ↑a ≠ ↑b ∧ lfpApprox f x ↑a = lfpApprox f x ↑b

Tactic:
;

Goal state after:
case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ↑b < (succ #α).ord ∧ ↑a ≠ ↑b ∧ lfpApprox f x ↑a = lfpApprox f x ↑b