mathlib-initiative/mathlib-tactics huggingface dataset:
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
H :
  ∀ ⦃B : Type (max u v)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
surj : Function.Surjective ⇑f.kerSquareLift
sqz : RingHom.ker f.kerSquareLift ^ 2 = ⊥
⊢ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A

Tactic:
obtain ⟨g, hg⟩ := H _ sqz (Ideal.quotientKerAlgEquivOfSurjective surj).symm.toAlgHom

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
H :
  ∀ ⦃B : Type (max u v)⦄ [inst : CommRing B] [inst_1 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Surjective (Ideal.Quotient.mkₐ R I).comp
P : Generators R A A := Generators.self R A
f : P.Ring →ₐ[R] A := IsScalarTower.toAlgHom R P.Ring A
surj : Function.Surjective ⇑f.kerSquareLift
sqz : RingHom.ker f.kerSquareLift ^ 2 = ⊥
g : A →ₐ[R] P.Ring ⧸ RingHom.ker f ^ 2
hg : (Ideal.Quotient.mkₐ R (RingHom.ker f.kerSquareLift)).comp g = ↑(Ideal.quotientKerAlgEquivOfSurjective surj).symm
⊢ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A
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)) =
    (D R T) ((algebraMap (Q.comp P).toExtension.Ring T) ((Q.toComp P).toExtensionHom.toAlgHom (X i)))

Tactic:
simp [Extension.Hom.toAlgHom]

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
a b : K
e : a • 1 + b • x = 0
hab : a = 0 → ¬b = 0
⊢ b ≠ 0

Tactic:
rintro rfl

Goal state after:
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
a : K
e : a • 1 + 0 • x = 0
hab : a = 0 → ¬0 = 0
⊢ False
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: case h
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
a b : K
e : a • 1 + b • x = 0
hab : a = 0 → ¬b = 0
this : IsUnit b
⊢ (algebraMap K L) (-↑this.unit⁻¹ * a) = x

Tactic:
rw [map_mul, ← Algebra.smul_def, algebraMap_eq_smul_one, eq_neg_iff_add_eq_zero.mpr e,
      smul_neg, neg_smul, neg_neg, smul_smul, this.val_inv_mul, one_smul]

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)
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

Tactic:
exact hm this

Goal state after:
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
inst✝⁴ : IsLocalRing R
inst✝³ : IsLocalRing S
inst✝² : IsLocalHom (algebraMap R S)
inst✝¹ : EssFiniteType R S
inst✝ : Algebra.IsSeparable (ResidueField R) (ResidueField S)
H : Ideal.map (algebraMap R S) (maximalIdeal R) = maximalIdeal S
this✝ : FormallyUnramified (ResidueField R) (ResidueField S)
this : FormallyUnramified R (ResidueField S)
x : S
hx : x ∈ Ideal.map (algebraMap R S) (maximalIdeal R)
⊢ 1 ⊗ₜ[S] (KaehlerDifferential.D R S) x = 0

Tactic:
induction hx using Submodule.span_induction with
  | zero => simp
  | mem x h => obtain ⟨x, hx, rfl⟩ := h; simp
  | add x y hx hy _ _ => simp [*, TensorProduct.tmul_add]
  | smul a x hx _ =>
    have : residue S x = 0 := by rwa [residue_eq_zero_iff, ← H]
    simp [*, TensorProduct.tmul_add, TensorProduct.smul_tmul', ← Algebra.algebraMap_eq_smul_one]

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
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
x s : P.Ring
hs : (algebraMap P.Ring S) s ∈ M
⊢ (IsLocalization.lift ⋯) (IsLocalization.mk' (Localization M') x ⟨s, ⋯⟩) =
    IsLocalization.mk' T ((algebraMap P.Ring S) x) ⟨(algebraMap P.Ring S) s, hs⟩

Tactic:
IsLocalization.lift_mk'_spec

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
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
x s : P.Ring
hs : (algebraMap P.Ring S) s ∈ M
⊢ ↑((IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) x =
    ↑((IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) ↑⟨s, ⋯⟩ *
      IsLocalization.mk' T ((algebraMap P.Ring S) x) ⟨(algebraMap P.Ring S) s, hs⟩
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case refine_1
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
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝⁸ : FormallySmooth R P.Ring
this✝⁷ : FormallySmooth P.Ring (Localization M')
this✝⁶ : FormallySmooth R Q.Ring
this✝⁵ : Module.Flat S T
this✝⁴ : Algebra P.Ring Q.Ring := inferInstance
this✝³ : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝² : Algebra (Localization M') T := fQ.toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring (Localization M') T
this : IsLocalizedModule M' (IsScalarTower.toAlgHom P.Ring S T).toLinearMap
⊢ f.toRingHom.FormallyEtale

Tactic:
exact RingHom.formallyEtale_algebraMap.mpr
      (FormallyEtale.of_isLocalization (M := M') (Rₘ := Localization M'))

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

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
p : Ideal R
inst✝¹⁰ : p.IsPrime
S : Type u_2
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : IsDomain R
inst✝⁶ : IsDomain S
inst✝⁵ : Module.Finite R S
inst✝⁴ : Module.Flat R S
inst✝³ : Fintype ↑(p.primesOver S)
G : Type u_3
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : IsGaloisGroup G R S
⊢ ∑ q, (↑q).ramificationIdx R * (↑q).inertiaDeg R = Nat.card G

Tactic:
let := IsGaloisGroup.finite G R S
  rw [sum_ramification_inertia_eq_finrank, IsGaloisGroup.card_eq_finrank' G R S]

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
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x✝ : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
x s : P.Ring
hs : (algebraMap P.Ring S) s ∈ M
⊢ (IsLocalization.lift ⋯) (IsLocalization.mk' (Localization M') x ⟨s, ⋯⟩) =
    IsLocalization.mk' T ((algebraMap P.Ring S) x) ⟨(algebraMap P.Ring S) s, hs⟩

Tactic:
IsLocalization.lift_mk'_spec

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
M : Submonoid S
inst✝ : IsLocalization M T
x✝ : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
x s : P.Ring
hs : (algebraMap P.Ring S) s ∈ M
⊢ ↑((IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) x =
    ↑((IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) ↑⟨s, ⋯⟩ *
      IsLocalization.mk' T ((algebraMap P.Ring S) x) ⟨(algebraMap P.Ring S) s, hs⟩
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
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
⊢ IsLocalizedModule M (map R R S T)

Tactic:
isLocalizedModule_iff_isBaseChange M T

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
M : Submonoid S
inst✝ : IsLocalization M T
⊢ IsBaseChange T (map R R S T)
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < ↑k
d : ℕ
z : ℤ
y : ℝ
yS : y ∈ s
hy : ↑z ≤ y * ↑d
⊢ y * ↑d ≤ ↑(k * ↑d)

Tactic:
push_cast

Goal state after:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < ↑k
d : ℕ
z : ℤ
y : ℝ
yS : y ∈ s
hy : ↑z ≤ y * ↑d
⊢ y * ↑d ≤ ↑k * ↑d
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_1
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n ↦ ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n ↦ ↑(f n) / ↑n, hg⟩
x : ℝ
xS : x ∈ s
z : ℝ
xz : z < x
K : ℕ
hK : (x - z)⁻¹ < ↑K
⊢ z ≤ mk g

Tactic:
refine le_mk_of_forall_le ⟨K, fun n nK => ?_⟩

Goal state after:
case refine_1
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
hg : IsCauSeq abs fun n ↦ ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n ↦ ↑(f n) / ↑n, hg⟩
x : ℝ
xS : x ∈ s
z : ℝ
xz : z < x
K : ℕ
hK : (x - z)⁻¹ < ↑K
n : ℕ
nK : n ≥ K
⊢ z ≤ ↑(↑g n)
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case h
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
hbdd' : BddAbove (-s)
⊢ IsLUB (-s) (Classical.choose ⋯)

Tactic:
exact Classical.choose_spec (Real.exists_isLUB hne' hbdd')

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

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

Tactic:
ε_pos

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

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

Tactic:
ε_pos

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

Goal state before:
pp: case inr
ι : Sort u_1
h✝ : Nonempty ι
⊢ ⨆ x, 0 = 0

Tactic:
exact ciSup_const

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

Goal state before:
pp: ⊢ ENNReal.ofReal 0 = 0

Tactic:
simp [ENNReal.ofReal]

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

Goal state before:
pp: ⊢ ENNReal.ofReal 1 = 1

Tactic:
simp [ENNReal.ofReal]

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

Goal state before:
pp: n : ℕ
⊢ ENNReal.ofReal ↑n = ↑n

Tactic:
simp [ENNReal.ofReal]

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 y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
x✝¹ x✝ : GroupSeminorm E
h' : x✝¹ ≤ x✝
⊢ x✝¹ x ≤ x✝ x

Tactic:
exact h' _

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 y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
x✝¹ x✝ : GroupSeminorm E
h' : x✝¹ ≤ x✝
⊢ x✝¹ y ≤ x✝ y

Tactic:
exact h' _

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

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

Tactic:
simp [ENNReal.ofReal]

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

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

Tactic:
simp [ENNReal.ofReal]

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

Goal state before:
pp: case refine_2
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 ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
hdiff : φ b - φ ↑(f P) = ∑ Q ∈ f.support \ {P}, φ ↑(f Q)
⊢ φ b - φ ↑(f P) ∈ ⨆ j, ⨆ (_ : j ≠ P), (fun P ↦ primaryComponent M₂ P.asIdeal) j

Tactic:
hdiff

Goal state after:
case refine_2
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 ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
hdiff : φ b - φ ↑(f P) = ∑ Q ∈ f.support \ {P}, φ ↑(f Q)
⊢ ∑ Q ∈ f.support \ {P}, φ ↑(f Q) ∈ ⨆ j, ⨆ (_ : j ≠ P), (fun P ↦ primaryComponent M₂ P.asIdeal) j
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
x y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
x✝¹ x✝ : NonarchAddGroupSeminorm E
h' : x✝¹ ≤ x✝
⊢ x✝¹ x ≤ x✝ x

Tactic:
exact h' _

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
x y : E
hs : s.Nonempty
this : Nonempty ↑s
p : ↑s
x✝¹ x✝ : NonarchAddGroupSeminorm E
h' : x✝¹ ≤ x✝
⊢ x✝¹ y ≤ x✝ y

Tactic:
exact h' _

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

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

Tactic:
rintro rfl

Goal state after:
⊢ 0 < ∞
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case mp
x : EReal
⊢ x = ⊤ → ∀ (y : ℝ), ↑y < x

Tactic:
rintro rfl

Goal state after:
case mp
⊢ ∀ (y : ℝ), ↑y < ⊤
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case mp
x : EReal
⊢ x = ⊥ → ∀ (y : ℝ), x < ↑y

Tactic:
rintro rfl

Goal state after:
case mp
⊢ ∀ (y : ℝ), ⊥ < ↑y
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 I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
h_prod : I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors +
          (Associates.mk v.asIdeal).count (Associates.mk J').factors) -
      ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors +
          (Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a'})).factors) =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) +
      (↑((Associates.mk v.asIdeal).count (Associates.mk J').factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a'})).factors))

Tactic:
push_cast

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 I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
h_prod : I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')
⊢ ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) +
        ↑((Associates.mk v.asIdeal).count (Associates.mk J').factors) -
      (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) +
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a'})).factors)) =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) +
      (↑((Associates.mk v.asIdeal).count (Associates.mk J').factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a'})).factors))
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
hb₀ : b = 0 → a = 0
hb : b = ∞ → a = 0
⊢ a * b⁻¹ * b = a

Tactic:
obtain rfl | hb₀ := eq_or_ne b 0
  · simp_all
  obtain rfl | hb := eq_or_ne b ⊤
  · simp_all
  · simp [mul_assoc, ENNReal.inv_mul_cancel, *]

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

Goal state before:
pp: a b : ℝ≥0∞
h : a * b = 1
⊢ b ≠ ∞

Tactic:
rintro rfl

Goal state after:
a : ℝ≥0∞
h : a * ∞ = 1
⊢ False
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ⊢ 3⁻¹ + 3⁻¹ + 3⁻¹ = 1

Tactic:
rw [← ENNReal.mul_inv_cancel three_ne_zero ofNat_ne_top]
  ring

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

Goal state before:
pp: a b c : ℝ≥0∞
hc✝ : c < a * b
a' : ℝ≥0∞
hc : c / b < a'
ha' : a' < a
⊢ b ≠ 0

Tactic:
rintro rfl

Goal state after:
a c a' : ℝ≥0∞
ha' : a' < a
hc✝ : c < a * 0
hc : c / 0 < a'
⊢ False
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
hc✝ : c < a * b
a' : ℝ≥0∞
hc : c / b < a'
ha' : a' < a
⊢ c ≠ ∞

Tactic:
rintro rfl

Goal state after:
a b a' : ℝ≥0∞
ha' : a' < a
hc✝ : ∞ < a * b
hc : ∞ / b < a'
⊢ False
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
⊢ (𝓤 α).HasBasis p fun x ↦ {p | edist p.1 p.2 < f x}

Tactic:
refine ⟨fun s => uniformity_basis_edist.mem_iff.trans ?_⟩

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s) ↔ ∃ i, p i ∧ {p | edist p.1 p.2 < f i} ⊆ s
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
⊢ (𝓤 α).HasBasis p fun x ↦ {p | edist p.1 p.2 ≤ f x}

Tactic:
refine ⟨fun s => uniformity_basis_edist.mem_iff.trans ?_⟩

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s) ↔ ∃ i, p i ∧ {p | edist p.1 p.2 ≤ f i} ⊆ s
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case neg
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 J : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
this : J⁻¹ * I ≤ J⁻¹ * J
⊢ count K v J ≤ count K v I

Tactic:
rw [inv_mul_cancel₀ hJ, FractionalIdeal.le_one_iff_exists_coeIdeal] at this

Goal state after:
case neg
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 J : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
this : ∃ I_1, ↑I_1 = J⁻¹ * I
⊢ count K v J ≤ count K v I
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inr.inl.inr
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
hf : ¬∃ i, f i = 0
⊢ ⨅ i, ∞ * f i = ∞

Tactic:
iInf_eq_top

Goal state after:
case inr.inl.inr
ι : Sort u_1
f : ι → ℝ≥0∞
hinfty : ∞ = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : ∞ = 0 → Nonempty ι
ha₀ : ∞ ≠ 0
hf : ¬∃ i, f i = 0
⊢ ∀ (i : ι), ∞ * f i = ∞
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x₁ y₁ x₂ y₂ : α
⊢ dist x₂ y₂ ≤ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂)

Tactic:
by
  rw [add_left_comm, dist_comm x₁, ← add_assoc]
  apply dist_triangle4

Goal state after: