mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
h : (if x' - y' = 0 then 0 else (↑p ^ padicValRat p (x' - y'))⁻¹) ≤ (↑p ^ (embedding ↑γ * exp (-1)).log.natAbs)⁻¹
H : ¬x' - y' = 0
⊢ exp (-padicValRat p (x' - y')) < embedding ↑γ

Tactic:
· rw [← lt_log_iff_exp_lt (embedding_unit_ne_zero _)]
        simp_all [← zpow_natCast, zpow_pos, inv_le_inv₀, zpow_le_zpow_iff_right₀ hp1', abs_le,
          Int.lt_iff_add_one_le]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ (n + 1))⁻¹.y.sign = (Int.negSucc n).sign

Tactic:
exact Int.sign_eq_neg_one_of_neg (neg_neg_of_pos (y_pow_succ_pos hax hay n))

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case h.inl.inl
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
x : ℕ
ih : ∀ m < x, ∀ {a : Solution₁ d}, 0 ≤ a.y → ↑m = a.x → 0 < ↑m → ∃ n, a = a₁ ^ n
hax : 0 < ↑x
hay : 0 ≤ Solution₁.y 1
hax' : ↑x = Solution₁.x 1
hy : 0 = Solution₁.y 1
⊢ 1 = a₁ ^ 0

pp: case h.inl.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
x : ℕ
ih : ∀ m < x, ∀ {a : Solution₁ d}, 0 ≤ a.y → ↑m = a.x → 0 < ↑m → ∃ n, a = a₁ ^ n
hax : 0 < ↑x
hay : 0 ≤ (-1).y
hax' : ↑x = (-1).x
hy : 0 = (-1).y
⊢ -1 = a₁ ^ 0

Tactic:
· simp

Goal state after:
case h.inl.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
x : ℕ
ih : ∀ m < x, ∀ {a : Solution₁ d}, 0 ≤ a.y → ↑m = a.x → 0 < ↑m → ∃ n, a = a₁ ^ n
hax : 0 < ↑x
hay : 0 ≤ (-1).y
hax' : ↑x = (-1).x
hy : 0 = (-1).y
⊢ -1 = a₁ ^ 0
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: case h
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
n k : ℕ
⊢ 1 ≤ 2

pp: case a
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
n k : ℕ
⊢ n ≤ n + k

Tactic:
· simp

Goal state after:
case a
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
n k : ℕ
⊢ n ≤ n + k
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: case hg
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
⊢ Tendsto (fun x ↦ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ x) atTop (𝓝 0)

Tactic:
apply bound'
    assumption

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case inl
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : DecidableEq K⟮X⟯
inst✝ : IsTrivialOn K v
hlt : 1 < v X
⊢ v 0 < 1 ↔ (inftyValuation K) 0 < 1

pp: case inr
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : DecidableEq K⟮X⟯
inst✝ : IsTrivialOn K v
hlt : 1 < v X
f : K⟮X⟯
hf : f ≠ 0
⊢ v f < 1 ↔ (inftyValuation K) f < 1

Tactic:
· simp

Goal state after:
case inr
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : DecidableEq K⟮X⟯
inst✝ : IsTrivialOn K v
hlt : 1 < v X
f : K⟮X⟯
hf : f ≠ 0
⊢ v f < 1 ↔ (inftyValuation K) f < 1
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ⌈↑m * s⌉ - 1 = j
⊢ False

Tactic:
sub_eq_iff_eq_add,

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ⌈↑m * s⌉ = j + 1
⊢ False
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑j < ↑⌊(↑j + 1) / r⌋ * r
⊢ ⌈↑⌊(↑j + 1) / r⌋ * r⌉ - 1 = j

Tactic:
sub_eq_iff_eq_add,

Goal state after:
case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑j < ↑⌊(↑j + 1) / r⌋ * r
⊢ ⌈↑⌊(↑j + 1) / r⌋ * r⌉ = j + 1
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
p : ℕ
⊢ p ∈ d.primeFactors → 0 < s.nu p

Tactic:
hpd

Goal state after:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
p : ℕ
hpd : p ∈ d.primeFactors
⊢ 0 < s.nu p
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case hfg
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
p : ℕ
⊢ p ∈ d.primeFactors → s.nu p < 1

Tactic:
hpd

Goal state after:
case hfg
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
p : ℕ
hpd : p ∈ d.primeFactors
⊢ s.nu p < 1
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r : ℝ
hr : Irrational r
x✝ k : ℤ
hk : k > 0
⊢ ⌈↑k * r⌉ - 1 = ⌊↑k * r⌋

Tactic:
sub_eq_iff_eq_add,

Goal state after:
r : ℝ
hr : Irrational r
x✝ k : ℤ
hk : k > 0
⊢ ⌈↑k * r⌉ = ⌊↑k * r⌋ + 1
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ 2 * 2 * m = (x - y) ^ 2 + (x + y) ^ 2

Tactic:
by rw [mul_assoc, h]; ring

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case inl
K : Type u_1
Γ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝² : v.IsNontrivial
inst✝¹ : IsTrivialOn K v
hle : v X ≤ 1
inst✝ : v.IsRankOneDiscrete
⊢ v 0 ≤ 1 ↔ (valuation K⟮X⟯ Pᵥ) 0 ≤ 1

pp: case inr
K : Type u_1
Γ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝² : v.IsNontrivial
inst✝¹ : IsTrivialOn K v
hle : v X ≤ 1
inst✝ : v.IsRankOneDiscrete
f : K⟮X⟯
hf0 : f ≠ 0
⊢ v f ≤ 1 ↔ (valuation K⟮X⟯ Pᵥ) f ≤ 1

Tactic:
· simp

Goal state after:
case inr
K : Type u_1
Γ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝² : v.IsNontrivial
inst✝¹ : IsTrivialOn K v
hle : v X ≤ 1
inst✝ : v.IsRankOneDiscrete
f : K⟮X⟯
hf0 : f ≠ 0
⊢ v f ≤ 1 ↔ (valuation K⟮X⟯ Pᵥ) f ≤ 1
Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
⊢ ↑(k * k + 1) = 0

Tactic:
Nat.cast_add,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
⊢ ↑(k * k) + ↑1 = 0
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: a b x y u v : ℕ
ha : ↑a = ↑x ^ 2 + ↑y ^ 2
hb : ↑b = ↑u ^ 2 + ↑v ^ 2
r s : ℤ
h : ↑a * ↑b = r ^ 2 + s ^ 2
⊢ ↑a * ↑b = ↑r.natAbs ^ 2 + ↑s.natAbs ^ 2

Tactic:
simpa only [Int.natCast_natAbs, sq_abs]

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case refine_2.refine_1
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
b''_li : LinearIndependent K b''
⊢ Submodule.span K (Set.range b'') = ⊤

