mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
hx : x ∈ f.ker ⊓ I • ⊤
y : TensorProduct R (↥I) M
hy : (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) y = x
⊢ Function.Injective ⇑(↑(TensorProduct.lid R N) ∘ₗ rTensor N (Submodule.subtype I))

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
hx : x ∈ f.ker ⊓ I • ⊤
y : TensorProduct R (↥I) M
hy : (↑(TensorProduct.lid R M) ∘ₗ rTensor M (Submodule.subtype I)) y = x
⊢ Function.Injective ⇑(rTensor N (Submodule.subtype I))
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝¹ x✝ : R
⊢ if x✝ * x✝¹ = 0 then x✝¹ * x✝ = 0 else True

Tactic:
simpa using

Goal state after:
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝¹ x✝ : R
⊢ x✝ = 0 ∨ x✝¹ = 0 → x✝¹ = 0 ∨ x✝ = 0
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: case refine_2.smul
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
r : R
hr : r ∈ I
m : M
hm : m ∈ f.ker
⊢ r • m ∈ f.ker ⊓ I • ⊤

Tactic:
simpa using

Goal state after:
case refine_2.smul
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
x : M
r : R
hr : r ∈ I
m : M
hm : m ∈ f.ker
⊢ r • m ∈ I • ⊤
Module: Mathlib.RingTheory.Valuation.Extension

Goal state before:
pp: R : Type u_1
A : Type u_2
ΓR : Type u_3
ΓA : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : LinearOrderedCommMonoidWithZero ΓR
inst✝² : LinearOrderedCommMonoidWithZero ΓA
inst✝¹ : Algebra R A
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : vR.HasExtension vA
x y : R
⊢ vA ((algebraMap R A) x) < vA ((algebraMap R A) y) ↔ vR x < vR y

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
ΓR : Type u_3
ΓA : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : LinearOrderedCommMonoidWithZero ΓR
inst✝² : LinearOrderedCommMonoidWithZero ΓA
inst✝¹ : Algebra R A
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : vR.HasExtension vA
x y : R
⊢ vA ((algebraMap R A) x) < vA ((algebraMap R A) y) ↔ vR x < vR y
Module: Mathlib.RingTheory.Valuation.Extension

Goal state before:
pp: R : Type u_1
A : Type u_2
ΓR : Type u_3
ΓA : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : LinearOrderedCommMonoidWithZero ΓR
inst✝² : LinearOrderedCommMonoidWithZero ΓA
inst✝¹ : Algebra R A
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : vR.HasExtension vA
x : R
⊢ vA ((algebraMap R A) x) ≤ 1 ↔ vR x ≤ 1

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
ΓR : Type u_3
ΓA : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : LinearOrderedCommMonoidWithZero ΓR
inst✝² : LinearOrderedCommMonoidWithZero ΓA
inst✝¹ : Algebra R A
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : vR.HasExtension vA
x : R
⊢ vA ((algebraMap R A) x) ≤ 1 ↔ vR x ≤ 1
Module: Mathlib.RingTheory.Valuation.Extension

Goal state before:
pp: R : Type u_1
A : Type u_2
ΓR : Type u_3
ΓA : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : LinearOrderedCommMonoidWithZero ΓR
inst✝² : LinearOrderedCommMonoidWithZero ΓA
inst✝¹ : Algebra R A
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : vR.HasExtension vA
x : R
⊢ vA ((algebraMap R A) x) < 1 ↔ vR x < 1

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
ΓR : Type u_3
ΓA : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : LinearOrderedCommMonoidWithZero ΓR
inst✝² : LinearOrderedCommMonoidWithZero ΓA
inst✝¹ : Algebra R A
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : vR.HasExtension vA
x : R
⊢ vA ((algebraMap R A) x) < 1 ↔ vR x < 1
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
this : ∀ {x : R} (h : x ∈ I * J), f (J.toCotangent ⟨x, ⋯⟩) = 0
x : J.Cotangent
hx : x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x' : ↥J
hx' : x' ∈ Submodule.comap (Submodule.subtype J) (I * J)
eq : J.toCotangent x' = x
⊢ x ∈ f.ker

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
this : ∀ {x : R} (h : x ∈ I * J), f (J.toCotangent ⟨x, ⋯⟩) = 0
x : J.Cotangent
hx : x ∈ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x' : ↥J
hx' : x' ∈ Submodule.comap (Submodule.subtype J) (I * J)
eq : J.toCotangent x' = x
⊢ f (J.toCotangent x') = 0
Module: Mathlib.RingTheory.Valuation.Extension

Goal state before:
pp: R : Type u_1
A : Type u_2
ΓR : Type u_3
ΓA : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : LinearOrderedCommMonoidWithZero ΓR
inst✝² : LinearOrderedCommMonoidWithZero ΓA
inst✝¹ : Algebra R A
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : vR.HasExtension vA
x : R
⊢ vA ((algebraMap R A) x) = 1 ↔ vR x = 1

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
ΓR : Type u_3
ΓA : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : LinearOrderedCommMonoidWithZero ΓR
inst✝² : LinearOrderedCommMonoidWithZero ΓA
inst✝¹ : Algebra R A
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : vR.HasExtension vA
x : R
⊢ vA ((algebraMap R A) x) ≤ 1 ∧ 1 ≤ vA ((algebraMap R A) x) ↔ vR x ≤ 1 ∧ 1 ≤ vR x
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : IsUnit ↑p
⊢ False

Tactic:
simpa using

Goal state after:
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : IsUnit ↑p
⊢ False
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
⊢ a ≠ 0 ∧ b ≠ 0

Tactic:
← mul_ne_zero_iff

Goal state after:
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
⊢ a * b ≠ 0
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ range (x + 1) ⊆ range n

Tactic:
simpa using

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ x < n
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ {(0, x)} ⊆ univ ×ˢ range (n + 1)

Tactic:
simpa using

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ x ≤ n
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ {(1, x)} ⊆ univ ×ˢ range (n + 1)

Tactic:
simpa using

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range (n + 1)
⊢ x ≤ n
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : 0 = a₂.coeff 0 / a₁.coeff 0
⊢ False

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : 0 = a₂.coeff 0 / a₁.coeff 0
⊢ False
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: 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
h : frobeniusRotation p ha₁ ha₂ = 0
⊢ solution p a₁ a₂ = 0

Tactic:
simpa using

Goal state after:
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
h : frobeniusRotation p ha₁ ha₂ = 0
⊢ solution p a₁ a₂ = 0
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : frobenius b * r' = q' * b
hq''' : q' ≠ 0
⊢ (algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' ≠ 0

Tactic:
simpa using

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
key : frobenius b * r' = q' * b
hq''' : q' ≠ 0
⊢ ¬(algebraMap (𝕎 k) (FractionRing (𝕎 k))) q' = 0
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
m : ℕ
r' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hr0 : ↑p ^ m * r' ≠ 0
n : ℕ
q' : 𝕎 k
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
hq0 : ↑p ^ n * q' ≠ 0
hrq : Localization.mk (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).1 (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).2 ≠ 0
b : 𝕎 k := frobeniusRotation p hr' hq'
⊢ (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b ≠ 0

Tactic:
simpa using

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a : FractionRing (𝕎 k)
m : ℕ
r' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hr0 : ↑p ^ m * r' ≠ 0
n : ℕ
q' : 𝕎 k
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
hq0 : ↑p ^ n * q' ≠ 0
hrq : Localization.mk (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).1 (↑p ^ m * r', ⟨↑p ^ n * q', hq⟩).2 ≠ 0
b : 𝕎 k := frobeniusRotation p hr' hq'
⊢ (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b ≠ 0
Module: Mathlib.RingTheory.ZMod.Torsion

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ : (ZMod p)ˣ
⊢ x✝ ∈ rootsOfUnity (p - 1) (ZMod p) ↔ x✝ ∈ ⊤

Tactic:
simpa using

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x✝ : (ZMod p)ˣ
⊢ ↑x✝ ^ (p - 1) = 1
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
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ Φ(p, k) x ≠ 0

Tactic:
simpa using

Goal state after:
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
⊢ Φ(p, k) x ≠ 0
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
hg : IsCofinal (range g)
⊢ #↑(range g) ≤ ℵ₀

Tactic:
simpa using

Goal state after:
α : 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
hg : IsCofinal (range g)
⊢ {x | ∃ y, g y = x}.Countable
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case nil
A : Type u_1
T : ↥(tree A)
x : List A
h : x ++ [] ∈ T
⊢ x ∈ T

Tactic:
simpa using

Goal state after:
case nil
A : Type u_1
T : ↥(tree A)
x : List A
h : x ++ [] ∈ T
⊢ x ∈ T
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:
simpa using

Goal state after:
A : Type u_1
T : ↥(tree A)
h : [] ∉ T
x : List A
⊢ x ∉ T
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:
simpa using

Goal state after:
α : Type v
s t : Set α
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
hα : cof α ≠ ℵ₀
hs : IsClub s
ht : IsClub t
⊢ IsClub (s ∩ t)
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case right
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
⊢ List.take x.length y ++ List.drop x.length y = x ++ List.drop x.length y

Tactic:
simpa using

Goal state after:
case right
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
⊢ List.take x.length y = x
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:
simpa using

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

Goal state before:
pp: case inr.refine_2.inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝¹ : Nonempty α
a : α
h✝ : NoMaxOrder α
h : IsCofinal (range fun n ↦ f^[n] a)
⊢ #↑(range fun n ↦ f^[n] a) ≤ ℵ₀

Tactic:
simpa using

Goal state after:
case inr.refine_2.inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝¹ : Nonempty α
a : α
h✝ : NoMaxOrder α
h : IsCofinal (range fun n ↦ f^[n] a)
⊢ {x | ∃ y, f^[y] a = x}.Countable
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:
simpa using

Goal state after:
A : Type u_1
T : ↥(tree A)
x y : List A
h : y <+: x ∧ [] ∈ subAt T x
h' : y.length ≤ x.length
⊢ x ∈ T
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

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

Tactic:
simpa using

Goal state after:
α : Type v
s : Set α
inst✝ : LinearOrder α
hs : IsStationary s
⊢ s.Nonempty
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

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

Tactic:
simpa using

Goal state after:
α : Type v
inst✝ : LinearOrder α
h : IsStationary ∅
⊢ False
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 using

Goal state after:
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
Module: Mathlib.SetTheory.Descriptive.Tree

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

Tactic:
simpa using

Goal state after:
case inr
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : z.length ≤ x.length
⊢ [] ∈ T → (z <+: x ↔ z <+: x ++ y)
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:
simpa using

Goal state after:
α : Type v
s t : Set α
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
hα : cof α ≠ ℵ₀
⊢ IsStationary (s ∪ t) ↔ IsStationary s ∨ IsStationary t
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:
simpa using

Goal state after:
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₃
⊢ 0 < o₁
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:
simpa using

Goal state after:
α : 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 #α)
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

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

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
a : Ordinal.{u}
⊢ ∀ i ≤ a, f (lfpApprox f x i) ≤ f (lfpApprox f x a)
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:
simpa using

Goal state after:
α : 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)
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case cons'
α : Type u_1
b✝¹ b✝ : Bool
b : Lists' α b✝
a : Lists' α true
a_ih✝ :
  ∀ (h : true = b✝),
    let l' := ⋯ ▸ b;
    ofList l'.toList = l'
IH :
  ∀ (h : true = true),
    let l' := ⋯ ▸ a;
    ofList l'.toList = l'
h : true = true
⊢ let l' := ⋯ ▸ b.cons' a;
  ofList l'.toList = l'

Tactic:
simpa using

Goal state after:
case cons'
α : Type u_1
b✝¹ b✝ : Bool
b : Lists' α b✝
a : Lists' α true
a_ih✝ :
  ∀ (h : true = b✝),
    let l' := ⋯ ▸ b;
    ofList l'.toList = l'
IH :
  ∀ (h : true = true),
    let l' := ⋯ ▸ a;
    ofList l'.toList = l'
h : true = true
⊢ ofList a.toList = a
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case refine_2
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : f x = x
o : Ordinal.{u}
this : lfpApprox f x 0 ∈ fixedPoints ⇑f
⊢ lfpApprox f x o = x

Tactic:
simpa using

Goal state after:
case refine_2
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : f x = x
o : Ordinal.{u}
this : lfpApprox f x 0 ∈ fixedPoints ⇑f
⊢ lfpApprox f x o = x
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : lfpApprox f x o = x
ho : o ≠ 0
hpos : 0 < o
hmem : lfpApprox f x 0 ∈ fixedPoints ⇑f
⊢ x ∈ fixedPoints ⇑f

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : lfpApprox f x o = x
ho : o ≠ 0
hpos : 0 < o
hmem : lfpApprox f x 0 ∈ fixedPoints ⇑f
⊢ IsFixedPt (⇑f) x
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2.inr.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hob : o < b
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
rw [CNF.of_lt ho hob]
        exact pairwise_singleton _ _

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case D1
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : Lists α
l : Lists' α true
IH₁ : trans a
IH₂ : ∀ (l' : Lists α), l' ∈ l.toList → trans l'
⊢ ∀ (l' : Lists α), l' ∈ (Lists'.cons a l).toList → trans l'

Tactic:
simpa using

Goal state after:
case D1
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : Lists α
l : Lists' α true
IH₁ : trans a
IH₂ : ∀ (l' : Lists α), l' ∈ l.toList → trans l'
⊢ trans a ∧ ∀ (a : Lists α), a ∈ l.toList → trans a
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
a : Ordinal.{u_1} × Ordinal.{u_1}
ha : a ∈ CNF b o
⊢ decide (a.toSigma.snd ≠ 0) = true

Tactic:
simpa using

Goal state after:
b o : Ordinal.{u_1}
a : Ordinal.{u_1} × Ordinal.{u_1}
ha : a ∈ CNF b o
⊢ ¬a.2 = 0
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ ∃ y, lfpApprox f ⊥ (succ #α).ord = ↑y

Tactic:
simpa using

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ IsFixedPt (⇑f) (lfpApprox f ⊥ (succ #α).ord)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inr.inr
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
ha : a ≠ 0
⊢ a ∉ map Prod.fst [(0, o)]

Tactic:
simpa using

Goal state after:
case inr.inr
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
ha : a ≠ 0
⊢ ¬a = 0
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
e' : Ordinal.{u_1}
⊢ (coeff b (b ^ e * x + y)) e' = (single e x + coeff b y) e'

Tactic:
rw [add_apply]

Goal state after:
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
⊢ (coeff b (b ^ e * x + y)) e' = (single e x) e' + (coeff b y) e'
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
h : IsOpen[inst✝³] {a}
ha : IsSuccLimit a
⊢ ∃ l, l < a

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
h : IsOpen[inst✝³] {a}
ha : IsSuccLimit a
⊢ ∃ l, l < a
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
h : IsOpen[inst✝³] {a}
ha : IsSuccLimit a
⊢ ∃ u, a < u

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
h : IsOpen[inst✝³] {a}
ha : IsSuccLimit a
⊢ ∃ u, a < u
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b e x : Ordinal.{u_1}
⊢ eval b (single e x) = b ^ e * x

Tactic:
simpa using

Goal state after:
b e x : Ordinal.{u_1}
⊢ eval b (single e x) = b ^ e * x