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

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn : p.Coprime n
σ : Gal(K/ℚ)
hσ : σ ∈ stabilizer Gal(K/ℚ) P
⊢ (galEquivZMod n K) σ ∈ Subgroup.zpowers (ZMod.unitOfCoprime p hn)

Tactic:
have hζ := IsCyclotomicExtension.zeta_spec n ℚ K

Goal state after:
n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn : p.Coprime n
σ : Gal(K/ℚ)
hσ : σ ∈ stabilizer Gal(K/ℚ) P
hζ : IsPrimitiveRoot (zeta n ℚ K) n
⊢ (galEquivZMod n K) σ ∈ Subgroup.zpowers (ZMod.unitOfCoprime p hn)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn : p.Coprime n
σ : Gal(K/ℚ)
hσ : σ ∈ stabilizer Gal(K/ℚ) P
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/ℤ ⧸ span {↑p}) :=
  (IsFractionRing.stabilizerHom Gal(K/ℚ) (span {↑p}) P (ℤ ⧸ span {↑p}) (𝓞 K ⧸ P)) ⟨σ, hσ⟩
this✝ : CharP (ℤ ⧸ span {↑p}) p
this : Finite (𝓞 K ⧸ P)
i : ℕ
hi : ∀ (x : 𝓞 K ⧸ P), τ x = x ^ Nat.card (ℤ ⧸ span {↑p}) ^ i
⊢ absNorm P ≠ 1

Tactic:
simpa using IsMaximal.ne_top inferInstance

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1
hx₀ : ↑expMapBasis y ≠ 0
⊢ Real.exp (y w₀) ≤ 1

Tactic:
exact Real.exp_le_one_iff.mpr (by simpa using hy w₀ (Set.mem_univ _))

Goal state after:
Module: Mathlib.NumberTheory.NumberField.ExistsRamified

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
H : Module.finrank ℚ K ≠ 1
p : ℕ
hp1 : Nat.Prime p
hp2 : ¬Algebra.IsUnramifiedIn 𝒪 (Ideal.span {↑p})
this✝ : IsDomain 𝒪
this : IsDedekindDomain 𝒪
⊢ ∃ P, ∃ (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
have := IsIntegralClosure.isTorsionFree ℤ (A := 𝒪) K

Goal state after:
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
H : Module.finrank ℚ K ≠ 1
p : ℕ
hp1 : Nat.Prime p
hp2 : ¬Algebra.IsUnramifiedIn 𝒪 (Ideal.span {↑p})
this✝¹ : IsDomain 𝒪
this✝ : IsDedekindDomain 𝒪
this : Module.IsTorsionFree ℤ 𝒪
⊢ ∃ P, ∃ (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case e_f
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this✝ : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
this : 0 = ∑ y, ∑ x_1, ↑(x (y, x_1)) * ∑ u, ↑(a' K a k y x_1 u) * (newBasis K) u
l : β
⊢ ∑ x_1, ↑(x (l, x_1)) * ∑ u, ↑(a' K a k l x_1 u) * (newBasis K) u = (fun j ↦ a k j) l * ξ K x l

Tactic:
rw [ξ, mul_sum]

Goal state after:
case e_f
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this✝ : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
this : 0 = ∑ y, ∑ x_1, ↑(x (y, x_1)) * ∑ u, ↑(a' K a k y x_1 u) * (newBasis K) u
l : β
⊢ ∑ x_1, ↑(x (l, x_1)) * ∑ u, ↑(a' K a k l x_1 u) * (newBasis K) u =
    ∑ i, (fun j ↦ a k j) l * (↑(x (l, i)) * (newBasis K) i)
Module: Mathlib.NumberTheory.Padics.ProperSpace

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
this : {y | ‖y‖ ≤ 1} ∈ 𝓝 0
⊢ LocallyCompactSpace ℚ_[p]

Tactic:
refine IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup ?_ this

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
this : {y | ‖y‖ ≤ 1} ∈ 𝓝 0
⊢ IsCompact {y | ‖y‖ ≤ 1}
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case e_f.e_f
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this✝ : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
this : 0 = ∑ y, ∑ x_1, ↑(x (y, x_1)) * ∑ u, ↑(a' K a k y x_1 u) * (newBasis K) u
l✝ : β
l : K →+* ℂ
⊢ ↑(x (l✝, l)) * ∑ u, ↑(a' K a k l✝ l u) * (newBasis K) u = (fun j ↦ a k j) l✝ * (↑(x (l✝, l)) * (newBasis K) l)

Tactic:
rw [← lin_1]

Goal state after:
case e_f.e_f
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this✝ : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
this : 0 = ∑ y, ∑ x_1, ↑(x (y, x_1)) * ∑ u, ↑(a' K a k y x_1 u) * (newBasis K) u
l✝ : β
l : K →+* ℂ
⊢ ↑(x (l✝, l)) * (a k l✝ * (newBasis K) l) = (fun j ↦ a k j) l✝ * (↑(x (l✝, l)) * (newBasis K) l)
Module: Mathlib.NumberTheory.Padics.Complex

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : 1 < ‖x‖
⊢ 1 < ‖(algebraMap ℚ_[p] (PadicAlgCl p)) x‖

Tactic:
rw [PadicAlgCl.norm_extends]

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : 1 < ‖x‖
⊢ 1 < ‖x‖
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ Continuous fun x ↦ Ring.multichoose x k

Tactic:
simp only [Ring.multichoose, BinomialRing.multichoose]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ Continuous fun x ↦ ⟨↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) / ↑k.factorial, ⋯⟩
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ ‖mahler k‖ = 1

Tactic:
by
  simp [← mahlerTerm_one]

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

Goal state before:
pp: case refine_2
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
y : ℚ_[↑(primesEquiv v)]
hy : y ∈ ↑(subring ↑(primesEquiv v))
⊢ y ∈ ⇑(padicEquiv v) '' ↑(HeightOneSpectrum.adicCompletionIntegers ℚ v)

Tactic:
obtain ⟨x, hx⟩ := (adicCompletionIntegers.padicIntEquiv v).surjective ⟨y, hy⟩
    refine ⟨x, x.2, by rw [← adicCompletionIntegers.coe_padicIntEquiv_apply, hx]⟩

Goal state after:
Module: Mathlib.NumberTheory.Padics.Measure.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
E : Type u_4
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R E
inst✝² : ContinuousSMul R E
μ : AbstractMeasure X R R
ν✝ : AbstractMeasure Y R R
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
ν : AbstractMeasure Y R R
⊢ Continuous (Function.uncurry fun x y ↦ (x.1.curry x.2) y)

Tactic:
rw [← (Homeomorph.prodAssoc C(X × Y, R) X Y).symm.comp_continuous_iff']

Goal state after:
X : Type u_1
Y : Type u_2
R : Type u_3
E : Type u_4
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R E
inst✝² : ContinuousSMul R E
μ : AbstractMeasure X R R
ν✝ : AbstractMeasure Y R R
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
ν : AbstractMeasure Y R R
⊢ Continuous ((Function.uncurry fun x y ↦ (x.1.curry x.2) y) ∘ ⇑(Homeomorph.prodAssoc C(X × Y, R) X Y).symm)
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : d < 0
a : Solution₁ d
⊢ a.x = 0 ∨ a.y = 0

Tactic:
have h := a.prop

Goal state after:
d : ℤ
h₀ : d < 0
a : Solution₁ d
h : a.x ^ 2 - d * a.y ^ 2 = 1
⊢ a.x = 0 ∨ a.y = 0
Module: Mathlib.NumberTheory.Pell

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

Tactic:
rw [Int.ofNat_eq_natCast, zpow_natCast]

Goal state after:
case ofNat
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
⊢ 0 < (a ^ n).x
Module: Mathlib.NumberTheory.Pell

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

Tactic:
rw [Int.ofNat_eq_natCast, zpow_natCast]

Goal state after:
case ofNat.succ
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ (n + 1)).y.sign = (↑(n + 1)).sign
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
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : Module K V
inst✝⁷ : IsScalarTower R K V
inst✝⁶ : AddCommGroup V'
inst✝⁵ : Module R V'
inst✝⁴ : Module S V'
inst✝³ : IsScalarTower R S V'
inst✝² : AddCommGroup V''
inst✝¹ : Module R V''
hRK : IsFractionRing R K
inst✝ : IsDedekindDomain R
hRS : RingHom.ker f ≠ ⊤
F : V'' →ₗ[R] V
hf : Function.Injective ⇑F
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
hb' : LinearIndependent S (⇑f' ∘ b)
⊢ LinearIndependent K (⇑F ∘ b)

Tactic:
contrapose hb' with hb

Goal state after:
R : Type u
inst✝¹⁵ : CommRing R
S : Type v
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : Module K V
inst✝⁷ : IsScalarTower R K V
inst✝⁶ : AddCommGroup V'
inst✝⁵ : Module R V'
inst✝⁴ : Module S V'
inst✝³ : IsScalarTower R S V'
inst✝² : AddCommGroup V''
inst✝¹ : Module R V''
hRK : IsFractionRing R K
inst✝ : IsDedekindDomain R
hRS : RingHom.ker f ≠ ⊤
F : V'' →ₗ[R] V
hf : Function.Injective ⇑F
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
hb : ¬LinearIndependent K (⇑F ∘ b)
⊢ ¬LinearIndependent S (⇑f' ∘ b)
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
w : ℕ → ℝ
⊢ (∑ d ∈ s.prodPrimes.divisors,
      ∑ d1 ∈ s.prodPrimes.divisors, ∑ d2 ∈ s.prodPrimes.divisors, if d = d1.lcm d2 then w d1 * w d2 * s.nu d else 0) =
    ∑ d1 ∈ s.prodPrimes.divisors, ∑ d2 ∈ s.prodPrimes.divisors, s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹

Tactic:
rw [sum_comm, sum_congr rfl]

Goal state after:
s : BoundingSieve
w : ℕ → ℝ
⊢ ∀ x ∈ s.prodPrimes.divisors,
    (∑ x_1 ∈ s.prodPrimes.divisors, ∑ d2 ∈ s.prodPrimes.divisors, if x_1 = x.lcm d2 then w x * w d2 * s.nu x_1 else 0) =
      ∑ d2 ∈ s.prodPrimes.divisors, s.nu x * w x * s.nu d2 * w d2 * (s.nu (x.gcd d2))⁻¹
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
⊢ (∑ x ∈ s.prodPrimes.divisors, ∑ d2 ∈ s.prodPrimes.divisors, if x = d1.lcm d2 then w d1 * w d2 * s.nu x else 0) =
    ∑ d2 ∈ s.prodPrimes.divisors, s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹

Tactic:
rw [sum_comm, sum_congr rfl]

Goal state after:
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
⊢ ∀ x ∈ s.prodPrimes.divisors,
    (∑ x_1 ∈ s.prodPrimes.divisors, if x_1 = d1.lcm x then w d1 * w x * s.nu x_1 else 0) =
      s.nu d1 * w d1 * s.nu x * w x * (s.nu (d1.gcd x))⁻¹
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: p : ℕ
inst✝ : Fact (Prime p)
hp : p % 4 ≠ 3
⊢ ¬Irreducible ↑p

Tactic:
_root_.irreducible_iff_prime,

Goal state after:
p : ℕ
inst✝ : Fact (Prime p)
hp : p % 4 ≠ 3
⊢ ¬_root_.Prime ↑p
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: m n : ℕ
hc : m.Coprime n
hm : IsSquare (-1)
hn : IsSquare (-1)
⊢ IsSquare (-1)

Tactic:
have : IsSquare (-1 : ZMod m × ZMod n) := by
    rw [show (-1 : ZMod m × ZMod n) = ((-1 : ZMod m), (-1 : ZMod n)) from rfl]
    obtain ⟨x, hx⟩ := hm
    obtain ⟨y, hy⟩ := hn
    rw [hx, hy]
    exact ⟨(x, y), rfl⟩
  simpa only [RingEquiv.map_neg_one] using this.map (ZMod.chineseRemainder hc).symm

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
⊢ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3

Tactic:
refine @induction_on_primes _ ?_ ?_ (fun p q hp hq hpq => ?_)

Goal state after:
case refine_1
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
⊢ 0 ∣ n → 0 % 4 ≠ 3

case refine_2
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
⊢ 1 ∣ n → 1 % 4 ≠ 3

case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
p q : ℕ
hp : Nat.Prime p
hq : q ∣ n → q % 4 ≠ 3
hpq : p * q ∣ n
⊢ p * q % 4 ≠ 3
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:
← hkmul,

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 = ↑p * ↑y
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℤ[X]
s : ℂ
⊢ Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)

Tactic:
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

Goal state after:
f : ℤ[X]
s : ℂ
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
⊢ Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
r : ℚ
hr : r ≠ 0
⊢ LiouvilleWith p (x * ↑r) ↔ LiouvilleWith p x

Tactic:
mul_rat_iff hr

Goal state after:
p x : ℝ
r : ℚ
hr : r ≠ 0
⊢ LiouvilleWith p x ↔ LiouvilleWith p x
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
p : Nat.Primes
hA : A ↑p =ᵐ[μ] ∅
hB : B ↑p =ᵐ[μ] ∅
⊢ A ↑p ∪ B ↑p ∪ C ↑p =ᵐ[μ] C ↑p

Tactic:
exact union_ae_eq_right_of_ae_eq_empty ((union_ae_eq_right_of_ae_eq_empty hA).trans hB)

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
i : ι
e : Lex ((i : ι) → (fun i ↦ α i) i)
h : ∀ f ∈ s, (∀ j < i, f j = sInf s j) → e i ≤ f i
⊢ e i ≤ sInf s i

Tactic:
rw [sInf_apply]
  apply le_sInf
  grind

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
⊢ ⊤ ∈ L

Tactic:
by simpa using! L.sInfClosed' <| empty_subset _

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s s' : Set α
⊢ IsExtent r s → IsExtent r s' → IsExtent r (s ∩ s')

Tactic:
IsExtent,

Goal state after:
α : Type u_2
β : Type u_3
r : α → β → Prop
s s' : Set α
⊢ s ∈ range (lowerPolar r) → s' ∈ range (lowerPolar r) → s ∩ s' ∈ range (lowerPolar r)
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : Std.Irrefl r'
⊢ ∀ ⦃a : α⦄, a ∈ c'.extent → ∀ ⦃b : α⦄, b ∈ c'.intent → a ≠ b

Tactic:
rintro x hx _ hx' rfl

Goal state after:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : Std.Irrefl r'
x : α
hx : x ∈ c'.extent
hx' : x ∈ c'.intent
⊢ False
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
⊢ ⨆ a, ↑a ∈ s

Tactic:
have : Countable A := hA_c

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
this : Countable ↑A
⊢ ⨆ a, ↑a ∈ s
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
⊢ ∀ t ⊆ ⋂₀ {t | s ⊆ t ∧ CountableSupClosed t},
    t.Nonempty → t.Countable → ∀ (x : α), IsLUB t x → x ∈ ⋂₀ {t | s ⊆ t ∧ CountableSupClosed t}

Tactic:
simp only [Set.subset_sInter_iff, Set.mem_ofPred_eq, and_imp, Set.mem_sInter]

Goal state after:
α : Type u_2
inst✝ : Preorder α
s : Set α
⊢ ∀ (t : Set α),
    (∀ (t' : Set α), s ⊆ t' → CountableSupClosed t' → t ⊆ t') →
      t.Nonempty → t.Countable → ∀ (x : α), IsLUB t x → ∀ (t : Set α), s ⊆ t → CountableSupClosed t → x ∈ t
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α β : Type u
c : Cardinal.{u}
l✝ : Filter α
inst✝ : CardinalInterFilter l✝ c
l : Set (Set α)
hc : 2 < c
hl : ∀ (S : Set (Set α)), #↑S < c → S ⊆ l → ⋂₀ S ∈ l
h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
s t : Set α
hs : s ∈ l
ht : t ∈ l
⊢ #↑{s, t} ≤ 2

Tactic:
calc
      _ ≤ #({t} : Set (Set α)) + 1 := Cardinal.mk_insert_le
      _ = 2 := by norm_num

Goal state after:
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: case mp.basic
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s✝ : Set α
hreg : c.IsRegular
s : Set α
hs : s ∈ g
⊢ ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s

Tactic:
| @basic s hs =>

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

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

Tactic:
· simpa using hf i.castSucc_le_succ

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LT α
⊢ (univ.chainHeight fun x1 x2 ↦ x1 < x2) = s.chainHeight fun x1 x2 ↦ x1 < x2

Tactic:
simpa using chainHeight_coe_univ s (· < ·)

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 ≤ (n + 1) • μ (closedBall 0 (δ / 2))

Tactic:
exact hδ

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
j : ℕ
b : α j
x✝ : ⟨i, a⟩ ≤ ⟨j, b⟩
hj : i + 1 = j
w✝ : ⟨i, a⟩.fst ≤ ⟨j, b⟩.fst
h✝ : π w✝ ⟨j, b⟩.snd = ⟨i, a⟩.snd
⊢ π ⋯ (π ⋯ b) = a

Tactic:
rwa [π_trans]

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case refine_1
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
⊢ ⨆ y ∈ Y, f a y = f a b

pp: case refine_2
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
⊢ ⨅ x ∈ X, f x b = f a b

pp: case refine_3
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
x✝ : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ f a y ≤ f x b

Tactic:
· apply le_antisymm
    · simp only [iSup_le_iff]
      exact h a ha
    · apply le_iSup₂ b hb

Goal state after:
case refine_2
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
⊢ ⨅ x ∈ X, f x b = f a b

case refine_3
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
x✝ : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ f a y ≤ f x b
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : 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✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
inst✝¹ : ClosedIciTopology E
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ -∫ (ω : Ω) in s, f j ω ∂μ ≤ -∫ (ω : Ω) in s, f i ω ∂μ

Tactic:
← integral_neg,

Goal state after:
Ω : 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✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
inst✝¹ : ClosedIciTopology E
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (a : Ω) in s, -f j a ∂μ ≤ -∫ (ω : Ω) in s, f i ω ∂μ