mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
⊢ ‖asiegel K a‖ ≤ c₂ K * A

Tactic:
rw [Matrix.norm_le_iff]

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
⊢ ∀ (i : α × (K →+* ℂ)) (j : β × (K →+* ℂ)), ‖asiegel K a i j‖ ≤ c₂ K * A

case hr
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
⊢ 0 ≤ c₂ K * A
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun i a ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ}, c ∈ m.digits n → f ↑c < ↑m
⊢ f ↑n = f ↑(ofDigits m L)

Tactic:
rw [Nat.ofDigits_digits m n]

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
s t : ℝ
hfm : f ↑m = ↑m ^ s
hfn : f ↑n = ↑n ^ t
⊢ ↑m ^ (logb ↑m ↑n * s) ≤ ↑n ^ s

Tactic:
rpow_mul (Nat.cast_nonneg m),

Goal state after:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
s t : ℝ
hfm : f ↑m = ↑m ^ s
hfn : f ↑n = ↑n ^ t
⊢ (↑m ^ logb ↑m ↑n) ^ s ≤ ↑n ^ s
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 : ℕ
x✝ : i ∈ range (n + 1)
⊢ ‖((-1) ^ (n - i) * ↑(n.choose i)) • (f (↑i + ↑(p ^ t)) - f ↑i)‖ ≤
    ‖↑(-1) ^ (n - i) * ↑(n.choose i)‖ * ‖f (↑i + ↑(p ^ t)) - f ↑i‖

Tactic:
rw [← Int.cast_smul_eq_zsmul ℤ_[p]]

Goal state after:
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 : ℕ
x✝ : i ∈ range (n + 1)
⊢ ‖↑((-1) ^ (n - i) * ↑(n.choose i)) • (f (↑i + ↑(p ^ t)) - f ↑i)‖ ≤
    ‖↑(-1) ^ (n - i) * ↑(n.choose i)‖ * ‖f (↑i + ↑(p ^ t)) - f ↑i‖
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: case refine_3
ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)
hVun : univ ⊆ ⋃ j, ↑(V j)
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : ⋃ i, ↑(W i) = ⋃ i, ↑(V i)
t : Finset (Fin n) := {j | W j ≠ ⊥}
x : X
hx : x ∈ univ
j : Fin n
hj : x ∈ ↑(W j)
⊢ x ∈ ⋃ j, ↑((fun k ↦ W ↑(t.equivFin.symm k)) j)

Tactic:
have : W j ≠ ⊥ := by simpa [← SetLike.coe_ne_coe, ← Set.nonempty_iff_ne_empty] using ⟨x, hj⟩

Goal state after:
case refine_3
ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)
hVun : univ ⊆ ⋃ j, ↑(V j)
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : ⋃ i, ↑(W i) = ⋃ i, ↑(V i)
t : Finset (Fin n) := {j | W j ≠ ⊥}
x : X
hx : x ∈ univ
j : Fin n
hj : x ∈ ↑(W j)
this : W j ≠ ⊥
⊢ x ∈ ⋃ j, ↑((fun k ↦ W ↑(t.equivFin.symm k)) j)
Module: Mathlib.NumberTheory.Pell

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

Tactic:
exact x_pow_pos hax n

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]
ha : (Polynomial.aeval a) F = 0
z' : ℤ_[p]
hz' : (Polynomial.aeval z') F = 0
hnormz' : ‖z' - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  (Polynomial.aeval (a + h)) F = (Polynomial.aeval a) F + (Polynomial.aeval a) (Polynomial.derivative F) * h + q * h ^ 2
this✝ : ((Polynomial.aeval a) (Polynomial.derivative F) + q * h) * h = 0
hne : ¬h = 0
this : (Polynomial.aeval a) (Polynomial.derivative F) + q * h = 0
⊢ (Polynomial.aeval a) (Polynomial.derivative F) = -q * h

Tactic:
simpa using eq_neg_of_add_eq_zero_left this

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
hx : a.x = b.x
⊢ a.y = b.y

Tactic:
have : d * a.y ^ 2 = d * b.y ^ 2 := by rw [a.prop_y, b.prop_y, hx]

Goal state after:
d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
hx : a.x = b.x
this : d * a.y ^ 2 = d * b.y ^ 2
⊢ a.y = b.y
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
⊢ ∃ a, IsFundamental a

Tactic:
let x₁ := Nat.find P

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
⊢ ∃ a, IsFundamental a
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : (a ^ n).x = (-a ^ n').x
H : (a ^ n').x < 0
⊢ False

Tactic:
exact lt_irrefl _ ((x_zpow_pos h.x_pos n').trans H)

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

Goal state before:
pp: case refine_2
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
E : Type u_6
inst✝¹¹ : Field E
inst✝¹⁰ : Algebra E L
inst✝⁹ : MulSemiringAction Gal(L/K) B
G : Type u_7
inst✝⁸ : Group G
inst✝⁷ : Finite G
inst✝⁶ : MulSemiringAction G L
inst✝⁵ : IsGaloisGroup G K L
inst✝⁴ : MulSemiringAction G B
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : SMulDistribClass Gal(L/K) B L
inst✝ : SMulDistribClass G B L
h : IsGaloisGroup (↥(inertia G P)) E L
x✝ : ↥(inertia Gal(L/K) P)
y z : B
left✝ : z ∈ nonZeroDivisors B
⊢ (algebraMap B L) ((P.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯).symm x✝ • y) /
      (algebraMap B L) ((P.inertiaEquiv (IsGaloisGroup.mulEquivAlgEquiv G K L) ⋯).symm x✝ • z) =
    (algebraMap B L) (x✝ • y) / (algebraMap B L) (x✝ • z)

Tactic:
inertiaEquiv_symm_apply_smul

Goal state after:
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
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
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), ∑ j, A i j • a j = 0
⊢ Submodule.span K (⇑(algebraMap S L) '' b) = ⊤

Tactic:
have d_smul : ∀ i, A.det • a i = 0 := by
    intro i
    calc
      A.det • a i = ∑ j, (B * A) i j • a j := ?_
      _ = ∑ k, B i k • ∑ j, A k j • a j := ?_
      _ = 0 := Finset.sum_eq_zero fun k _ => ?_
    · simp only [B, Matrix.adjugate_mul, Matrix.smul_apply, Matrix.one_apply, smul_eq_mul, ite_true,
        mul_ite, mul_one, mul_zero, ite_smul, zero_smul, Finset.sum_ite_eq, Finset.mem_univ]
    · simp only [Matrix.mul_apply, Finset.smul_sum, Finset.sum_smul, smul_smul]
      rw [Finset.sum_comm]
    · rw [A_smul, smul_zero]

Goal state after:
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
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), ∑ j, A i j • a j = 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
⊢ Submodule.span K (⇑(algebraMap S L) '' b) = ⊤
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₁ * (a * a₁⁻¹)

Tactic:
mul_comm a,

Goal state after:
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₁ * (a₁⁻¹ * a)
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r : ℝ
hr : Irrational r
⊢ {x | ∃ k > 0, beattySeq' r k = x} = {x | ∃ k > 0, beattySeq r k = x}

Tactic:
dsimp only [beattySeq, beattySeq']
  congr! 4; rename_i k; rw [and_congr_right_iff]; intro hk; congr!
  rw [sub_eq_iff_eq_add, Int.ceil_eq_iff, Int.cast_add, Int.cast_one, add_sub_cancel_right]
  refine ⟨(Int.floor_le _).lt_of_ne fun h ↦ ?_, (Int.lt_floor_add_one _).le⟩
  exact (hr.intCast_mul hk.ne').ne_int ⌊k * r⌋ h.symm

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
⊢ s.totalMass * mainSum muPlus + ∑ d ∈ s.prodPrimes.divisors, muPlus d * rem d ≤
    s.totalMass * mainSum muPlus + errSum muPlus

Tactic:
rw [errSum]
    gcongr _ + ∑ d ∈ _, ?_ with d
    rw [← abs_mul]
    exact le_abs_self (muPlus d * s.rem d)

Goal state after:
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
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
⊢ finrank (R ⧸ p) (S ⧸ map f p) = finrank K L

Tactic:
have b_eq_b' : ⇑b = (Submodule.mkQ (map (algebraMap R S) p)).restrictScalars R ∘ b' :=
    funext fun i => (Ideal.Quotient.mk_surjective (b i)).choose_spec.symm

Goal state after:
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'
⊢ finrank (R ⧸ p) (S ⧸ map f p) = finrank K L
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ (∑ l ∈ s.prodPrimes.divisors, if l ∣ d then selbergTerms l else 0) = selbergTerms d * (s.nu d)⁻¹

Tactic:
by
  calc
    (∑ l ∈ divisors s.prodPrimes, if l ∣ d then s.selbergTerms l else 0) =
        ∑ l ∈ divisors s.prodPrimes, if l ∣ d then s.selbergTerms (d / l) else 0 := by
      simp_rw [← sum_filter, Nat.divisors_filter_dvd_of_dvd prodPrimes_ne_zero hd,
        sum_div_divisors d s.selbergTerms]
    _ = s.selbergTerms d *
          ∑ l ∈ divisors s.prodPrimes, if l ∣ d then (s.selbergTerms l)⁻¹ else 0 := by
      simp_rw [← sum_filter, mul_sum]
      congr! 1 with l hl
      simp only [mem_filter, mem_divisors, ne_eq] at hl
      rw [selbergTerms_isMultiplicative.map_div_of_coprime hl.2]
      · ring
      · apply coprime_of_squarefree_mul <|
          (Nat.div_mul_cancel hl.2).symm ▸ (squarefree_of_dvd_prodPrimes hd)
      · exact (selbergTerms_pos hl.1.1).ne'
    _ = s.selbergTerms d * (s.nu d)⁻¹ := by rw [← nu_inv_eq_sum_divisors_inv_selbergTerms hd]

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

Goal state before:
pp: case refine_2
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ 1 / A ≤ ↑b ^ f.natDegree * |x - ↑a / ↑b|

Tactic:
· lift b to ℕ using zero_le_one.trans b1.le
    specialize h a b.pred
    rwa [← Nat.cast_succ, Nat.succ_pred_eq_of_pos (zero_lt_one.trans _), ← mul_assoc, ←
      div_le_iff₀ hA] at h
    exact Int.ofNat_lt.mp b1

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
⊢ ⋃ i ∈ {y | orderOf y = n}, (fun x ↦ a • x) '' ball i δ ⊆ ⋃ x ∈ {y | orderOf y = orderOf a * n}, ball x δ

Tactic:
image_smul,

Goal state after:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
⊢ ⋃ i ∈ {y | orderOf y = n}, a • ball i δ ⊆ ⋃ x ∈ {y | orderOf y = orderOf a * n}, ball x δ
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : orderOf a ^ 2 ∣ n
⊢ ⋃ i ∈ {y | orderOf y = n}, (fun x ↦ a • x) '' ball i δ = ⋃ x ∈ {y | orderOf y = n}, ball x δ

Tactic:
image_smul,

Goal state after:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : orderOf a ^ 2 ∣ n
⊢ ⋃ i ∈ {y | orderOf y = n}, a • ball i δ = ⋃ x ∈ {y | orderOf y = n}, ball x δ
Module: Mathlib.Order.CompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CompletePartialOrder α
inst✝ : Preorder β
f : α → β
⊢ ScottContinuous f ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))

Tactic:
refine ⟨fun h d hd₁ hd₂ ↦ h hd₁ hd₂ hd₂.isLUB_sSup, fun h d hne hd a hda ↦ ?_⟩

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CompletePartialOrder α
inst✝ : Preorder β
f : α → β
h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))
d : Set α
hne : d.Nonempty
hd : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ IsLUB (f '' d) (f a)
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
⊢ c.intent ⊆ d.intent ↔ d ≤ c

Tactic:
by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rw [← extent_subset_extent_iff, ← c.lowerPolar_intent, ← d.lowerPolar_intent]
    exact lowerPolar_anti _ h
  · rw [← c.upperPolar_extent, ← d.upperPolar_extent]
    exact upperPolar_anti _ h

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

Goal state before:
pp: n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
x : α
hx : f (last n) ≤ x
⊢ Monotone ((last (n + 1)).insertNth x f)

Tactic:
rw [Fin.monotone_iff_le_succ]
  intro i
  obtain ⟨i, rfl⟩ | rfl := i.eq_castSucc_or_eq_last
  · simpa only [insertNth_last', snoc_castSucc, Fin.succ_castSucc]
      using hf i.castSucc_le_succ
  · simpa

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
⊢ μ univ ≤ Finset.univ.card • μ (closedBall 0 (δ / 2))

Tactic:
Finset.card_univ,

Goal state after:
A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
B : ↑(Icc 0 n) → Set A := fun j ↦ closedBall (↑j • ξ) (δ / 2)
hB : ∀ (j : ↑(Icc 0 n)), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (B j)
h : Pairwise (Disjoint on B)
⊢ μ univ ≤ Fintype.card ↑(Icc 0 n) • μ (closedBall 0 (δ / 2))
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 t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
a b c d : α
hab : a ≤ b
hbd : b ≤ d
hac : a ≤ c
hcd : c ≤ d
had : r a d
⊢ r b c

Tactic:
by
  suffices r (b ⊓ c ⊓ (b ⊔ c)) (d ⊓ (b ⊔ c)) by
    simpa [h₂, inf_eq_right.mpr (sup_le hbd hcd)] using this
  apply (h₄ (inf_le_of_left_le hbd) _).1
  simpa [sup_eq_right.mpr (le_inf hab hac), sup_eq_left.mpr (inf_le_of_left_le hbd)] using
    ((h₄ (le_trans hab hbd) had).2 : r (a ⊔ b ⊓ c) (d ⊔ b ⊓ c))

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n m : Nucleus X
h : range ⇑m ⊆ range ⇑n
x : X
⊢ n x ≤ n (m x)

Tactic:
exact n.monotone m.le_apply

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 | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}.PairwiseDisjoint id

Tactic:
intro a ha a' ha' h

Goal state after:
α✝ : 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 : α
ha : a ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}
a' : α
ha' : a' ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}
h : a ≠ a'
⊢ Function.onFun Disjoint id a a'
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 : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
⊢ f a b ≤ ⨆ y ∈ Y, ⨅ x ∈ X, f x y

Tactic:
· rw [← h.2]
      apply le_trans (le_rfl) (le_iSup₂ b hb)

Goal state after:
Module: Mathlib.Order.ScottContinuity.Complete

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α → β
h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → f (sSup d) = sSup (f '' d)
x✝¹ : Set α
d₁ : x✝¹.Nonempty
d₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) x✝¹
x✝ : α
hda : IsLUB x✝¹ x✝
⊢ sSup (f '' x✝¹) = f x✝

Tactic:
← (h d₁ d₂),

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α → β
h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → f (sSup d) = sSup (f '' d)
x✝¹ : Set α
d₁ : x✝¹.Nonempty
d₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) x✝¹
x✝ : α
hda : IsLUB x✝¹ x✝
⊢ f (sSup x✝¹) = f x✝
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 : Martingale f ℱ μ
n : ℕ
⊢ predictablePart f ℱ μ n =ᵐ[μ] 0

Tactic:
rw [predictablePart, ← Finset.sum_const_zero (s := Finset.range n)]

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 : Martingale f ℱ μ
n : ℕ
⊢ ∑ i ∈ Finset.range n, μ[f (i + 1) - f i | ↑ℱ i] =ᵐ[μ] ∑ _x ∈ Finset.range n, 0
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: 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 : ℕ
s : E
⊢ MeasurableSet (X m ⁻¹' {s})

Tactic:
(by aesop : X m ⁻¹' {s} = {ω | (n + 1, ω) ∈ h𝓕.approx m ⁻¹' {s}})

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 : ℕ
s : E
⊢ MeasurableSet {ω | (n + 1, ω) ∈ ⇑(StronglyMeasurable.approx h𝓕 m) ⁻¹' {s}}
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case mpr
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
a : Ω
h : τ a ≤ ↑i ∧ ∀ (x : Ω), τ x < ↑i → ¬τ a ≤ τ x
⊢ τ a = ↑i

Tactic:
· exact h.1.eq_or_lt.resolve_right fun h_lt => h.2 a h_lt 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 ι
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
⊢ ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s

Tactic:
obtain ⟨k₁, hk₁_mem, hk₁_s⟩ := h_exists

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
k₁ : ι
hk₁_mem : k₁ ∈ Set.Icc n m
hk₁_s : u k₁ ω ∈ s
⊢ ∃ k ∈ Set.Icc n (min m i), u k ω ∈ s