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

Goal state before:
pp: case pos
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
hu : IsMaxRank u
this : span ℤ (Set.range ⇑(basisOfIsMaxRank hu)) ≤ span ℤ (Set.range ⇑(basisOfIsMaxRank hv))
⊢ ZLattice.covolume (span ℤ (Set.range ⇑(basisOfIsMaxRank hu))) volume /
      ZLattice.covolume (span ℤ (Set.range ⇑(basisOfIsMaxRank hv))) volume =
    ↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K))

Tactic:
covolume_div_covolume_eq_relIndex _ _ this,

Goal state after:
case pos
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
hu : IsMaxRank u
this : span ℤ (Set.range ⇑(basisOfIsMaxRank hu)) ≤ span ℤ (Set.range ⇑(basisOfIsMaxRank hv))
⊢ ↑((span ℤ (Set.range ⇑(basisOfIsMaxRank hu))).toAddSubgroup.relIndex
        (span ℤ (Set.range ⇑(basisOfIsMaxRank hv))).toAddSubgroup) =
    ↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h₁ : MeasurableSet (normAtAllPlaces ⁻¹' compactSet K)
h₂ : MeasurableSet (normAtAllPlaces ⁻¹' ↑expMapBasis '' interior (paramSet K))
⊢ volume (normAtAllPlaces ⁻¹' compactSet K) = volume (normAtAllPlaces ⁻¹' ↑expMapBasis '' interior (paramSet K))

Tactic:
rw [volume_eq_two_pow_mul_two_pi_pow_mul_integral Set.preimage_image_preimage h₁,
    normAtAllPlaces_image_preimage_of_nonneg (fun x a w ↦ nonneg_of_mem_compactSet K a w),
    volume_eq_two_pow_mul_two_pi_pow_mul_integral Set.preimage_image_preimage h₂,
    normAtAllPlaces_image_preimage_expMapBasis, setLIntegral_congr (compactSet_ae K),
    setLIntegral_expMapBasis_image measurableSet_closure (by fun_prop),
    setLIntegral_expMapBasis_image measurableSet_interior (by fun_prop),
    setLIntegral_congr (closure_paramSet_ae_interior K)]

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 (ZMod.unitOfCoprime p hn✝) ≤ Nat.card ↑(⇑↑(galEquivZMod n K) '' ↑(stabilizer Gal(K/ℚ) P))

Tactic:
change _ ≤ Nat.card ((galEquivZMod n K).toEquiv '' _)

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 (ZMod.unitOfCoprime p hn✝) ≤ Nat.card ↑(⇑(galEquivZMod n K).toEquiv '' ↑(stabilizer Gal(K/ℚ) P))
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, Nat.Prime p ∧ ¬Algebra.IsUnramifiedIn 𝒪 (Ideal.span {↑p})

Tactic:
have : 0 < Module.finrank ℚ K := Module.finrank_pos
  have : 2 < |discr K| := abs_discr_gt_two (by lia)
  obtain ⟨p, hp1, hp2⟩ := (discr K).exists_prime_and_dvd (by linarith)
  use p.natAbs, p.prime_iff_natAbs_prime.mp hp1
  simpa [← not_dvd_discr_iff_isUnramifiedIn K 𝒪 hp1]

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

Goal state before:
pp: case calc_4
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
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) ≤
    c K * A * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2))

Tactic:
rw [mul_assoc, mul_assoc]

Goal state after:
case calc_4
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
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * (house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2))) ≤
    c K * (A * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)))
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case inr.inr
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
h_ineq2 : ∀ (k : ℕ), 0 < k → f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹
h₁ : n ≠ 1
⊢ f ↑n ≤ 1

Tactic:
refine le_of_tendsto_of_tendsto tendsto_const_nhds ?_ (eventually_atTop.mpr ⟨1, h_ineq2⟩)

Goal state after:
case inr.inr
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
h_ineq2 : ∀ (k : ℕ), 0 < k → f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹
h₁ : n ≠ 1
⊢ Tendsto (fun b ↦ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑b)⁻¹ * ↑b ^ (↑b)⁻¹) atTop (𝓝 1)
Module: Mathlib.NumberTheory.Padics.MahlerBasis

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

Tactic:
simp only [Ring.choose]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
⊢ Continuous fun x ↦ Ring.multichoose (x - ↑k + 1) k
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsUniformInducing ⇑((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom)

Tactic:
have hp0' : 0 < (p : ℚ) := by simp [Nat.Prime.pos Fact.out]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
⊢ IsUniformInducing ⇑((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom)
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0

Tactic:
obtain ⟨m, hm⟩ : ∃ m : ℤ, {q : ℚ | q.1 ^ 2 - d * (q.den : ℤ) ^ 2 = m}.Infinite := by
    contrapose! hM
    refine (congr_arg _ (ext fun x => ?_)).mp (Finite.biUnion (finite_Ioo (-M) M) fun m _ => hM m)
    simp only [abs_lt, mem_ofPred, mem_Ioo, mem_iUnion, exists_prop, exists_eq_right']

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
⊢ ¬‖(Polynomial.aeval z) (Polynomial.derivative F)‖ = 0

Tactic:
by rw [hz.1]; apply deriv_norm_ne_zero; assumption

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inl
d : ℤ
a : Solution₁ d
h : IsFundamental a
hn : 0 ≤ 0
⊢ 0 ≤ (a ^ 0).y

pp: case inr
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn✝ : 0 ≤ n
hn : 0 < n
⊢ 0 ≤ (a ^ n).y

Tactic:
· simp only [zpow_zero, y_one, le_refl]

Goal state after:
case inr
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn✝ : 0 ≤ n
hn : 0 < n
⊢ 0 ≤ (a ^ n).y
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
z1 : ℤ_[p] := ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
z' : ℤ_[p] := z - z1
hdist :
  ‖(Polynomial.aeval z') (Polynomial.derivative F) - (Polynomial.aeval z) (Polynomial.derivative F)‖ <
    ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
⊢ ‖(Polynomial.aeval z') (Polynomial.derivative F)‖ = ‖(Polynomial.aeval a) (Polynomial.derivative F)‖

Tactic:
sub_eq_add_neg,

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
n : ℕ
z : ℤ_[p]
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
z1 : ℤ_[p] := ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
z' : ℤ_[p] := z - z1
hdist :
  ‖(Polynomial.aeval z') (Polynomial.derivative F) + -(Polynomial.aeval z) (Polynomial.derivative F)‖ <
    ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
⊢ ‖(Polynomial.aeval z') (Polynomial.derivative F)‖ = ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
f : K⟮X⟯
inst✝ : IsTrivialOn K v
hlt : 1 < v X
hf : f ≠ 0
⊢ v f = v X ^ f.intDegree

Tactic:
by
  induction f using RatFunc.induction_on with
  | f p q hq =>
    rw [intDegree_div (by grind only) (by grind only), v.map_div, zpow_sub₀ (ne_zero_of_lt hlt)]
    simp_rw [intDegree_polynomial, zpow_natCast, ← coePolynomial_eq_algebraMap]
    have hp : p ≠ 0 := by contrapose hf; simp [hf]
    rw [valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X _ hlt hp,
      valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X _ hlt hq]

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

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
γL : (ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)))ˣ
a✝ : True
e : ℕ := v.asIdeal.ramificationIdx' w.asIdeal
σL : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ :=
  WithVal.valueGroupOrderIso₀ (valuation L w)
σw : (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ) :=
  valueGroup₀_equiv_withZeroMulInt (valuation L w)
σwV : ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)) ≃*o
  (MonoidWithZeroHom.ofClass (WithVal.valuation (valuation L w))).ValueGroup₀ :=
  ValuativeRel.ValueGroupWithZero.orderMonoidIso (WithVal.valuation (valuation L w))
m : WithZero (Multiplicative ℤ) := σw (σL (σwV ↑γL))
σvV : ValuativeRel.ValueGroupWithZero (WithVal (valuation K v)) ≃*o
  (MonoidWithZeroHom.ofClass (WithVal.valuation (valuation K v))).ValueGroup₀ :=
  ValuativeRel.ValueGroupWithZero.orderMonoidIso (WithVal.valuation (valuation K v))
σv : (MonoidWithZeroHom.ofClass (valuation K v)).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ) :=
  valueGroup₀_equiv_withZeroMulInt (valuation K v)
σK : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass (valuation K v)).ValueGroup₀ :=
  WithVal.valueGroupOrderIso₀ (valuation K v)
γK : ValuativeRel.ValueGroupWithZero (WithVal (valuation K v)) := σvV.symm (σK.symm (σv.symm (exp (m.log / ↑e))))
hγK : γK ≠ 0
x : WithVal (valuation K v)
hx : ((valuation K v) x.ofVal).log < (exp (m.log / ↑e)).log
hx₀ : x ≠ 0
⊢ σw (σL (σwV ↑γL)) ≠ 0

Tactic:
simp [EmbeddingLike.map_eq_zero_iff (f := σwV)]

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
l : ℕ
hl : Squarefree l
hnu_nonzero : s.nu l ≠ 0
⊢ (selbergTerms l)⁻¹ =
    ∑ x ∈ l.divisorsAntidiagonal,
      match x with
      | (d, e) => ↑(μ d) * (s.nu e)⁻¹

Tactic:
simp only [selbergTerms_apply, mul_inv, inv_inv,
    Finset.prod_inv_distrib, s.nu_mult.prodPrimeFactors_one_sub_of_squarefree _ hl, mul_sum]

Goal state after:
s : BoundingSieve
l : ℕ
hl : Squarefree l
hnu_nonzero : s.nu l ≠ 0
⊢ ∑ i ∈ l.divisors, (s.nu l)⁻¹ * (↑(μ i) * s.nu i) = ∑ x ∈ l.divisorsAntidiagonal, ↑(μ x.1) * (s.nu x.2)⁻¹
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x : ℤ[i]
⊢ toComplex x = 0 ↔ x = 0

Tactic:
by
  rw [← toComplex_zero, toComplex_inj]

Goal state after:
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
p : ℕ
⊢ ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * |c| ^ p * ‖s‖)

Tactic:
rw [P_eq_integral_exp_mul_eval (f p) s, mul_comm s, norm_mul, norm_mul, norm_exp]

Goal state after:
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ Real.exp s.re * (‖∫ (x : ℝ) in 0..1, cexp (-(x • s)) * eval (x • s) (f p)‖ * ‖s‖) ≤
    Real.exp s.re * (Real.exp ‖s‖ * |c| ^ p * ‖s‖)
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case calc_1
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
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
e : Ideal S → ℕ := p.ramificationIdx'
⊢ ∑ x ∈ (factors (map f p)).toFinset.attach, e ↑x * p.inertiaDeg' ↑x =
    ∑ P ∈ (factors (map f p)).toFinset.attach, finrank (R ⧸ p) (S ⧸ ↑P ^ e ↑P)

Tactic:
refine Finset.sum_congr rfl fun P _ => ?_

Goal state after:
case calc_1
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
p : Ideal R
inst✝ : p.IsMaximal
hp0 : p ≠ ⊥
e : Ideal S → ℕ := p.ramificationIdx'
P : ↥(factors (map f p)).toFinset
x✝ : P ∈ (factors (map f p)).toFinset.attach
⊢ e ↑P * p.inertiaDeg' ↑P = finrank (R ⧸ p) (S ⧸ ↑P ^ e ↑P)
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∏ x, ↑x = ∏ x ∈ Ico 1 (p - 1).succ, ↑x

Tactic:
refine prod_bij (fun a _ => (a : ZMod p).val) ?_ ?_ ?_ ?_

Goal state after:
case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ a ∈ univ, (↑a).val ∈ Ico 1 (p - 1).succ

case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ a₁ ∈ univ, ∀ a₂ ∈ univ, (↑a₁).val = (↑a₂).val → a₁ = a₂

case refine_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ b ∈ Ico 1 (p - 1).succ, ∃ a, ∃ (_ : a ∈ univ), (↑a).val = b

case refine_4
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ a ∈ univ, ↑a = ↑(↑a).val
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
⊢ Bounded (fun x1 x2 ↦ x1 < x2) (Iic a)

Tactic:
simp only [← bounded_le_iff_bounded_lt, bounded_le_Iic]

Goal state after:
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : NoMinOrder α
a : α
⊢ Bounded (fun x1 x2 ↦ x1 > x2) (Ici a)

Tactic:
by
  simp only [← bounded_ge_iff_bounded_gt, bounded_ge_Ici]

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

Goal state before:
pp: p x : ℝ
r : ℚ
⊢ LiouvilleWith p (x - ↑r) ↔ LiouvilleWith p x

Tactic:
sub_eq_add_neg,

Goal state after:
p x : ℝ
r : ℚ
⊢ LiouvilleWith p (x + -↑r) ↔ LiouvilleWith p x
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: x : ℝ
H : ∀ (p : ℝ), LiouvilleWith p x
n b : ℕ
hb : 1 < b
a : ℤ
hne : x ≠ ↑a / ↑b
hlt : |x - ↑a / ↑b| < ↑b ^ (-↑n)
⊢ |x - ↑a / ↑↑b| < 1 / ↑↑b ^ n

Tactic:
simpa [rpow_neg] using hlt

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
x : β
⊢ ∀ b ∈ upperBounds (⇑f '' (principal x).left), f x ≤ b

Tactic:
refine fun y hy ↦ hy ?_

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
x : β
y : α
hy : y ∈ upperBounds (⇑f '' (principal x).left)
⊢ f x ∈ ⇑f '' (principal x).left
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : DedekindCut α
⊢ a < b ↔ ∃ c, a ≤ principal c ∧ principal c < b

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨c, hca, hcb⟩ ↦ lt_of_le_of_lt hca hcb⟩
  rw [← intent_ssubset_intent_iff, Set.ssubset_iff_exists] at h
  simpa [← not_le, le_principal_iff] using h.2

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

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

pp: case inr.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
b : α
hb : r b a
ho✝ : o ≤ ⋯.rank
ho : o < ⋯.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o

Tactic:
exacts [⟨b, ha b hb, rfl⟩, IH _ hb ho]

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

Goal state before:
pp: ι α β : Type u
c : Cardinal.{u}
l : Filter α
inst✝² : CardinalInterFilter l c
l₁ l₂ : Filter α
c₁ c₂ : Cardinal.{u}
inst✝¹ : CardinalInterFilter l₁ c₁
inst✝ : CardinalInterFilter l₂ c₂
⊢ CardinalInterFilter (l₁ ⊓ l₂) (min c₁ c₂)

Tactic:
have : CardinalInterFilter l₁ (c₁ ⊓ c₂) :=
    CardinalInterFilter.of_cardinalInterFilter_of_le l₁ inf_le_left
  have : CardinalInterFilter l₂ (c₁ ⊓ c₂) :=
    CardinalInterFilter.of_cardinalInterFilter_of_le l₂ inf_le_right
  exact cardinalInterFilter_inf_eq _ _

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
h : ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s
⊢ s ∈ cardinalGenerate g ⋯

Tactic:
rcases h with ⟨S, Sg, Sct, hS⟩

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
⊢ s ∈ cardinalGenerate g ⋯
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
j : Fin n
hj : j.castSucc < i.castSucc
⊢ i.castSucc.succ.insertNth x f j.castSucc.castSucc < i.castSucc.succ.insertNth x f j.castSucc.succ

Tactic:
grind [insertNth_apply_below, castPred_castSucc]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℤ
⊢ ↑n ∈ Set.Ioi a ↔ n ∈ Set.Ioi ⌊a⌋

Tactic:
by simp [floor_lt]

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 : α
hab : a ≤ b
⊢ SurjOn f (Icc a b) (Icc (f a) (f b))

Tactic:
intro p hp
  rcases eq_endpoints_or_mem_Ioo_of_mem_Icc hp with (rfl | rfl | hp')
  · exact ⟨a, left_mem_Icc.mpr hab, rfl⟩
  · exact ⟨b, right_mem_Icc.mpr hab, rfl⟩
  · exact image_mono Ioo_subset_Icc_self <|
      surjOn_Ioo_of_monotone_surjective h_mono h_surj a b hp'

Goal state after:
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: case refine_3
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
⊢ (∃ x, MonotoneOn f s ∧ MonotoneOn g s) → MonovaryOn f g s

Tactic:
rintro ⟨_, hf, hg⟩
    exact hf.monovaryOn hg

Goal state after:
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ r (x ⊓ y ⊓ z) (y ⊓ z)

Tactic:
suffices r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z)) by
        rw [inf_comm x, inf_assoc]
        simpa [inf_comm x, ← inf_inf_distrib_left] using this

Goal state after:
α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z))
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
x y z : α
hxy : r x y
hyz : r y z
⊢ r (x ⊓ y ⊓ (y ⊓ z)) ((x ⊔ y) ⊓ (y ⊓ z))

Tactic:
exact (h₄ inf_le_sup (h₂.mp hxy)).1

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: case refine_3
X : Type u_1
inst✝ : CompleteLattice X
s : Set (Nucleus X)
x y : X
f : Nucleus X
hf : f ∈ s
⊢ (⨅ f ∈ s, f x) ⊓ ⨅ f ∈ s, f y ≤ f x ∧ (⨅ f ∈ s, f x) ⊓ ⨅ f ∈ s, f y ≤ f y

Tactic:
exact ⟨inf_le_of_left_le <| iInf₂_le f hf, inf_le_of_right_le <| iInf₂_le f hf⟩

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
hy : y ≥ x
⊢ m (m y ⇨ n y) ⇨ n (m y ⇨ n y) = m y ⇨ n y

Tactic:
rw [map_himp_apply, himp_himp, ← map_inf, inf_of_le_right (le_trans n.le_apply le_himp)]

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m : Nucleus X
x y : X
n : Nucleus X
⊢ rangeFactorization ⇑n ⊤ = ⊤

Tactic:
by ext; exact map_top n

Goal state after:
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := {J | IsIdeal J ∧ ↑I ⊆ J ∧ Disjoint (↑F) J}
IinS : ↑I ∈ S
chainub : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := Jidl.toIdeal
⊢ ∃ J, J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J

Tactic:
use J

Goal state after:
case h
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := ⋯
IinS : ↑I ∈ S
chainub : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
JF : Disjoint (↑F) Jset
J : Ideal α := ⋯
⊢ J.IsPrime ∧ I ≤ J ∧ Disjoint ↑F ↑J