mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
h : ¬a = 0
⊢ 1 * a = a

Tactic:
one_mul

Goal state after:
case neg
K : Type u_1
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
h : ¬a = 0
⊢ a = a
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: case neg
p x y : ℕ
hp : Nat.Prime p
h : (p - 1) * ((x - y) / (p - 1)) = x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
hn : IsCoprime (↑p) n
⊢ 1 * n ^ y ≡ n ^ y [ZMOD ↑p]

Tactic:
one_mul

Goal state after:
case neg
p x y : ℕ
hp : Nat.Prime p
h : (p - 1) * ((x - y) / (p - 1)) = x - y
hxy : y ≤ x
hy : 0 < y
n : ℤ
hn : IsCoprime (↑p) n
⊢ n ^ y ≡ n ^ y [ZMOD ↑p]
Module: Mathlib.FieldTheory.Finite.Basic

Goal state before:
pp: F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1

Tactic:
have h₁ := FiniteField.pow_card_sub_one_eq_one a ha

Goal state after:
F : Type u_3
inst✝¹ : Field F
inst✝ : Fintype F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
h₁ : a ^ (Fintype.card F - 1) = 1
⊢ a ^ (Fintype.card F / 2) = 1 ∨ a ^ (Fintype.card F / 2) = -1
Module: Mathlib.RingTheory.Artinian.Ring

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr : ↑s ^ n.succ • r = ↑s ^ n • 1
⊢ ∃ r, IsLocalization.mk' L 1 s = (algebraMap R L) r

Tactic:
use r

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsArtinianRing R
S : Submonoid R
L : Type u_2
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
inst✝ : IsLocalization S L
r₁ : R
s : ↥S
n : ℕ
r : R
hr : ↑s ^ n.succ • r = ↑s ^ n • 1
⊢ IsLocalization.mk' L 1 s = (algebraMap R L) r
Module: Mathlib.GroupTheory.Submonoid.Inverses

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : ↥S
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ 1 * ↑z = ↑z

Tactic:
one_mul

Goal state after:
M : Type u_1
inst✝ : Monoid M
S : Submonoid M
x y : M
z : ↥S
h₁ : y * ↑z = 1
h₂ : x * y = 1
⊢ ↑z = ↑z
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Function.Injective f
hf' : Continuous[inst✝¹, inst✝] f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
⊢ {x} = f ⁻¹' {f x}

Tactic:
rw [← Set.image_singleton, Set.preimage_image_eq _ hf]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: J : Ideal ℤ
⊢ span {↑(absNorm J)} = J

Tactic:
obtain ⟨g, rfl⟩ := IsPrincipalIdealRing.principal J

Goal state after:
g : ℤ
⊢ span {↑(absNorm (ℤ ∙ g))} = ℤ ∙ g
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: J : Ideal ℤ
⊢ Nat.Prime (absNorm J) ↔ Prime J

Tactic:
obtain ⟨g, rfl⟩ := IsPrincipalIdealRing.principal J

Goal state after:
g : ℤ
⊢ Nat.Prime (absNorm (ℤ ∙ g)) ↔ Prime (ℤ ∙ g)
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : ¬length B M ≠ ⊤
this : ¬length A M ≠ ⊤
⊢ length A M = length B M * length (ResidueField A) (ResidueField B)

Tactic:
not_ne_iff

Goal state after:
case neg
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁹ : CommRing A
inst✝⁸ : CommRing B
inst✝⁷ : IsLocalRing A
inst✝⁶ : IsLocalRing B
inst✝⁵ : Algebra A B
inst✝⁴ : IsLocalHom (algebraMap A B)
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : Module B M
inst✝ : IsScalarTower A B M
h : length B M = ⊤
this : length A M = ⊤
⊢ length A M = length B M * length (ResidueField A) (ResidueField B)
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
q : Ideal S
r : Ideal T
inst✝ : r.LiesOver q
⊢ q.inertiaDeg R ∣ r.inertiaDeg R

Tactic:
use r.inertiaDeg S
  rw [← inertiaDeg_tower]

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

Goal state before:
pp: case pos
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hp : map f p ≤ P
H : ∀ (n : ℕ), ∃ k, map f p ≤ P ^ k ∧ n < k
⊢ p.ramificationIdx' P ≠ 1 ↔ map f p ≤ P ^ 2

pp: case neg
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hp : map f p ≤ P
H : ∃ n, ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
⊢ p.ramificationIdx' P ≠ 1 ↔ map f p ≤ P ^ 2

Tactic:
· obtain ⟨k, hk, h2k⟩ := H 2
    simp [Ideal.ramificationIdx'_eq_zero H, hk.trans (Ideal.pow_le_pow_right h2k.le)]

Goal state after:
case neg
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hp : map f p ≤ P
H : ∃ n, ∀ (k : ℕ), map f p ≤ P ^ k → k ≤ n
⊢ p.ramificationIdx' P ≠ 1 ↔ map f p ≤ P ^ 2
Module: Mathlib.RingTheory.LocalRing.Length

Goal state before:
pp: case neg
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
h : ¬length A M ≠ ⊤
this : ¬length B (B ⊗[A] M) ≠ ⊤
⊢ length B (B ⊗[A] M) = length A M * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))

Tactic:
not_ne_iff

Goal state after:
case neg
A : Type u_1
B : Type u_2
M : Type u_3
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : IsLocalRing A
inst✝⁵ : IsLocalRing B
inst✝⁴ : Algebra A B
inst✝³ : IsLocalHom (algebraMap A B)
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Flat A B
h : length A M = ⊤
this : length B (B ⊗[A] M) = ⊤
⊢ length B (B ⊗[A] M) = length A M * length B (B ⧸ Ideal.map (algebraMap A B) (maximalIdeal A))
Module: Mathlib.RingTheory.Ideal.IdempotentFG

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
e : IsIdempotentElem I
⊢ I ≤ I • I

Tactic:
by
          rw [smul_eq_mul]
          exact e.ge

Goal state after:
Module: Mathlib.RingTheory.Ideal.IdempotentFG

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h : I.FG
⊢ (∃ e, IsIdempotentElem e ∧ I = R ∙ e) → IsIdempotentElem I

Tactic:
· rintro ⟨e, he, rfl⟩
    simp [IsIdempotentElem, Ideal.span_singleton_mul_span_singleton, he.eq]

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
inst✝ : QuasiFinite R T
P : Ideal S
hP : P.IsPrime
f : P.ResidueField ⊗[R] T →ₐ[P.ResidueField] P.Fiber T :=
  TensorProduct.lift (ofId P.ResidueField (P.Fiber T)) (AlgHom.restrictScalars R TensorProduct.includeRight) ⋯
⊢ Function.Surjective ⇑f

Tactic:
rw [← AlgHom.coe_restrictScalars' (R := S), ← AlgHom.coe_toLinearMap, ← LinearMap.range_eq_top,
      ← top_le_iff, ← TensorProduct.span_tmul_eq_top, Submodule.span_le]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
inst✝ : QuasiFinite R T
P : Ideal S
hP : P.IsPrime
f : P.ResidueField ⊗[R] T →ₐ[P.ResidueField] P.Fiber T :=
  TensorProduct.lift (ofId P.ResidueField (P.Fiber T)) (AlgHom.restrictScalars R TensorProduct.includeRight) ⋯
⊢ {t | ∃ m n, m ⊗ₜ[S] n = t} ⊆ ↑(AlgHom.restrictScalars S f).toLinearMap.range
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : CommRing T
inst✝² : Algebra R S
inst✝¹ : Algebra R T
inst✝ : QuasiFinite R S
f : S →ₐ[R] T
H : ∀ (x : T), ∃ s, IsUnit (f s) ∧ x * f s ∈ f.range
⊢ ∀ (y : ↥(Submonoid.comap f (IsUnit.submonoid T))), IsUnit (f ↑y)

Tactic:
by simp [IsUnit.mem_submonoid_iff]

Goal state after:
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B ⧸ I
P : Generators R A A := Generators.self R A
hP : Function.Injective ⇑P.toExtension.cotangentComplex
l : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g : A →ₐ[R] P.Ring ⧸ RingHom.ker (IsScalarTower.toAlgHom R P.Ring A).toRingHom ^ 2
hg : (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift.comp g = AlgHom.id R A
σ : B ⧸ I → B := Function.surjInv ⋯
x : P.Ring
⊢ (aeval (⇑(algebraMap B (B ⧸ I)) ∘ σ ∘ ⇑f)) x = f ((algebraMap P.Ring A) x)

Tactic:
P.algebraMap_eq,

Goal state after:
R : Type u
A : Type v
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_1
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
I : Ideal B
hI : I ^ 2 = ⊥
f : A →ₐ[R] B ⧸ I
P : Generators R A A := Generators.self R A
hP : Function.Injective ⇑P.toExtension.cotangentComplex
l : P.toExtension.CotangentSpace →ₗ[A] P.toExtension.Cotangent
hl : l ∘ₗ P.toExtension.cotangentComplex = LinearMap.id
g : A →ₐ[R] P.Ring ⧸ RingHom.ker (IsScalarTower.toAlgHom R P.Ring A).toRingHom ^ 2
hg : (IsScalarTower.toAlgHom R P.Ring A).kerSquareLift.comp g = AlgHom.id R A
σ : B ⧸ I → B := Function.surjInv ⋯
x : P.Ring
⊢ (aeval (⇑(algebraMap B (B ⧸ I)) ∘ σ ∘ ⇑f)) x = f (↑(aeval P.val) x)
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
F : I →₀ I →₀ R := Finsupp.onFinset f.support (fun j ↦ b.repr (x * f j)) ⋯
hG : ∀ j ∉ f.support.biUnion fun i ↦ (a i).support, b.repr (f.sum fun i y ↦ (a i) j • y) = 0
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun i ↦ (a i).support) (fun j ↦ b.repr (f.sum fun i y ↦ (a i) j • y)) ⋯
this : ∀ (i : I), ((b.repr (x * f i)).sum fun j k ↦ k • b j ⊗ₜ[R] b i) = (x * f i) ⊗ₜ[R] b i
⊢ ∑ x_1 ∈ f.support, (x * f x_1) ⊗ₜ[R] b x_1 = ∑ i ∈ f.support, (x * f i) ⊗ₜ[R] (1 * b i)

Tactic:
one_mul

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsArtinianRing R
p : PrimeSpectrum S
inst✝ : FiniteType R S
H✝ : IsClopen {p}
this✝ : IsNoetherianRing S
this : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H : {p} = ↑(PrimeSpectrum.basicOpen e)
hep : e ∉ p.asIdeal
f : Localization.Away e →ₐ[S] Localization.AtPrime p.asIdeal := IsLocalization.Away.liftAlgHom e ⋯
⊢ QuasiFiniteAt R p.asIdeal

Tactic:
have h₁ := (PrimeSpectrum.localization_away_comap_range (Localization.Away e) e).trans H.symm

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsArtinianRing R
p : PrimeSpectrum S
inst✝ : FiniteType R S
H✝ : IsClopen {p}
this✝ : IsNoetherianRing S
this : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H : {p} = ↑(PrimeSpectrum.basicOpen e)
hep : e ∉ p.asIdeal
f : Localization.Away e →ₐ[S] Localization.AtPrime p.asIdeal := IsLocalization.Away.liftAlgHom e ⋯
h₁ : Set.range (PrimeSpectrum.comap (algebraMap S (Localization.Away e))) = {p}
⊢ QuasiFiniteAt R p.asIdeal
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: R : Type u_4
inst✝² : CommRing R
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Function.Surjective ⇑(algebraMap R A)
⊢ FormallySmooth R A ↔ IsIdempotentElem (RingHom.ker (algebraMap R A))

Tactic:
by
  rw [Algebra.FormallySmooth.iff_split_surjection (Algebra.ofId R A) h]
  constructor
  · intro ⟨g, hg⟩
    let e : A ≃ₐ[R] R ⧸ RingHom.ker (algebraMap R A) ^ 2 :=
      .ofAlgHom _ _ (Ideal.Quotient.algHom_ext _ (by ext)) hg
    rw [IsIdempotentElem, ← pow_two, ← Ideal.mk_ker (I := _ ^ 2), ← Ideal.Quotient.algebraMap_eq,
      ← e.toAlgHom.comp_algebraMap, RingHom.ker_comp_of_injective _ (by exact e.injective)]
  · intro H
    let e := (Ideal.quotientEquivAlgOfEq _ ((pow_two _).trans H)).trans
      (Ideal.quotientKerAlgEquivOfSurjective (f := Algebra.ofId R A) h)
    exact ⟨e.symm.toAlgHom, AlgHom.ext <| h.forall.mpr fun x ↦ by simp⟩

Goal state after:
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: case e_f
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
hA : IsNilpotent (IsLocalRing.maximalIdeal A)
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A := ⋯
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A := ⋯
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := ⋯
⊢ ∀ (x : A) (y : A ⧸ IsLocalRing.maximalIdeal A),
    (↑K ((ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ e'.toLinearMap)) (x ⊗ₜ[K] y) =
      (↑K
          (TensorProduct.AlgebraTensorModule.lift
            (↑K (lsmul A A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap.flip).flip))
        (x ⊗ₜ[K] y)

Tactic:
intro r s

Goal state after:
case e_f
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
hA : IsNilpotent (IsLocalRing.maximalIdeal A)
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A :=
  let __spread.0 := ofId K (A ⧸ IsLocalRing.maximalIdeal A);
  let __spread.1 := Equiv.ofBijective ⇑(algebraMap K (A ⧸ IsLocalRing.maximalIdeal A)) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  (TensorProduct.congr AlgEquiv.refl e.symm).trans (TensorProduct.rid K A A)
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := e'.toLinearMap ∘ₗ sec K A (A ⧸ IsLocalRing.maximalIdeal A)
r : A
s : A ⧸ IsLocalRing.maximalIdeal A
⊢ (↑K ((ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ e'.toLinearMap)) (r ⊗ₜ[K] s) =
    (↑K
        (TensorProduct.AlgebraTensorModule.lift
          (↑K (lsmul A A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap.flip).flip))
      (r ⊗ₜ[K] s)
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝⁴ : FiniteType K A
this✝³ : Module.Finite K (Localization.AtPrime Q)
this✝² : IsField (Localization.AtPrime Q)
this✝¹ : Field (Localization.AtPrime Q) := this✝².toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
this✝ : (algebraMap A (Localization.AtPrime Q)) ((aeval x) q) = 0
m : K[X]
hm : (aeval x) m ∈ Q.primeCompl
hm' : p ∣ m * q
H : q * q ∣ p
this : (algebraMap A Q.ResidueField) ((aeval x) m) = 0
⊢ False

Tactic:
Q.algebraMap_residueField_eq_zero

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this✝⁴ : FiniteType K A
this✝³ : Module.Finite K (Localization.AtPrime Q)
this✝² : IsField (Localization.AtPrime Q)
this✝¹ : Field (Localization.AtPrime Q) := this✝².toField
q : K[X] := minpoly K ((algebraMap A Q.ResidueField) x)
this✝ : (algebraMap A (Localization.AtPrime Q)) ((aeval x) q) = 0
m : K[X]
hm : (aeval x) m ∈ Q.primeCompl
hm' : p ∣ m * q
H : q * q ∣ p
this : (aeval x) m ∈ Q
⊢ False
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hq : q.IsPrime
hpS : map (algebraMap R S) p ≠ ⊥
hq' : q ≠ ⊥
this : q.IsMaximal
I : Ideal S
hqI : q ⊔ I = ⊤
h :
  map (algebraMap R S) p =
    q ^ Multiset.count q (UniqueFactorizationMonoid.normalizedFactors (map (algebraMap R S) p)) * I
⊢ p.ramificationIdx' q = q.ramificationIdx R

Tactic:
replace hqI : ¬ I ≤ q := by
    contrapose! hqI
    rw [sup_of_le_left hqI]
    exact hq.ne_top

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hq : q.IsPrime
hpS : map (algebraMap R S) p ≠ ⊥
hq' : q ≠ ⊥
this : q.IsMaximal
I : Ideal S
h :
  map (algebraMap R S) p =
    q ^ Multiset.count q (UniqueFactorizationMonoid.normalizedFactors (map (algebraMap R S) p)) * I
hqI : ¬I ≤ q
⊢ p.ramificationIdx' q = q.ramificationIdx R
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
hne : s.Nonempty
hbdd : BddAbove s
⊢ ∃ x, IsLUB s x

Tactic:
by
  rcases hne, hbdd with ⟨⟨L, hL⟩, ⟨U, hU⟩⟩
  have : ∀ d : ℕ, BddAbove { m : ℤ | ∃ y ∈ s, (m : ℝ) ≤ y * d } := by
    obtain ⟨k, hk⟩ := exists_int_gt U
    refine fun d => ⟨k * d, fun z h => ?_⟩
    rcases h with ⟨y, yS, hy⟩
    refine Int.cast_le.1 (hy.trans ?_)
    push_cast
    gcongr
    exact (hU yS).trans hk.le
  choose f hf using fun d : ℕ =>
    Int.exists_greatest_of_bdd (this d) ⟨⌊L * d⌋, L, hL, Int.floor_le _⟩
  have hf₁ : ∀ n > 0, ∃ y ∈ s, ((f n / n : ℚ) : ℝ) ≤ y := fun n n0 =>
    let ⟨y, yS, hy⟩ := (hf n).1
    ⟨y, yS, by simpa using (div_le_iff₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _)).2 hy⟩
  have hf₂ : ∀ n > 0, ∀ y ∈ s, (y - ((n : ℕ) : ℝ)⁻¹) < (f n / n : ℚ) := by
    intro n n0 y yS
    have := (Int.sub_one_lt_floor _).trans_le (Int.cast_le.2 <| (hf n).2 _ ⟨y, yS, Int.floor_le _⟩)
    simp only [Rat.cast_div, Rat.cast_intCast, Rat.cast_natCast, gt_iff_lt]
    rwa [lt_div_iff₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _), sub_mul, inv_mul_cancel₀]
    exact (Nat.cast_pos.2 n0).ne'
  have hg : IsCauSeq abs (fun n => f n / n : ℕ → ℚ) := by
    intro ε ε0
    suffices ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, (f j / j - f k / k : ℚ) < ε by
      refine ⟨_, fun j ij => abs_lt.2 ⟨?_, this _ ij _ le_rfl⟩⟩
      rw [neg_lt, neg_sub]
      exact this _ le_rfl _ ij
    intro j ij k ik
    replace ij := le_trans (Nat.le_ceil _) (Nat.cast_le.2 ij)
    replace ik := le_trans (Nat.le_ceil _) (Nat.cast_le.2 ik)
    have j0 := Nat.cast_pos.1 ((inv_pos.2 ε0).trans_le ij)
    have k0 := Nat.cast_pos.1 ((inv_pos.2 ε0).trans_le ik)
    rcases hf₁ _ j0 with ⟨y, yS, hy⟩
    refine lt_of_lt_of_le ((Rat.cast_lt (K := ℝ)).1 ?_) ((inv_le_comm₀ ε0 (Nat.cast_pos.2 k0)).1 ik)
    simpa using sub_lt_iff_lt_add'.2 (lt_of_le_of_lt hy <| sub_lt_iff_lt_add.1 <| hf₂ _ k0 _ yS)
  let g : CauSeq ℚ abs := ⟨fun n => f n / n, hg⟩
  refine ⟨mk g, ⟨fun x xS => ?_, fun y h => ?_⟩⟩
  · refine le_of_forall_lt_imp_le_of_dense fun z xz => ?_
    obtain ⟨K, hK⟩ := exists_nat_gt (x - z)⁻¹
    refine le_mk_of_forall_le ⟨K, fun n nK => ?_⟩
    replace xz := sub_pos.2 xz
    replace hK := hK.le.trans (Nat.cast_le.2 nK)
    have n0 : 0 < n := Nat.cast_pos.1 ((inv_pos.2 xz).trans_le hK)
    refine le_trans ?_ (hf₂ _ n0 _ xS).le
    rwa [le_sub_comm, inv_le_comm₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _) xz]
  · exact
      mk_le_of_forall_le
        ⟨1, fun n n1 =>
          let ⟨x, xS, hx⟩ := hf₁ _ n1
          le_trans hx (h xS)⟩

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case pos
s : Set ℝ≥0
hs : s.Nonempty
H : BddAbove s
⊢ ↑(sSup s) = sSup (toReal '' s)

Tactic:
have A : sSup (Subtype.val '' s) ∈ Set.Ici 0 := by
      apply Real.sSup_nonneg
      rintro - ⟨y, -, rfl⟩
      exact y.2
    exact (@subset_sSup_of_within ℝ (Set.Ici (0 : ℝ)) _ _ (_) s hs H A).symm

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case inl
ι : Sort u_1
h✝ : IsEmpty ι
⊢ ⨅ x, 0 = 0

Tactic:
exact Real.iInf_of_isEmpty _

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case neg
s : Set ℝ≥0
hs : s.Nonempty
H : ¬BddAbove s
⊢ ↑(sSup s) = sSup (toReal '' s)

Tactic:
simp only [csSup_of_not_bddAbove H, csSup_empty, bot_eq_zero', NNReal.coe_zero]
    apply (Real.sSup_of_not_bddAbove ?_).symm
    contrapose H
    exact bddAbove_coe.1 H

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: a b : ℝ≥0
h : a < b
⊢ a < 1 * b

Tactic:
one_mul

Goal state after:
a b : ℝ≥0
h : a < b
⊢ a < b
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℝ≥0
hx : x ≠ 0
⊢ 1 < 1 * x ↔ 1 < x

Tactic:
one_mul

Goal state after:
x : ℝ≥0
hx : x ≠ 0
⊢ 1 < x ↔ 1 < x
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < ↑q
⊢ 1 ≤ ↑q * ↑q.den - 1 * ↑q.den

Tactic:
one_mul

Goal state after:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : 1 < ↑q
⊢ 1 ≤ ↑q * ↑q.den - ↑q.den
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: r : ℝ≥0
n : ℕ
hn : r < ↑n
⊢ ∃ n, ↑r < ↑n

Tactic:
exact ⟨n, coe_lt_natCast.2 hn⟩

Goal state after:
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a b : ℝ≥0∞
ha : ¬a = ∞
hb : b = ∞
⊢ (a + b).toReal ≤ a.toReal + b.toReal

Tactic:
by simp only [hb, add_top, toReal_top, add_zero, toReal_nonneg]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : Group E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
⊢ (if x * y = 1 then 0 else 1) ≤ (if x = 1 then 0 else 1) + if y = 1 then 0 else 1

Tactic:
by
        by_cases hx : x = 1
        · rw [if_pos hx, hx, one_mul, zero_add]
        · rw [if_neg hx]
          refine le_add_of_le_of_nonneg ?_ ?_ <;> split_ifs <;> norm_num

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑J₁ * ↑(Ideal.span {a}) = ↑J * ↑(Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)

Tactic:
← coeIdeal_mul,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑J * ↑(Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ count K v I =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors)
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
⊢ a ∈ (closure[inst✝¹] t)ᶜ

Tactic:
exact disjoint_left.1 hd ha

Goal state after: