mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ Function.Surjective
    ⇑(TensorProduct.lift (ofId p.ResidueField q.ResidueField) (IsScalarTower.toAlgHom R S q.ResidueField) ⋯)

Tactic:
let q' : Ideal (p.Fiber S) := (PrimeSpectrum.primesOverOrderIsoFiber R S p ⟨q, ‹_›, ‹_›⟩).asIdeal

Goal state after:
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
⊢ Function.Surjective
    ⇑(TensorProduct.lift (ofId p.ResidueField q.ResidueField) (IsScalarTower.toAlgHom R S q.ResidueField) ⋯)
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
P : Type u_2
C : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : CommRing C
inst✝³ : Algebra R C
inst✝² : CommRing P
inst✝¹ : Algebra R P
P₁ : Extension R A
P₂ : Extension R A
inst✝ : FormallySmooth R P₁.Ring
⊢ P₂.infinitesimal.ker ^ 2 = ⊥

Tactic:
ker_infinitesimal

Goal state after:
R : Type u
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_1
P : Type u_2
C : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : CommRing C
inst✝³ : Algebra R C
inst✝² : CommRing P
inst✝¹ : Algebra R P
P₁ : Extension R A
P₂ : Extension R A
inst✝ : FormallySmooth R P₁.Ring
⊢ P₂.ker.cotangentIdeal ^ 2 = ⊥
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
f : P →ₐ[R] A
hf : Function.Surjective ⇑f
⊢ FormallySmooth R A ↔ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A

Tactic:
let := f.toAlgebra

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
f : P →ₐ[R] A
hf : Function.Surjective ⇑f
this : Algebra P A := f.toAlgebra
⊢ FormallySmooth R A ↔ ∃ g, f.kerSquareLift.comp g = AlgHom.id R A
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 σ
⊢ ↑(compEquiv Q P).symm ∘ₗ LinearMap.inr T Q.toExtension.CotangentSpace (T ⊗[S] P.toExtension.CotangentSpace) =
    LinearMap.liftBaseChange T (Extension.CotangentSpace.map (Q.toComp P).toExtensionHom)

Tactic:
by
  classical
  apply (P.cotangentSpaceBasis.baseChange T).ext
  intro i
  apply (Q.comp P).cotangentSpaceBasis.repr.injective
  ext j
  simp only [compEquiv, LinearEquiv.trans_symm, LinearEquiv.symm_symm,
    Basis.baseChange_apply, LinearMap.coe_comp, LinearEquiv.coe_coe, LinearMap.coe_inr,
    Function.comp_apply, LinearEquiv.trans_apply, Basis.repr_symm_apply, pderiv_X, toComp_val,
    Basis.repr_linearCombination, LinearMap.liftBaseChange_tmul, one_smul, repr_CotangentSpaceMap]
  obtain (j | j) := j <;>
    simp only [Basis.prod_repr_inr, Basis.baseChange_repr_tmul,
      Basis.repr_self, Basis.prod_repr_inl, map_zero, Finsupp.coe_zero,
      Pi.zero_apply, ne_eq, not_false_eq_true, Pi.single_eq_of_ne, Pi.single_apply,
      Finsupp.single_apply, ite_smul, one_smul, zero_smul, Sum.inr.injEq,
      MonoidWithZeroHom.map_ite_one_zero, reduceCtorEq]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra R B
inst✝⁵ : IsScalarTower R A B
p : Ideal A
P : Ideal B
inst✝⁴ : P.LiesOver p
inst✝³ : p.IsPrime
inst✝² : P.IsPrime
inst✝¹ : IsUnramifiedAt R p
inst✝ : IsUnramifiedAt A P
this : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
⊢ IsUnramifiedAt R P

Tactic:
have : FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime P) :=
    .of_restrictScalars A _ _

Goal state after:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝¹¹ : CommRing R
inst✝¹⁰ : CommRing A
inst✝⁹ : CommRing B
inst✝⁸ : Algebra R A
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra R B
inst✝⁵ : IsScalarTower R A B
p : Ideal A
P : Ideal B
inst✝⁴ : P.LiesOver p
inst✝³ : p.IsPrime
inst✝² : P.IsPrime
inst✝¹ : IsUnramifiedAt R p
inst✝ : IsUnramifiedAt A P
this✝ : Algebra (Localization.AtPrime p) (Localization.AtPrime P) := Localization.AtPrime.algebraOfLiesOver p P
this : FormallyUnramified (Localization.AtPrime p) (Localization.AtPrime P)
⊢ IsUnramifiedAt R P
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
l : { l // l ∘ₗ kerToTensor R P S = LinearMap.id }
p s : P
this : ∀ (x y : S ⊗[P] Ω[P⁄R]), ↑(↑l x) * ↑(↑l y) = 0
⊢ (s - ↑(↑l (1 ⊗ₜ[P] (D R P) s))) * ↑(↑l (1 ⊗ₜ[P] (D R P) p)) = ↑(↑l ((algebraMap P S) s ⊗ₜ[P] (D R P) p))

Tactic:
rw [sub_mul]

Goal state after:
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
l : { l // l ∘ₗ kerToTensor R P S = LinearMap.id }
p s : P
this : ∀ (x y : S ⊗[P] Ω[P⁄R]), ↑(↑l x) * ↑(↑l y) = 0
⊢ s * ↑(↑l (1 ⊗ₜ[P] (D R P) p)) - ↑(↑l (1 ⊗ₜ[P] (D R P) s)) * ↑(↑l (1 ⊗ₜ[P] (D R P) p)) =
    ↑(↑l ((algebraMap P S) s ⊗ₜ[P] (D R P) p))
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
⊢ (algebraMap K L).range = ⊤

Tactic:
by
  classical
  have : Nontrivial (L ⊗[K] L) := by
    rw [← not_subsingleton_iff_nontrivial, ← rank_zero_iff (R := K), rank_tensorProduct',
      mul_eq_zero, or_self, rank_zero_iff, not_subsingleton_iff_nontrivial]
    infer_instance
  rw [← top_le_iff]
  intro x _
  obtain ⟨n, hn⟩ := IsPurelyInseparable.pow_mem K (ringExpChar K) x
  have : ExpChar (L ⊗[K] L) (ringExpChar K) := by
    refine expChar_of_injective_ringHom (algebraMap K _).injective (ringExpChar K)
  have : (1 ⊗ₜ x - x ⊗ₜ 1 : L ⊗[K] L) ^ (ringExpChar K) ^ n = 0 := by
    rw [sub_pow_expChar_pow, TensorProduct.tmul_pow, one_pow, TensorProduct.tmul_pow, one_pow]
    obtain ⟨r, hr⟩ := hn
    rw [← hr, algebraMap_eq_smul_one, TensorProduct.smul_tmul, sub_self]
  have H : (1 ⊗ₜ x : L ⊗[K] L) = x ⊗ₜ 1 := by
    have inst : IsReduced (L ⊗[K] L) := isReduced_of_field L _
    exact sub_eq_zero.mp (IsNilpotent.eq_zero ⟨_, this⟩)
  by_cases h' : LinearIndependent K ![1, x]
  · have h := h'.linearIndepOn_id
    let S := h.extend (Set.subset_univ _)
    let a : S := ⟨1, h.subset_extend _ (by simp)⟩
    have ha : Basis.extend h a = 1 := by simp [a]
    let b : S := ⟨x, h.subset_extend _ (by simp)⟩
    have hb : Basis.extend h b = x := by simp [b]
    by_cases e : a = b
    · obtain rfl : 1 = x := congr_arg Subtype.val e
      exact ⟨1, map_one _⟩
    have := DFunLike.congr_fun
      (DFunLike.congr_arg ((Basis.extend h).tensorProduct (Basis.extend h)).repr H) (a, b)
    simp only [Basis.tensorProduct_repr_tmul_apply, ← ha, ← hb, Basis.repr_self, smul_eq_mul,
      Finsupp.single_apply, e, Ne.symm e, ↓reduceIte, mul_one, mul_zero, one_ne_zero] at this
  · rw [LinearIndependent.pair_iff] at h'
    simp only [not_forall, not_and, exists_prop] at h'
    obtain ⟨a, b, e, hab⟩ := h'
    have : IsUnit b := by
      rw [isUnit_iff_ne_zero]
      rintro rfl
      rw [zero_smul, ← algebraMap_eq_smul_one, add_zero,
        (injective_iff_map_eq_zero' _).mp (algebraMap K L).injective] at e
      cases hab e rfl
    use (-this.unit⁻¹ * a)
    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.RamificationInertia.Ramification

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hq : q.IsPrime
hpS : map (algebraMap R S) p ≠ ⊥
hq' : q ≠ ⊥
this : q.IsMaximal
I : Ideal S
hqI : ¬I ≤ q
h :
  map (algebraMap R (Localization.AtPrime q)) p =
    map (algebraMap S (Localization.AtPrime q)) (q ^ p.ramificationIdx' q * I)
⊢ p.ramificationIdx' q = q.ramificationIdx R

Tactic:
Ideal.map_mul,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hq : q.IsPrime
hpS : map (algebraMap R S) p ≠ ⊥
hq' : q ≠ ⊥
this : q.IsMaximal
I : Ideal S
hqI : ¬I ≤ q
h :
  map (algebraMap R (Localization.AtPrime q)) p =
    map (algebraMap S (Localization.AtPrime q)) (q ^ p.ramificationIdx' q) *
      map (algebraMap S (Localization.AtPrime q)) I
⊢ p.ramificationIdx' q = q.ramificationIdx R
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✝¹ : Algebra.QuasiFinite R S
inst✝ : Fintype ↑(p.primesOver S)
this : Fintype (PrimeSpectrum (p.Fiber S)) := ⋯
⊢ ∀ x ∈ Finset.univ,
    (↑((primesOverOrderIsoFiber R S p).symm.toEquiv x)).ramificationIdx R *
        (↑((primesOverOrderIsoFiber R S p).symm.toEquiv x)).inertiaDeg R =
      finrank p.ResidueField (Localization.AtPrime x.asIdeal)

Tactic:
intro q _

Goal state after:
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✝¹ : Algebra.QuasiFinite R S
inst✝ : Fintype ↑(p.primesOver S)
this : Fintype (PrimeSpectrum (p.Fiber S)) := Fintype.ofFinite (PrimeSpectrum (p.Fiber S))
q : PrimeSpectrum (p.Fiber S)
a✝ : q ∈ Finset.univ
⊢ (↑((primesOverOrderIsoFiber R S p).symm.toEquiv q)).ramificationIdx R *
      (↑((primesOverOrderIsoFiber R S p).symm.toEquiv q)).inertiaDeg R =
    finrank p.ResidueField (Localization.AtPrime q.asIdeal)
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
inst✝ : q.LiesOver p
H✝ : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)
s✝ : Finset R
hs : Ideal.span ↑s✝ = RingHom.ker (algebraMap R S)
this : ∀ (x : ↥s✝), (algebraMap R (Localization.AtPrime p)) ↑x = 0
m : ↥s✝ → ↥p.primeCompl
hm : ∀ (x : ↥s✝), ↑(m x) * ↑x = 0
H : RingHom.ker (algebraMap R S) ≤ RingHom.ker (algebraMap R (Away ↑(∏ i, m i)))
r' s : R
e : r' = ↑(∏ i, m i) * s
x : R
w✝ : ↥(Submonoid.powers r')
n : ℕ
hn : (algebraMap R S) (r' ^ n * x) = 0
k : ℕ
hk : ↑⟨(fun x ↦ ↑(∏ i, m i) ^ x) k, ⋯⟩ * (r' ^ n * x) = 0
⊢ IsLocalization.mk' (Away r') x w✝ = 0

Tactic:
refine (IsLocalization.mk'_eq_zero_iff _ _).mpr ⟨⟨_, k + n, rfl⟩, ?_⟩

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
inst✝ : q.LiesOver p
H✝ : Function.Injective ⇑(localRingHom p q (algebraMap R S) ⋯)
s✝ : Finset R
hs : Ideal.span ↑s✝ = RingHom.ker (algebraMap R S)
this : ∀ (x : ↥s✝), (algebraMap R (Localization.AtPrime p)) ↑x = 0
m : ↥s✝ → ↥p.primeCompl
hm : ∀ (x : ↥s✝), ↑(m x) * ↑x = 0
H : RingHom.ker (algebraMap R S) ≤ RingHom.ker (algebraMap R (Away ↑(∏ i, m i)))
r' s : R
e : r' = ↑(∏ i, m i) * s
x : R
w✝ : ↥(Submonoid.powers r')
n : ℕ
hn : (algebraMap R S) (r' ^ n * x) = 0
k : ℕ
hk : ↑⟨(fun x ↦ ↑(∏ i, m i) ^ x) k, ⋯⟩ * (r' ^ n * x) = 0
⊢ ↑⟨(fun x ↦ r' ^ x) (k + n), ⋯⟩ * x = 0
Module: Mathlib.Data.DFinsupp.Encodable

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), Countable (α i)
⊢ Countable (Π₀ (i : ι), α i)

Tactic:
let _ := Encodable.ofCountable ι

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : Countable ι
inst✝ : ∀ (i : ι), Countable (α i)
x✝ : Encodable ι := Encodable.ofCountable ι
⊢ Countable (Π₀ (i : ι), α i)
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
⊢ ∀ x ⊆ s, x.Nonempty → (-1) ^ #x • (⋂ i ∈ x, S i).indicator f a = 0

Tactic:
intro t hts ht

Goal state after:
case neg
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∉ ⋃ i ∈ s, S i
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
⊢ (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a = 0
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 t : Set M
hs₀ : s.Nonempty
hs₁ : BddBelow s
ht₀ : t.Nonempty
ht₁ : BddAbove t
⊢ sInf (s / t) = sInf s / sSup t

Tactic:
by
  rw [div_eq_mul_inv, csInf_mul hs₀ hs₁ ht₀.inv ht₁.inv, csInf_inv ht₀ ht₁, div_eq_mul_inv]

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

Goal state before:
pp: x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this✝ : a * x⁻¹ < 1
this : a * x⁻¹ * x ≤ y
⊢ a ≤ y

Tactic:
rwa [mul_assoc, inv_mul_cancel₀ hx, mul_one] at this

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

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

Tactic:
rw [← map_one f]

Goal state after:
case pos
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : g < 1
⊢ f ↑g < f 1
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a b : ℝ≥0∞
hr : a ≠ ∞
hp : b ≠ ∞
h : a ≤ b
⊢ (min a b).toReal = min a.toReal b.toReal

Tactic:
by simp only [h, ENNReal.toReal_mono hp h, min_eq_left]

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
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : AddGroupSeminorm E
x✝¹ x✝ : E
⊢ r • p (x✝¹ + x✝) ≤ r • p x✝¹ + r • p x✝

Tactic:
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, ← mul_add]
        gcongr
        apply map_add_le_add

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

Goal state before:
pp: case inr.inr
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ∞
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal

Tactic:
have hq' : 0 < q := lt_of_lt_of_le hp hpq

Goal state after:
case inr.inr
p q : ℝ≥0∞
hpq : p ≤ q
hp : 0 < p
hq : q < ∞
hq' : 0 < q
⊢ p = 0 ∧ q = 0 ∨
    p = 0 ∧ q = ∞ ∨
      p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: x y z : ℝ≥0∞
hy : y ≠ 0
hz : z ≠ 0
h : ∀ y' < y, ∀ z' < z, y' + z' ≤ x
⊢ ∃ j, j < z

Tactic:
exact ⟨0, hz.bot_lt⟩

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

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

Tactic:
by
  induction x <;> induction y <;> simp_all

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z = edist y z

Tactic:
apply edist_congr_right h

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

Goal state before:
pp: 𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝ : Group E
f : GroupSeminorm E
x y : E
⊢ f (x⁻¹ * y) = f (y⁻¹ * x)

Tactic:
by convert! map_inv_eq_map f (y⁻¹ * x) using 2; group

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

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ ↑x⁻¹.toNNReal = (↑x.toNNReal)⁻¹

Tactic:
← @coe_inv (Real.toNNReal x) (by simp [hx]),

Goal state after:
x : ℝ
hx : 0 < x
⊢ ↑x⁻¹.toNNReal = ↑x.toNNReal⁻¹
Module: Mathlib.Data.ENNReal.Inv

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

Tactic:
by
  rw [ENNReal.ofReal, ENNReal.ofReal, ← @coe_inv (Real.toNNReal x) (by simp [hx]), coe_inj,
    ← Real.toNNReal_inv]

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

Goal state before:
pp: x r y : ℝ
⊢ x - y ≤ r ∧ y - x ≤ r ↔ x - r ≤ y ∧ y ≤ x + r

Tactic:
← sub_le_iff_le_add',

Goal state after:
x r y : ℝ
⊢ x - y ≤ r ∧ y - x ≤ r ↔ x - r ≤ y ∧ y - x ≤ r
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
q : HeightOneSpectrum R
hq : q ∈ s ∧ ¬q = p'
⊢ ∏ q ∈ s \ {q}, q.asIdeal ≤ p

Tactic:
exact Ideal.prod_le_inf.trans (Finset.inf_le (b := p') (by simpa [hp's] using Ne.symm hq.2))

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
⊢ SecondCountableTopology α

Tactic:
refine EMetric.secondCountable_of_almost_dense_set fun ε ε0 => ?_

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
H : ∀ ε > 0, ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∃ t, t.Countable ∧ ⋃ x ∈ t, closedEBall x ε = univ
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
⊢ TendstoUniformlyOn F f p s ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε

Tactic:
refine ⟨fun H ε hε => H _ (edist_mem_uniformity hε), fun H u hu => ?_⟩
  rcases mem_uniformity_edist.1 hu with ⟨ε, εpos, hε⟩
  exact (H ε εpos).mono fun n hs x hx => hε (hs x hx)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
x : R
hxI : x ∈ I
hx : x ≠ 0
⊢ ∃ y, I = Ideal.span {x, y}

Tactic:
obtain ⟨y, rfl⟩ := exists_sup_span_eq (I.span_singleton_le_iff_mem.mpr hxI) (by simpa)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
x : R
hx : x ≠ 0
y : R
hxI : x ∈ Ideal.span {x} ⊔ Ideal.span {y}
⊢ ∃ y_1, Ideal.span {x} ⊔ Ideal.span {y} = Ideal.span {x, y_1}
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
r : ℝ
hr : r < 0
⊢ sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r

pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
⊢ sphere x 0 = sphere x.1 0 ×ˢ closedBall x.2 0 ∪ closedBall x.1 0 ×ˢ sphere x.2 0

pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
⊢ sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r

Tactic:
· simp [hr]

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
⊢ sphere x 0 = sphere x.1 0 ×ˢ closedBall x.2 0 ∪ closedBall x.1 0 ×ˢ sphere x.2 0

case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
⊢ sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: case inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
h : 0 < r ∨ Nonempty β
hr : r < 0
⊢ sphere x r = (⋃ i, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r

pp: case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
⊢ sphere x 0 = (⋃ i, Function.eval i ⁻¹' sphere (x i) 0) ∩ closedBall x 0

pp: case inr.inr
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
h : 0 < r ∨ Nonempty β
hr : 0 < r
⊢ sphere x r = (⋃ i, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r

Tactic:
· simp [hr]

Goal state after:
case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
⊢ sphere x 0 = (⋃ i, Function.eval i ⁻¹' sphere (x i) 0) ∩ closedBall x 0

case inr.inr
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
h : 0 < r ∨ Nonempty β
hr : 0 < r
⊢ sphere x r = (⋃ i, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
ht : t.Nonempty
h : x ∉ t
⊢ ∃ u, Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t

Tactic:
rcases htx.exists_seq_strictMono_tendsto_of_notMem h ht with ⟨u, hu⟩

Goal state after:
case neg
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
ht : t.Nonempty
h : x ∉ t
u : ℕ → α
hu : StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
⊢ ∃ u, Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Tendsto u atTop (𝓝 x) ∧ ∀ (n : ℕ), u n ∈ t
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
⊢ {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable

Tactic:
nontriviality α

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
⊢ {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}.Countable
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
r : ℝ
hpos : 0 < r
hr : ∀ (x : E), x ≠ 1 → r ≤ ‖x‖
x y : E
hne : x ≠ y
⊢ x⁻¹ * y ≠ 1

Tactic:
simpa [inv_mul_eq_one] using hne

Goal state after: