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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x✝ : mixedSpace K
⊢ (∃ x,
      (x ∈ {x | (toMixed K) x ∈ fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} ∧
          ∃ y ∈ ↑↑((FractionalIdeal.mk0 K) J), (mixedEmbedding K) y = ↑↑(toMixed K) x) ∧
        (↑(toMixed K)).toEquiv x = x✝) ↔
    (x✝ ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x✝) ∧ mixedEmbedding.norm x✝ ≤ s

Tactic:
FractionalIdeal.coe_mk0

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
x✝ : mixedSpace K
⊢ (∃ x,
      (x ∈ {x | (toMixed K) x ∈ fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} ∧
          ∃ y ∈ ↑↑↑J, (mixedEmbedding K) y = ↑↑(toMixed K) x) ∧
        (↑(toMixed K)).toEquiv x = x✝) ↔
    (x✝ ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x✝) ∧ mixedEmbedding.norm x✝ ≤ s
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case calc_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ |↑((Algebra.norm ℚ) α)| = ‖(algebraMap ℚ ℂ) ((Algebra.norm ℚ) α)‖

Tactic:
eq_ratCast,

Goal state after:
case calc_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ |↑((Algebra.norm ℚ) α)| = ‖↑((Algebra.norm ℚ) α)‖
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
⊢ (∀ (n : ℕ), f ↑n = g ↑n) ↔ f = g

Tactic:
refine ⟨fun h ↦ ?_, fun h n ↦ congrFun (congrArg DFunLike.coe h) ↑n⟩

Goal state after:
f g : AbsoluteValue ℚ ℝ
h : ∀ (n : ℕ), f ↑n = g ↑n
⊢ f = g
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case convert_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
x✝² : euclidean.mixedSpace K
x✝¹ : ℝ
x✝ : x✝² ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K
h : 0 < x✝¹
⊢ x✝¹ • x✝² ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K

Tactic:
Set.mem_preimage,

Goal state after:
case convert_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
x✝² : euclidean.mixedSpace K
x✝¹ : ℝ
x✝ : x✝² ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K
h : 0 < x✝¹
⊢ (toMixed K) (x✝¹ • x✝²) ∈ fundamentalCone K
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case h.inr
α : 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
hsign : A i j ≤ 0
⊢ v j * A i j ≤ ↑B * (A i j)⁺

Tactic:
posPart_eq_zero.2 hsign

Goal state after:
case h.inr
α : 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
hsign : A i j ≤ 0
⊢ v j * A i j ≤ ↑B * 0
Module: Mathlib.NumberTheory.Padics.Complex

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℂ_[p]
⊢ ‖x‖ = Valued.v.norm x

Tactic:
congr!
  exact norm_eq_norm' p

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (fun s ↦ ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
⊢ ∃ t, ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
by
    rcases eq_or_ne f 0 with rfl | hf
    · -- silly case : f = 0
      simp
    have : 0 < ‖f‖ / p ^ s := div_pos (norm_pos_iff.mpr hf) (mod_cast pow_pos hp.out.pos _)
    obtain ⟨δ, hδpos, hδf⟩ := f.uniform_continuity _ this
    obtain ⟨t, ht⟩ := PadicInt.exists_pow_neg_lt p hδpos
    exact ⟨t, fun x y hxy ↦  by simpa only [dist_eq_norm_sub] using (hδf (hxy.trans_lt ht)).le⟩

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : WithVal (Rat.padicValuation p)
⊢ withValUniformEquiv ↑x = ↑((WithVal.equiv (Rat.padicValuation p)) x)

Tactic:
simpa [Equiv.toUniformEquivOfIsUniformInducing] using!
    extension_coe (Padic.isUniformInducing_cast_withVal (p := p)).uniformContinuous _

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Algebra R ℚ
inst✝¹ : IsFractionRing R ℚ
inst✝ : IsIntegralClosure R ℤ ℚ
p : Nat.Primes
⊢ ℚ_[↑p] ≃A[ℚ] HeightOneSpectrum.adicCompletion ℚ (primesEquiv.symm p)

Tactic:
by
  apply (ContinuousAlgEquiv.cast (primesEquiv.apply_symm_apply p).symm).trans
    (adicCompletion.padicEquiv (primesEquiv.symm p)).symm

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 (contractSnd ν).toFun

Tactic:
refine continuous_of_continuous_uncurry _ (ν.continuous.comp ?_)
    apply continuous_of_continuous_uncurry
    rw [← (Homeomorph.prodAssoc C(X × Y, R) X Y).symm.comp_continuous_iff']
    exact ContinuousEval.continuous_eval

Goal state after:
Module: Mathlib.NumberTheory.PrimesCongruentOne

Goal state before:
pp: 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)
⊢ (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)

Tactic:
have : ((b : ℤ) : ZMod p) = ↑(Int.castRingHom (ZMod p) b) := by simp

Goal state after:
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)
this : ↑↑b = (Int.castRingHom (ZMod p)) ↑b
⊢ (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
⊢ p • ⊤ = p • M.mkQ.range

Tactic:
M.range_mkQ

Goal state after:
R : Type u
inst✝¹⁶ : CommRing R
S : Type v
inst✝¹⁵ : CommRing S
inst✝¹⁴ : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹³ : Field K
inst✝¹² : Algebra R K
L : Type u_2
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra S L
inst✝⁹ : IsFractionRing S L
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
⊢ p • ⊤ = p • ⊤
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
hb : a ∈ {b, b⁻¹, -b, -b⁻¹}
n : ℕ
hn : b = a₁ ^ n
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

Tactic:
rcases hb with (rfl | rfl | rfl | hb)

Goal state after:
case inl
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
n : ℕ
hbx : 0 < a.x
hby : 0 ≤ a.y
hn : a = a₁ ^ n
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

case inr.inl
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
⊢ ∃ n, b⁻¹ = a₁ ^ n ∨ b⁻¹ = -a₁ ^ n

case inr.inr.inl
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
⊢ ∃ n, -b = a₁ ^ n ∨ -b = -a₁ ^ n

case inr.inr.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
hb : a ∈ {-b⁻¹}
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inl
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : a₁ ^ (n₂ * n₁ + -1) = 1 ∨ -a₁ ^ (n₂ * n₁ + -1) = 1
⊢ a₁ ^ n₂ = a₁

Tactic:
← sub_eq_add_neg

Goal state after:
case inl
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : a₁ ^ (n₂ * n₁ - 1) = 1 ∨ -a₁ ^ (n₂ * n₁ - 1) = 1
⊢ a₁ ^ n₂ = a₁
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s
h₃ : ↑j < ↑k + ↑m
h₄ : ↑k + ↑m < ↑j + 1
⊢ False

Tactic:
rw [← Int.cast_one] at h₄

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s
h₃ : ↑j < ↑k + ↑m
h₄ : ↑k + ↑m < ↑j + ↑1
⊢ False
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⟯ Γ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
a b : K[X]
hab : v ↑(a * b) < 1 ∧ a ≠ 0 ∧ b ≠ 0
hb : ¬IsUnit b
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
hπᵥ : πᵥ = a * b
hbpos : 0 < b.degree
⊢ a.degree < a.degree + b.degree

Tactic:
degree_eq_natDegree hab.2.1,

Goal state after:
K : Type u_1
Γ : Type u_2
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
a b : K[X]
hab : v ↑(a * b) < 1 ∧ a ≠ 0 ∧ b ≠ 0
hb : ¬IsUnit b
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
hπᵥ : πᵥ = a * b
hbpos : 0 < b.degree
⊢ ↑a.natDegree < ↑a.natDegree + b.degree
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ 2 * 2 * m = (x - y) ^ 2 + (x + y) ^ 2

Tactic:
rw [mul_assoc, h]; ring

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

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

Tactic:
simp_rw [← sum_filter, mul_sum]
      congr! 1 with l hl
      simp only [mem_filter, mem_divisors, ne_eq] at hl
      rw [selbergTerms_isMultiplicative.map_div_of_coprime hl.2]
      · ring
      · apply coprime_of_squarefree_mul <|
          (Nat.div_mul_cancel hl.2).symm ▸ (squarefree_of_dvd_prodPrimes hd)
      · exact (selbergTerms_pos hl.1.1).ne'

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: p : ℕ
hp : Prime p
this : Fact (Prime p)
a b c d : ℤ
k : ℕ
⊢ a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k

Tactic:
← @Nat.cast_inj ℤ

Goal state after:
p : ℕ
hp : Prime p
this : Fact (Prime p)
a b c d : ℤ
k : ℕ
⊢ ↑(a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2) = ↑k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case refine_1.convert_1
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
this : LinearIndependent (R ⧸ p) (⇑(↑R (Submodule.mkQ (map f p))) ∘ b')
⊢ RingHom.ker (algebraMap R (R ⧸ p)) ≠ ⊤

pp: case refine_1.convert_2
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
this : LinearIndependent (R ⧸ p) (⇑(↑R (Submodule.mkQ (map f p))) ∘ b')
⊢ Function.Injective ⇑(↑R (Algebra.linearMap S L))

Tactic:
· rw [Quotient.algebraMap_eq, Ideal.mk_ker]
      exact hp.ne_top

Goal state after:
case refine_1.convert_2
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
this : LinearIndependent (R ⧸ p) (⇑(↑R (Submodule.mkQ (map f p))) ∘ b')
⊢ Function.Injective ⇑(↑R (Algebra.linearMap S L))
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case h
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hfp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S
⊢ p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' x + Quotient.mk'' y) =
    p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' x) +
      p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' y)

Tactic:
| _ x y
     => 

Goal state after:
case h
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hfp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S
⊢ p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' x + Quotient.mk'' y) =
    p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' x) +
      p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' y)
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case h
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hfp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R
y : S
⊢ p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' x • Quotient.mk'' y) =
    (RingHom.id (R ⧸ p)) (Quotient.mk'' x) • p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' y)

Tactic:
| _ x y
     => 

Goal state after:
case h
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hfp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R
y : S
⊢ p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' x • Quotient.mk'' y) =
    (RingHom.id (R ⧸ p)) (Quotient.mk'' x) • p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' y)
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
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop := fun i ↦ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ e)) = (e - e) • Module.rank (R ⧸ p) (S ⧸ P)

Tactic:
Nat.sub_self,

Goal state after:
case refine_2
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop := fun i ↦ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ e)) = 0 • Module.rank (R ⧸ p) (S ⧸ P)
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
⊢ liouvilleNumber ↑m ≠ ↑p / ↑m ^ n ! ∧ |liouvilleNumber ↑m - ↑p / ↑m ^ n !| < 1 / (↑m ^ n !) ^ n

Tactic:
← partialSum_add_remainder m1 n,

Goal state after:
m : ℕ
hm : 2 ≤ m
mZ1 : 1 < ↑m
m1 : 1 < ↑m
n p : ℕ
hp : partialSum (↑m) n = ↑p / ↑m ^ n !
⊢ partialSum (↑m) n + remainder (↑m) n ≠ ↑p / ↑m ^ n ! ∧
    |partialSum (↑m) n + remainder (↑m) n - ↑p / ↑m ^ n !| < 1 / (↑m ^ n !) ^ n
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p q x : ℝ
h : LiouvilleWith p x
hlt✝ : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
n : ℕ
hnC : C < ↑n ^ (p - q)
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hn : 0 < ↑n
⊢ C < ↑n ^ (p + -q)

Tactic:
← sub_eq_add_neg

Goal state after:
p q x : ℝ
h : LiouvilleWith p x
hlt✝ : q < p
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
this : ∀ᶠ (n : ℕ) in atTop, C < ↑n ^ (p - q)
n : ℕ
hnC : C < ↑n ^ (p - q)
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
hn : 0 < ↑n
⊢ C < ↑n ^ (p - q)
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b ↦ ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), volume (B a b) = ↑(2 / ↑b ^ r)
b : ℕ
⊢ ↑((↑b + 1) * (2 / ↑b ^ r)) = ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))

Tactic:
by
        have : 1 - r ≠ 0 := by linarith
        rw [ENNReal.coe_inj]
        simp [add_mul, div_eq_mul_inv, NNReal.rpow_neg, NNReal.rpow_sub' this, mul_add,
          mul_left_comm]

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

Goal state before:
pp: p : ℝ
hp : 1 < p
m : ℤ
h : LiouvilleWith p ↑m
⊢ False

Tactic:
rename' m => M

Goal state after:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
⊢ False
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)
⊢ ∃ a b, 1 < b ∧ x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n

Tactic:
exact ⟨a, b, mod_cast hb, hne, by simpa [rpow_neg] using hlt⟩

Goal state after:
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: case refine_1.inr.inr
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' ↦ s x' y' ∨ s x' x ∧ s y y'
a b c : α
ax : s a x
yb : s y b
bx : s b x
yc : s y c
⊢ s' a c

Tactic:
exact Or.inr ⟨ax, yc⟩

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

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

Tactic:
obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero (Fin.ne_zero_of_lt hj)
    grind [insertNth_apply_same, insertNth_apply_above, hf j.castSucc_le_succ]

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 (y ⊔ z) (x ⊔ y ⊔ z)

Tactic:
by
        simpa [sup_comm y x, sup_sup_distrib_left y x z, sup_assoc] using
          ((h₄ inf_le_sup (h₂.mp hxy)).2 : r (x ⊓ y ⊔ (y ⊔ z)) (x ⊔ y ⊔ (y ⊔ z)))

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

Goal state before:
pp: case mk.mk
α : Type u_1
s✝ t x y z : α
S : Set α
inst✝ : CompleteLattice α
P Q : Partition s✝
s : α
parts✝¹ : Set α
sSupIndep'✝¹ : sSupIndep parts✝¹
bot_notMem'✝¹ : ⊥ ∉ parts✝¹
sSup_eq'✝¹ : sSup parts✝¹ = s
parts✝ : Set α
sSupIndep'✝ : sSupIndep parts✝
bot_notMem'✝ : ⊥ ∉ parts✝
sSup_eq'✝ : sSup parts✝ = s
h :
  { parts := parts✝¹, sSupIndep' := sSupIndep'✝¹, bot_notMem' := bot_notMem'✝¹, sSup_eq' := sSup_eq'✝¹ }.parts =
    { parts := parts✝, sSupIndep' := sSupIndep'✝, bot_notMem' := bot_notMem'✝, sSup_eq' := sSup_eq'✝ }.parts
⊢ { parts := parts✝¹, sSupIndep' := sSupIndep'✝¹, bot_notMem' := bot_notMem'✝¹, sSup_eq' := sSup_eq'✝¹ } =
    { parts := parts✝, sSupIndep' := sSupIndep'✝, bot_notMem' := bot_notMem'✝, sSup_eq' := sSup_eq'✝ }

Tactic:
simpa using h

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
P : Partition ⊥
x : α
⊢ x ∉ P

Tactic:
rintro hxP

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
P : Partition ⊥
x : α
hxP : x ∈ P
⊢ False
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
s✝ t✝¹ x y z : α
S✝ : Set α
S : Set (Set α)
u s t✝ : Set α
a b c : α
P✝ Q P : Partition u
x✝⁴ x✝³ x✝² : α
x✝¹ : P.Rel x✝⁴ x✝³
x✝ : P.Rel x✝³ x✝²
t : Set α
ht : t ∈ P
ha : x✝⁴ ∈ t
hb : x✝³ ∈ t
t' : Set α
ht' : t' ∈ P
hb' : x✝³ ∈ t'
hc : x✝² ∈ t'
⊢ x✝² ∈ t

Tactic:
eq_of_mem_of_mem ht ht' hb hb'

Goal state after:
α : Type u_1
s✝ t✝¹ x y z : α
S✝ : Set α
S : Set (Set α)
u s t✝ : Set α
a b c : α
P✝ Q P : Partition u
x✝⁴ x✝³ x✝² : α
x✝¹ : P.Rel x✝⁴ x✝³
x✝ : P.Rel x✝³ x✝²
t : Set α
ht : t ∈ P
ha : x✝⁴ ∈ t
hb : x✝³ ∈ t
t' : Set α
ht' : t' ∈ P
hb' : x✝³ ∈ t'
hc : x✝² ∈ t'
⊢ x✝² ∈ t'