Tactic:
· rw [Set.range_comp]
      refine FinrankQuotientMap.span_eq_top p hp.ne_top _ (top_le_iff.mp ?_)
      -- The nicest way to show `S ≤ span b' ⊔ pS` is by reducing both sides modulo pS.
      -- However, this would imply distinguishing between `pS` as `S`-ideal,
      -- and `pS` as `R`-submodule, since they have different (non-defeq) quotients.
      -- Instead we'll lift `x mod pS ∈ span b` to `y ∈ span b'` for some `y - x ∈ pS`.
      intro x _
      have mem_span_b : ((Submodule.mkQ (map (algebraMap R S) p)) x : S ⧸ map (algebraMap R S) p) ∈
          Submodule.span (R ⧸ p) (Set.range b) := b.mem_span _
      rw [← @Submodule.restrictScalars_mem R,
        Submodule.restrictScalars_span R (R ⧸ p) Ideal.Quotient.mk_surjective, b_eq_b',
        Set.range_comp, ← Submodule.map_span] at mem_span_b
      obtain ⟨y, y_mem, y_eq⟩ := Submodule.mem_map.mp mem_span_b
      suffices y + -(y - x) ∈ _ by simpa
      rw [LinearMap.restrictScalars_apply, Submodule.mkQ_apply, Submodule.mkQ_apply,
        Submodule.Quotient.eq] at y_eq
      exact add_mem (Submodule.mem_sup_left y_mem) (neg_mem <| Submodule.mem_sup_right y_eq)

Goal state after:
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMinOrder α
a : α
⊢ Bounded (fun x1 x2 ↦ x1 > x2) (Ici a)

Tactic:
simp only [← bounded_ge_iff_bounded_gt, bounded_ge_Ici]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case mp
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
⊢ (∃ b, (∃ m < n, m.gcd n = 1 ∧ ↑(↑m / ↑n) = b) ∧ ‖x - b‖ < δ) → ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ

Tactic:
rintro ⟨y, ⟨m, hm₁, hm₂, rfl⟩, hx⟩; exact ⟨m, hm₁, hm₂, hx⟩

Goal state after:
Module: Mathlib.Order.CompleteLattice.PiLex

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
e : Lex ((i : ι) → (fun i ↦ α i) i)
he : e ∈ s
⊢ e ≤ sSup s

pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
e : Lex ((i : ι) → (fun i ↦ α i) i)
h : e ∈ upperBounds s
⊢ sSup s ≤ e

Tactic:
· by_contra! hs
    obtain ⟨a, ha⟩ := hs
    exact ha.2.not_ge (le_sSup_apply he fun j hj ↦ (ha.1 j hj).symm)

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
e : Lex ((i : ι) → (fun i ↦ α i) i)
h : e ∈ upperBounds s
⊢ sSup s ≤ e
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝¹ : Std.Trichotomous r'
inst✝ : IsTrans α r'
x : α
x✝ : x ∈ ⊤
hx : x ∉ c'.extent
y : α
hy : y ∈ c'.extent
⊢ ¬x = y

Tactic:
exact (hx <| · ▸ hy)

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : CompleteLattice α
hs : ∀ (A : ℕ → α), (∀ (n : ℕ), A n ∈ s) → ⨆ n, A n ∈ s
x : α
f : ℕ → α
hAs : range f ⊆ s
hA_ne : (range f).Nonempty
hAc : (range f).Countable
hx : IsLUB (range f) x
⊢ ∀ (n : ℕ), f n ∈ s

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : CompleteLattice α
hs : CountableSupClosed s
A : Set α
hA_c : A.Countable
hA_ne : A.Nonempty
hA : ∀ a ∈ A, a ∈ s
⊢ sSup A ∈ s

Tactic:
rw [sSup_eq_iSup']

Goal state after:
α : Type u_2
s : Set α
inst✝ : CompleteLattice α
hs : CountableSupClosed s
A : Set α
hA_c : A.Countable
hA_ne : A.Nonempty
hA : ∀ a ∈ A, a ∈ s
⊢ ⨆ a, ↑a ∈ s
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : SemilatticeSup α
hs : CountableSupClosed s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ {a, b} ⊆ s

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
β : Type u_3
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
t : Set β
hs : CountableSupClosed s
ht : CountableSupClosed t
A : Set (α × β)
hAst : A ⊆ s ×ˢ t
hA_ne : A.Nonempty
hAc : A.Countable
x : α
y : β
hxy : IsLUB (Prod.fst '' A) (x, y).1 ∧ IsLUB (Prod.snd '' A) (x, y).2
⊢ Prod.fst '' A ⊆ s

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
β : Type u_3
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
t : Set β
hs : CountableSupClosed s
ht : CountableSupClosed t
A : Set (α × β)
hAst : A ⊆ s ×ˢ t
hA_ne : A.Nonempty
hAc : A.Countable
x : α
y : β
hxy : IsLUB (Prod.fst '' A) (x, y).1 ∧ IsLUB (Prod.snd '' A) (x, y).2
⊢ Prod.snd '' A ⊆ t

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
this : CountableSupClosed (⋂₀ {t | s ⊆ t ∧ CountableSupClosed t})
⊢ s ⊆ ⋂₀ {t | s ⊆ t ∧ CountableSupClosed t}

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
this : CountableSupClosed (⋂₀ {t | s ⊆ t ∧ CountableSupClosed t})
⊢ CountableSupClosed (⋂₀ {t | s ⊆ t ∧ CountableSupClosed t})

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
a : α
b : β
u : Set α
hu : u ⊆ s
hu_ne : u.Nonempty
hu_c : u.Countable
hu_lub : IsLUB u a
v : Set β
hv : v ⊆ t
hv_ne : v.Nonempty
hv_c : v.Countable
hv_lub : IsLUB v b
⊢ u ×ˢ v ⊆ s ×ˢ t

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : Order.Coframe α
hs : SupClosed s
a : α
ha : a ∈ countableInfClosure s
b : α
hb : b ∈ countableInfClosure s
⊢ a ⊔ b ∈ countableInfClosure s

Tactic:
mem_countableInfClosure_iff_iInf

Goal state after:
α : Type u_2
s : Set α
inst✝ : Order.Coframe α
hs : SupClosed s
a : α
ha : ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨅ n, t n = a
b : α
hb : ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨅ n, t n = b
⊢ ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨅ n, t n = a ⊔ b
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: case mpr.superset
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s s✝ t✝ : Set α
a✝ : CardinalGenerateSets g s✝
st : s✝ ⊆ t✝
ih : s✝ ∈ f
⊢ t✝ ∈ f

Tactic:
exact mem_of_superset ih st

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inr.inr
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
j : Fin (n + 1)
hj : i.castSucc < j
⊢ i.castSucc.succ.insertNth x f j.castSucc < i.castSucc.succ.insertNth x f j.succ

Tactic:
obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero (Fin.ne_zero_of_lt hj)
    grind [insertNth_apply_same, insertNth_apply_above]

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : ↑n ≤ (⇑e '' s).chainHeight r'
a : Set β
ha₁ : a ⊆ ⇑e '' s
ha₂ : a.encard = ↑n
ha₃ : IsChain r' a
⊢ a ⊆ range ⇑e

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : ↑n ≤ s.chainHeight r
a : Set α
ha₁ : a ⊆ s
ha₂ : a.encard = ↑n
ha₃ : IsChain r a
⊢ ⇑e '' a ⊆ ⇑e '' s

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
b : α
n : ℤ
⊢ ↑n ∈ Set.Iio b ↔ n ∈ Set.Iio ⌈b⌉

Tactic:
simp [lt_ceil]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
b : α
n : ℕ
⊢ ↑n ∈ Set.Iio b ↔ n ∈ Finset.Iio ⌈b⌉₊

Tactic:
simp [lt_ceil]

Goal state after:
Module: Mathlib.Order.Interval.Lex

Goal state before:
pp: α : Type ?u.3
inst✝¹ : LT α
inst✝ : LE α
⊢ (1, 1).1 ≤ (1, 1).2

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.Interval.Lex

Goal state before:
pp: α : Type ?u.3
inst✝¹ : LT α
inst✝ : LE α
⊢ (1, 2).1 ≤ (1, 2).2

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.Interval.Lex

Goal state before:
pp: α : Type ?u.3
inst✝¹ : LT α
inst✝ : LE α
⊢ (1, 3).1 ≤ (1, 3).2

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.Interval.Lex

Goal state before:
pp: α : Type ?u.3
inst✝¹ : LT α
inst✝ : LE α
⊢ (2, 2).1 ≤ (2, 2).2

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.Interval.Lex

Goal state before:
pp: α : Type ?u.3
inst✝¹ : LT α
inst✝ : LE α
⊢ (2, 3).1 ≤ (2, 3).2

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.Interval.Lex

Goal state before:
pp: α : Type ?u.3
inst✝¹ : LT α
inst✝ : LE α
⊢ (3, 3).1 ≤ (3, 3).2

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
⊢ ∀ (a b : αs), (∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd) → (∃ (h : b.fst ≤ a.fst), π h a.snd = b.snd) → a = b

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
a : α
x✝ : a ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}
p : α
hp : p ∈ P
q : α
hq : q ∈ Q
ha : a = p ⊓ q
⊢ a ≤ (p, q).1 ⊓ (p, q).2

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
h1 : ∀ (x : α), f a = f x ↔ a = x
⊢ f a = f b → (a = b ∧ ∀ (c : α), f a = f c ↔ a = c) ∨ P.Rel a b

Tactic:
by grind

Goal state after:
Module: Mathlib.Order.UpperLower.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s₁ s₂ : UpperSet α
t₁ t₂ : UpperSet β
⊢ s₁ ×ˢ t₁ ⊔ s₂ ×ˢ t₂ = ⊤ ↔ s₁ ⊔ s₂ = ⊤ ∨ t₁ ⊔ t₂ = ⊤

Tactic:
prod_sup_prod,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s₁ s₂ : UpperSet α
t₁ t₂ : UpperSet β
⊢ (s₁ ⊔ s₂) ×ˢ (t₁ ⊔ t₂) = ⊤ ↔ s₁ ⊔ s₂ = ⊤ ∨ t₁ ⊔ t₂ = ⊤
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case inl
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ MeasurableSet ∅

pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' {⊥} ×ˢ A = ∅

Tactic:
· simp

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n : ℕ
A : Set Ω
hA : MeasurableSet A
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' {⊥} ×ˢ A = ∅
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case inr.inl
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
⊢ MeasurableSet ∅

pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A = ∅

Tactic:
· simp

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hni : n < i
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A = ∅
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i j : ι
A : Set Ω
hA : MeasurableSet A
hji : j ≤ i
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi j ×ˢ A = (Subtype.val ⁻¹' Set.Ioc j i) ×ˢ A

Tactic:
by grind

Goal state after:
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
i j : ι
A : Set Ω
hA : MeasurableSet A
hij : i ≤ j
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi j ×ˢ A = ∅

Tactic:
by grind

Goal state after:
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m✝
u : ι → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
i : ι
this✝ : MeasurableSpace (ι × Ω) := 𝓕.predictable
this : MeasurableSpace (↑(Set.Iic i) × Ω) := Subtype.instMeasurableSpace.prod (↑𝓕 i)
X : ℕ → ↑(Set.Iic i) × Ω → E := fun m x ↦ (StronglyMeasurable.approx h𝓕 m) (↑x.1, x.2)
m : ℕ
⊢ Set.range (X m) ⊆ Set.range ⇑(StronglyMeasurable.approx h𝓕 m)

Tactic:
by grind

Goal state after:
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
⊢ ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0

Tactic:
intro k hk

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
k : ℕ
hk : i ≤ k
⊢ μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: case refine_2
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁸ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
ℱ : Filtration ι m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : Lattice E
inst✝³ : ContinuousSup E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f g : ι → Ω → E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
i j : ι
hij : i ≤ j
⊢ g i ≤ᵐ[μ] μ[(f ⊔ g) j | ↑ℱ i]

Tactic:
exact EventuallyLE.trans (hg.2.1 i j hij)
      (condExp_mono (hg.integrable _) (Integrable.sup (hf.integrable j) (hg.integrable j))
        (Eventually.of_forall fun x => le_sup_right))

Goal state after: