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

Goal state before:
pp: 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
n i : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ i + 1 ≠ p ^ t

Tactic:
by omega

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ ‖↑x‖ ≤ 1 ↔ ¬p ∣ x.den

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Padic.norm_rat_le_one h⟩

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
h : ‖↑x‖ ≤ 1
⊢ ¬p ∣ x.den
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : |↑q - ξ| < 1 / ↑q.den ^ 2
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ 1 / ↑q.den ^ 2 ≤ 1

Tactic:
div_le_one h0,

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : |↑q - ξ| < 1 / ↑q.den ^ 2
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ 1 ≤ ↑q.den ^ 2
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
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
⊢ ¬‖(Polynomial.aeval z) (Polynomial.derivative F)‖ = 0

Tactic:
hz.1

Goal state after:
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
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
⊢ ¬‖(Polynomial.aeval a) (Polynomial.derivative F)‖ = 0
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : CommRing B
P : Ideal B
D : Type u_5
inst✝⁶ : Field D
inst✝⁵ : Algebra D L
inst✝⁴ : MulSemiringAction Gal(L/K) B
D' : Type u_8
inst✝³ : Field D'
inst✝² : Algebra D' L
inst✝¹ : IsDecompositionField K L P D
inst✝ : IsDecompositionField K L P D'
x : D
⊢ (algebraMap D' L) ((ringEquiv K L P D D') x) = (algebraMap D L) x

Tactic:
simp [IsDecompositionField.ringEquiv, IsGaloisGroup.ringEquiv]

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

Goal state before:
pp: K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : CommRing B
P : Ideal B
D : Type u_5
inst✝⁶ : Field D
inst✝⁵ : Algebra D L
inst✝⁴ : MulSemiringAction Gal(L/K) B
D' : Type u_8
inst✝³ : Field D'
inst✝² : Algebra D' L
inst✝¹ : IsDecompositionField K L P D
inst✝ : IsDecompositionField K L P D'
x : D'
⊢ (algebraMap D L) ((ringEquiv K L P D D').symm x) = (algebraMap D' L) x

Tactic:
simp [IsDecompositionField.ringEquiv, IsGaloisGroup.ringEquiv]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: 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
a : Solution₁ d
hay : 0 ≤ a.y
hax' : ↑x = a.x
hax : 0 < ↑x
hy : 0 < a.y
hx₁ : 1 < a.x
hyy : 0 ≤ (a * a₁⁻¹).y
x' : ℕ
hx' : ↑x' = (a * a₁⁻¹).x
hxx₁ : 0 < ↑x'
hxx₂ : ↑x' < a.x
n : ℕ
hn : a * a₁⁻¹ = a₁ ^ n
⊢ a = a₁ ^ (n + 1)

Tactic:
rw [pow_succ', ← hn, mul_comm a, ← mul_assoc, mul_inv_cancel, one_mul]

Goal state after:
Module: Mathlib.NumberTheory.Pell

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

Tactic:
rw [zpow_one]

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
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
z1 : ℤ_[p] := ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
z' : ℤ_[p] := z - z1
hdist :
  ‖(Polynomial.aeval z') (Polynomial.derivative F) + -(Polynomial.aeval z) (Polynomial.derivative F)‖ <
    ‖-(Polynomial.aeval z) (Polynomial.derivative F)‖
this : ‖(Polynomial.aeval z') (Polynomial.derivative F)‖ = ‖(Polynomial.aeval z) (Polynomial.derivative F)‖
⊢ ‖(Polynomial.aeval z') (Polynomial.derivative F)‖ = ‖(Polynomial.aeval a) (Polynomial.derivative F)‖

Tactic:
hz.1

Goal state after:
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 : ℕ
z : ℤ_[p]
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
z1 : ℤ_[p] := ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
z' : ℤ_[p] := z - z1
hdist :
  ‖(Polynomial.aeval z') (Polynomial.derivative F) + -(Polynomial.aeval z) (Polynomial.derivative F)‖ <
    ‖-(Polynomial.aeval z) (Polynomial.derivative F)‖
this : ‖(Polynomial.aeval z') (Polynomial.derivative F)‖ = ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
⊢ ‖(Polynomial.aeval z') (Polynomial.derivative F)‖ = ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
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
⊢ Tendsto (fun n ↦ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n) atTop (𝓝 0)

Tactic:
← mul_zero ‖F.derivative.aeval a‖

Goal state after:
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 n ↦ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n) atTop
    (𝓝 (‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * 0))
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑j ≤ (↑⌈(↑j + 1) / r⌉ - 1) * r
⊢ j ∈ {x | ∃ k, beattySeq r k = x} ∨ ∃ k, ↑k < ↑j / r ∧ (↑j + 1) / r ≤ ↑k + 1

Tactic:
· refine Or.inl ⟨⌈(j + 1) / r⌉ - 1, ?_⟩
    rw [beattySeq, Int.floor_eq_iff, Int.cast_sub, Int.cast_one, ← lt_div_iff₀ h, sub_lt_iff_lt_add]
    exact ⟨‹_›, Int.ceil_lt_add_one _⟩

Goal state after:
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
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }
y : ℕ
hy : k ^ 2 + 1 = p * y
⊢ { re := ↑k, im := 1 } * { re := ↑k, im := -1 } = ↑p * ↑y

Tactic:
rw [← hkmul, ← Nat.cast_mul p, ← hy]

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
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hk₀ : k ≠ 0
hkltp : 1 + k * k < p * p
hpk₁ : ¬↑p ∣ { re := ↑k, im := -1 }
hpk₂ : ¬↑p ∣ { re := ↑k, im := 1 }
y : ℕ
hy : k ^ 2 + 1 = p * y
⊢ ↑k ^ 2 + 1 = ↑(k ^ 2 + 1)
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℤ[X]
s : ℂ
⊢ ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c ^ p

Tactic:
have : Bornology.IsBounded
      ((fun x : ℝ ↦ max (x * ‖s‖) 1 * ‖aeval (x * s) f‖) '' Set.Ioc 0 1) := by
    have h :
      (fun x : ℝ ↦ max (x * ‖s‖) 1 * ‖aeval (x * s) f‖) '' Set.Ioc 0 1 ⊆
        (fun x : ℝ ↦ max (x * ‖s‖) 1 * ‖aeval (x * s) f‖) '' Set.Icc 0 1 :=
      Set.image_mono Set.Ioc_subset_Icc_self
    refine (IsCompact.image isCompact_Icc ?_).isBounded.subset h
    fun_prop

Goal state after:
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
⊢ ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c ^ p
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
h : ∀ x ∈ (fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1, |x| ≤ c
⊢ ∃ c ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c ^ p

Tactic:
refine P_le _ s c (fun p x hx => ?_)

Goal state after:
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
h : ∀ x ∈ (fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1, |x| ≤ c
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ ‖eval (x • s) (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p))‖ ≤ c ^ p
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
p : Ideal R
P : Ideal S
hfp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
inst✝¹ : IsDedekindDomain S
inst✝ : P.IsPrime
hP : P ≠ ⊥
i : ℕ
hi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by
  choose a a_mem a_notMem using
    SetLike.exists_of_lt
      (Ideal.pow_right_strictAnti P hP (Ideal.IsPrime.ne_top inferInstance) (le_refl i.succ))
  refine (LinearEquiv.ofBijective ?_ ⟨?_, ?_⟩).symm
  · exact quotientToQuotientRangePowQuotSucc p P a_mem
  · exact quotientToQuotientRangePowQuotSucc_injective p P hi a_mem a_notMem
  · exact quotientToQuotientRangePowQuotSucc_surjective p P hP hi a_mem a_notMem

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

Goal state before:
pp: case refine_2
⊢ range Rat.cast ⊆ {x | x ∈ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)}

Tactic:
rintro _ ⟨r, rfl⟩
    simp only [mem_iInter, mem_iUnion]
    refine fun n => ⟨r.num * 2, r.den * 2, ?_, ?_⟩
    · have := r.pos; lia
    · convert! @mem_ball_self ℝ _ (r : ℝ) _ _
      · push_cast
        -- Workaround for https://github.com/leanprover/lean4/pull/6438; this eliminates an
        -- `Expr.mdata` that would cause `norm_cast` to skip a numeral.
        rw [Eq.refl (2 : ℝ)]
        norm_cast
        simp [Rat.divInt_mul_right (two_ne_zero)]
      · refine one_div_pos.2 (pow_pos (Int.cast_pos.2 ?_) _)
        exact mul_pos (Int.natCast_pos.2 r.pos) zero_lt_two

Goal state after:
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_3.refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ ↑b ≠ 0

pp: case refine_3.refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ (↑(Units.mk0 ↑b ?refine_3.refine_1)).val = b

Tactic:
· intro h; apply hb.1; apply_fun val at h
      simpa only [val_cast_of_lt hb.right, val_zero] using h

Goal state after:
case refine_3.refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ (↑(Units.mk0 ↑b ⋯)).val = b
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ (a : ℤ), x ≠ ↑a / ↑b → 1 / ↑b ^ n ≤ |x - ↑a / ↑b|
this : ∀ b > 1, ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
⊢ False

Tactic:
have : ∀ᶠ m : ℕ in atTop, ∀ b < N, 1 < b → ∀ a : ℤ, 1 / (b : ℝ) ^ m ≤ |x - a / b| :=
    (finite_lt_nat N).eventually_all.2 fun b _hb => eventually_imp_distrib_left.2 (this b)

Goal state after:
x : ℝ
hx : Liouville x
n N : ℕ
hN : ∀ (b : ℕ), N ≤ b → ∀ (a : ℤ), x ≠ ↑a / ↑b → 1 / ↑b ^ n ≤ |x - ↑a / ↑b|
this✝ : ∀ b > 1, ∀ᶠ (m : ℕ) in atTop, ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
this : ∀ᶠ (m : ℕ) in atTop, ∀ b < N, 1 < b → ∀ (a : ℤ), 1 / ↑b ^ m ≤ |x - ↑a / ↑b|
⊢ False
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
⊢ ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p

Tactic:
rintro ⟨p, hp⟩

Goal state after:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
p : ℕ
hp : Nat.Prime p
⊢ addOrderOf (u ⟨p, hp⟩) = ↑⟨p, hp⟩
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
⊢ ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ

Tactic:
rintro ⟨p, hp⟩

Goal state after:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
p : ℕ
hp : Nat.Prime p
⊢ A ↑⟨p, hp⟩ =ᵐ[μ] ∅ ∨ A ↑⟨p, hp⟩ =ᵐ[μ] univ
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L✝ L : CompleteSublattice α
s : Set β
hs : s ⊆ ⇑f '' ↑L
⊢ sSup s ∈ ⇑f '' ↑L

Tactic:
obtain ⟨t, ht, rfl⟩ := subset_image_iff.mp hs
    rw [← map_sSup]
    exact mem_image_of_mem f (sSupClosed ht)

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
⊢ ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ

Tactic:
rintro ⟨p, hp⟩

Goal state after:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
p : ℕ
hp : Nat.Prime p
⊢ B ↑⟨p, hp⟩ =ᵐ[μ] ∅ ∨ B ↑⟨p, hp⟩ =ᵐ[μ] univ
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst✝² : CardinalInterFilter l c
l₁ l₂ : Filter α
inst✝¹ : CardinalInterFilter l₁ c
inst✝ : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #↑S < c
s : (s : Set α) → s ∈ S → Set α
hs : ∀ (s_1 : Set α) (a : s_1 ∈ S), s s_1 a ∈ l₁
t : (s : Set α) → s ∈ S → Set α
ht : ∀ (s : Set α) (a : s ∈ S), t s a ∈ l₂
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
⊢ ⋂₀ S ∈ l₁ ⊓ l₂

Tactic:
replace hs : (⋂ i ∈ S, s i ‹_›) ∈ l₁ := (cardinal_bInter_mem hSc).2 hs

Goal state after:
ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst✝² : CardinalInterFilter l c
l₁ l₂ : Filter α
inst✝¹ : CardinalInterFilter l₁ c
inst✝ : CardinalInterFilter l₂ c
S : Set (Set α)
hSc : #↑S < c
s t : (s : Set α) → s ∈ S → Set α
ht : ∀ (s : Set α) (a : s ∈ S), t s a ∈ l₂
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hs : ⋂ i, ⋂ (h : i ∈ S), s i h ∈ l₁
⊢ ⋂₀ S ∈ l₁ ⊓ l₂
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:
by
  intro x y z hxy hyz
  exact closed_interval h₂ h₄ (x ⊓ y ⊓ z) _ _ (x ⊔ y ⊔ z) (by simp [inf_assoc, inf_le_left])
    (by simp [sup_assoc, le_sup_left]) inf_le_right le_sup_right
    (h₃ (by simpa [inf_assoc] using inf_le_of_right_le inf_le_sup)
    (by simp [sup_assoc, le_sup_right]) (h₃
    (by simpa [inf_assoc] using inf_le_right (b := y ⊓ z)) inf_le_sup (by
      suffices r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z)) by
        rw [inf_comm x, inf_assoc]
        simpa [inf_comm x, ← inf_inf_distrib_left] using this
      exact (h₄ inf_le_sup (h₂.mp hxy)).1) (h₂.mp hyz)) (by
        simpa [sup_comm y x, sup_sup_distrib_left y x z, sup_assoc] using
          ((h₄ inf_le_sup (h₂.mp hxy)).2 : r (x ⊓ y ⊔ (y ⊔ z)) (x ⊔ y ⊔ (y ⊔ z)))))

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
ha : a ∈ u
hab : f a = b
hb : b ∉ u
⊢ False

Tactic:
exact hab ▸ hb <| hf.apply_mem ha

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
this : t₁.root = ⊥
⊢ False

Tactic:
exact t₁.root_ne_bot_of_mem_subtrees ht₁ this

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s✝ : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a b : X
s : ↥S
⊢ b ≤ a ⇨ ↑s ↔ Sublocale.restrictAux✝ S (a ⊓ b) ≤ s

Tactic:
simp [inf_comm, S.giAux.gc.le_iff_le]

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
⊢ sInf {s | ⊤ ≤ ↑s} = ⊤

Tactic:
by
    refine le_antisymm le_top ?_
    change _ ≤ restrictAux S ⊤
    rw [← Subtype.coe_le_coe, S.giAux.gc.u_top]
    simp [restrictAux, sInf]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
this✝ : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
this : MeasurableSpace Ω := ↑𝓕 n
X : ℕ → Ω → E := fun m_1 ↦ Function.curry (⇑(StronglyMeasurable.approx h𝓕 m_1)) (n + 1)
⊢ StronglyMeasurable (u (n + 1))

Tactic:
refine ⟨(fun m ↦ SimpleFunc.mk (X m) ?_ ?_), (fun ω ↦ h𝓕.tendsto_approx ⟨(n + 1), ω⟩)⟩

Goal state after:
case refine_1
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
this✝ : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
this : MeasurableSpace Ω := ↑𝓕 n
X : ℕ → Ω → E := fun m ↦ Function.curry (⇑(StronglyMeasurable.approx h𝓕 m)) (n + 1)
m : ℕ
⊢ ∀ (x : E), MeasurableSet (X m ⁻¹' {x})

case refine_2
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
n : ℕ
this✝ : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
this : MeasurableSpace Ω := ↑𝓕 n
X : ℕ → Ω → E := fun m ↦ Function.curry (⇑(StronglyMeasurable.approx h𝓕 m)) (n + 1)
m : ℕ
⊢ (Set.range (X m)).Finite
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case refine_2.ht
Ω : 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 x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
e : E
he : e ∈ Set.range (Y m)
n : ℕ
ω : Ω
hnω : Y m (n, ω) = e
⊢ e ∈ ⋃ k ∈ Finset.range (m + 1), Set.range (Function.curry (X m) k)

Tactic:
simp_rw [Set.mem_iUnion, Set.mem_range]

Goal state after:
case refine_2.ht
Ω : 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 x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
e : E
he : e ∈ Set.range (Y m)
n : ℕ
ω : Ω
hnω : Y m (n, ω) = e
⊢ ∃ i, ∃ (_ : i ∈ Finset.range (m + 1)), ∃ y, Function.curry (X m) i y = e
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n m : ι
ω : Ω
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ m ≤ m

Tactic:
exact le_rfl

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 i : ι
ω : Ω
inst✝ : WellFoundedLT ι
h' : hittingAfter u s n ω ≤ ↑i
h : hittingAfter u s n ω = ⊤
⊢ False

Tactic:
simp [h] at h'

Goal state after: