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

Goal state before:
pp: case h
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
c : StandardOneDimIsocrystal p k m
⊢ Φ(p, k) (F ((LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb) c)) =
    F ((LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb) (Φ(p, k) c))

Tactic:
LinearEquiv.smulOfNeZero_apply,

Goal state after:
case h
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
c : StandardOneDimIsocrystal p k m
⊢ Φ(p, k) (F (b • c)) = F ((LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb) (Φ(p, k) c))
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := fun t ↦ Nat.rec a (fun x IH ↦ sSup (range fun x ↦ f x IH)) t
⊢ BddAbove (range g)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.WittVector.Isocrystal

Goal state before:
pp: case h
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
c : StandardOneDimIsocrystal p k m
⊢ Φ(p, k) (F (b • c)) = F ((LinearEquiv.smulOfNeZero K(p, k) (StandardOneDimIsocrystal p k m) b hb) (Φ(p, k) c))

Tactic:
LinearEquiv.smulOfNeZero_apply,

Goal state after:
case h
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
F : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
c : StandardOneDimIsocrystal p k m
⊢ Φ(p, k) (F (b • c)) = F (b • Φ(p, k) c)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
⊢ ∃ f,
    ∀ (x y : 𝕎 k),
      f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
        (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

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

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
hf : ∀ (i : ι), IsClub (f i)
⊢ ∀ x ∈ range f, IsClub x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
⊢ ∃ f,
    ∀ (x y : 𝕎 k),
      (x * y).coeff (n + 1) =
        x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) + y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) +
          f (truncateFun (n + 1) x) (truncateFun (n + 1) y)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
hf : ∀ (i : ι), IsClub (f i)
⊢ IsClub (⋂ i, f i)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
f : α → β
inst✝ : Nonempty α
hf : Monotone f
hf' : ¬IsCofinal (range (rangeSplitting f))
⊢ EventuallyConst f atTop

Tactic:
by

Goal state after:
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 α)
⊢ Nonempty α

Tactic:
by

Goal state after:
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 α)
⊢ EventuallyConst f atTop

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.RingTheory.WittVector.Isocrystal

Goal state before:
pp: p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
⊢ ∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)

Tactic:
by

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

Goal state after:
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
⊢ IsClub (⋂₀ s)

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ↑(count p n) ≤ Cardinal.mk ↑{k | p k}

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ↑(count p n) ≤ {k | p k}.encard

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : {k | p k}.Finite
⊢ {k | p k}.encard ≠ ⊤

Tactic:
by

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : {k | p k}.Finite
⊢ count p n ≤ {k | p k}.ncard

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ⊢ UnivLE.{u, v} ↔ Nonempty (Ordinal.{u} ↪ Ordinal.{v})

Tactic:
by

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

Goal state before:
pp: ⊢ UnivLE.{u, v} ∨ UnivLE.{v, u}

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
y : A
ys : List A
ih : ∀ {x : List A}, x ++ ys ∈ T → x ∈ T
x : List A
h : x ++ y :: ys ∈ T
⊢ x ++ [?m.43] ++ ys ∈ T

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x y : List A
h' : x <+: y
h : y ∈ T
⊢ x ∈ T

Tactic:
by

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

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
⊢ T = ⊥ → [] ∉ T

Tactic:
by

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

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
h : [] ∉ T
⊢ T = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
ι : Sort u_1
f : ι → Set α
inst✝ : Countable ι
hα : cof α ≠ ℵ₀
hf : ∀ (i : ι), IsClub (f i)
⊢ IsClub (⋂₀ range f)

Tactic:
apply IsClub.sInter_of_countable hα (countable_range f)

Goal state after:
α : Type v
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
ι : Sort u_1
f : ι → Set α
inst✝ : Countable ι
hα : cof α ≠ ℵ₀
hf : ∀ (i : ι), IsClub (f i)
⊢ ∀ x ∈ range f, IsClub x
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
ι : Sort u_1
f : ι → Set α
inst✝ : Countable ι
hα : cof α ≠ ℵ₀
hf : ∀ (i : ι), IsClub (f i)
⊢ IsClub (⋂ i, f i)

Tactic:
rw [← sInter_range]
  apply IsClub.sInter_of_countable hα (countable_range f)
  simpa

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

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
m n : ℕ
x : ↥T
⊢ take m (take n x) = take (min m n) x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
ι : Sort u_1
f : ι → Set α
inst✝ : Countable ι
hα : cof α ≠ ℵ₀
hf : ∀ (i : ι), IsClub (f i)
⊢ IsClub (⋂ i, f i)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
s t : Set α
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
hα : cof α ≠ ℵ₀
hs : IsClub s
ht : IsClub t
⊢ IsClub (s ∩ t)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x : ↥T
m n : ℕ
⊢ take m x = take n x ↔ min m (↑x).length = min n (↑x).length

Tactic:
by

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

Goal state before:
pp: A : Type u_1
S T : ↥(tree A)
x y x✝¹ : List A
a : A
x✝ : x✝¹ ++ [a] ∈ (fun x_1 ↦ x ++ x_1) ⁻¹' ↑T
⊢ (fun x_1 ↦ x ++ x_1) x✝¹ ++ [a] ∈ T

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: A : Type u_1
S T : ↥(tree A)
x✝ y : List A
n : ℕ
x : ↥T
⊢ List.drop n ↑x ∈ subAt T ↑(take n x)

Tactic:
by

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

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x y : List A
hl : y.length ≤ x.length
⊢ y ∈ pullSub T x ↔ y <+: x ∧ [] ∈ T

Tactic:
by

Goal state after:
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
⊢ y ∈ pullSub T x → ∃ z ∈ T, y = x ++ z

Tactic:
by

Goal state after:
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
⊢ (∃ z ∈ T, y = x ++ z) → y ∈ pullSub T x

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ IsNormal (Subtype.val ∘ ⇑(enum s hs)) ↔ IsClub s

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
s : Set α
inst✝ : LinearOrder α
⊢ ¬IsStationary s ↔ ∃ t, IsClub t ∧ Disjoint s t

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
s : Set α
inst✝ : LinearOrder α
hs : IsStationary s
⊢ s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
⊢ IsStationary Set.univ ↔ Nonempty α

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
⊢ ¬IsStationary ∅

Tactic:
by

Goal state after:
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
⊢ S ≤ subAt T x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
⊢ pullSub T [] = T

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
s : Set α
inst✝ : LinearOrder α
hs : ¬IsCofinal sᶜ
⊢ IsStationary s

Tactic:
by

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

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 : x.length ≤ z.length
hp : ¬x <+: z
h : List.take x.length z <+: x
right✝ : List.drop x.length z ∈ pullSub T y
⊢ (List.take x.length z).length = x.length

Tactic:
by

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 : x.length ≤ z.length
hp : ¬x <+: z
right✝ : List.drop (x ++ y).length z ∈ T
h : List.take x.length z <+: x
⊢ (List.take x.length z).length = x.length

Tactic:
by

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
⊢ [].length ≤ y.length

Tactic:
by

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 ++ y).length

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
h : IsStationary (⋃₀ s)
⊢ ∃ x ∈ s, IsStationary x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
ι : Sort u_1
f : ι → Set α
hα : cof α ≤ 1
⊢ IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i)

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : OrderTop α
s : Set (Set α)
⊢ cof α ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : OrderTop α
ι : Sort u_1
f : ι → Set α
⊢ cof α ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
h : IsStationary (⋃₀ s)
⊢ ∃ x ∈ s, IsStationary x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
⊢ IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : s.Countable
⊢ IsStationary (⋃₀ s) ↔ ∃ x ∈ s, IsStationary x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
ι : Sort u_1
f : ι → Set α
inst✝ : Countable ι
hα : cof α ≠ ℵ₀
⊢ IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
s t : Set α
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
hα : cof α ≠ ℵ₀
⊢ IsStationary (s ∪ t) ↔ IsStationary s ∨ IsStationary t

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Commute

Goal state before:
pp: o₂ : Ordinal.{u_1}
hcomm : AddCommute 0 o₂
ih : ∀ y < 0 + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : 0 ≤ o₂
⊢ o₂ * ↑0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Commute

Goal state before:
pp: o₂ : Ordinal.{u_1}
hcomm : AddCommute 0 o₂
ih : ∀ y < 0 + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : 0 ≤ o₂
⊢ o₂ * ↑1 = o₂

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Commute

Goal state before:
pp: o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih : ∀ y < o₁ + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
⊢ o₁ + (o₁ + o₃) = o₁ + (o₃ + o₁)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Commute

Goal state before:
pp: o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih : ∀ y < o₁ + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
⊢ o₁ + o₃ < o₁ + o₂

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: C : Ordinal.{u_2} → Sort u_1
b : Ordinal.{u_2}
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ CNF.rec b H0 H 0 = H0

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_2}
C : Ordinal.{u_2} → Sort u_1
ho : o ≠ 0
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ CNF.rec b H0 H o = H o ho (CNF.rec b H0 H (o % b ^ log b o))

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Commute

Goal state before:
pp: o₁ o₂ : Ordinal.{u_1}
⊢ AddCommute o₁ o₂ ↔ ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
g : Ordinal.{u} → α
h_inj : InjOn g (Iio (succ #α).ord)
h : lift.{u, u + 1} #↑(Iio (succ #α).ord) ≤ lift.{u + 1, u} #α
⊢ #↑(Iio (succ #α).ord) = lift.{u + 1, u} (succ #α)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
g : Ordinal.{u} → α
⊢ ¬InjOn g (Iio (succ #α).ord)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
⊢ Monotone (lfpApprox f x)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
⊢ lfpApprox f x 0 = x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
⊢ x ≤ lfpApprox f x a

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a < b
⊢ f (lfpApprox f x a) ≤ lfpApprox f x b

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ CNF b (b ^ e * x + y) = (e, x) :: CNF b y

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: o : Ordinal.{u_1}
ho : o ≠ 0
⊢ CNF 0 o = [(0, o)]

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: o : Ordinal.{u_1}
ho : o ≠ 0
⊢ CNF 1 o = [(0, o)]

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
hb : b ≤ 1
ho : o ≠ 0
⊢ CNF b o = [(0, o)]

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
ho : o ≠ 0
hb : o < b
⊢ CNF b o = [(0, o)]

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
a : Ordinal.{u}
⊢ lfpApprox f x (a + 1) = f (lfpApprox f x a)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o) = o

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ x ≤ lfpApprox f x ↑⟨0, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l : List (Lists α)
⊢ (ofList l).toList = l

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
b : Ordinal.{u}
hab : b < a
⊢ f (lfpApprox f x b) ≤ lfpApprox f x ↑⟨b + 1, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
b : Bool
h : true = b
l : Lists' α b
⊢ let l' := ⋯ ▸ l;
  ofList l'.toList = l'

Tactic:
by

Goal state after: