mathlib-initiative/mathlib-tactics huggingface dataset:
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
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 : K
this : s • (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) r = r • e s
⊢ (↑K ((ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ e'.toLinearMap)) (r ⊗ₜ[K] e s) =
    (↑K
        (TensorProduct.AlgebraTensorModule.lift
          (↑K (lsmul A A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap.flip).flip))
      (r ⊗ₜ[K] e s)

Tactic:
simpa [ofId, e']

Goal state after:
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
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)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A
hf₃ : IsIdempotentElem (1 - f 1)
hf₄ : f 1 = 1
x : K
⊢ (⇑e.symm ∘ ⇑(algebraMap A (A ⧸ IsLocalRing.maximalIdeal A))) ((algebraMap K A) x) = x

Tactic:
by simp

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

Goal state before:
pp: case hz
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.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := ⋯
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace := ⋯
⊢ (CotangentSpace.compEquiv Q P)
      ((↑(CotangentSpace.compEquiv Q P).symm ∘ₗ
          LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace))
        z) =
    (CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)

Tactic:
simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, LinearMap.coe_inr, Function.comp_apply,
      LinearEquiv.apply_symm_apply, z]

Goal state after:
case hz
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.ker
hx : Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker
y : (Q.comp P).toExtension.Cotangent := Extension.Cotangent.mk (Q.kerCompPreimage P x)
hy : (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) y = Extension.Cotangent.mk x
z : T ⊗[S] P.toExtension.CotangentSpace :=
  ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2
⊢ (0, ((CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)).2) =
    (CotangentSpace.compEquiv Q P) ((Q.comp P).toExtension.cotangentComplex y)
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝¹ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
h' : LinearIndependent K ![1, x]
h : LinearIndepOn K _root_.id (Set.range ![1, x])
S : Set L := h.extend ⋯
⊢ 1 ∈ Set.range ![1, x]

Tactic:
by simp

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

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝¹ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
h' : LinearIndependent K ![1, x]
h : LinearIndepOn K _root_.id (Set.range ![1, x])
S : Set L := h.extend ⋯
a : ↑S := ⟨1, ⋯⟩
ha : (Basis.extend h) a = 1
⊢ x ∈ Set.range ![1, x]

Tactic:
by simp

Goal state after:
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)
⊢ (aeval ((algebraMap A Q.ResidueField) x)) q = (algebraMap (Localization.AtPrime Q) Q.ResidueField) 0

Tactic:
minpoly.aeval,

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)
⊢ 0 = (algebraMap (Localization.AtPrime Q) Q.ResidueField) 0
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case tmul.tmul
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
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
a : Q.Ring
b : ↥P.ker
c : Q.Ring
d : ↥P.ker
h₂ : ↑b • Cotangent.mk d = 0
⊢ (a * ↑((f.mapKer halg) b)) • c • 1 ⊗ₜ[S] Cotangent.mk d = 0

Tactic:
TensorProduct.smul_tmul',

Goal state after:
case tmul.tmul
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
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
a : Q.Ring
b : ↥P.ker
c : Q.Ring
d : ↥P.ker
h₂ : ↑b • Cotangent.mk d = 0
⊢ (a * ↑((f.mapKer halg) b)) • (c • 1) ⊗ₜ[S] Cotangent.mk d = 0
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case tmul.tmul
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
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
this✝¹ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring Q.Ring T
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
a : Q.Ring
b : ↥P.ker
c : Q.Ring
d : ↥P.ker
⊢ ↑(e (a ⊗ₜ[P.Ring] b)) •
      (LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk))
        (c ⊗ₜ[P.Ring] d) =
    0

Tactic:
| tmul c d =>

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

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
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
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.Ring
y : ↥P.ker
⊢ (tensorCotangentInvFun f halg H) (x • Cotangent.mk ⟨f.toRingHom ↑y, ⋯⟩) = x • 1 ⊗ₜ[S] Cotangent.mk y

Tactic:
let := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra

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
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
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : Q.Ring
y : ↥P.ker
this : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
⊢ (tensorCotangentInvFun f halg H) (x • Cotangent.mk ⟨f.toRingHom ↑y, ⋯⟩) = x • 1 ⊗ₜ[S] Cotangent.mk 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✝³ : Module.Finite R S
inst✝² : q.LiesOver p
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
s : Finset S
hs : Submodule.span R ↑s = ⊤
⊢ Submodule.span (Localization.AtPrime p) ↑(IsScalarTower.toAlgHom R S (Localization.AtPrime q)).toLinearMap.range = ⊤

Tactic:
LinearMap.coe_range,

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 (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : AtPrime.IsLiesOverAlgebra p q
s : Finset S
hs : Submodule.span R ↑s = ⊤
⊢ Submodule.span (Localization.AtPrime p)
      (Set.range ⇑(IsScalarTower.toAlgHom R S (Localization.AtPrime q)).toLinearMap) =
    ⊤
Module: Mathlib.RingTheory.RamificationInertia.Ramification

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
inst✝ : Module.Flat S T
⊢ r.ramificationIdx S ∣ r.ramificationIdx R

Tactic:
by
  use q.ramificationIdx R
  rw [mul_comm, ← ramificationIdx_tower]

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

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
hy : ∀ a ∈ I ^ n₁, a • y = 0
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ a ∈ I ^ n₂, a • z = 0
a : A
ha : a ∈ I ^ max n₁ n₂
⊢ n₁ ≤ max n₁ n₂

Tactic:
by simp

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

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ a ∈ I ^ n₂, a • z = 0
a : A
hy : a • y = 0
ha : a ∈ I ^ max n₁ n₂
⊢ n₂ ≤ max n₁ n₂

Tactic:
by simp

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice

Goal state before:
pp: M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
⊢ sInf s⁻¹ = (sSup s)⁻¹

Tactic:
rw [← image_inv_eq_inv]
  exact ((OrderIso.inv _).map_csSup' hs₀ hs₁).symm

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

Goal state before:
pp: ⊢ ¬(∅.Nonempty ∧ BddAbove ∅)

Tactic:
by simp

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

Goal state before:
pp: x : ℝ≥0
⊢ nnabs ↑x = x

Tactic:
by simp

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

Goal state before:
pp: x : ℝ
⊢ ↑|x|.toNNReal = ↑(nnabs x)

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
⊢ nnabs ↑n = ↑n

Tactic:
by simp

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

Goal state before:
pp: n : ℕ
inst✝ : n.AtLeastTwo
⊢ nnabs (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
by simp

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

Goal state before:
pp: a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ 0 ≤ 1 / ↑k

Tactic:
by simp

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

Goal state before:
pp: case h
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := ⋯
hu : u = if g < 1 then g else g⁻¹
hfu : f ↑u < 1
n : ℕ
hn : f ↑u ^ n < r
⊢ f ↑(u ^ n) < r

Tactic:
rwa [Units.val_pow_eq_pow_val, map_pow]

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✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
⊢ ⨆ p, ↑p 1 = 0

Tactic:
by simp

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

Goal state before:
pp: x : ℝ≥0∞
⊢ x = ↑1 ∨ x = ⊤ ∧ 1 = 0 ↔ x = 1

Tactic:
by simp

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✝¹ : Group F
inst✝ : Group G
p q : GroupSeminorm E
f : F →* E
s : Set (GroupSeminorm E)
h : BddAbove s
x : E
⊢ ⨆ p, ↑p x⁻¹ = ⨆ p, ↑p x

Tactic:
by simp

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

Goal state before:
pp: E : Type u_3
inst✝ : Group E
ι : Type u_6
f : ι → GroupSeminorm E
h : BddAbove (range f)
x : E
⊢ ∀ (x_1 : ι), ↑(rangeFactorization f x_1) x = (f x_1) x

Tactic:
by simp

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

Goal state before:
pp: r : ℝ≥0∞
h : r ≠ ∞
⊢ ∃ n, r < ↑n

Tactic:
by
  lift r to ℝ≥0 using h
  rcases exists_nat_gt r with ⟨n, hn⟩
  exact ⟨n, coe_lt_natCast.2 hn⟩

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

Goal state before:
pp: a : ℝ≥0∞
⊢ 0 < a.toNNReal ↔ 0 < a ∧ a < ∞

Tactic:
induction a <;> simp

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

Goal state before:
pp: p : ℝ
n : ℕ
hn : n ≠ 0
⊢ ENNReal.ofReal p < ↑n ↔ p < ↑n

Tactic:
exact mod_cast ofReal_lt_ofReal_iff (Nat.cast_pos.2 hn.bot_lt)

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

Goal state before:
pp: p : ℝ
⊢ 1 ≤ ENNReal.ofReal p ↔ 1 ≤ p

Tactic:
by
  exact mod_cast natCast_le_ofReal one_ne_zero

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✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
⊢ ⨆ p, ↑p 0 = 0

Tactic:
by simp

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✝ : AddGroup E
p q : NonarchAddGroupSeminorm E
s : Set (NonarchAddGroupSeminorm E)
h : BddAbove s
⊢ ∀ (r : E), ⨆ p, ↑p (-r) = ⨆ p, ↑p r

Tactic:
by simp

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

Goal state before:
pp: a : ℝ≥0∞
⊢ (a * ∞).toNNReal = 0

Tactic:
by simp

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

Goal state before:
pp: a : ℝ≥0∞
⊢ (∞ * a).toNNReal = 0

Tactic:
by simp

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

Goal state before:
pp: a : ℝ≥0∞
n : ℕ
⊢ (n • a).toReal = n • a.toReal

Tactic:
by simp

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

Goal state before:
pp: E : Type u_3
inst✝ : AddGroup E
ι : Type u_6
f : ι → NonarchAddGroupSeminorm E
h : BddAbove (range f)
x : E
⊢ ∀ (x_1 : ι), ↑(rangeFactorization f x_1) x = (f x_1) x

Tactic:
by simp

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

Goal state before:
pp: a : ℝ≥0∞
⊢ ¬a < 0

Tactic:
by simp

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

Goal state before:
pp: a b c : ℝ≥0∞
hle : a ≤ b + c
hb : b = ∞ → a = ∞
hc : c = ∞ → a = ∞
⊢ a.toReal ≤ b.toReal + c.toReal

Tactic:
refine le_trans (toReal_mono' hle ?_) toReal_add_le
  simpa only [add_eq_top, or_imp] using And.intro hb hc

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

Goal state before:
pp: x y : ℝ
⊢ { toFun := Real.toEReal, inj' := coe_injective } x ≤ { toFun := Real.toEReal, inj' := coe_injective } y ↔ x ≤ y

Tactic:
by simp

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

Goal state before:
pp: ι : Sort u_1
⊢ ⨆ x, 0 = 0

Tactic:
by simp

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

Goal state before:
pp: x : ℝ
⊢ WithBot.some '' WithTop.some '' Iic x = Ioc ⊥ ↑x

Tactic:
rw [WithTop.image_coe_Iic, WithBot.image_coe_Iic]

Goal state after:
x : ℝ
⊢ Ioc ⊥ ↑↑x = Ioc ⊥ ↑x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ ↑x ∈ {⊥, ⊤}ᶜ

Tactic:
by simp

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

Goal state before:
pp: x : ℝ
⊢ (fun x ↦ (↑x).toReal) ((fun x ↦ ⟨↑x, ⋯⟩) x) = x

Tactic:
by simp

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a⁻¹ ≠ ∞ ↔ a ≠ 0

Tactic:
by simp

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a⁻¹ ≠ 0 ↔ a ≠ ∞

Tactic:
by simp

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Tactic:
simpa only [inv_inv] using @ENNReal.inv_le_inv a b⁻¹

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

Goal state before:
pp: a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
⊢ a * b⁻¹ ≤ c ↔ a ≤ c / b⁻¹

Tactic:
refine (ENNReal.le_div_iff_mul_le ?_ ?_).symm

Goal state after:
case refine_1
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
⊢ b⁻¹ ≠ 0 ∨ c ≠ 0

case refine_2
a b c : ℝ≥0∞
hb0 : b ≠ 0 ∨ c ≠ ∞
hbt : b ≠ ∞ ∨ c ≠ 0
⊢ b⁻¹ ≠ ∞ ∨ c ≠ ∞
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
⊢ a ≤ 1 * a

Tactic:
rw [one_mul]

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

Goal state before:
pp: a b c : ℝ≥0∞
ha₀ : a ≠ 0
ha : a ≠ ∞
⊢ b⁻¹ < c⁻¹ ↔ c < b

Tactic:
by simp

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ ∞

Tactic:
rw [← pos_iff_ne_zero, div_pos_iff]

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

Goal state before:
pp: case e'_2
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
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ exps v =
    { support := Finite.toFinset h_exps, toFun := exps, mem_support_toFun := ⋯ }.prod fun x1 x2 ↦ ↑x1.asIdeal ^ x2

Tactic:
finprod_eq_finsetProd_of_mulSupport_subset (s := h_exps.toFinset),

Goal state after:
case e'_2
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
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ ∏ i ∈ Finite.toFinset h_exps, ↑i.asIdeal ^ exps i =
    { support := Finite.toFinset h_exps, toFun := exps, mem_support_toFun := ⋯ }.prod fun x1 x2 ↦ ↑x1.asIdeal ^ x2

case e'_2.h
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
exps : HeightOneSpectrum R → ℤ
h_exps : ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, exps v = 0
⊢ (mulSupport fun v ↦ ↑v.asIdeal ^ exps v) ⊆ ↑(Finite.toFinset h_exps)
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α × β
⊢ max (edist x.1 x.1) (edist x.2 x.2) = 0

Tactic:
by simp

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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
| I

Tactic:
rw [← finprod_heightOneSpectrum_factorization hI h]

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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
| ∏ᶠ (v : HeightOneSpectrum R),
    ↑v.asIdeal ^
      (↑((Associates.mk v.asIdeal).count (Associates.mk (Classical.choose ⋯)).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors))
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y z : α
⊢ dist x y ≤ dist z x + dist z y

Tactic:
by
  rw [dist_comm z]; apply dist_triangle

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ x ∈ sphere y ε ↔ y ∈ sphere x ε

Tactic:
mem_sphere',

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ dist y x = ε ↔ y ∈ sphere x ε
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ closedEBall x ↑ε = closedBall x ↑ε

Tactic:
← closedEBall_ofReal ε.coe_nonneg,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ closedEBall x ↑ε = closedEBall x (ENNReal.ofReal ↑ε)