mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

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
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
hp_bot : map f p ≠ ⊥
hvp : ¬v = p
⊢ emultiplicity w (map f p) = ↑(v.ramificationIdx' w) * emultiplicity v p

Tactic:
emultiplicity_eq_zero_of_irreducible_ne hv hp.irreducible hvp,

Goal state after:
case neg
R : Type u
inst✝⁶ : CommRing R
S : Type v
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsDedekindDomain S
inst✝² : IsDedekindDomain R
inst✝¹ : FaithfulSMul R S
v : Ideal R
w : Ideal S
p : Ideal R
hv : Irreducible v
hp : Prime p
hw : Irreducible w
hw_bot : w ≠ ⊥
inst✝ : w.LiesOver v
hp_bot : map f p ≠ ⊥
hvp : ¬v = p
⊢ emultiplicity w (map f p) = ↑(v.ramificationIdx' w) * 0
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✝ : EssFiniteType R S
this : ∀ (t : S ⊗[R] S), (TensorProduct.lmul' R) t = 1 ↔ 1 - t ∈ KaehlerDifferential.ideal R S
e : S ⊗[R] S
he₁ : IsIdempotentElem e
he₂ : Ideal.span (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Ideal.span {e}
s : S
⊢ e ∣ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1

Tactic:
by
        rw [← Ideal.mem_span_singleton, ← he₂]
        exact Ideal.subset_span ⟨s, rfl⟩

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
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
inst✝ : QuasiFiniteAt R Q
f : Localization.AtPrime Q →ₐ[R] Localization.AtPrime P := IsLocalization.liftAlgHom ⋯
x s : S
hs : s ∈ P.primeCompl
⊢ IsUnit (f ((algebraMap S (Localization.AtPrime Q)) s))

Tactic:
by simpa [f] using IsLocalization.map_units _ ⟨s, hs⟩

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

Goal state before:
pp: case mp
R : Type u
A : Type v
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
P : Extension R A
inst✝ : FormallySmooth R P.Ring
e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent := ⋯
⊢ (∃ l, l ∘ₗ kerCotangentToTensor R P.Ring A = LinearMap.id) → ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id

Tactic:
intro ⟨l, hl⟩
    exact ⟨(e.comp l).extendScalarsOfSurjective P.algebraMap_surjective,
      LinearMap.ext (DFunLike.congr_fun hl : _)⟩

Goal state after:
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h2
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
⊢ Extension.Cotangent.mk z ∈ Submodule.span T ↑(Extension.Cotangent.map (Q.toComp P).toExtensionHom).range

Tactic:
← Submodule.restrictScalars_mem (Q.comp P).Ring,

Goal state after:
case h2
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
⊢ Extension.Cotangent.mk z ∈
    Submodule.restrictScalars (Q.comp P).Ring
      (Submodule.span T ↑(Extension.Cotangent.map (Q.toComp P).toExtensionHom).range)
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case hF
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
i : σ
⊢ (D R T) ((algebraMap S T) (P.val i)) =
    (Q.comp P).toExtension.toKaehler
      ((Extension.CotangentSpace.map (Q.toComp P).toExtensionHom) (1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)))

Tactic:
conv_rhs => enter [2]; tactic => exact Extension.CotangentSpace.map_tmul ..

Goal state after:
case hF
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
i : σ
⊢ (D R T) ((algebraMap S T) (P.val i)) =
    (Q.comp P).toExtension.toKaehler
      ((algebraMap S T) 1 ⊗ₜ[(Q.comp P).toExtension.Ring]
        (D R (Q.comp P).toExtension.Ring) ((Q.toComp P).toExtensionHom.toAlgHom (X i)))
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case refine_1
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
P' : Type u_2 := P ⧸ RingHom.ker (algebraMap P S) ^ 2
h₁ : Surjective ⇑(algebraMap P' S)
h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥
e₁ : (RingHom.ker (algebraMap P S)).Cotangent ≃ₗ[P] ↥(RingHom.ker (algebraMap P' S)) :=
  (RingHom.ker (algebraMap P S)).cotangentEquivIdeal ≪≫ₗ
    LinearEquiv.restrictScalars P
      (LinearEquiv.ofEq (RingHom.ker (IsScalarTower.toAlgHom R P S).toRingHom).cotangentIdeal
        (RingHom.ker (IsScalarTower.toAlgHom R P S).kerSquareLift.toRingHom) ⋯)
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)
H : kerCotangentToTensor R P S = ↑e₂ ∘ₗ ↑P (kerToTensor R P' S) ∘ₗ ↑e₁
x✝ : { l // l ∘ₗ kerCotangentToTensor R P S = LinearMap.id }
l : S ⊗[P] Ω[P⁄R] →ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent
hl : l ∘ₗ kerCotangentToTensor R P S = LinearMap.id
⊢ ∀ (m : P') (x : S ⊗[P'] Ω[P'⁄R]),
    (↑(↑e₁ ∘ₗ l ∘ₗ ↑e₂)).toFun (m • x) = (RingHom.id P') m • (↑(↑e₁ ∘ₗ l ∘ₗ ↑e₂)).toFun x

Tactic:
rintro x y

Goal state after:
case refine_1
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
P' : Type u_2 := P ⧸ RingHom.ker (algebraMap P S) ^ 2
h₁ : Surjective ⇑(algebraMap P' S)
h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥
e₁ : (RingHom.ker (algebraMap P S)).Cotangent ≃ₗ[P] ↥(RingHom.ker (algebraMap P' S)) :=
  (RingHom.ker (algebraMap P S)).cotangentEquivIdeal ≪≫ₗ
    LinearEquiv.restrictScalars P
      (LinearEquiv.ofEq (RingHom.ker (IsScalarTower.toAlgHom R P S).toRingHom).cotangentIdeal
        (RingHom.ker (IsScalarTower.toAlgHom R P S).kerSquareLift.toRingHom) ⋯)
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)
H : kerCotangentToTensor R P S = ↑e₂ ∘ₗ ↑P (kerToTensor R P' S) ∘ₗ ↑e₁
x✝ : { l // l ∘ₗ kerCotangentToTensor R P S = LinearMap.id }
l : S ⊗[P] Ω[P⁄R] →ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent
hl : l ∘ₗ kerCotangentToTensor R P S = LinearMap.id
x : P'
y : S ⊗[P'] Ω[P'⁄R]
⊢ (↑(↑e₁ ∘ₗ l ∘ₗ ↑e₂)).toFun (x • y) = (RingHom.id P') x • (↑(↑e₁ ∘ₗ l ∘ₗ ↑e₂)).toFun y
Module: Mathlib.RingTheory.Unramified.LocalRing

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
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
hq : p.primesOver S = {q}
inst✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
x : R
s : ↥p.primeCompl
hx : (localRingHom p q (algebraMap R S) ⋯) (IsLocalization.mk' (Localization.AtPrime p) x s) = 0
a : S
haq : a ∉ q
e : a * (algebraMap R S) x = 0
r : R
hrp : r ∉ p
t : S
e' : (algebraMap R S) r = a * t
⊢ IsLocalization.mk' (Localization.AtPrime p) x s = 0

Tactic:
refine (IsLocalization.mk'_eq_zero_iff _ _).mpr
    ⟨⟨r, hrp⟩, FaithfulSMul.algebraMap_injective R S ?_⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
p : Ideal R
inst✝³ : p.IsPrime
q : Ideal S
inst✝² : q.IsPrime
hq : p.primesOver S = {q}
inst✝¹ : Algebra.IsIntegral R S
inst✝ : FaithfulSMul R S
x : R
s : ↥p.primeCompl
hx : (localRingHom p q (algebraMap R S) ⋯) (IsLocalization.mk' (Localization.AtPrime p) x s) = 0
a : S
haq : a ∉ q
e : a * (algebraMap R S) x = 0
r : R
hrp : r ∉ p
t : S
e' : (algebraMap R S) r = a * t
⊢ (algebraMap R S) (↑⟨r, hrp⟩ * x) = (algebraMap R S) 0
Module: Mathlib.RingTheory.Unramified.LocalRing

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
inst✝⁶ : p.IsPrime
q : Ideal S
inst✝⁵ : q.IsPrime
hq : p.primesOver S = {q}
inst✝⁴ : Module.Finite R S
inst✝³ : q.LiesOver p
inst✝² : Algebra.IsUnramifiedAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
H : Function.Surjective ⇑(algebraMap p.ResidueField q.ResidueField)
this : Module.Finite (Localization.AtPrime p) (Localization.AtPrime q)
⊢ ⊤ ≤ (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)).range

Tactic:
apply Submodule.le_of_le_smul_of_le_jacobson_bot Module.Finite.fg_top (maximalIdeal_le_jacobson _)

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
p : Ideal R
inst✝⁶ : p.IsPrime
q : Ideal S
inst✝⁵ : q.IsPrime
hq : p.primesOver S = {q}
inst✝⁴ : Module.Finite R S
inst✝³ : q.LiesOver p
inst✝² : Algebra.IsUnramifiedAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
H : Function.Surjective ⇑(algebraMap p.ResidueField q.ResidueField)
this : Module.Finite (Localization.AtPrime p) (Localization.AtPrime q)
⊢ ⊤ ≤
    (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)).range ⊔
      maximalIdeal (Localization.AtPrime p) • ⊤
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case right
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
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
⊢ Function.Surjective ⇑(LinearMap.liftBaseChange T (H1Cotangent.map f))

Tactic:
· intro x
    have : Function.Exact (h1Cotangentι.baseChange T) (P.cotangentComplex.baseChange T) :=
      Module.Flat.lTensor_exact T (LinearMap.exact_subtype_ker_map _)
    obtain ⟨a, ha⟩ := (this ((Extension.tensorCotangent f halg H₂).symm x.1)).mp (by
      apply (Extension.tensorCotangentSpaceOfFormallyEtale f H₁).injective
      rw [LinearEquiv.map_zero, ← x.2]
      have : (CotangentSpace.map f).liftBaseChange T ∘ₗ P.cotangentComplex.baseChange T =
          Q.cotangentComplex ∘ₗ (Cotangent.map f).liftBaseChange T := by
        ext x; obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x; dsimp
        simp only [CotangentSpace.map_tmul,
          map_one, Hom.toAlgHom_apply, one_smul, cotangentComplex_mk]
      exact (DFunLike.congr_fun this _).trans (DFunLike.congr_arg Q.cotangentComplex
        ((tensorCotangent f halg H₂).apply_symm_apply x.1)))
    refine ⟨a, Subtype.ext (.trans ?_ ((LinearEquiv.eq_symm_apply _).mp ha))⟩
    change (h1Cotangentι ∘ₗ (H1Cotangent.map f).liftBaseChange T) _ =
      ((Cotangent.map f).liftBaseChange T ∘ₗ h1Cotangentι.baseChange T) _
    congr 1
    ext; dsimp

Goal state after:
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 : ¬I ≤ q
h :
  map (algebraMap S (Localization.AtPrime q)) (map (algebraMap R S) p) =
    map (algebraMap S (Localization.AtPrime q)) (q ^ p.ramificationIdx' q * I)
⊢ p.ramificationIdx' q = q.ramificationIdx R

Tactic:
rw [map_map, ← IsScalarTower.algebraMap_eq, Ideal.map_mul, Ideal.map_pow,
    map_eq_top_of_not_le (Localization.AtPrime q) hqI, mul_top, AtPrime.map_eq_maximalIdeal] at h

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
hqI : ¬I ≤ q
h :
  map (algebraMap R (Localization.AtPrime q)) p =
    IsLocalRing.maximalIdeal (Localization q.primeCompl) ^ p.ramificationIdx' q
⊢ p.ramificationIdx' q = q.ramificationIdx R
Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Goal state before:
pp: M : Type u_1
inst✝³ : CompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
⊢ sSup s⁻¹ = (sInf s)⁻¹

Tactic:
by
  rw [← image_inv_eq_inv, sSup_image]
  exact ((OrderIso.inv M).map_sInf _).symm

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ
s✝ : Set ℝ
a : ℝ
s : Set ℝ
hs : ¬BddBelow s
⊢ sInf s = sInf ∅

Tactic:
simp [hs, sInf_def, sSup_def]

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

Goal state before:
pp: s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
⊢ sInf s ≤ a ↔ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε

Tactic:
le_iff_forall_pos_lt_add

Goal state after:
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
⊢ (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) ↔ ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
⊢ a ≤ sSup s ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x

Tactic:
le_iff_forall_pos_lt_add

Goal state after:
s : Set ℝ
a : ℝ
h : BddAbove s
h' : s.Nonempty
⊢ (∀ (ε : ℝ), 0 < ε → a < sSup s + ε) ↔ ∀ ε < 0, ∃ x ∈ s, a + ε < x
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ι : Sort u_2
s : ι → ℝ≥0
⊢ sSup (toReal '' Set.range fun i ↦ s i) = sSup (Set.range fun i ↦ ↑(s i))

Tactic:
← Set.range_comp

Goal state after:
ι : Sort u_2
s : ι → ℝ≥0
⊢ sSup (Set.range (toReal ∘ fun i ↦ s i)) = sSup (Set.range fun i ↦ ↑(s i))
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ι : Sort u_2
s : ι → ℝ≥0
⊢ sInf (toReal '' Set.range fun i ↦ s i) = sInf (Set.range fun i ↦ ↑(s i))

Tactic:
← Set.range_comp

Goal state after:
ι : Sort u_2
s : ι → ℝ≥0
⊢ sInf (Set.range (toReal ∘ fun i ↦ s i)) = sInf (Set.range fun i ↦ ↑(s i))
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: b a : ℝ≥0
h : ↑a ≤ ↑b
⊢ (↑a).toReal ≤ ↑b

Tactic:
simpa using h

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

Goal state before:
pp: ⊢ ⋃ n, Iio ↑n = {∞}ᶜ

Tactic:
by
  ext x
  rw [mem_iUnion]
  exact ⟨fun ⟨n, hn⟩ => ne_top_of_lt hn, ENNReal.exists_nat_gt⟩

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf : Surjective ⇑φ
⊢ Surjective ⇑(map P.asIdeal φ)

Tactic:
rintro ⟨y, hy⟩

Goal state after:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf : Surjective ⇑φ
y : M₂
hy : y ∈ primaryComponent M₂ P.asIdeal
⊢ ∃ a, (map P.asIdeal φ) a = ⟨y, hy⟩
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: r : ℝ
⊢ 0 < ENNReal.ofReal r ↔ 0 < r

Tactic:
ENNReal.ofReal_pos

Goal state after:
r : ℝ
⊢ 0 < r ↔ 0 < r
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case mp
a b : ℝ≥0∞
⊢ a * b < ∞ → a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0

Tactic:
intro h
    rw [← or_assoc, or_iff_not_imp_right, or_iff_not_imp_right]
    intro hb ha
    exact ⟨lt_top_of_mul_ne_top_left h.ne hb, lt_top_of_mul_ne_top_right h.ne ha⟩

Goal state after:
Module: Mathlib.Topology.Order.T5

Goal state before:
pp: case refine_2
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
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
hyc : y ≤ c
hya : y < a
⊢ False

Tactic:
exact hxy (Icc_subset_uIcc ⟨hya.le, hx.1⟩) ha

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
⊢ a + iInf f = ⨅ b, a + f b

Tactic:
rw [add_comm, iInf_add]; simp [add_comm]

Goal state after:
Module: Mathlib.Topology.UniformSpace.OfFun

Goal state before:
pp: X : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
d : X → X → M
refl : ∀ (x : X), d x x = 0
symm : ∀ (x y : X), d x y = d y x
triangle : ∀ (x y z : X), d x z ≤ d x y + d y z
half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε
r : M
hr : r > 0
⊢ SetRel.id ⊆ {x | d x.1 x.2 < r}

Tactic:
by simp [Set.subset_def, *]

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
hx : ↑x ≠ ⊥
y : ℝ
hy : ↑y ≠ ⊤
h : ↑x ≤ ↑y
⊢ (↑x).toReal ≤ (↑y).toReal

Tactic:
simpa using h

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case bot
x z : EReal
h : x < z
ha₁ : x < ⊥
ha₂ : ⊥ < z
⊢ ∃ y, x < ↑y ∧ ↑y < z

Tactic:
| bot =>

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case top
x z : EReal
h : x < z
ha₁ : x < ⊤
ha₂ : ⊤ < z
⊢ ∃ y, x < ↑y ∧ ↑y < z

Tactic:
exact (not_top_lt ha₂).elim

Goal state after:
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : EReal
hx : x ≤ 0
⊢ x.toENNReal = 0

Tactic:
by
  rw [toENNReal, if_neg (fun h ↦ ?_)]
  · exact ENNReal.ofReal_of_nonpos (toReal_nonpos hx)
  · exact zero_ne_top <| top_le_iff.mp <| h ▸ hx

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
hv : ↑v.asIdeal ≠ 0
h_self : ↑v.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑v.asIdeal
hv_irred : Irreducible (Associates.mk v.asIdeal)
⊢ count K v ↑v.asIdeal = 1

Tactic:
count_well_defined K v hv h_self,

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
hv : ↑v.asIdeal ≠ 0
h_self : ↑v.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑v.asIdeal
hv_irred : Irreducible (Associates.mk v.asIdeal)
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk v.asIdeal).factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {1})).factors) =
    1
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: m n : ℕ
⊢ ↑m < ↑n ↔ m < n

Tactic:
rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_lt_coe_iff, Nat.cast_lt]

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

Goal state before:
pp: a b c : ℝ≥0∞
h : 0 < b → b < a → c ≠ 0
⊢ 0 < b → b < a → c⁻¹ ≠ ∞

Tactic:
simpa using h

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

Goal state before:
pp: a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
x✝¹ x✝ : ↑(Iic a)
⊢ { toFun := fun x ↦ ⟨↑↑x, ⋯⟩, invFun := fun x ↦ ⟨(↑x).toNNReal, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } x✝¹ ≤
      { toFun := fun x ↦ ⟨↑↑x, ⋯⟩, invFun := fun x ↦ ⟨(↑x).toNNReal, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } x✝ ↔
    x✝¹ ≤ x✝

Tactic:
simp only [Equiv.coe_fn_mk, Subtype.mk_le_mk, coe_le_coe, Subtype.coe_le_coe]

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ eball x ε
⊢ 0 < ε - edist y x

Tactic:
simpa using h

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
x✝¹ : ℝ≥0∞
x✝ : ⊥ < x✝¹
⊢ ∞ * f i < x✝¹

Tactic:
by simpa [hi]

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
i : ι
hi : f i = 0
x✝¹ : ℝ≥0∞
x✝ : ⊥ < x✝¹
⊢ f i < x✝¹

Tactic:
by simpa [hi]

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

Goal state before:
pp: x y : ℝ
hy : 0 < y
⊢ ENNReal.ofReal x * ENNReal.ofReal y⁻¹ = ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹

Tactic:
ofReal_inv_of_pos hy

Goal state after:
x y : ℝ
hy : 0 < y
⊢ ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹ = ENNReal.ofReal x * (ENNReal.ofReal y)⁻¹
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
h : y ∈ ball x ε
⊢ dist y x ≤ ε - (ε - dist y x)

Tactic:
sub_sub_self

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
h : y ∈ ball x ε
⊢ dist y x ≤ dist y x
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
f : ι → ℕ
⊢ BddAbove (range fun x ↦ ↑(f x)) ↔ BddAbove (Nat.cast '' range f)

Tactic:
← Set.range_comp

Goal state after:
ι : Sort u_3
f : ι → ℕ
⊢ BddAbove (range fun x ↦ ↑(f x)) ↔ BddAbove (range (Nat.cast ∘ f))
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
inst✝ : Nonempty ι
a g : ℝ≥0
h : ι → ℝ≥0
H : ∀ (j : ι), a ≤ g * h j
⊢ a ≤ g * iInf h

Tactic:
by
  rw [mul_iInf]
  exact le_ciInf H

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: z : ℝ≥0
⊢ nndist z 0 = z

Tactic:
rw [nndist_comm]

Goal state after:
z : ℝ≥0
⊢ nndist 0 z = z
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
h : a < b
⊢ frontier (Ioo a b) = {a, b}

Tactic:
rw [frontier, closure_Ioo h.ne, interior_Ioo, Icc_sdiff_Ioo_same h.le]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: case pos
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

Tactic:
by_cases hkj : k = j

Goal state after:
case pos
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
hkj : k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)

case neg
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
hki : k = i
hkj : ¬k = j
⊢ nndist (if k = i then a else 0) (if k = j then b else 0) ≤ max (nndist a 0) (nndist b 0)