mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: case pos
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✝¹ y✝ z✝ : R
x✝ : ¬if 0 = 0 then z✝ = 0 else True
h✝¹ : y✝ * z✝ = 0
h✝ : y✝ = 0
⊢ x✝¹ * z✝ = 0 → x✝¹ = 0

pp: case neg
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✝¹ y✝ z✝ : R
x✝ : ¬if 0 = 0 then z✝ = 0 else True
h✝¹ : y✝ * z✝ = 0
h✝ : ¬y✝ = 0
⊢ x✝¹ * z✝ = 0 → True

pp: case pos
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✝¹ y✝ z✝ : R
x✝ : ¬if 0 = 0 then z✝ = 0 else True
h✝¹ : ¬y✝ * z✝ = 0
h✝ : y✝ = 0
⊢ True → x✝¹ = 0

pp: case neg
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✝¹ y✝ z✝ : R
x✝ : ¬if 0 = 0 then z✝ = 0 else True
h✝¹ : ¬y✝ * z✝ = 0
h✝ : ¬y✝ = 0
⊢ True → True

Tactic:
<;>

Goal state after:
case pos
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✝¹ y✝ z✝ : R
x✝ : ¬if 0 = 0 then z✝ = 0 else True
h✝¹ : y✝ * z✝ = 0
h✝ : y✝ = 0
⊢ x✝¹ * z✝ = 0 → x✝¹ = 0

case neg
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✝¹ y✝ z✝ : R
x✝ : ¬if 0 = 0 then z✝ = 0 else True
h✝¹ : y✝ * z✝ = 0
h✝ : ¬y✝ = 0
⊢ x✝¹ * z✝ = 0 → True

case pos
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✝¹ y✝ z✝ : R
x✝ : ¬if 0 = 0 then z✝ = 0 else True
h✝¹ : ¬y✝ * z✝ = 0
h✝ : y✝ = 0
⊢ True → x✝¹ = 0

case neg
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✝¹ y✝ z✝ : R
x✝ : ¬if 0 = 0 then z✝ = 0 else True
h✝¹ : ¬y✝ * z✝ = 0
h✝ : ¬y✝ = 0
⊢ True → True
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: case pos
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
h✝ : 0 = 0
⊢ ¬1 = 0

pp: case neg
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
h✝ : ¬0 = 0
⊢ ¬True

Tactic:
<;>

Goal state after:
case pos
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
h✝ : 0 = 0
⊢ ¬1 = 0

case neg
R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
h✝ : ¬0 = 0
⊢ ¬True
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: case pos
R Γ : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
inst✝¹ : IsDomain R
inst✝ : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible 1
x✝¹ x✝ : R
h✝ : x✝ = 0
⊢ 1 x✝¹ ≤ 1 x✝ ↔ x✝¹ = 0

pp: case neg
R Γ : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
inst✝¹ : IsDomain R
inst✝ : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible 1
x✝¹ x✝ : R
h✝ : ¬x✝ = 0
⊢ 1 x✝¹ ≤ 1 x✝ ↔ True

Tactic:
<;>

Goal state after:
case pos
R Γ : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
inst✝¹ : IsDomain R
inst✝ : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible 1
x✝¹ x✝ : R
h✝ : x✝ = 0
⊢ 1 x✝¹ ≤ 1 x✝ ↔ x✝¹ = 0

case neg
R Γ : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
inst✝¹ : IsDomain R
inst✝ : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible 1
x✝¹ x✝ : R
h✝ : ¬x✝ = 0
⊢ 1 x✝¹ ≤ 1 x✝ ↔ True
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ 1 (↑r * ↑u) = 1 (↑t * ↑s)

pp: case hb
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ (valuation R) ↑s ≠ 0

pp: case hd
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ (valuation R) ↑u ≠ 0

Tactic:
<;>

Goal state after:
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ 1 (↑r * ↑u) = 1 (↑t * ↑s)

case hb
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ (valuation R) ↑s ≠ 0

case hd
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ (valuation R) ↑u ≠ 0
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
S : Type u_2
inst✝¹⁰ : CommRing S
R' : Type u_3
S' : Type u_4
inst✝⁹ : CommRing R'
inst✝⁸ : CommRing S'
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R S S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : Module.Flat R S
surj : Function.Surjective ⇑(algebraMap R R')
surjS : Function.Surjective ⇑(algebraMap S S')
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
sq0 : RingHom.ker (algebraMap R R') ^ 2 = ⊥
smoothq : FormallySmooth R' S'
P : Extension R S := (Generators.self R S).toExtension
⊢ FormallySmooth R S

Tactic:
let : Algebra.FormallySmooth R P.Ring := instFormallySmoothMvPolynomial S

Goal state after:
R : Type u_1
inst✝¹¹ : CommRing R
S : Type u_2
inst✝¹⁰ : CommRing S
R' : Type u_3
S' : Type u_4
inst✝⁹ : CommRing R'
inst✝⁸ : CommRing S'
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R R'
inst✝⁵ : Algebra R' S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S'
inst✝² : IsScalarTower R S S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : Module.Flat R S
surj : Function.Surjective ⇑(algebraMap R R')
surjS : Function.Surjective ⇑(algebraMap S S')
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
sq0 : RingHom.ker (algebraMap R R') ^ 2 = ⊥
smoothq : FormallySmooth R' S'
P : Extension R S := (Generators.self R S).toExtension
this : FormallySmooth R P.Ring := instFormallySmoothMvPolynomial S
⊢ FormallySmooth R S
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((rename (Prod.mk 0)) (wittPolynomial p ℤ n)).vars ⊆ univ ×ˢ range (n + 1)

pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((rename (Prod.mk 1)) (wittPolynomial p ℤ n)).vars ⊆ univ ×ˢ range (n + 1)

Tactic:
<;>

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((rename (Prod.mk 0)) (wittPolynomial p ℤ n)).vars ⊆ univ ×ˢ range (n + 1)

case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((rename (Prod.mk 1)) (wittPolynomial p ℤ n)).vars ⊆ univ ×ˢ range (n + 1)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆
    univ ×ˢ range (n + 1)

pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆
    univ ×ˢ range (n + 1)

Tactic:
<;>

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆
    univ ×ˢ range (n + 1)

case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆
    univ ×ˢ range (n + 1)
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 : ℕ
x y✝ : 𝕎 k
this : ↑p = 0
y : 𝕎 k
⊢ 0 ^ 0 * y.coeff 0 ^ p ^ (n + 1 - 0) = y.coeff 0 ^ p ^ (n + 1)

pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y✝ : 𝕎 k
this : ↑p = 0
y : 𝕎 k
⊢ 0 ∈ range (n + 1 + 1)

pp: case h₀
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y✝ : 𝕎 k
this : ↑p = 0
y : 𝕎 k
⊢ ∀ b ∈ range (n + 1 + 1), b ≠ 0 → 0 ^ b * y.coeff b ^ p ^ (n + 1 - b) = 0

Tactic:
<;>

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y✝ : 𝕎 k
this : ↑p = 0
y : 𝕎 k
⊢ 0 ^ 0 * y.coeff 0 ^ p ^ (n + 1 - 0) = y.coeff 0 ^ p ^ (n + 1)

case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y✝ : 𝕎 k
this : ↑p = 0
y : 𝕎 k
⊢ 0 ∈ range (n + 1 + 1)

case h₀
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y✝ : 𝕎 k
this : ↑p = 0
y : 𝕎 k
⊢ ∀ b ∈ range (n + 1 + 1), b ≠ 0 → 0 ^ b * y.coeff b ^ p ^ (n + 1 - b) = 0
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case e_a.e_a.e_a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
this : ↑p = 0
sum_zero_pow_mul_pow_p :
  ∀ (y : 𝕎 k), ∑ x ∈ range (n + 1 + 1), 0 ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)
⊢ ∑ x_1 ∈ range (n + 1 + 1), 0 ^ x_1 * x.coeff x_1 ^ p ^ (n + 1 - x_1) = x.coeff 0 ^ p ^ (n + 1)

pp: case e_a.e_a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
this : ↑p = 0
sum_zero_pow_mul_pow_p :
  ∀ (y : 𝕎 k), ∑ x ∈ range (n + 1 + 1), 0 ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)
⊢ ∑ x ∈ range (n + 1 + 1), 0 ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)

Tactic:
<;>

Goal state after:
case e_a.e_a.e_a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
this : ↑p = 0
sum_zero_pow_mul_pow_p :
  ∀ (y : 𝕎 k), ∑ x ∈ range (n + 1 + 1), 0 ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)
⊢ ∑ x_1 ∈ range (n + 1 + 1), 0 ^ x_1 * x.coeff x_1 ^ p ^ (n + 1 - x_1) = x.coeff 0 ^ p ^ (n + 1)

case e_a.e_a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
this : ↑p = 0
sum_zero_pow_mul_pow_p :
  ∀ (y : 𝕎 k), ∑ x ∈ range (n + 1 + 1), 0 ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)
⊢ ∑ x ∈ range (n + 1 + 1), 0 ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case inl
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : Fin 2 × ℕ
f₀ : (↑↑(univ ×ˢ range (a.2 + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p a.2)
x y : TruncatedWittVector p (a.2 + 1) k
ha : a ∈ ↑(univ ×ˢ range (a.2 + 1))
S : Set (Fin 2 × ℕ) := {a_1 | a_1.2 = a.2 ∨ a_1.2 < a.2}
⊢ a.2 < a.2 + 1

pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ ↑(univ ×ˢ range (n + 1))
S : Set (Fin 2 × ℕ) := {a | a.2 = n ∨ a.2 < n}
h✝ : a.2 < n
⊢ a.2 < n + 1

Tactic:
<;>

Goal state after:
case inl
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : Fin 2 × ℕ
f₀ : (↑↑(univ ×ˢ range (a.2 + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p a.2)
x y : TruncatedWittVector p (a.2 + 1) k
ha : a ∈ ↑(univ ×ˢ range (a.2 + 1))
S : Set (Fin 2 × ℕ) := {a_1 | a_1.2 = a.2 ∨ a_1.2 < a.2}
⊢ a.2 < a.2 + 1

case inr
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
f₀ : (↑↑(univ ×ˢ range (n + 1)) → k) → k
hf₀ : ∀ (x : Fin 2 × ℕ → k), f₀ (x ∘ Subtype.val) = (aeval x) (polyOfInterest p n)
x y : TruncatedWittVector p (n + 1) k
a : Fin 2 × ℕ
ha : a ∈ ↑(univ ×ˢ range (n + 1))
S : Set (Fin 2 × ℕ) := {a | a.2 = n ∨ a.2 < n}
h✝ : a.2 < n
⊢ a.2 < n + 1
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inr.inr.refine_1
α : 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 : BddAbove (range g)
t : Set α
ht : t ∈ s
⊢ sSup (range g) ∈ upperBounds (range fun n ↦ f ⟨t, ht⟩ (g n))

pp: case inr.inr.refine_2
α : 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 : BddAbove (range g)
t : Set α
ht : t ∈ s
b : α
hb : b ∈ upperBounds (range fun n ↦ f ⟨t, ht⟩ (g n))
⊢ b ∈ upperBounds (range g)

Tactic:
<;>

Goal state after:
case inr.inr.refine_1
α : 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 : BddAbove (range g)
t : Set α
ht : t ∈ s
⊢ sSup (range g) ∈ upperBounds (range fun n ↦ f ⟨t, ht⟩ (g n))

case inr.inr.refine_2
α : 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 : BddAbove (range g)
t : Set α
ht : t ∈ s
b : α
hb : b ∈ upperBounds (range fun n ↦ f ⟨t, ht⟩ (g n))
⊢ b ∈ upperBounds (range g)
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case neg.mp
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
⊢ z ∈ pullSub (pullSub T y) x → z ∈ pullSub T (x ++ y)

pp: case neg.mpr
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
⊢ z ∈ pullSub T (x ++ y) → z ∈ pullSub (pullSub T y) x

Tactic:
<;>

Goal state after:
case neg.mp
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
⊢ z ∈ pullSub (pullSub T y) x → z ∈ pullSub T (x ++ y)

case neg.mpr
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
⊢ z ∈ pullSub T (x ++ y) → z ∈ pullSub (pullSub T y) x
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case neg.mp
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
⊢ z ∈ pullSub T (x ++ y)

pp: case neg.mpr
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
⊢ z ∈ pullSub (pullSub T y) x

Tactic:
<;>

Goal state after:
case neg.mp
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
⊢ z ∈ pullSub T (x ++ y)

case neg.mpr
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
⊢ z ∈ pullSub (pullSub T y) x
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case refine_1.hι
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ lift.{v, v} #↑s < lift.{v, v} (cof α)

pp: case refine_1.hf
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ ∀ (i : ↑s), IsClub (f ↑i ⋯)

Tactic:
<;>

Goal state after:
case refine_1.hι
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ lift.{v, v} #↑s < lift.{v, v} (cof α)

case refine_1.hf
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
f : (x : Set α) → x ∈ s → Set α
hf : ∀ (x : Set α) (_ : x ∈ s), IsClub (f x _)
hxf : ∀ (x : Set α) (_ : x ∈ s), Disjoint x (f x _)
⊢ ∀ (i : ↑s), IsClub (f ↑i ⋯)
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case nil
α : Type u_1
⊢ (ofList []).toList = []

pp: case cons
α : Type u_1
head✝ : Lists α
tail✝ : List (Lists α)
tail_ih✝ : (ofList tail✝).toList = tail✝
⊢ (ofList (head✝ :: tail✝)).toList = head✝ :: tail✝

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
⊢ (ofList []).toList = []

case cons
α : Type u_1
head✝ : Lists α
tail✝ : List (Lists α)
tail_ih✝ : (ofList tail✝).toList = tail✝
⊢ (ofList (head✝ :: tail✝)).toList = head✝ :: tail✝
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case nil
α : Type u_1
l : Lists' α true
⊢ ofList [] ⊆ nil → ofList [] = nil

pp: case cons
α : Type u_1
l : Lists' α true
head✝ : Lists α
tail✝ : List (Lists α)
tail_ih✝ : ofList tail✝ ⊆ nil → ofList tail✝ = nil
⊢ ofList (head✝ :: tail✝) ⊆ nil → ofList (head✝ :: tail✝) = nil

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
l : Lists' α true
⊢ ofList [] ⊆ nil → ofList [] = nil

case cons
α : Type u_1
l : Lists' α true
head✝ : Lists α
tail✝ : List (Lists α)
tail_ih✝ : ofList tail✝ ⊆ nil → ofList tail✝ = nil
⊢ ofList (head✝ :: tail✝) ⊆ nil → ofList (head✝ :: tail✝) = nil
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
⊢ Monotone lfpApprox

Tactic:
intro f g h x a
  induction a using WellFoundedLT.induction with | ind i IH
  rw [lfpApprox, lfpApprox]
  exact sup_le_sup_left (iSup₂_mono fun j hj ↦ (f.mono (IH j hj)).trans (h _)) _

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1.antisymm.antisymm.left
α : 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₂✝

pp: case C1.antisymm.antisymm.right
α : 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₁

Tactic:
<;>

Goal state after:
case C1.antisymm.antisymm.left
α : 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₂✝

case C1.antisymm.antisymm.right
α : 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₁
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case atom
α : Type u_1
a✝ : α
⊢ 0 < sizeOf (Lists'.atom a✝)

pp: case nil
α : Type u_1
⊢ 0 < sizeOf Lists'.nil

pp: case cons'
α : Type u_1
b✝ : Bool
a✝¹ : Lists' α b✝
a✝ : Lists' α true
⊢ 0 < sizeOf (a✝¹.cons' a✝)

Tactic:
<;>

Goal state after:
case atom
α : Type u_1
a✝ : α
⊢ 0 < sizeOf (Lists'.atom a✝)

case nil
α : Type u_1
⊢ 0 < sizeOf Lists'.nil

case cons'
α : Type u_1
b✝ : Bool
a✝¹ : Lists' α b✝
a✝ : Lists' α true
⊢ 0 < sizeOf (a✝¹.cons' a✝)
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case atom.mp
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ ⟨false, Lists'.atom a✝⟩ = ⟨false, l₂⟩ → Lists'.atom a✝ = l₂

pp: case atom.mpr
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ Lists'.atom a✝ = l₂ → ⟨false, Lists'.atom a✝⟩ = ⟨false, l₂⟩

Tactic:
<;>

Goal state after:
case atom.mp
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ ⟨false, Lists'.atom a✝⟩ = ⟨false, l₂⟩ → Lists'.atom a✝ = l₂

case atom.mpr
α : Type u_1
inst✝ : DecidableEq α
l₂ : Lists' α false
a✝ : α
⊢ Lists'.atom a✝ = l₂ → ⟨false, Lists'.atom a✝⟩ = ⟨false, l₂⟩
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case inl
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
x✝ : a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a) := x✝
he : s ∩ Iic a = ∅
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a

pp: case inr
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
x✝ : a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a) := x✝
hne : (s ∩ Iic a).Nonempty
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a

Tactic:
· simp [he] at h

Goal state after:
case inr
a : Ordinal.{u}
s : Set Ordinal.{u}
tfae_1_to_2 : a ∈ closure s → a ∈ closure (s ∩ Iic a)
x✝ : a ∈ closure (s ∩ Iic a)
h : a ∈ closure (s ∩ Iic a) := x✝
hne : (s ∩ Iic a).Nonempty
⊢ (s ∩ Iic a).Nonempty ∧ sSup (s ∩ Iic a) = a