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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
⊢ 𝒑.ramificationIdxIn (𝓞 K) = p - 1

Tactic:
by
  rw [← pow_one p] at hK
  rw [ramificationIdxIn_eq_of_prime_pow p 0, pow_zero, one_mul]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: case refine_2
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
this : IsGalois ℚ K
hn : ¬p ∣ n
⊢ orderOf ↑p ≤ (span {↑p}).inertiaDegIn (𝓞 K)

Tactic:
inertiaDegIn_eq_of_not_dvd p K hn

Goal state after:
case refine_2
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
this : IsGalois ℚ K
hn : ¬p ∣ n
⊢ orderOf ↑p ≤ orderOf ↑p
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: case refine_2
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
this : IsGalois ℚ K
hn : ¬p ∣ n
⊢ orderOf (ZMod.unitOfCoprime p hn✝) ≤ Nat.card ↑(⇑(galEquivZMod n K).toEquiv '' ↑(stabilizer Gal(K/ℚ) P))

Tactic:
rw [Nat.card_image_equiv, SetLike.coe_sort_coe, Ideal.card_stabilizer_eq (span {(p : ℤ)}),
      ramificationIdxIn_eq_of_not_dvd p K hn, one_mul, ← orderOf_injective _ Units.coeHom_injective,
      Units.coeHom_apply, ZMod.coe_unitOfCoprime, inertiaDegIn_eq_of_not_dvd p K hn]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
⊢ 0 ≤ if h : ∃ δ, HasDirichletDensity S δ then h.choose else 0

Tactic:
split_ifs with h

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
h : ∃ δ, HasDirichletDensity S δ
⊢ 0 ≤ h.choose

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
h : ¬∃ δ, HasDirichletDensity S δ
⊢ 0 ≤ 0
Module: Mathlib.NumberTheory.NumberField.DirichletDensity

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
⊢ (if h : ∃ δ, HasDirichletDensity S δ then h.choose else 0) ≤ 1

Tactic:
split_ifs with h

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
h : ∃ δ, HasDirichletDensity S δ
⊢ h.choose ≤ 1

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
h : ¬∃ δ, HasDirichletDensity S δ
⊢ 0 ≤ 1
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, ∃ (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
by
  obtain ⟨p, hp1, hp2⟩ := NumberField.exists_not_isUnramifiedIn (𝒪 := 𝒪) H
  have := (IsIntegralClosure.algebraMap_injective 𝒪 ℤ K).isDomain
  have := IsIntegralClosure.isDedekindDomain ℤ ℚ K 𝒪
  have := IsIntegralClosure.isTorsionFree ℤ (A := 𝒪) K
  have := IsIntegralClosure.isIntegral_algebra ℤ (A := 𝒪) K
  grind [Algebra.isUnramifiedIn_iff_forall_of_isDedekindDomain]

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: ⊢ Tendsto (fun k ↦ ↑k ^ (↑k)⁻¹) atTop (𝓝 1)

Tactic:
simp_rw [← one_div]
  exact Tendsto.comp tendsto_rpow_div tendsto_natCast_atTop_atTop

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
⊢ ∑ x, -(↑B * (A i x)⁻) ≤ ∑ j, A i j * v j

Tactic:
gcongr ∑ _ : β, ?_ with j _

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
⊢ -(↑B * (A i j)⁻) ≤ A i j * v j
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
⊢ ∑ j, A i j * v j ≤ ∑ j, ↑B * (A i j)⁺

Tactic:
gcongr ∑ _ : β, ?_ with j _

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
⊢ A i j * v j ≤ ↑B * (A i j)⁺
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
x : ℚ
⊢ f ↑x.num ^ c / f ↑x.den ^ c = g ↑x.num / g ↑x.den

Tactic:
h x.den,

Goal state after:
f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
x : ℚ
⊢ f ↑x.num ^ c / g ↑x.den = g ↑x.num / g ↑x.den
Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion

Goal state before:
pp: G : Type u_1
inst✝³ : AddGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformAddGroup G
inst✝ : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : U ∈ 𝓝 0
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : C ∈ 𝓝 0
C_closed : IsClosed C
this : ⇑toCompl ⁻¹' C ∈ 𝓝 0
W : OpenAddSubgroup G
hCW : ↑W ⊆ ⇑toCompl ⁻¹' C
V : Set (Completion G) := ⋯
⊢ ↑(map toCompl ↑W).topologicalClosure ∈ 𝓝 0

Tactic:
apply (isDenseInducing_toCompl _).closure_image_mem_nhds

Goal state after:
G : Type u_1
inst✝³ : AddGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformAddGroup G
inst✝ : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : U ∈ 𝓝 0
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : C ∈ 𝓝 0
C_closed : IsClosed C
this : ⇑toCompl ⁻¹' C ∈ 𝓝 0
W : OpenAddSubgroup G
hCW : ↑W ⊆ ⇑toCompl ⁻¹' C
V : Set (Completion G) := ⋯
⊢ ↑↑W ∈ 𝓝 0
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
⊢ CauchySeq fun s ↦ ∏ i ∈ s, f i

Tactic:
apply cauchySeq_finset_iff_prod_vanishing.mpr
  intro U hU
  -- Since `G` is nonarchimedean, `U` contains an open subgroup `V`.
  rcases is_nonarchimedean U hU with ⟨V, hV⟩
  /- Let `s` be the set of all indices `i : α` such that `f i ∉ V`. By our assumption `hf`, this is
  finite. -/
  use (tendsto_def.mp hf V V.mem_nhds_one).toFinset
  /- For any `t : Finset α` disjoint from `s`, the product `∏ i ∈ t, f i` is a product of elements
  of `V`, so it is an element of `V` too. Thus, `∏ i ∈ t, f i ∈ U`, as desired. -/
  intro t ht
  apply hV
  apply Subgroup.prod_mem
  intro i hi
  simpa using Finset.disjoint_left.mp ht hi

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
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalRing R
μ : AbstractMeasure X R R
ν : AbstractMeasure Y R R
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
f : C(X, R)
g : C(Y, R)
⊢ ((prodMk' μ) ν) (f.comp fst * g.comp snd) = μ f * ν g

Tactic:
by
  simp only [prodMk'_apply, mul_comm (μ f) (ν g), ← smul_eq_mul, ← map_smul]
  congr 1 with x
  simp_rw [ContinuousMap.smul_apply, smul_eq_mul, mul_comm (ν g) (f x), contractSnd_apply,
    ← smul_eq_mul, ← map_smul]
  rfl

Goal state after:
Module: Mathlib.NumberTheory.PrimesCongruentOne

Goal state before:
pp: case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]

Tactic:
have hroot : IsRoot (cyclotomic k (ZMod p)) (castRingHom (ZMod p) b) := by
    have : ((b : ℤ) : ZMod p) = ↑(Int.castRingHom (ZMod p) b) := by simp
    rw [IsRoot.def, ← map_cyclotomic_int k (ZMod p), eval_map, coe_castRingHom,
      ← Int.cast_natCast, this, eval₂_hom, Int.coe_castRingHom, ZMod.intCast_zmod_eq_zero_iff_dvd]
    apply Int.dvd_natAbs.1
    exact mod_cast minFac_dvd (eval (↑b) (cyclotomic k ℤ)).natAbs

Goal state after:
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
Module: Mathlib.NumberTheory.Pell

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

Tactic:
H,

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

Goal state before:
pp: d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
⊢ |d * (a.y * b.y)| < |a.x| * b.x

Tactic:
← abs_of_pos hb,

Goal state after:
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
⊢ |d * (a.y * b.y)| < |a.x| * |b.x|
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
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ d * (a₁.y ^ 2 - a.y ^ 2) ≤ 0

Tactic:
H,

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ a₁.x ^ 2 - a.x ^ 2 ≤ 0
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case f
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
p q : K[X]
x✝ : ¬q = 0
h0 : ¬p = 0 ∧ ¬q = 0
h1 : v ((algebraMap K[X] K⟮X⟯) p) / v ((algebraMap K[X] K⟮X⟯) q) < 1
hor : ¬v ↑p = 1 ∨ ¬v ↑q = 1
⊢ ∀ (r : K[X]), v ↑r ≠ 1 → r ≠ 0 → {p | v ↑p < 1 ∧ ¬p = 0}.Nonempty

Tactic:
exact fun r hr hr0 ↦ ⟨r, lt_iff_le_and_ne.mpr
      ⟨Polynomial.valuation_le_one_of_valuation_X_le_one _ hle r, hr⟩, hr0⟩

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case a.inr
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq' s k = j
⊢ j ∈ {n | 0 < n}

Tactic:
· rw [Set.mem_ofPred_eq, ← hjk, beattySeq', sub_pos, Int.lt_ceil, Int.cast_one]
      exact one_lt_mul_of_le_of_lt (by norm_cast) hrs.symm.lt

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case a
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
hb₁ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq s k = x} ↔ j ∈ {x | ∃ k, beattySeq s k = x}
hb₂ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq' s k = x} ↔ j ∈ {x | ∃ k, beattySeq' s k = x}
⊢ j ∈ {x | ∃ k > 0, beattySeq r k = x} ∆ {x | ∃ k > 0, beattySeq' s k = x}

Tactic:
Set.mem_symmDiff,

Goal state after:
case a
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
hb₁ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq s k = x} ↔ j ∈ {x | ∃ k, beattySeq s k = x}
hb₂ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq' s k = x} ↔ j ∈ {x | ∃ k, beattySeq' s k = x}
⊢ j ∈ {x | ∃ k > 0, beattySeq r k = x} ∧ j ∉ {x | ∃ k > 0, beattySeq' s k = x} ∨
    j ∈ {x | ∃ k > 0, beattySeq' s k = x} ∧ j ∉ {x | ∃ k > 0, beattySeq r k = x}
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

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

Tactic:
· induction f using RatFunc.induction_on with
    | f p q hq0 =>
      have hp0 : p ≠ 0 := by simp_all
      set pi := πᵥ with hpi_def
      have hpi : v.IsUniformizer (pi : RatFunc K) := uniformizingPolynomial_isUniformizer hle
      simp only [map_div₀, valuation_of_algebraMap, intValuation_def, exp_neg, if_neg hp0,
        if_neg hq0, div_inv_eq_mul]
      rw [valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hp0,
        valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hq0]
      simp_all [div_le_one₀, inv_mul_le_one₀,
        (pow_le_pow_iff_right_of_lt_one₀ (by simp_all) (IsRankOneDiscrete.generator_lt_one v))]

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:

Tactic:
mainSum (lambdaSquared w) =
    ∑ d1 ∈ divisors s.prodPrimes, ∑ d2 ∈ divisors s.prodPrimes, (∑ l ∈ divisors s.prodPrimes,
      if l ∣ d1.gcd d2 then (s.selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0)
        := ?caseA
    _ = ∑ l ∈ divisors s.prodPrimes, ∑ d1 ∈ divisors s.prodPrimes, ∑ d2 ∈ divisors s.prodPrimes,
      if l ∣ Nat.gcd d1 d2 then (s.selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0
        := ?caseB
    _ = ∑ l ∈ divisors s.prodPrimes,
      (s.selbergTerms l)⁻¹ * (∑ d ∈ divisors s.prodPrimes, if l ∣ d then s.nu d * w d else 0) ^ 2
        := ?caseC

Goal state after:
case caseA
s : BoundingSieve
w : ℕ → ℝ
⊢ mainSum (lambdaSquared w) =
    ∑ d1 ∈ s.prodPrimes.divisors,
      ∑ d2 ∈ s.prodPrimes.divisors,
        ∑ l ∈ s.prodPrimes.divisors,
          if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0

case caseB
s : BoundingSieve
w : ℕ → ℝ
⊢ (∑ d1 ∈ s.prodPrimes.divisors,
      ∑ d2 ∈ s.prodPrimes.divisors,
        ∑ l ∈ s.prodPrimes.divisors,
          if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0) =
    ∑ l ∈ s.prodPrimes.divisors,
      ∑ d1 ∈ s.prodPrimes.divisors,
        ∑ d2 ∈ s.prodPrimes.divisors,
          if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0

case caseC
s : BoundingSieve
w : ℕ → ℝ
⊢ (∑ l ∈ s.prodPrimes.divisors,
      ∑ d1 ∈ s.prodPrimes.divisors,
        ∑ d2 ∈ s.prodPrimes.divisors,
          if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0) =
    ∑ l ∈ s.prodPrimes.divisors,
      (selbergTerms l)⁻¹ * (∑ d ∈ s.prodPrimes.divisors, if l ∣ d then s.nu d * w d else 0) ^ 2
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: case hbc
n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ 2 ≤ m ^ n !

Tactic:
exact hm.trans <| le_self_pow₀ (one_le_two.trans hm) <| by positivity

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

Goal state before:
pp: 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 : |x - ↑a / ↑b| < 1 / ↑b ^ (r + f.natDegree)
b0 : 0 < ↑b
⊢ ↑b ^ f.natDegree * |x - ↑a / ↑b| < ↑b ^ f.natDegree * |x - ↑a / ↑b|

Tactic:
lt_div_iff₀' (pow_pos b0 _),

Goal state after:
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 + f.natDegree) * |x - ↑a / ↑b| < 1
b0 : 0 < ↑b
⊢ ↑b ^ f.natDegree * |x - ↑a / ↑b| < ↑b ^ f.natDegree * |x - ↑a / ↑b|
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b
⊢ a ∈ Finset.Icc 0 ↑b

Tactic:
sub_div' hb0.ne',

Goal state after:
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : |(x * ↑b - ↑a) / ↑b| < 1 / ↑b
⊢ a ∈ Finset.Icc 0 ↑b
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: ⊢ ∀ᵐ (x : ℝ), ∀ p > 2, ¬LiouvilleWith p x

Tactic:
simpa only [ae_iff, not_forall, Classical.not_not, ofPred_exists] using
    volume_iUnion_setOfPred_liouvilleWith

Goal state after:
Module: Mathlib.Order.Category.CompleteLat

Goal state before:
pp: α β : CompleteLat
e : ↑α ≃o ↑β
a✝ : ↑α
⊢ (ConcreteCategory.hom
        (ConcreteCategory.ofHom { toFun := ⇑e, map_sInf' := ⋯, map_sSup' := ⋯ } ≫
          ConcreteCategory.ofHom { toFun := ⇑e.symm, map_sInf' := ⋯, map_sSup' := ⋯ }))
      a✝ =
    (ConcreteCategory.hom (𝟙 α)) a✝

Tactic:
exact e.symm_apply_apply _

Goal state after:
Module: Mathlib.Order.Category.FinBddDistLat

Goal state before:
pp: α β : FinBddDistLat
e : ↑α.toDistLat ≃o ↑β.toDistLat
a✝ : ↑α.toDistLat
⊢ (Hom.hom
        (ofHom
            (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }) ≫
          ofHom
            (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
            { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })))
      a✝ =
    (Hom.hom (𝟙 α)) a✝

Tactic:
exact e.symm_apply_apply _

Goal state after:
Module: Mathlib.Order.Category.FinBoolAlg

Goal state before:
pp: α β : FinBoolAlg
e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg
a✝ : ↑α.toBoolAlg
⊢ (ConcreteCategory.hom
        (InducedCategory.homMk
            (BoolAlg.ofHom
              (let __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
              { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })) ≫
          InducedCategory.homMk
            (BoolAlg.ofHom
              (let __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
              { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }))))
      a✝ =
    (ConcreteCategory.hom (𝟙 α)) a✝

Tactic:
exact e.symm_apply_apply _

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
⊢ x ⊓ y ∈ carrier

Tactic:
suffices x ⊓ y = sInf {x, y} by exact this ▸ sInfClosed' (fun z hz ↦ by aesop)
    simp [sInf_singleton]

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: case refine_1
α : Type u_2
s : Set α
a : α
inst✝ : CompleteLattice α
h_csc : CountableSupClosed {a | ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨆ n, t n = a}
⊢ s ⊆ {a | ∃ t, (∀ (n : ℕ), t n ∈ s) ∧ ⨆ n, t n = a}

Tactic:
exact fun a ha ↦ ⟨fun _ ↦ a, by simp [ha]⟩

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : Order.Coframe α
hs : SupClosed s
⊢ SupClosed (countableInfClosure s)

Tactic:
by
  rintro a ha b hb
  rw [mem_countableInfClosure_iff_iInf] at ha hb ⊢
  obtain ⟨t, ht, hts, rfl⟩ := ha
  obtain ⟨u, hu, hus, rfl⟩ := hb
  rw [iInf_sup_iInf]
  refine ⟨fun n ↦ t (Nat.unpair n).1 ⊔ u (Nat.unpair n).2, fun n ↦ ?_, ?_⟩
  · simp only
    exact hs (ht (Nat.unpair n).1) (hu (Nat.unpair n).2)
  · rw [iInf_unpair (f := (fun n m ↦ t n ⊔ u m)), iInf_prod']

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

Goal state before:
pp: case mpr
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sg : S ⊆ g
Sct : #↑S < c
hS : ⋂₀ S ⊆ s
⊢ s ∈ cardinalGenerate g ⋯

Tactic:
have : CardinalInterFilter (cardinalGenerate g (IsRegular.nat_lt hreg 2)) c :=
    cardinalInter_ofCardinalGenerate _ _

Goal state after:
case mpr
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sg : S ⊆ g
Sct : #↑S < c
hS : ⋂₀ S ⊆ s
this : CardinalInterFilter (cardinalGenerate g ⋯) c
⊢ s ∈ cardinalGenerate g ⋯
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
this : Nonempty { t // t ⊆ s ∧ IsChain r t }
t : { t // t ⊆ s ∧ IsChain r t }
ht : (↑t).encard = ⨆ i, (↑i).encard
⊢ ∃ t ⊆ s, t.encard = s.chainHeight r ∧ IsChain r t

Tactic:
exact ⟨t.1, t.2.1, ht, t.2.2⟩

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
⊢ (⇑e '' s).chainHeight r' = s.chainHeight r

Tactic:
by
  refine eq_of_forall_natCast_le_iff fun n ↦ ⟨fun hn ↦ ?_, fun hn ↦ ?_⟩
  · obtain ⟨a, ha₁, ha₂, ha₃⟩ := exists_isChain_of_le_chainHeight n hn
    rw [← ha₂, ← Set.encard_preimage_of_injective_subset_range e.injective (by grind)]
    exact encard_le_chainHeight_of_isChain _ _ (preimage_subset ha₁ e.injective.injOn) <|
      ha₃.preimage_relEmbedding e
  · obtain ⟨a, ha₁, ha₂, ha₃⟩ := exists_isChain_of_le_chainHeight n hn
    rw [← ha₂, ← e.injective.encard_image]
    exact encard_le_chainHeight_of_isChain _ _ (by grind) <| ha₃.image e

Goal state after:
Module: Mathlib.Order.Interval.Set.SurjOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
⊢ SurjOn f (Ioc a b) (Ioc (f a) (f b))

Tactic:
by
  simpa using! surjOn_Ico_of_monotone_surjective h_mono.dual h_surj (toDual b) (toDual a)

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 β
r : α → α → Prop
h₁ : Std.Refl r
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✝ : α
h : r x✝ y✝
⊢ r y✝ x✝

Tactic:
by simpa [h₂, inf_comm, sup_comm, ← h₂] using h

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

Goal state before:
pp: α : Type u_1
s : α
inst✝ : CompleteLattice α
P : Partition s
hs : s ≠ ⊥
hP : ↑P = ∅
⊢ False

Tactic:
simp [← P.sSup_eq, hP, sSup_empty] at hs

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

Goal state before:
pp: case refine_1
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a : α
ha : a ∈ u
⊢ P.Rel a (if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯)

Tactic:
split_ifs with h

Goal state after:
case pos
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a : α
ha : a ∈ u
h : ∃ b, P.Rel a ↑b
⊢ P.Rel a (f₀ h.choose)

case neg
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a : α
ha : a ∈ u
h : ¬∃ b, P.Rel a ↑b
⊢ P.Rel a (P.rep ⋯)