mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.LocalRing.Length

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

Tactic:
by_cases h : IsFiniteLength B M
  · obtain ⟨s, hs_bot, hs_top⟩ := isFiniteLength_iff_exists_compositionSeries.mp h
    rw [← length_compositionSeries s hs_bot hs_top]
    suffices ∀ k, length A (s k) = k * Module.length (ResidueField A) (ResidueField B) by
      rw [← Fin.val_last s.length, ← this, ← RelSeries.last, hs_top]
      exact length_top.symm
    intro k
    induction k using Fin.induction with
    | zero => rw [← RelSeries.head, hs_bot]; simp
    | succ i hi => simpa [hi, add_one_mul] using (s.step i).length_restrictScalars A
  · have : ¬ IsFiniteLength A M := by
      contrapose! h
      rw [isFiniteLength_iff_isNoetherian_isArtinian] at h ⊢
      exact h.imp (isNoetherian_of_tower A) (isArtinian_of_tower A)
    rw [← length_ne_top_iff, not_ne_iff] at h this
    have ne : length (ResidueField A) (ResidueField B) ≠ 0 := by
      simpa [pos_iff_ne_zero] using Module.length_pos
    rw [h, this, ENat.top_mul ne]

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

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
inst✝ : IsDedekindDomain S
hp : map f p ≠ ⊥
hP : P.IsPrime
⊢ p.ramificationIdx' P = multiplicity P (map f p)

Tactic:
by_cases hP₂ : P = ⊥
  · rw [hP₂, ← Ideal.zero_eq_bot, multiplicity_zero_eq_zero_of_ne_zero _ hp]
    exact Ideal.ramificationIdx'_of_not_le (mt le_bot_iff.mp hp)
  rw [multiplicity_eq_of_emultiplicity_eq_some]
  rw [ramificationIdx'_eq_normalizedFactors_count hp hP hP₂, ← normalize_eq P,
    ← UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors _ hp, normalize_eq]
  exact irreducible_iff_prime.mpr <| prime_of_isPrime hP₂ hP

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

Goal state before:
pp: case h₁
R : Type v
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w
inst✝¹ : CommRing B
inst✝ : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ ⦃S : Type w⦄ [inst : CommRing S] (I : Ideal S),
    I ^ 2 = ⊥ → ∀ [inst_1 : Algebra R S], Function.Injective (Ideal.Quotient.mkₐ R I).comp

pp: case h₂
R : Type v
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w
inst✝¹ : CommRing B
inst✝ : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ ⦃S : Type w⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ [inst_1 : Algebra R S], Function.Injective (Ideal.Quotient.mkₐ R I).comp) →
        (∀ [inst_1 : Algebra R (S ⧸ I)],
            Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
          ∀ [inst_1 : Algebra R S], Function.Injective (Ideal.Quotient.mkₐ R J).comp

Tactic:
· intro B _ I hI _; exact FormallyUnramified.comp_injective I hI

Goal state after:
case h₂
R : Type v
inst✝⁴ : CommRing R
A : Type u
inst✝³ : CommRing A
inst✝² : Algebra R A
B : Type w
inst✝¹ : CommRing B
inst✝ : FormallyUnramified R A
I : Ideal B
hI : IsNilpotent I
⊢ ∀ ⦃S : Type w⦄ [inst : CommRing S] (I J : Ideal S),
    I ≤ J →
      (∀ [inst_1 : Algebra R S], Function.Injective (Ideal.Quotient.mkₐ R I).comp) →
        (∀ [inst_1 : Algebra R (S ⧸ I)],
            Function.Injective (Ideal.Quotient.mkₐ R (Ideal.map (Ideal.Quotient.mk I) J)).comp) →
          ∀ [inst_1 : Algebra R S], Function.Injective (Ideal.Quotient.mkₐ R J).comp
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case mp.refine_2
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}
⊢ e ∈ Ideal.span {e}

Tactic:
Ideal.mem_span_singleton

Goal state after:
case mp.refine_2
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}
⊢ e ∣ e
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : CommRing T
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
M : Submonoid S
inst✝¹ : IsLocalization M T
inst✝ : QuasiFinite R S
P : Ideal S
hP : P.IsPrime
p : P.ResidueField
s : S
t : ↥M
ht : ¬(algebraMap S P.ResidueField) ↑t = 0
⊢ (s • p) ⊗ₜ[S] 1 = (fun x ↦ x * TensorProduct.includeRight ((algebraMap S T) ↑t)) (p ⊗ₜ[S] IsLocalization.mk' T s t)

Tactic:
· dsimp; simp [Algebra.algebraMap_eq_smul_one, smul_tmul]

Goal state after:
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
s : S
⊢ 1 ⊗ₜ[R] s * elem R S = s ⊗ₜ[R] 1 * elem R S

Tactic:
rw [← sub_eq_zero, ← sub_mul, one_tmul_sub_tmul_one_mul_elem]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
B : Type u_1
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u_4
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker g)
x : A
| (Ideal.quotientKerAlgEquivOfSurjective hg).symm (f x)

Tactic:
rw [← AlgEquiv.coe_toAlgHom, ← AlgHom.comp_apply,
    ← FormallySmooth.mk_lift (A := A) _ hg']

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
B : Type u_1
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u_4
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker g)
x : A
| (Ideal.Quotient.mk (RingHom.ker g))
    ((lift (RingHom.ker g) hg' ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm).comp f)) x)
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : FiniteType R S
p : Ideal R
inst✝⁵ : p.IsPrime
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : q.LiesOver p
inst✝² : QuasiFiniteAt R q
inst✝¹ : Algebra (Localization.AtPrime p) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra p q
q' : Ideal (p.Fiber S) := ((PrimeSpectrum.primesOverOrderIsoFiber R S p) ⟨q, ⋯⟩).asIdeal
hq' : q = Ideal.comap TensorProduct.includeRight.toRingHom q'
this✝ : QuasiFiniteAt p.ResidueField q'
this : q'.IsMaximal
⊢ (Ideal.ResidueField.map q q' TensorProduct.includeRight.toRingHom hq').comp
      ↑(TensorProduct.lift (ofId p.ResidueField q.ResidueField) (IsScalarTower.toAlgHom R S q.ResidueField) ⋯) =
    algebraMap (p.Fiber S) q'.ResidueField

Tactic:
ext <;> simp [IsScalarTower.algebraMap_apply R S q.ResidueField]

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
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
x : P.Ring ⧸ RingHom.ker f.toRingHom ^ 2
⊢ (↑f.kerSquareLift).kerLift ((Ideal.Quotient.mk (RingHom.ker f.kerSquareLift)) x) =
    (Ideal.quotientKerAlgEquivOfSurjective surj) ((Ideal.Quotient.mk (RingHom.ker f.kerSquareLift)) x)

Tactic:
simp only [Ideal.quotientKerAlgEquivOfSurjective_apply]

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

Goal state before:
pp: case monomial.add
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₁
Q : Generators S T ι
n : ι →₀ ℕ
r : S
y₁ y₂ : MvPolynomial ι S
hy₁ : (δAux R Q) ((monomial n) r * y₁) = (monomial n) r • (δAux R Q) y₁ + y₁ • (δAux R Q) ((monomial n) r)
hy₂ : (δAux R Q) ((monomial n) r * y₂) = (monomial n) r • (δAux R Q) y₂ + y₂ • (δAux R Q) ((monomial n) r)
⊢ (δAux R Q) ((monomial n) r * (y₁ + y₂)) =
    (monomial n) r • (δAux R Q) (y₁ + y₂) + (y₁ + y₂) • (δAux R Q) ((monomial n) r)

Tactic:
simp only [map_add, smul_add, hy₁, hy₂, mul_add, add_smul]; abel

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ unramifiedLocus R A = Set.univ ↔ FormallyUnramified R A

Tactic:
rw [unramifiedLocus_eq_compl_support, compl_eq_comm, Set.compl_univ, eq_comm,
    Module.support_eq_empty_iff, Algebra.formallyUnramified_iff]

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' : m * q ∈ Ideal.span {p}
⊢ ¬q ^ 2 ∣ p

Tactic:
Ideal.mem_span_singleton

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 ^ 2 ∣ p
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: S : Type u_1
inst✝⁵ : CommRing S
q : Ideal S
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R S
inst✝² : q.IsPrime
inst✝¹ : Algebra.EssFiniteType R S
inst✝ : Algebra.IsUnramifiedAt R q
⊢ q.ramificationIdx R = 1

Tactic:
by
  let p := q.under R
  let Rp := Localization.AtPrime p
  let Sq := Localization.AtPrime q
  let : Algebra Rp Sq := Localization.AtPrime.algebraOfLiesOver p q
  have : Algebra.EssFiniteType Rp Sq := Algebra.EssFiniteType.of_comp R Rp Sq
  rw [ramificationIdx_def, ENat.toNat_eq_iff_eq_natCast, Nat.cast_one, Module.length_eq_one_iff,
    isSimpleModule_iff_isCoatom, ← Ideal.isMaximal_def, IsLocalRing.isMaximal_iff,
    IsScalarTower.algebraMap_eq R Rp Sq, ← map_map, Localization.AtPrime.map_eq_maximalIdeal]
  exact Algebra.FormallyUnramified.map_maximalIdeal

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
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)
x : Localization.AtPrime q
a : Localization.AtPrime p
ha :
  (algebraMap (Localization.AtPrime q) q.ResidueField)
      ((algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) a) =
    (algebraMap (Localization.AtPrime q) q.ResidueField) x
⊢ x ∈
    (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)).range ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q))

Tactic:
ResidueField.algebraMap_eq,

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)
x : Localization.AtPrime q
a : Localization.AtPrime p
ha :
  (residue (Localization.AtPrime q)) ((algebraMap (Localization.AtPrime p) (Localization.AtPrime q)) a) =
    (residue (Localization.AtPrime q)) x
⊢ x ∈
    (Algebra.linearMap (Localization.AtPrime p) (Localization.AtPrime q)).range ⊔
      Submodule.restrictScalars (Localization.AtPrime p) (maximalIdeal (Localization.AtPrime q))
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁴ : CommRing A
I : Ideal A
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
φ : M₁ →ₗ[A] M₂
⊢ Submodule.map (primaryComponent M₁ I).subtype (map I φ).ker =
    Submodule.map φ.ker.subtype (primaryComponent (↥φ.ker) I)

Tactic:
aesop (add norm [map, Subtype.ext_iff, primaryComponent_mem])

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

Goal state before:
pp: ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ
⊢ ⨅ i, f i = 0

Tactic:
iInf_of_isEmpty,

Goal state after:
ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ
⊢ sInf ∅ = 0
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: p q : ℝ
hp : 0 ≤ p
⊢ ↑(p * q).toNNReal = ↑(p.toNNReal * q.toNNReal)

Tactic:
simp [mul_max_of_nonneg, hp]

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

Goal state before:
pp: n : ℕ
⊢ (↑n).toReal = ↑n

Tactic:
rw [← ENNReal.ofReal_natCast n, ENNReal.toReal_ofReal (Nat.cast_nonneg _)]

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

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
h : a.toNNReal ≤ b.toNNReal
⊢ ↑a.toNNReal ≤ b

Tactic:
← coe_toNNReal hb,

Goal state after:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
h : a.toNNReal ≤ b.toNNReal
⊢ ↑a.toNNReal ≤ ↑b.toNNReal
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
h : a.toNNReal < b.toNNReal
⊢ ↑a.toNNReal < b

Tactic:
← coe_toNNReal hb,

Goal state after:
a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
h : a.toNNReal < b.toNNReal
⊢ ↑a.toNNReal < ↑b.toNNReal
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: s : Set ℝ≥0∞
hf : ∀ r ∈ s, r ≠ ∞
⊢ (sInf s).toReal = sInf (ENNReal.toReal '' s)

Tactic:
by
  simp only [ENNReal.toReal, toNNReal_sInf s hf, NNReal.coe_sInf, Set.image_image]

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

Goal state before:
pp: ι : Sort u_1
a : ℝ≥0∞
p : ι → Prop
h : ∃ i, p i
f : ι → ℝ≥0∞
⊢ a + ⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), a + f i

Tactic:
have : Nonempty {i // p i} := nonempty_subtype.2 h
  simp only [iSup_subtype', add_iSup]

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

Goal state before:
pp: x y : EReal
⊢ x * y = y * x

Tactic:
by
  induction x <;> induction y <;>
    try { rfl }
  rw [← coe_mul, ← coe_mul, mul_comm]

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

Goal state before:
pp: case pos
x : EReal
h : x ≠ ⊥
h' : x = ⊤
⊢ ↑x.toReal ≤ x

Tactic:
simp only [h', le_top]

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

Goal state before:
pp: case inr
x : EReal
hx : x ≤ 0
⊢ ↑0 = max 0 x

Tactic:
max_eq_left hx,

Goal state after:
case inr
x : EReal
hx : x ≤ 0
⊢ ↑0 = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ⊢ 1 - 2⁻¹ = 2⁻¹

Tactic:
by
  rw [← one_div, sub_half one_ne_top]

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

Goal state before:
pp: γ : Type u_3
U : UniformSpace γ
m : MetricSpace γ
H : 𝓤 γ = 𝓤 γ
⊢ m.replaceUniformity H = m

Tactic:
by
  ext; rfl

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

Goal state before:
pp: γ : Type u_3
U : TopologicalSpace γ
m : MetricSpace γ
H : U = PseudoMetricSpace.toUniformSpace.toTopologicalSpace
⊢ m.replaceTopology H = m

Tactic:
by
  ext; rfl

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

Goal state before:
pp: case mp
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
a1 : ℝ
a2 : a1 > 0
a3 : ι → Prop
a4 : ∀ᶠ (i : ι) in f, a3 i
a5 : ∀ ⦃x : α⦄, dist x x₀ < a1 → ∀ ⦃i : ι⦄, a3 i → p (x, i).swap
⊢ ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)

Tactic:
exact ⟨a3, a4, a1, a2, fun _ b1 b2 b3 => a5 b3 b1⟩

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

Goal state before:
pp: case mpr
α : Type u
ι : Type u_2
inst✝ : PseudoMetricSpace α
f : Filter ι
x₀ : α
p : ι × α → Prop
a1 : ι → Prop
a2 : ∀ᶠ (i : ι) in f, a1 i
a3 : ℝ
a4 : a3 > 0
a5 : ∀ ⦃i : ι⦄, a1 i → ∀ ⦃x : α⦄, dist x x₀ < a3 → p (i, x)
⊢ ∃ ε > 0, ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i).swap

Tactic:
exact ⟨a3, a4, a1, a2, fun _ b1 b2 b3 => a5 b3 b1⟩

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
X : Type u_3
e : PseudoEMetricSpace X
dist : X → X → ℝ
dist_nonneg : ∀ (x y : X), 0 ≤ dist x y
h : ∀ (x y : X), edist x y = ENNReal.ofReal (dist x y)
x✝¹ x✝ : X
⊢ edist x✝¹ x✝ = ENNReal.ofReal (dist x✝¹ x✝)

Tactic:
by simp only [h]

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

Goal state before:
pp: case neg
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
h : ¬BddBelow s
⊢ sSup (a • s) = a • sInf s

Tactic:
Real.sSup_of_not_bddAbove (mt (bddAbove_smul_iff_of_neg ha').1 h),

Goal state after:
case neg
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
s : Set ℝ
hs : s.Nonempty
ha' : a < 0
h : ¬BddBelow s
⊢ 0 = a • sInf s
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: x r y : ℝ
⊢ y ∈ ball x r ↔ y ∈ Ioo (x - r) (x + r)

Tactic:
by
    rw [mem_ball, dist_comm, Real.dist_eq, abs_sub_lt_iff, mem_Ioo, ← sub_lt_iff_lt_add',
      sub_lt_comm]

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

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

Tactic:
by
  rw [nndist_comm]
  exact NNReal.nndist_zero_eq_val z

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

Goal state before:
pp: case refine_2
R✝ : Type u_1
inst✝⁸ : CommRing R✝
K✝ : Type u_2
inst✝⁷ : Field K✝
inst✝⁶ : Algebra R✝ K✝
inst✝⁵ : IsFractionRing R✝ K✝
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
a c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
H : Ideal.span {↑c.den} * a.num ≤ c.num * Ideal.span {↑a.den}
x : R
hx : Ideal.span {↑c.den} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {↑a.den}
⊢ a * FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑a.den * (algebraMap R K) ↑c.den) +
      FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) x) =
    c * FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑a.den * (algebraMap R K) ↑c.den)

Tactic:
← FractionalIdeal.spanSingleton_mul_spanSingleton,

Goal state after:
case refine_2
R✝ : Type u_1
inst✝⁸ : CommRing R✝
K✝ : Type u_2
inst✝⁷ : Field K✝
inst✝⁶ : Algebra R✝ K✝
inst✝⁵ : IsFractionRing R✝ K✝
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
a c : FractionalIdeal R⁰ K
hac : a ≤ c
ha : a ≠ 0
hb : 1 ≠ 0
H : Ideal.span {↑c.den} * a.num ≤ c.num * Ideal.span {↑a.den}
x : R
hx : Ideal.span {↑c.den} * a.num ⊔ Ideal.span {x} = c.num * Ideal.span {↑a.den}
⊢ a *
        (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑a.den) *
          FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑c.den)) +
      FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) x) =
    c *
      (FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑a.den) *
        FractionalIdeal.spanSingleton R⁰ ((algebraMap R K) ↑c.den))
Module: Mathlib.Analysis.Normed.Group.Constructions

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedGroup (G i)
f : (i : ι) → G i
r : ℝ
inst✝ : Nonempty ι
⊢ ‖f‖ ≤ r ↔ ∀ (b : ι), ‖f b‖ ≤ r

Tactic:
by_cases hr : 0 ≤ r
  · exact pi_norm_le_iff_of_nonneg' hr
  · exact
      iff_of_false (fun h => hr <| (norm_nonneg' _).trans h) fun h =>
        hr <| (norm_nonneg' _).trans <| h <| Classical.arbitrary _

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s
h_empty : t = ∅
⊢ s ∈ atBot

Tactic:
compl_univ_iff.mpr h_empty,

Goal state after:
case refine_1
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : univ ⊆ s
h_empty : t = ∅
⊢ s ∈ atBot
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ sInf (f '' [[a, b]]) ≤ sSup (f '' [[a, b]])

Tactic:
refine csInf_le_csSup (nonempty_uIcc.image _) ?_ ?_

Goal state after:
case refine_1
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddBelow (f '' [[a, b]])

case refine_2
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b : α
h : ContinuousOn f [[a, b]]
⊢ BddAbove (f '' [[a, b]])
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
⊢ ∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)

Tactic:
let S N := (fun p : ℕ × ℕ => dist (s p.1) (s p.2)) '' { p | p.1 ≥ N ∧ p.2 ≥ N }

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N ↦ (fun p ↦ dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
⊢ ∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)