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

Goal state before:
pp: case succ
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
⊢ ‖Δ_[1]^[n + (k + 1) * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ (k + 1)

Tactic:
add_mul,

Goal state after:
case succ
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
⊢ ‖Δ_[1]^[n + (k * p ^ t + 1 * p ^ t)] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ (k + 1)
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R ℚ
inst✝¹ : IsIntegralClosure R ℤ ℚ
inst✝ : IsFractionRing R ℚ
x : R
y : ℤ
hy : (algebraMap ℤ ℚ) y = (algebraMap R ℚ) x
⊢ (algebraMap R ℚ) ((algebraMap ℤ R) y) = (algebraMap R ℚ) x

Tactic:
by simp only [← IsScalarTower.algebraMap_apply, hy]

Goal state after:
Module: Mathlib.NumberTheory.PowModTotient

Goal state before:
pp: case succ
x k n : ℕ
hn : 1 < n
h : x.Coprime n
l : ℕ
ih : x ^ (k + l * φ n) % n = x ^ k % n
⊢ x ^ (k + (l + 1) * φ n) % n = x ^ k % n

Tactic:
add_mul,

Goal state after:
case succ
x k n : ℕ
hn : 1 < n
h : x.Coprime n
l : ℕ
ih : x ^ (k + l * φ n) % n = x ^ k % n
⊢ x ^ (k + (l * φ n + 1 * φ n)) % n = x ^ k % n
Module: Mathlib.NumberTheory.PowModTotient

Goal state before:
pp: case succ
x k n : ℕ
hn : 1 < n
h : x.Coprime n
l : ℕ
ih : x ^ (k + l * φ n) % n = x ^ k % n
⊢ x ^ (k + l * φ n + φ n) % n = x ^ k % n

Tactic:
pow_add_totient_mod_eq hn h,

Goal state after:
case succ
x k n : ℕ
hn : 1 < n
h : x.Coprime n
l : ℕ
ih : x ^ (k + l * φ n) % n = x ^ k % n
⊢ x ^ (k + l * φ n) % n = x ^ k % n
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
⊢ a.x ^ 2 = 1 + d * a.y ^ 2

Tactic:
← a.prop

Goal state after:
d : ℤ
a : Solution₁ d
⊢ a.x ^ 2 = a.x ^ 2 - d * a.y ^ 2 + d * a.y ^ 2
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
⊢ d * a.y ^ 2 = a.x ^ 2 - 1

Tactic:
← a.prop

Goal state after:
d : ℤ
a : Solution₁ d
⊢ d * a.y ^ 2 = a.x ^ 2 - (a.x ^ 2 - d * a.y ^ 2)
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
⊢ 0 < (a ^ Int.negSucc n).x

Tactic:
| negSucc n =>

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ (a * a₁⁻¹).x < a.x

Tactic:
simp only [x_mul, x_inv, y_inv, mul_neg, add_neg_lt_iff_le_add']
  refine lt_of_mul_lt_mul_left ?_ h.2.1.le
  calc a₁.y * (a.x * a₁.x)
    _ = a.x * a₁.y * a₁.x := by ring
    _ ≤ a.y * a₁.x * a₁.x := by have := h.1; have := x_mul_y_le_y_mul_x h hax hay; gcongr
  rw [mul_assoc, ← sq, a₁.prop_x, ← sub_neg]
  suffices a.y - a.x * a₁.y < 0 by convert! this using 1; ring
  rw [sub_neg, ← abs_of_pos hay, ← abs_of_pos h.2.1, ← abs_of_pos <| zero_lt_one.trans hax, ←
    abs_mul, ← sq_lt_sq, mul_pow, a.prop_x]
  calc
    a.y ^ 2 = 1 * a.y ^ 2 := (one_mul _).symm
    _ ≤ d * a.y ^ 2 := (mul_le_mul_iff_left₀ <| sq_pos_of_pos hay).mpr h.d_pos
    _ < d * a.y ^ 2 + 1 := lt_add_one _
    _ = (1 + d * a.y ^ 2) * 1 := by rw [add_comm, mul_one]
    _ ≤ (1 + d * a.y ^ 2) * a₁.y ^ 2 :=
      (mul_le_mul_iff_right₀ (by have := h.d_pos; positivity)).mpr (sq_pos_of_pos h.2.1)

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inl.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : a₁ ^ 0 = -a₁ ^ (n₂ * n₁ - 1)
⊢ a₁ ^ n₂ = a₁

Tactic:
exact False.elim (ha₁.zpow_ne_neg_zpow hn₁)

Goal state after:
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: 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
hnsol : (Polynomial.aeval a) F ≠ 0
z : ℤ_[p]
hev : (Polynomial.aeval z) F = 0
hnlt : ‖z - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
⊢ ‖z - soln‖ = ‖z - a + (a - soln)‖

Tactic:
rw [sub_add_sub_cancel]

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

Goal state before:
pp: 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.IsEquiv (valuation K⟮X⟯ Pᵥ)

Tactic:
isEquiv_iff_val_le_one

Goal state after:
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
⊢ ∀ {x : K⟮X⟯}, v x ≤ 1 ↔ (valuation K⟮X⟯ Pᵥ) x ≤ 1
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x : ℤ[i]
⊢ norm x = 0 ↔ x = 0

Tactic:
rw [← Int.cast_inj (α := ℝ)]

Goal state after:
x : ℤ[i]
⊢ ↑(norm x) = ↑0 ↔ x = 0
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x y : ℤ[i]
hy : y ≠ 0
⊢ toComplex y ≠ 0

Tactic:
by rwa [Ne, ← toComplex_zero, toComplex_inj]

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n x y : ℕ
h : n = x ^ 2 + y ^ 2
hc : x.Coprime y
⊢ IsSquare (-1)

Tactic:
zify at h
  exact ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime h hc.isCoprime

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ p_k * m ^ (k + 1)! * m ^ (k + 1)! + m ^ k ! * 1 * m ^ (k + 1)! =
    (p_k * m ^ ((k + 1)! - k !) + 1) * (m ^ k ! * m ^ (k + 1)!)

Tactic:
add_mul,

Goal state after:
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ p_k * m ^ (k + 1)! * m ^ (k + 1)! + m ^ k ! * 1 * m ^ (k + 1)! =
    p_k * m ^ ((k + 1)! - k !) * (m ^ k ! * m ^ (k + 1)!) + 1 * (m ^ k ! * m ^ (k + 1)!)
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ p_k * m ^ ((k + 1) * k !) * m ^ ((k + 1) * k !) + m ^ k ! * 1 * m ^ ((k + 1) * k !) =
    p_k * m ^ ((k + 1) * k ! - k !) * (m ^ k ! * m ^ ((k + 1) * k !)) + m ^ k ! * m ^ ((k + 1) * k !)

Tactic:
add_mul,

Goal state after:
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ p_k * m ^ (k * k ! + 1 * k !) * m ^ (k * k ! + 1 * k !) + m ^ k ! * 1 * m ^ (k * k ! + 1 * k !) =
    p_k * m ^ (k * k ! + 1 * k ! - k !) * (m ^ k ! * m ^ (k * k ! + 1 * k !)) + m ^ k ! * m ^ (k * k ! + 1 * k !)
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : IsFractionRing S L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
⊢ ∑ P ∈ IsDedekindDomain.primesOverFinset p S, p.ramificationIdx' P * p.inertiaDeg' P = finrank K L

Tactic:
set e := ramificationIdx' p (S := S)

Goal state after:
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
inst✝¹³ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Algebra R K
inst✝⁸ : IsFractionRing R K
inst✝⁷ : Algebra S L
inst✝⁶ : IsFractionRing S L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Module.Finite R S
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
e : Ideal S → ℕ := p.ramificationIdx'
⊢ ∑ P ∈ IsDedekindDomain.primesOverFinset p S, e P * p.inertiaDeg' P = finrank K L
Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual

Goal state before:
pp: x : ℝ
⊢ x ∈ {x | Liouville x} ↔ x ∈ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}

Tactic:
simp only [mem_iInter, mem_iUnion, Liouville, mem_ofPred_eq, exists_prop, Set.mem_sdiff,
    mem_singleton_iff, mem_ball, Real.dist_eq, and_comm]

Goal state after:
Module: Mathlib.Order.Comparable

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ a < b ∨ AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b ∨ b < a ∨ IncompRel (fun x1 x2 ↦ x1 ≤ x2) a b

Tactic:
by
  simp_rw [lt_iff_le_not_ge]
  tauto

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
a b : DedekindCut α
h : a < b
c : α
hac : a < principal c
hcb : principal c ≤ b
d : α
had : a ≤ principal d
hdc : principal d < principal c
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
simp only [principal_lt_principal] at hdc

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : DenselyOrdered α
a b : DedekindCut α
h : a < b
c : α
hac : a < principal c
hcb : principal c ≤ b
d : α
had : a ≤ principal d
hdc : d < c
⊢ ∃ a_1, a < a_1 ∧ a_1 < b
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 : β
⊢ IsLUB A (x, y) → (x, y) ∈ s ×ˢ t

Tactic:
hxy

Goal state after:
α : 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 A (x, y)
⊢ (x, y) ∈ s ×ˢ t
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
⊢ r x y → r y z → r x z

Tactic:
hxy

Goal state after:
α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
⊢ r y z → r x z
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ x ⊓ y ⊓ z ≤ x

Tactic:
by simp [inf_assoc, inf_le_left]

Goal state after:
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : FunLike F α β
inst✝ : LatticeHomClass F α β
f : F
w✝ x✝² y✝ z✝ : α
x✝¹ : (Setoid.ker ⇑f) w✝ x✝²
x✝ : (Setoid.ker ⇑f) y✝ z✝
⊢ (Setoid.ker ⇑f) (w✝ ⊓ y✝) (x✝² ⊓ z✝)

Tactic:
simp_all +instances only [Setoid.ker, onFun, map_inf]

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
x✝¹ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
this : IsStronglyAtomic αs
a₀ : αs
ha₀ : a₀.fst = 0
ha₀inf : (Ici a₀).Infinite
x✝ : αs
i : ℕ
a : α i
⊢ ∀ (a_1 : ℕ) (b : α a_1), ⟨i, a⟩ ≤ ⟨a_1, b⟩ → i + 1 = a_1 → ∃ x, π ⋯ x = a ∧ ⟨i + 1, x⟩ = ⟨a_1, b⟩

Tactic:
exact fun j b ⟨_, _⟩ hj ↦ ⟨π hj.le b, by rwa [π_trans], by cases hj; rw [π_refl]⟩

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : BooleanAlgebra P
I : Ideal P
inst✝ : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
⊢ x ⊓ y ∈ I → x ∉ I → y ∈ I

Tactic:
hxy

Goal state after:
P : Type u_1
inst✝¹ : BooleanAlgebra P
I : Ideal P
inst✝ : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
⊢ x ∉ I → y ∈ I
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case a
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ f a b ≤ ⨅ x ∈ X, f x b

Tactic:
simp only [le_iInf_iff]

Goal state after:
case a
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ ∀ i ∈ X, f a b ≤ f i b
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
s x : α
inst✝ : CompleteLattice α
P Q : Partition s
h : P ≤ Q
hx : x ∈ P
y : α
hy : y ∈ Q
hxy : x ≤ y
z : α
x✝ : (fun y ↦ y ∈ Q ∧ x ≤ y) z
hz : z ∈ Q
hxz : x ≤ z
this : Disjoint z y
⊢ x = ⊥

Tactic:
exact le_bot_iff.mp (this hxz hxy)

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

Goal state before:
pp: α : Type u_1
s : α
inst✝ : CompleteLattice α
a : α
⊢ a ∈ ⊤ ↔ a = s ∧ a ≠ ⊥

Tactic:
rw [top_def, mem_removeBot, mem_singleton_iff]

Goal state after:
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: case h
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
J₁S : ↑J₁ ∉ S
J₂S : ↑J₂ ∉ S
J₁F : ¬Disjoint ↑F ↑J₁
J₂F : ¬Disjoint ↑F ↑J₂
c₁ : α
c₁F : c₁ ∈ ↑F
c₁J₁ : c₁ ∈ ↑J₁
c₂ : α
c₂F : c₂ ∈ ↑F
c₂J₂ : c₂ ∈ ↑J₂
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
⊢ a₁ ⊓ a₂ ∉ J

Tactic:
let b := b₁ ⊔ b₂

Goal state after:
case h
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
J₁S : ↑J₁ ∉ S
J₂S : ↑J₂ ∉ S
J₁F : ¬Disjoint ↑F ↑J₁
J₂F : ¬Disjoint ↑F ↑J₂
c₁ : α
c₁F : c₁ ∈ ↑F
c₁J₁ : c₁ ∈ ↑J₁
c₂ : α
c₂F : c₂ ∈ ↑F
c₂J₂ : c₂ ∈ ↑J₂
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
⊢ a₁ ⊓ a₂ ∉ J
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case pos
α : Type u_1
s u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun f
hs : u ⊆ s
a : α
haS : a ∈ s
ha : a ∈ u
⊢ f a ∈ s

pp: case neg
α : Type u_1
s u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun f
hs : u ⊆ s
a : α
haS : a ∈ s
ha : a ∉ u
⊢ f a ∈ s

Tactic:
· exact hs <| hf.apply_mem ha

Goal state after:
case neg
α : Type u_1
s u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun f
hs : u ⊆ s
a : α
haS : a ∈ s
ha : a ∉ u
⊢ f a ∈ s
Module: Mathlib.Order.Partition.Basic

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

Tactic:
rintro (h | h)

Goal state after:
case inl.inl
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
h1 : ∀ (x : α), f a = f x ↔ a = x
h : a = b ∧ ∀ (c : α), f a = f c ↔ a = c
⊢ f a = f b

case inl.inr
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
h1 : ∀ (x : α), f a = f x ↔ a = x
h : P.Rel a b
⊢ f a = f b
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : findAtom r = ⊥
⊢ r = ⊥

Tactic:
by
    unfold findAtom at h
    have := Nat.find_min' (bot_le (a := r)).exists_pred_iterate h
    replace : Nat.find (bot_le (a := r)).exists_pred_iterate = 0 := by lia
    simpa [this] using h

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

Goal state before:
pp: case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m_1 x ↦
    match x.1 with
    | 0 => (h₀.approx m_1) x.2
    | n.succ => (⋯.approx m_1) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
n : ℕ
ω : Ω
⊢ Tendsto (fun m ↦ X m (n, ω)) atTop (𝓝 (Function.uncurry u (n, ω)))

Tactic:
rcases n with rfl | n
      · exact h₀.tendsto_approx ω
      · exact (h n).tendsto_approx ω

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
k : ι
hk₁ : ↑k < hittingAfter u s n ω
hk₂ : n ≤ k
h : u k ω ∈ s
⊢ hittingAfter u s n ω ≤ ↑k

Tactic:
hittingAfter,

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
k : ι
hk₁ : ↑k < hittingAfter u s n ω
hk₂ : n ≤ k
h : u k ω ∈ s
⊢ (if ∃ j, n ≤ j ∧ u j ω ∈ s then ↑(sInf {i | n ≤ i ∧ u i ω ∈ s}) else ⊤) ≤ ↑k
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (hittingBtwn u s n m ω) ω ∈ s

Tactic:
simp_rw [hittingBtwn, if_pos h_exists]

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (sInf (Set.Icc n m ∩ {i | u i ω ∈ s})) ω ∈ s
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
h_exists : ∃ j, n ≤ j ∧ u j ω ∈ s
⊢ u (hittingAfter u s n ω).untopA ω ∈ s

Tactic:
hittingAfter,

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
h_exists : ∃ j, n ≤ j ∧ u j ω ∈ s
⊢ u (if ∃ j, n ≤ j ∧ u j ω ∈ s then ↑(sInf {i | n ≤ i ∧ u i ω ∈ s}) else ⊤).untopA ω ∈ s
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s
⊢ hittingBtwn u s n m ω ≤ i

Tactic:
simp_rw [hittingBtwn, if_pos h_exists]

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
m : ι
hin : n ≤ i
him : i ≤ m
his : u i ω ∈ s
h_exists : ∃ k ∈ Set.Icc n m, u k ω ∈ s
⊢ sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) ≤ i
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
hin : n ≤ i
his : u i ω ∈ s
h_exists : ∃ k, n ≤ k ∧ u k ω ∈ s
⊢ hittingAfter u s n ω ≤ ↑i

Tactic:
hittingAfter,

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
hin : n ≤ i
his : u i ω ∈ s
h_exists : ∃ k, n ≤ k ∧ u k ω ∈ s
⊢ (if ∃ j, n ≤ j ∧ u j ω ∈ s then ↑(sInf {i | n ≤ i ∧ u i ω ∈ s}) else ⊤) ≤ ↑i
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : hittingAfter u s n ω < ↑i
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ j, n ≤ j ∧ u j ω ∈ s
h_le : ↑n ≤ hittingAfter u s n ω
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s

Tactic:
hittingAfter,

Goal state after:
case mp
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : (if ∃ j, n ≤ j ∧ u j ω ∈ s then ↑(sInf {i | n ≤ i ∧ u i ω ∈ s}) else ⊤) < ↑i
h_top : hittingAfter u s n ω ≠ ⊤
h_exists : ∃ j, n ≤ j ∧ u j ω ∈ s
h_le : ↑n ≤ hittingAfter u s n ω
⊢ ∃ j ∈ Set.Ico n i, u j ω ∈ s
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hF : ¬∃ j ∈ Set.Icc n m, u j ω ∈ F
t : ι
ht : t ∈ Set.Icc n m ∧ u t ω ∈ E
⊢ m ≤ sInf (Set.Icc n m ∩ {i | u i ω ∈ E})

Tactic:
exact absurd ⟨t, ht.1, hEF ht.2⟩ hF

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

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hF : ¬∃ j, n ≤ j ∧ u j ω ∈ F
t : ι
ht : n ≤ t ∧ u t ω ∈ E
⊢ ⊤ ≤ ↑(sInf {j | n ≤ j ∧ u j ω ∈ E})

Tactic:
exact absurd ⟨t, ht.1, hEF ht.2⟩ hF

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

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
hnm : n ≤ m
ω : Ω
h_n : ∃ j, n ≤ j ∧ u j ω ∈ s
h_m : ∃ j, m ≤ j ∧ u j ω ∈ s
⊢ ↑(sInf {j | n ≤ j ∧ u j ω ∈ s}) ≤ ↑(sInf {j | m ≤ j ∧ u j ω ∈ s})

Tactic:
norm_cast
    gcongr
    exacts [⟨n, by simp [mem_lowerBounds]; grind⟩]

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun m ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω
⊢ ∑ k ∈ Finset.range (upcrossingsBefore a b f N ω),
      (stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω) ≤
    ∑ k ∈ Finset.range N,
      (stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω)

Tactic:
by
        refine Finset.sum_le_sum_of_subset_of_nonneg
          (Finset.range_subset_range.2 (upcrossingsBefore_le f ω hab)) fun i _ hi => ?_
        by_cases hi' : i = upcrossingsBefore a b f N ω
        · subst hi'
          simp only [stoppedValue]
          rw [upperCrossingTime_eq_of_upcrossingsBefore_lt hab (Nat.lt_succ_self _)]
          by_cases heq : lowerCrossingTime a b f N (upcrossingsBefore a b f N ω) ω = N
          · rw [heq, sub_self]
          · rw [sub_nonneg]
            exact le_trans (stoppedValue_lowerCrossingTime heq) hf
        · rw [sub_eq_zero_of_upcrossingsBefore_lt hab]
          rw [Finset.mem_range, not_lt] at hi
          exact lt_of_le_of_ne hi (Ne.symm hi')

Goal state after: