mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: case mpr
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [Small.{w, u} B] [inst_2 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial Ω[A⁄R]
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
f : Ideal (A ⊗[R] A ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) :=
  RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom
⊢ ↑f₁ = ↑f₂

Tactic:
refine H
      (RingHom.ker (TensorProduct.lmul' R (S := A)).kerSquareLift.toRingHom) ?_ ?_

Goal state after:
case mpr.refine_1
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [Small.{w, u} B] [inst_2 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial Ω[A⁄R]
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
f : Ideal (A ⊗[R] A ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) :=
  RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom
⊢ RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom ^ 2 = ⊥

case mpr.refine_2
R : Type v
inst✝³ : CommRing R
A : Type u
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Small.{w, u} A
H :
  ∀ ⦃B : Type u⦄ [inst : CommRing B] [Small.{w, u} B] [inst_2 : Algebra R B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
h : Nontrivial Ω[A⁄R]
f₁ f₂ : { f // (TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R A }
e : f₁ ≠ f₂
f : Ideal (A ⊗[R] A ⧸ RingHom.ker (TensorProduct.lmul' R).toRingHom ^ 2) :=
  RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom
⊢ (Ideal.Quotient.mkₐ R (RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom)).comp ↑f₁ =
    (Ideal.Quotient.mkₐ R (RingHom.ker (TensorProduct.lmul' R).kerSquareLift.toRingHom)).comp ↑f₂
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
⊢ (∑ a ∈ f.support, (b.repr (x * f a)).sum fun b' c ↦ c • b b' ⊗ₜ[R] b a) =
    ∑ a_1 ∈ f.support.biUnion fun i ↦ (a i).support,
      (b.repr (f.sum fun i y ↦ (a i) a_1 • y)).sum fun b' c ↦ c • b b' ⊗ₜ[R] b a_1

Tactic:
trans (x ⊗ₜ 1) * elem R S
      · simp_rw [this, hf, Finsupp.sum, Finset.mul_sum, TensorProduct.tmul_mul_tmul, one_mul]
      · rw [← one_tmul_mul_elem, hf, finite_of_free_aux]
        rfl

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
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : FormallySmooth R P
inst✝¹ : Algebra P A
inst✝ : IsScalarTower R P A
hf : Function.Surjective ⇑(algebraMap P A)
⊢ (Subsingleton (H1Cotangent R A) ∧ ∃ i, mapBaseChange R P A ∘ₗ i = LinearMap.id) ↔
    ∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id

Tactic:
← kerCotangentToTensor_injective_iff hf

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
P : Type u_2
inst✝⁴ : CommRing P
inst✝³ : Algebra R P
inst✝² : FormallySmooth R P
inst✝¹ : Algebra P A
inst✝ : IsScalarTower R P A
hf : Function.Surjective ⇑(algebraMap P A)
⊢ (Function.Injective ⇑(kerCotangentToTensor R P A) ∧ ∃ i, mapBaseChange R P A ∘ₗ i = LinearMap.id) ↔
    ∃ l, l ∘ₗ kerCotangentToTensor R P A = LinearMap.id
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: 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 σ
⊢ Function.Exact
    ⇑(SnakeLemma.δ' (LinearMap.baseChange T P.toExtension.cotangentComplex) (Q.comp P).toExtension.cotangentComplex
        Q.toExtension.cotangentComplex
        (LinearMap.liftBaseChange T (Extension.Cotangent.map (Q.toComp P).toExtensionHom))
        (Extension.Cotangent.map (Q.ofComp P).toExtensionHom) ⋯
        (LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
        (Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) ⋯ ⋯ ⋯ Extension.h1Cotangentι ⋯
        (LinearMap.baseChange T P.toExtension.toKaehler) ⋯ ⋯ ⋯)
    ⇑(mapBaseChange R S T)

Tactic:
apply SnakeLemma.exact_δ_left (π₂ := (Q.comp P).toExtension.toKaehler)
    (hπ₂ := (Q.comp P).toExtension.exact_cotangentComplex_toKaehler)

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 σ
⊢ mapBaseChange R S T ∘ₗ LinearMap.baseChange T P.toExtension.toKaehler =
    (Q.comp P).toExtension.toKaehler ∘ₗ
      LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)

case h
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 σ
⊢ Function.Surjective ⇑(LinearMap.baseChange T P.toExtension.toKaehler)
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
x : A
hx : IsNilpotent x
f : A →ₐ[K] AlgebraicClosure K ⊗[K] A := TensorProduct.includeRight
this✝ :
  ⇑f = ⇑(LinearMap.rTensor A (ofId K (AlgebraicClosure K)).toLinearMap ∘ₗ (TensorProduct.lid K A).symm.toLinearMap)
this : Function.Injective ⇑(LinearMap.rTensor A (ofId K (AlgebraicClosure K)).toLinearMap)
⊢ Function.Injective
    ⇑(LinearMap.rTensor A (ofId K (AlgebraicClosure K)).toLinearMap ∘ₗ (TensorProduct.lid K A).symm.toLinearMap)

Tactic:
by
      exact this.comp (Algebra.TensorProduct.lid K A).symm.injective

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
inst✝ : Algebra.FormallyEtale S T
⊢ Function.Bijective ⇑(lift (↑S ((Algebra.linearMap T (Module.End T (Ω[S⁄R] →ₗ[S] Ω[T⁄R]))).flip (map R R S T))))

Tactic:
convert! (tensorKaehlerEquivOfFormallyEtale R S T).bijective using 1

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✝ : Algebra.FormallyEtale S T
⊢ ⇑(lift (↑S ((Algebra.linearMap T (Module.End T (Ω[S⁄R] →ₗ[S] Ω[T⁄R]))).flip (map R R S T)))) =
    ⇑(tensorKaehlerEquivOfFormallyEtale R S T)
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
⊢ ¬q ^ 2 ∣ p

Tactic:
rw [pow_two]

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
⊢ ¬q * q ∣ p
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case e'_5
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₂
τ : Type w₅
Q : Generators S T ι
P : Generators R S σ
W : Generators R T τ
inst✝ : Flat S T
f : W.Hom Q
g : P.Hom W
⊢ Extension.H1Cotangent.map f.toExtensionHom ∘ₗ ↑(equiv W (Q.comp P)).symm =
    Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom

Tactic:
· change (Extension.H1Cotangent.map f.toExtensionHom).restrictScalars T ∘ₗ
      (Extension.H1Cotangent.map _) = _
    rw [← Extension.H1Cotangent.map_comp, Extension.H1Cotangent.map_eq]

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✝¹ : AddCommMonoid M
inst✝ : Module A M
x : M
⊢ x ∈ primaryComponent M I ↔ ∃ n, x ∈ torsionBySet A M ↑(I ^ n)

Tactic:
by
  simp only [primaryComponent, mem_torsionBySet_iff, SetLike.coe_sort_coe, Subtype.forall]
  constructor
  · intro a
    rw [Submodule.mem_iSup_of_directed] at a
    · simpa using a
    · intro x y
      use max x y
      simp [torsionBySet_le_torsionBySet_pow]
  · aesop (add safe Submodule.mem_iSup_of_mem)

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

Goal state before:
pp: case refine_2
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⟩
y : ℝ
h : y ∈ upperBounds s
⊢ mk g ≤ y

Tactic:
· 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.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_2
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
⊢ ⨅ q, f ↑↑q ≤ ⨅ r, f ↑r

Tactic:
· refine le_ciInf fun q => ?_
    have hq := q.prop
    rw [mem_Ioi] at hq
    obtain ⟨y, hxy, hyq⟩ := exists_rat_btwn hq
    refine (ciInf_le ?_ ?_).trans ?_
    · refine ⟨hf.some, fun z => ?_⟩
      rintro ⟨u, rfl⟩
      suffices hfu : f u ∈ f '' Ioi x from hf.choose_spec hfu
      exact ⟨u, u.prop, rfl⟩
    · exact ⟨y, hxy⟩
    · refine hf_mono (le_trans ?_ hyq.le)
      norm_cast

Goal state after:
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.den + 1 ≤ ↑q

Tactic:
← le_sub_iff_add_le,

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

Goal state before:

Tactic:
((2 * k ^ 2 : ℕ) + 1 : ℝ) ≤ 2 ^ (2 * k) := mod_cast Nat.two_mul_sq_add_one_le_two_pow_two_mul _
    _ = (1 / k * k + 1 : ℝ) ^ (2 * k) := by simp [posk.ne']; norm_num
    _ ≤ ((1 / k + 1) ^ k : ℝ) ^ (2 * k) := by gcongr; exact mul_add_one_le_add_one_pow (by simp) _
    _ = (1 / k + 1 : ℝ) ^ (2 * k ^ 2) := by rw [← pow_mul, mul_left_comm, sq]
    _ < a ^ (2 * k ^ 2) := by gcongr

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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : (algebraMap R K) ↑d ≠ 0
⊢ ¬((algebraMap R K) n = 0 ∨ (algebraMap R K) ↑d = 0)

Tactic:
not_or

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
n : R
hn : n ≠ 0
d : ↥R⁰
hd_ne_zero : (algebraMap R K) ↑d ≠ 0
⊢ ¬(algebraMap R K) n = 0 ∧ ¬(algebraMap R K) ↑d = 0
Module: Mathlib.Order.Interval.Set.OrdConnectedComponent

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
⊢ s.ordConnectedComponent x = ∅ ↔ x ∉ s

Tactic:
← not_nonempty_iff_eq_empty,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
⊢ ¬(s.ordConnectedComponent x).Nonempty ↔ x ∉ s
Module: Mathlib.Data.ENNReal.Operations

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

Tactic:
induction a <;> simp [← coe_sub]

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

Goal state before:
pp: case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ (∀ (i : ι), a.toReal ≤ f i) ↔ ∀ (i : ι), a ≤ ENNReal.ofReal (f i)

pp: case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ 0 ≤ ⨅ i, f i

Tactic:
· exact forall_congr' fun i ↦ (le_ofReal_iff_toReal_le ha (h _)).symm

Goal state after:
case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ 0 ≤ ⨅ i, f i
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: s : Set ℝ≥0∞
a : ℝ≥0∞
hs : s.Nonempty
⊢ a + ⨆ a ∈ s, a = ⨆ b ∈ s, a + b

Tactic:
add_biSup hs

Goal state after:
s : Set ℝ≥0∞
a : ℝ≥0∞
hs : s.Nonempty
⊢ ⨆ i ∈ s, a + i = ⨆ b ∈ s, a + b
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
⊢ count K v (I * I') = count K v I + count K v I'

Tactic:
have hJ_ne_zero : Associates.mk J ≠ 0 := Associates.mk_ne_zero.mpr (ideal_factor_ne_zero hI haJ)

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
⊢ count K v (I * I') = count K v I + count K v I'
Module: Mathlib.Data.ENNReal.Inv

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

Tactic:
← inv_inj,

Goal state after:
a : ℝ≥0∞
⊢ a⁻¹⁻¹ = 1⁻¹ ↔ a = 1
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ∞
h : b = c / a
⊢ a * b = c

Tactic:
rw [h, ENNReal.mul_div_cancel ha ha']

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

Goal state before:
pp: ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ∞
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
this✝ : Nonempty { a // f a ≠ ∞ }
this : Nonempty κ
hg : ⨅ j, g j ≠ ∞
i : ι
hi : f i ≠ ∞
⊢ a ≤ f ↑⟨i, hi⟩ * ⨅ j, g j

Tactic:
simpa [mul_iInf fun h ↦ (hi h).elim] using ha i

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ ball x ε = ∅ ↔ ε ≤ 0

Tactic:
← not_nonempty_iff_eq_empty,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ ¬(ball x ε).Nonempty ↔ ε ≤ 0
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ closedBall x ε = ∅ ↔ ε < 0

Tactic:
← not_nonempty_iff_eq_empty,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ ¬(closedBall x ε).Nonempty ↔ ε < 0
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: case refine_2
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0
hε : ↑ε > 0
⊢ {p | ↑(d p.1 p.2) < ↑ε} ∈ ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | ↑(d p.1 p.2) < ε}

Tactic:
refine mem_iInf_of_mem (ε : ℝ≥0∞) (mem_iInf_of_mem (ENNReal.coe_pos.2 hε) ?_)

Goal state after:
case refine_2
α : Type u_3
d : α → α → ℝ≥0
ε : ℝ≥0
hε : ↑ε > 0
⊢ {p | ↑(d p.1 p.2) < ↑ε} ∈ 𝓟 {p | ↑(d p.1 p.2) < ↑ε}
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

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

Tactic:
rw [← eball_ofReal]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ eball x ↑ε = eball x (ENNReal.ofReal ↑ε)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
x : Filter β
a : α
⊢ Tendsto f x (𝓝 a) ↔ Tendsto (fun b ↦ dist (f b) a) x (𝓝 0)

Tactic:
← nhds_comap_dist a,

Goal state after:
α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
x : Filter β
a : α
⊢ Tendsto f x (comap (fun x ↦ dist x a) (𝓝 0)) ↔ Tendsto (fun b ↦ dist (f b) a) x (𝓝 0)
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: case base
α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n : ℕ
⊢ dist (f m) (f m) ≤ ∑ i ∈ Finset.Ico m m, dist (f i) (f (i + 1))

Tactic:
Finset.Ico_self,

Goal state after:
case base
α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n : ℕ
⊢ dist (f m) (f m) ≤ ∑ i ∈ ∅, dist (f i) (f (i + 1))
Module: Mathlib.Topology.Metrizable.Basic

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
t : Set X
hts : t ⊆ s
htc : t.Countable
hst : s ⊆ closure[inst✝¹] t
⊢ SeparableSpace ↑s

Tactic:
lift t to Set s using hts

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
t : Set ↑s
htc : (Subtype.val '' t).Countable
hst : s ⊆ closure[inst✝¹] (Subtype.val '' t)
⊢ SeparableSpace ↑s
Module: Mathlib.Topology.Bornology.Constructions

Goal state before:
pp: α : Type u_1
inst✝ : Bornology α
s : Set α
⊢ IsBounded (s ×ˢ s) ↔ IsBounded s

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | hs); · simp
  exact (isBounded_prod_of_nonempty (hs.prod hs)).trans and_self_iff

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

Goal state before:
pp: case base
α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
⊢ edist (f m) (f m) ≤ ∑ i ∈ Finset.Ico m m, edist (f i) (f (i + 1))

Tactic:
Finset.Ico_self,

Goal state after:
case base
α : Type u
inst✝ : PseudoEMetricSpace α
f : ℕ → α
m n : ℕ
⊢ edist (f m) (f m) ≤ ∑ i ∈ ∅, edist (f i) (f (i + 1))
Module: Mathlib.Analysis.Normed.Group.Real

Goal state before:
pp: r : ℝ
hr : 0 ≤ r
⊢ ‖r‖ₑ = ENNReal.ofReal r

Tactic:
← ofReal_norm,

Goal state after:
r : ℝ
hr : 0 ≤ r
⊢ ENNReal.ofReal ‖r‖ = ENNReal.ofReal r
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
s✝ t : Set α
inst✝⁵ : Bornology α
inst✝⁴ : Preorder α
inst✝³ : IsOrderBornology α
β : Type u_2
inst✝² : Preorder β
inst✝¹ : Bornology β
inst✝ : IsOrderBornology β
s : Set (α × β)
⊢ (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ IsBounded (snd '' s) ↔
    (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ BddBelow (snd '' s) ∧ BddAbove (snd '' s)

Tactic:
isBounded_iff_bddBelow_bddAbove

Goal state after:
α : Type u_1
s✝ t : Set α
inst✝⁵ : Bornology α
inst✝⁴ : Preorder α
inst✝³ : IsOrderBornology α
β : Type u_2
inst✝² : Preorder β
inst✝¹ : Bornology β
inst✝ : IsOrderBornology β
s : Set (α × β)
⊢ (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ BddBelow (snd '' s) ∧ BddAbove (snd '' s) ↔
    (BddBelow (fst '' s) ∧ BddAbove (fst '' s)) ∧ BddBelow (snd '' s) ∧ BddAbove (snd '' s)
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α✝ : Type u_1
s✝ t : Set α✝
inst✝⁵ : Bornology α✝
inst✝⁴ : Preorder α✝
inst✝³ : IsOrderBornology α✝
ι : Type u_2
α : ι → Type u_3
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → Bornology (α i)
inst✝ : ∀ (i : ι), IsOrderBornology (α i)
s : Set ((i : ι) → α i)
⊢ (∀ (i : ι), IsBounded (Function.eval i '' s)) ↔
    ∀ (x : ι), BddBelow (Function.eval x '' s) ∧ BddAbove (Function.eval x '' s)

Tactic:
isBounded_iff_bddBelow_bddAbove

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

Goal state before:
pp: α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
s : Set α
hs : IsBounded sᶜ
⊢ s ∈ Filter.atTop

Tactic:
isBounded_iff_bddBelow_bddAbove

Goal state after:
α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
s : Set α
hs : BddBelow sᶜ ∧ BddAbove sᶜ
⊢ s ∈ Filter.atTop
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 I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * (J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I) = J
H' : ¬I'.divMod I J' = 0
⊢ ↑I ⊓ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ≤ ↑J

Tactic:
mul_inf₀
      (zero_le _),

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 I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this :
  (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓
      (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * (spanSingleton R⁰ (I'.divMod I J') * I) =
    J
H' : ¬I'.divMod I J' = 0
⊢ ↑I ⊓ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ≤ ↑J
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: case mpr
α : Type u
β : Type v
inst✝² : PseudoMetricSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
γ : Type u_3
F : β → γ → α
s : Set γ
⊢ (∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε) → UniformCauchySeqOn F atTop s

Tactic:
· intro h u hu
    rcases Metric.mem_uniformity_dist.mp hu with ⟨ε, hε, hab⟩
    rcases h ε hε with ⟨N, hN⟩
    rw [prod_atTop_atTop_eq, eventually_atTop]
    use (N, N)
    intro b hb x hx
    rcases hb with ⟨hbl, hbr⟩
    exact hab (hN b.fst hbl.ge b.snd hbr.ge x hx)

Goal state after:
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n ↦ diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N ↦ ⋯.some
n N : ℕ
⊢ n ≤ N → u N ∈ s n

Tactic:
hn

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → Set α
h0 : IsComplete (s 0)
hs : ∀ (n : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s n)
h's : ∀ (n : ℕ), Bornology.IsBounded (s n)
h : ∀ (N : ℕ), (⋂ n, ⋂ (_ : n ≤ N), s n).Nonempty
h' : Tendsto (fun n ↦ diam (s n)) atTop (𝓝 0)
u : ℕ → α := fun N ↦ ⋯.some
n N : ℕ
hn : n ≤ N
⊢ u N ∈ s n