mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map id (inclusion R A hS))
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] f

Tactic:
simp_rw [continuous_iff_continuousAt, ContinuousAt]

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map id (inclusion R A hS))
⊢ ∀ (x : Y × Πʳ (i : ι), [R i, A i]), Tendsto f (𝓝 x) (𝓝 (f x))
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ x + y ≠ 0

pp: x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ x ^ n - y ^ n ≠ 0

Tactic:
· lia

Goal state after:
x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ x ^ n - y ^ n ≠ 0
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
n : Type u_3
inst✝² : Finite n
X : Type u_4
inst✝¹ : TopologicalSpace X
A : n → ι → Type u_5
inst✝ : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst✝ j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst✝¹] (f ∘ Pi.map fun x ↦ inclusion (A x) (C x) hS)
⊢ Continuous[Pi.topologicalSpace, inst✝¹] f

Tactic:
simp_rw [continuous_iff_continuousAt, ContinuousAt]

Goal state after:
ι : Type u_1
n : Type u_3
inst✝² : Finite n
X : Type u_4
inst✝¹ : TopologicalSpace X
A : n → ι → Type u_5
inst✝ : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst✝ j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst✝¹] (f ∘ Pi.map fun x ↦ inclusion (A x) (C x) hS)
⊢ ∀ (x : (j : n) → Πʳ (i : ι), [A j i, C j i]), Tendsto f (𝓝 x) (𝓝 (f x))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : mixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in (mixedEmbedding.polarCoord K).target,
      (∏ w, (x.2 w).1) • f (↑(mixedEmbedding.polarCoord K).symm x) =
    ∫ (x : mixedSpace K), f x

Tactic:
by
  rw [← (volume_preserving_mixedSpaceToRealMixedSpace_symm K).integral_comp
    (mixedSpaceToRealMixedSpace K).symm.measurableEmbedding, ← integral_comp_polarCoordReal_symm,
    polarCoord_target_eq_polarCoordReal_target, polarCoord_symm_eq, Function.comp_def]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
h₁ :
  (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite
      (↥(unitLattice K) ⧸ span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u)))
⊢ span ℤ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i))) ≤ unitLattice K

Tactic:
Submodule.span_le

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
h₁ :
  (Subgroup.closure (Set.range u) ⊔ torsion K).index ≠ 0 ↔
    Finite
      (↥(unitLattice K) ⧸ span ℤ (Set.range (⇑(logEmbeddingEquiv K) ∘ ⇑Additive.toMul.symm ∘ QuotientGroup.mk ∘ u)))
⊢ (Set.range fun i ↦ (logEmbedding K) (Additive.ofMul (u i))) ⊆ ↑(unitLattice K)
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : K
φ : K →+* ℂ := Classical.choice ⋯
⊢ (complexConj K) ((complexConj K) x) = x

Tactic:
exact isConj_apply_apply (isConj_complexConj K φ) x

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x : 𝓞 K
hx : mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) x)) ≠ 0
hu : u • (mixedEmbedding K) ((algebraMap (𝓞 K) K) x) ∈ fundamentalCone K
⊢ (mixedEmbedding K) ↑(↑u * x) = u • (mixedEmbedding K) ((algebraMap (𝓞 K) K) x)

Tactic:
simp_rw [unitSMul_smul, ← map_mul]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
⊢ ↑((unitsComplexConj K) u) = ↑u ↔ u ∈ realUnits K

Tactic:
mem_realUnits_iff,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
⊢ ↑((unitsComplexConj K) u) = ↑u ↔ ∃ v, (algebraMap (𝓞 ↥K⁺) (𝓞 K)) ↑v = ↑u
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
ζ : ↥(torsion K)
⊢ (unitsComplexConj K) ↑ζ = ↑ζ⁻¹

Tactic:
apply coe_injective

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
ζ : ↥(torsion K)
⊢ (fun x ↦ (algebraMap (𝓞 K) K) ↑x) ((unitsComplexConj K) ↑ζ) = (fun x ↦ (algebraMap (𝓞 K) K) ↑x) ↑ζ⁻¹
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
x✝ y✝ : (𝓞 K)ˣ
⊢ x✝ * y✝ * ((unitsComplexConj K) (x✝ * y✝))⁻¹ = x✝ * ((unitsComplexConj K) x✝)⁻¹ * (y✝ * ((unitsComplexConj K) y✝)⁻¹)

Tactic:
apply coe_injective

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
x✝ y✝ : (𝓞 K)ˣ
⊢ (fun x ↦ (algebraMap (𝓞 K) K) ↑x) (x✝ * y✝ * ((unitsComplexConj K) (x✝ * y✝))⁻¹) =
    (fun x ↦ (algebraMap (𝓞 K) K) ↑x) (x✝ * ((unitsComplexConj K) x✝)⁻¹ * (y✝ * ((unitsComplexConj K) y✝)⁻¹))
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ exponent θ ↔ ¬comap (algebraMap ℤ (𝓞 K)) (conductor ℤ θ) ≤ span {↑p}

pp: K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsCoatom (span {↑p})

Tactic:
← under_def,

Goal state after:
K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ¬p ∣ exponent θ ↔ ¬under ℤ (conductor ℤ θ) ≤ span {↑p}

K : Type u_1
inst✝¹ : Field K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsCoatom (span {↑p})
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁷ : Field F
inst✝⁶ : IsTotallyReal F
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
this✝ : IsTotallyReal ↥(algebraMap F K).fieldRange
this : IsQuadraticExtension (↥(algebraMap F K).fieldRange) K
⊢ (algebraMap F K).fieldRange = maximalRealSubfield K

Tactic:
exact eq_maximalRealSubfield K (algebraMap F K).fieldRange

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
⊢ regOfFamily u / regOfFamily v =
    ↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K))

Tactic:
by
  classical
  by_cases hu : IsMaxRank u
  · have : span ℤ (Set.range (basisOfIsMaxRank hu)) ≤ span ℤ (Set.range (basisOfIsMaxRank hv)) := by
      rw [← toAddSubgroup_le, span_basisOfIsMaxRank hu, span_basisOfIsMaxRank hv,
        ← map_logEmbedding_sup_torsion (Subgroup.closure (Set.range u)).toAddSubgroup,
        ← map_logEmbedding_sup_torsion (Subgroup.closure (Set.range v)).toAddSubgroup,
        ← SupHomClass.map_sup, ← SupHomClass.map_sup]
      exact AddSubgroup.map_mono <| (OrderIso.le_iff_le Subgroup.toAddSubgroup).mpr h
    rw [regOfFamily_of_isMaxRank hu, regOfFamily_of_isMaxRank hv,
      covolume_div_covolume_eq_relIndex _ _ this, span_basisOfIsMaxRank hu,
      span_basisOfIsMaxRank hv, AddSubgroup.relIndex_map_map, logEmbedding_ker,
      ← OrderIso.map_sup, ← OrderIso.map_sup, ← Subgroup.relIndex_toAddSubgroup]
  · rw [regOfFamily_eq_zero hu, zero_div, eq_comm, Nat.cast_eq_zero]
    have : (Subgroup.closure (Set.range v) ⊔ torsion K).index ≠ 0 := by
      rw [← Subgroup.finiteIndex_iff, ← finiteIndex_iff_sup_torsion_finiteIndex]
      exact isMaxRank_iff_closure_finiteIndex.mp hv
    rwa [← mul_eq_zero_iff_right this, Subgroup.relIndex_mul_index h,
      ← Subgroup.not_finiteIndex_iff, ← finiteIndex_iff_sup_torsion_finiteIndex,
      ← isMaxRank_iff_closure_finiteIndex.not]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ Associated ((hζ.toInteger - 1) ^ (p - 1)) ↑p

Tactic:
rw [← eval_one_cyclotomic_prime (R := 𝓞 K) (p := p),
    cyclotomic_eq_prod_X_sub_primitiveRoots hζ.toInteger_isPrimitiveRoot, eval_prod]
  simp only [eval_sub, eval_X, eval_C]
  rw [← Nat.totient_prime hp.out, ← hζ.toInteger_isPrimitiveRoot.card_primitiveRoots,
    ← Finset.prod_const]
  refine Associated.prod _ _ _ fun η hη ↦ ?_
  have hη' : IsPrimitiveRoot (η : K) p :=
    (isPrimitiveRoot_of_mem_primitiveRoots hη).map_of_injective RingOfIntegers.coe_injective
  simpa using (associated_sub_one_of_isPrimitiveRoot p hζ hη').neg_right

Goal state after:
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
⊢ (𝒑.primesOver (𝓞 K)).ncard = 1

Tactic:
by
  rw [← pow_one p] at hK
  exact ncard_primesOver_of_prime_pow p 0 K

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : 𝓞 K
hα0 : α ≠ 0
⊢ ∃ w, 1 ≤ w ↑α

Tactic:
by_contra! h_neg

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : 𝓞 K
hα0 : α ≠ 0
h_neg : ∀ (w : InfinitePlace K), w ↑α < 1
⊢ False
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ∑ j, ‖(basisMatrix K)ᵀ⁻¹ i j‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖ ≤
    ∑ j, ‖(basisMatrix K)ᵀ⁻¹‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖

Tactic:
gcongr
      exact norm_entry_le_entrywise_sup_norm ((basisMatrix K).transpose)⁻¹

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case refine_1
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hp : Nat.Prime p
this : Fact (Nat.Prime p)
t : ℝ
ht : 0 < t
hpt : f ↑p = ↑p ^ (-t)
n : ℕ
⊢ f ↑n ^ t⁻¹ = (padic p) ↑n

pp: case refine_2
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hp : Nat.Prime p
this : Fact (Nat.Prime p)
t : ℝ
ht : 0 < t
hpt : f ↑p = ↑p ^ (-t)
q : ℕ
x✝ : (fun p ↦ ∃ (h : Fact (Nat.Prime p)), ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic p) ↑n) q
hq : Fact (Nat.Prime q)
heq : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic q) ↑n
⊢ q = p

Tactic:
· rcases eq_or_ne n 0 with rfl | hn
    · simp [ht.ne']
    · rcases Nat.exists_eq_pow_mul_and_not_dvd hn p hp.ne_one with ⟨_, m, hpm, rfl⟩
      have := (padicNorm.nat_eq_one_iff m).mpr hpm
      simp_all [← rpow_natCast, ← rpow_mul, mul_comm t, mul_inv_cancel_right₀ ht.ne',
        eq_one_of_not_dvd bdd hp0 hp1 hmin hpm]

Goal state after:
case refine_2
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hp : Nat.Prime p
this : Fact (Nat.Prime p)
t : ℝ
ht : 0 < t
hpt : f ↑p = ↑p ^ (-t)
q : ℕ
x✝ : (fun p ↦ ∃ (h : Fact (Nat.Prime p)), ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic p) ↑n) q
hq : Fact (Nat.Prime q)
heq : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic q) ↑n
⊢ q = p
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
⊢ t ≤ s

Tactic:
← rpow_le_rpow_left_iff (x := n) (mod_cast hn),

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
⊢ ↑n ^ t ≤ ↑n ^ s
Module: Mathlib.NumberTheory.Padics.AddChar

Goal state before:
pp: p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
R : Type u_1
inst✝⁴ : NormedRing R
inst✝³ : Algebra ℤ_[p] R
inst✝² : IsBoundedSMul ℤ_[p] R
inst✝¹ : IsUltrametricDist R
inst✝ : CompleteSpace R
r : R
hr : Tendsto (fun x ↦ r ^ x) atTop (𝓝 0)
⊢ Nat.choose 0 0 • r ^ 0 = 1

Tactic:
Nat.choose_self,

Goal state after:
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
R : Type u_1
inst✝⁴ : NormedRing R
inst✝³ : Algebra ℤ_[p] R
inst✝² : IsBoundedSMul ℤ_[p] R
inst✝¹ : IsUltrametricDist R
inst✝ : CompleteSpace R
r : R
hr : Tendsto (fun x ↦ r ^ x) atTop (𝓝 0)
⊢ 1 • r ^ 0 = 1
Module: Mathlib.NumberTheory.Padics.AddChar

Goal state before:
pp: p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
R : Type u_1
inst✝⁴ : NormedRing R
inst✝³ : Algebra ℤ_[p] R
inst✝² : IsBoundedSMul ℤ_[p] R
inst✝¹ : IsUltrametricDist R
inst✝ : CompleteSpace R
r : R
hr : Tendsto (fun x ↦ r ^ x) atTop (𝓝 0)
⊢ 1 • r ^ 0 + Nat.choose 1 1 • r ^ 1 = 1 + r

Tactic:
Nat.choose_self,

Goal state after:
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
R : Type u_1
inst✝⁴ : NormedRing R
inst✝³ : Algebra ℤ_[p] R
inst✝² : IsBoundedSMul ℤ_[p] R
inst✝¹ : IsUltrametricDist R
inst✝ : CompleteSpace R
r : R
hr : Tendsto (fun x ↦ r ^ x) atTop (𝓝 0)
⊢ 1 • r ^ 0 + 1 • r ^ 1 = 1 + r
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
⊢ Δ_[1]^[n + R] f 0 = R.choose R • Δ_[1]^[n + R] f 0

Tactic:
Nat.choose_self,

Goal state after:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
⊢ Δ_[1]^[n + R] f 0 = 1 • Δ_[1]^[n + R] f 0
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
h : (if x' - y' = 0 then 0 else (↑p ^ padicValRat p (x' - y'))⁻¹) ≤ (↑p ^ (embedding ↑γ * exp (-1)).log.natAbs)⁻¹
H : ¬x' - y' = 0
⊢ exp (-padicValRat p (x' - y')) < embedding ↑γ

Tactic:
rw [← lt_log_iff_exp_lt (embedding_unit_ne_zero _)]
        simp_all [← zpow_natCast, zpow_pos, inv_le_inv₀, zpow_le_zpow_iff_right₀ hp1', abs_le,
          Int.lt_iff_add_one_le]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 ≤ a.x - 1

Tactic:
by rw [sub_nonneg]; exact h.1.le

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑j ≤ (↑⌈(↑j + 1) / r⌉ - 1) * r
⊢ ↑j ≤ (↑⌈(↑j + 1) / r⌉ - 1) * r ∧ ↑⌈(↑j + 1) / r⌉ - 1 < (↑j + 1) / r

Tactic:
sub_lt_iff_lt_add

Goal state after:
case inr
r : ℝ
j : ℤ
h : r > 0
h✝ : ↑j ≤ (↑⌈(↑j + 1) / r⌉ - 1) * r
⊢ ↑j ≤ (↑⌈(↑j + 1) / r⌉ - 1) * r ∧ ↑⌈(↑j + 1) / r⌉ < (↑j + 1) / r + 1
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: p : ℕ
inst✝ : Fact (Prime p)
hp : p % 4 ≠ 3
⊢ ∃ a b, a ^ 2 + b ^ 2 = p

Tactic:
apply sq_add_sq_of_nat_prime_of_not_irreducible p

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

Goal state before:
pp: f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
⊢ ∃ c' ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (f p) s‖ ≤ c' ^ p

Tactic:
clear c hc

Goal state after:
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
⊢ ∃ c' ≥ 0, ∀ (p : ℕ), p ≠ 0 → ‖P (f p) s‖ ≤ c' ^ p
Module: Mathlib.Topology.Instances.Irrational

Goal state before:
pp: x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m ↦ (↑n)⁻¹ * ↑m)
B : x ∉ range fun m ↦ (↑n)⁻¹ * ↑m
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑n)

Tactic:
rcases Metric.mem_nhds_iff.1 (A.isOpen_compl.mem_nhds B) with ⟨ε, ε0, hε⟩

Goal state after:
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m ↦ (↑n)⁻¹ * ↑m)
B : x ∉ range fun m ↦ (↑n)⁻¹ * ↑m
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun m ↦ (↑n)⁻¹ * ↑m)ᶜ
⊢ ∀ᶠ (ε : ℝ) in 𝓝 0, ∀ (m : ℤ), ε ≤ dist x (↑m / ↑n)
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case neg
R : Type u
inst✝¹⁷ : CommRing R
S : Type v
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
hp0 : ¬p = ⊥
hP : P ∈ IsDedekindDomain.primesOverFinset p S
⊢ 0 < p.inertiaDeg' P

Tactic:
exact Nat.pos_iff_ne_zero.mpr <| inertiaDeg'_ne_zero p P

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

Goal state before:
pp: case refine_2
R : Type u
inst✝¹⁷ : CommRing R
S : Type v
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
P : Ideal S
hP : P ∈ IsDedekindDomain.primesOverFinset p S
this✝ : P.IsPrime
this : P.LiesOver p
⊢ 1 ≤ p.inertiaDeg' P

Tactic:
exact Nat.pos_iff_ne_zero.mpr <| inertiaDeg'_ne_zero p P

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

Goal state before:
pp: p x : ℝ
n : ℕ
hn : n ≠ 0
⊢ LiouvilleWith p (↑n * x) ↔ LiouvilleWith p x

Tactic:
rw [mul_comm, mul_nat_iff hn]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
⊢ (fun y ↦ y ^ m) '' approxOrderOf A n δ ⊆ approxOrderOf A n (↑m * δ)

Tactic:
rintro - ⟨a, ha, rfl⟩

Goal state after:
A : Type u_1
inst✝ : SeminormedCommGroup A
m n : ℕ
δ : ℝ
hm : 0 < m
hmn : n.Coprime m
a : A
ha : a ∈ approxOrderOf A n δ
⊢ (fun y ↦ y ^ m) a ∈ approxOrderOf A n (↑m * δ)
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
⊢ (fun y ↦ y ^ m) '' approxOrderOf A (n * m) δ ⊆ approxOrderOf A n (↑m * δ)

Tactic:
rintro - ⟨a, ha, rfl⟩

Goal state after:
A : Type u_1
inst✝ : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A (n * m) δ
⊢ (fun y ↦ y ^ m) a ∈ approxOrderOf A n (↑m * δ)
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case mp
δ : ℝ
x : UnitAddCircle
n : ℕ
hn : 0 < n
m : ℕ
hm₁ : m < n
hm₂ : m.gcd n = 1
hx : ‖x - ↑(↑m / ↑n)‖ < δ
⊢ ∃ m < n, gcd m n = 1 ∧ ‖x - ↑(↑m / ↑n)‖ < δ

Tactic:
exact ⟨m, hm₁, hm₂, hx⟩

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
x✝ : α
⊢ (∀ b ∈ A.right, x✝ ≤ b) ↔ x✝ ∈ A.left

Tactic:
← lowerBounds_right,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
x✝ : α
⊢ (∀ b ∈ A.right, x✝ ≤ b) ↔ x✝ ∈ lowerBounds A.right
Module: Mathlib.Order.Concept

Goal state before:
pp: case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s✝ : Set α
t : Set β
a : α
b : β
r' : α → α → Prop
c d : Concept α β r
c' : Concept α α r'
s : Set (Concept α β r)
x✝ : Concept α β r
hc : x✝ ∈ s
⊢ x✝ ≤ sSup s

Tactic:
exact intent_subset_intent_iff.1 <| biInter_subset_of_mem hc

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Rank

Goal state before:
pp: case inr
α : Type u
a✝ : α
r : α → α → Prop
o : Ordinal.{u}
ha✝ : Acc r a✝
ho✝ : o ≤ ha✝.rank
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a), o < ⋯.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o
ho : o < ⋯.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o

Tactic:
rw [rank_eq, Ordinal.lt_iSup_iff] at ho

Goal state after:
case inr
α : Type u
a✝ : α
r : α → α → Prop
o : Ordinal.{u}
ha✝ : Acc r a✝
ho✝ : o ≤ ha✝.rank
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a), o < ⋯.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o
ho : ∃ i, o < Order.succ ⋯.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s t : Set α
ht : ∀ (t' : Set α), s ⊆ t' → CountableSupClosed t' → t ⊆ t'
ht_ne : t.Nonempty
ht_c : t.Countable
x : α
hx : IsLUB t x
t' : Set α
hst' : s ⊆ t'
⊢ CountableSupClosed t' → x ∈ t'

Tactic:
ht'

Goal state after:
α : Type u_2
inst✝ : Preorder α
s t : Set α
ht : ∀ (t' : Set α), s ⊆ t' → CountableSupClosed t' → t ⊆ t'
ht_ne : t.Nonempty
ht_c : t.Countable
x : α
hx : IsLUB t x
t' : Set α
hst' : s ⊆ t'
ht' : CountableSupClosed t'
⊢ x ∈ t'
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : SemilatticeInf X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
⊢ (⇑m ⊓ ⇑n) (x ⊓ y) = (⇑m ⊓ ⇑n) x ⊓ (⇑m ⊓ ⇑n) y

Tactic:
by simp [inf_inf_inf_comm]

Goal state after:
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
J J' : Set α
h : J' ∈ R.leftFixedPoints
h₁ : J ⊆ J'
⊢ R.rightDual (R.leftDual J) ⊆ J'

Tactic:
rw [← h]
  apply R.gc_leftDual_rightDual.monotone_u
  apply R.gc_leftDual_rightDual.monotone_l
  exact h₁

Goal state after:
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
⊢ ⨅ x ∈ X, f x b ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y

Tactic:
apply iInf₂_mono

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

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

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

Tactic:
· exact congrArg _ h.1

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