mathlib-initiative/mathlib-tactics huggingface dataset:
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⁻¹) * (algebraMap K L) a = x

Tactic:
← Algebra.smul_def,

Goal state after:
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
⊢ -↑this.unit⁻¹ • (algebraMap K L) a = x
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
⊢ FormallyUnramified R S

Tactic:
by
  constructor
  have : FormallyUnramified (ResidueField R) (ResidueField S) := .of_isSeparable _ _
  have : FormallyUnramified R (ResidueField S) := .comp _ (ResidueField R) _
  rw [← subsingleton_tensorProduct (R := S)]
  refine subsingleton_of_forall_eq 0 fun x ↦ ?_
  obtain ⟨x, rfl⟩ := (KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange R S
    (ResidueField S) Ideal.Quotient.mk_surjective x).mp (Subsingleton.elim _ _)
  obtain ⟨⟨x, hx⟩, rfl⟩ := Ideal.toCotangent_surjective _ x
  simp only [KaehlerDifferential.kerCotangentToTensor_toCotangent]
  replace hx : x ∈ Ideal.map (algebraMap R S) (maximalIdeal R) := by simpa [H] using hx
  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
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T

Tactic:
letI P : Extension R S := (Generators.self R S).toExtension

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
⊢ T ⊗[S] H1Cotangent R S ≃ₗ[T] H1Cotangent R T
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 ⋯
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 : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
x s : P.Ring
hs : s ∈ M'
⊢ (algebraMap P.Ring (Localization M')) x =
    (algebraMap P.Ring (Localization M')) ↑⟨s, hs⟩ *
      IsLocalizedModule.mk' (Algebra.linearMap P.Ring (Localization M')) x ⟨s, hs⟩

Tactic:
← Algebra.smul_def,

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 ⋯
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 : ↥P.ker →ₗ[P.Ring] ↥(RingHom.ker fQ) := f.mapKer ⋯
x s : P.Ring
hs : s ∈ M'
⊢ (algebraMap P.Ring (Localization M')) x =
    ↑⟨s, hs⟩ • IsLocalizedModule.mk' (Algebra.linearMap P.Ring (Localization M')) x ⟨s, hs⟩
Module: Mathlib.LinearAlgebra.Countable

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Countable R
inst✝ : Module.Finite R M
n : ℕ
s : Fin n → M
h : Submodule.span R (Set.range s) = ⊤
⊢ Set.univ.Countable

Tactic:
have : Countable (Submodule.span R (Set.range s)) := inferInstance

Goal state after:
M : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Countable R
inst✝ : Module.Finite R M
n : ℕ
s : Fin n → M
h : Submodule.span R (Set.range s) = ⊤
this : Countable ↥(Submodule.span R (Set.range s))
⊢ Set.univ.Countable
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: 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)
ε : ℚ
ε0 : ε > 0
this : ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, ↑(f j) / ↑j - ↑(f k) / ↑k < ε
⊢ ∃ i, ∀ j ≥ i, |(fun n ↦ ↑(f n) / ↑n) j - (fun n ↦ ↑(f n) / ↑n) i| < ε

Tactic:
refine ⟨_, fun j ij => abs_lt.2 ⟨?_, this _ ij _ le_rfl⟩⟩

Goal state after:
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)
ε : ℚ
ε0 : ε > 0
this : ∀ j ≥ ⌈ε⁻¹⌉₊, ∀ k ≥ ⌈ε⁻¹⌉₊, ↑(f j) / ↑j - ↑(f k) / ↑k < ε
j : ℕ
ij : j ≥ ⌈ε⁻¹⌉₊
⊢ -ε < (fun n ↦ ↑(f n) / ↑n) j - (fun n ↦ ↑(f n) / ↑n) ⌈ε⁻¹⌉₊
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I

Tactic:
have hf := hasFiniteMulSupport hI
  have h_ne_zero : v.maxPowDividing I ≠ 0 := pow_ne_zero _ v.ne_bot
  rw [← mul_finprod_cond_ne v hf, pow_add, pow_one, finprod_cond_ne _ _ hf]
  intro h_contr
  have hv_prime : Prime v.asIdeal := Ideal.prime_of_isPrime v.ne_bot v.isPrime
  obtain ⟨w, hw, hvw'⟩ :=
    Prime.exists_mem_finset_dvd hv_prime ((mul_dvd_mul_iff_left h_ne_zero).mp h_contr)
  have hw_prime : Prime w.asIdeal := Ideal.prime_of_isPrime w.ne_bot w.isPrime
  have hvw := Prime.dvd_of_dvd_pow hv_prime hvw'
  rw [Prime.dvd_prime_iff_associated hv_prime hw_prime, associated_iff_eq] at hvw
  exact (Finset.mem_erase.mp hw).1 (HeightOneSpectrum.ext hvw.symm)

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

Goal state before:
pp: a b : ℝ≥0
ha : 0 < a
hb : b < 1
⊢ ∃ n, b ^ n < a

Tactic:
simpa only [← coe_pow, NNReal.coe_lt_coe] using
    exists_pow_lt_of_lt_one (NNReal.coe_pos.2 ha) (NNReal.coe_lt_coe.2 hb)

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

Goal state before:
pp: x y : ℝ
hy : 0 ≤ y
⊢ y⁻¹.toNNReal * x.toNNReal = y.toNNReal⁻¹ * x.toNNReal

Tactic:
Real.toNNReal_inv

Goal state after:
x y : ℝ
hy : 0 ≤ y
⊢ y.toNNReal⁻¹ * x.toNNReal = y.toNNReal⁻¹ * x.toNNReal
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' // x < ↑r' }
r : { q' // x < ↑q' }
⊢ ⨅ r, f ↑r ≤ f ↑↑r

Tactic:
obtain ⟨y, hxy, hyr⟩ := exists_rat_btwn r.prop

Goal state after:
case refine_1
f : ℝ → ℝ
x : ℝ
hf : BddBelow (f '' Ioi x)
hf_mono : Monotone f
this : Nonempty { r' // x < ↑r' }
r : { q' // x < ↑q' }
y : ℚ
hxy : x < ↑y
hyr : ↑y < ↑↑r
⊢ ⨅ r, f ↑r ≤ f ↑↑r
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ⊢ ¬BddBelow (range fun x ↦ ↑x)

Tactic:
by
  dsimp only [BddBelow, lowerBounds]
  rw [Set.not_nonempty_iff_eq_empty]
  ext
  simpa using exists_rat_lt _

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

Goal state before:
pp: case neg
Γ₀ : 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
hfg0 : f ↑g ≠ 0
hg1' : 1 < g
⊢ f ↑g⁻¹ < 1

Tactic:
rw [Units.val_inv_eq_inv_val, map_inv₀, inv_lt_one_iff hfg0, ← map_one f]

Goal state after:
case neg
Γ₀ : 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
hfg0 : f ↑g ≠ 0
hg1' : 1 < g
⊢ f 1 < f ↑g
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
p q : GroupSeminorm E
⊢ 0 + q 1 = 0

Tactic:
map_one_eq_zero q,

Goal state after:
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
p q : GroupSeminorm E
⊢ 0 + 0 = 0
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: a : ℝ≥0∞
b : ℝ≥0
h : a ≤ ↑b
⊢ a.toReal ≤ ↑b

Tactic:
lift a to ℝ≥0 using ne_top_of_le_ne_top coe_ne_top h

Goal state after:
b a : ℝ≥0
h : ↑a ≤ ↑b
⊢ (↑a).toReal ≤ ↑b
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: E : Type u_3
inst✝ : Group E
s : Set (GroupSeminorm E)
hs : ¬BddAbove s
⊢ sSup s = 0

Tactic:
simp [SupSet.sSup, hs]

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

Goal state before:
pp: E : Type u_3
inst✝ : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
⊢ (sSup s) x = ⨆ p, ↑p x

Tactic:
simp [SupSet.sSup, hs]

Goal state after:
E : Type u_3
inst✝ : Group E
s : Set (GroupSeminorm E)
hs : BddAbove s
x : E
⊢ { toFun := fun x ↦ ⨆ p, ↑p x, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ } x = ⨆ p, ↑p x
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: E : Type u_3
inst✝ : CommGroup E
p q : GroupSeminorm E
x : E
⊢ 0 ∈ lowerBounds (range fun y ↦ p y + q (x / y))

Tactic:
rintro _ ⟨x, rfl⟩

Goal state after:
E : Type u_3
inst✝ : CommGroup E
p q : GroupSeminorm E
x✝ x : E
⊢ 0 ≤ (fun y ↦ p y + q (x✝ / y)) x
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✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x : E
p q : GroupSeminorm E
r : ℝ
hr : 0 < r
⊢ 0 + q 1 < r

Tactic:
map_one_eq_zero q,

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x : E
p q : GroupSeminorm E
r : ℝ
hr : 0 < r
⊢ 0 + 0 < r
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✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ : E
p q : GroupSeminorm E
x : E
⊢ p x + q 1 ≤ p x

Tactic:
map_one_eq_zero q,

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ : E
p q : GroupSeminorm E
x : E
⊢ p x + 0 ≤ p x
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 / (algebraMap R K) ↑d = 0

Tactic:
div_eq_zero_iff,

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.Analysis.Normed.Group.Seminorm

Goal state before:
pp: E : Type u_3
inst✝ : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : ¬BddAbove s
⊢ sSup s = 0

Tactic:
simp [SupSet.sSup, hs]

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

Goal state before:
pp: E : Type u_3
inst✝ : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
⊢ (sSup s) x = ⨆ p, ↑p x

Tactic:
simp [SupSet.sSup, hs]

Goal state after:
E : Type u_3
inst✝ : AddGroup E
s : Set (NonarchAddGroupSeminorm E)
hs : BddAbove s
x : E
⊢ { toFun := fun x ↦ ⨆ p, ↑p x, map_zero' := ⋯, add_le_max' := ⋯, neg' := ⋯ } x = ⨆ p, ↑p x
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: E : Type u_3
inst✝ : AddCommGroup E
p q : NonarchAddGroupSeminorm E
x : E
⊢ 0 ∈ lowerBounds (range fun y ↦ p y + q (x - y))

Tactic:
rintro _ ⟨x, rfl⟩

Goal state after:
E : Type u_3
inst✝ : AddCommGroup E
p q : NonarchAddGroupSeminorm E
x✝ x : E
⊢ 0 ≤ (fun y ↦ p y + q (x✝ - y)) x
Module: Mathlib.Data.ENNReal.Operations

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

Tactic:
rw [← sub_sub_cancel ha (h _)]

Goal state after:
case inr
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
h : ∀ (x : ι), f x ≤ a
i : ι
⊢ a - (a - f i) ≤ a - ⨅ i, a - f i
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
⊢ y + z ≤ x

Tactic:
simpa using biSup_add_biSup_le' (by exact ⟨0, hy.bot_lt⟩) (by exact ⟨0, hz.bot_lt⟩) h

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

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

Tactic:
contrapose! h
  simpa using biSup_add_biSup_le' (by exact ⟨0, hy.bot_lt⟩) (by exact ⟨0, hz.bot_lt⟩) h

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

Goal state before:
pp: x y : ℝ
⊢ WithBot.some '' WithTop.some '' Ico x y = Ico ↑x ↑y

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

Goal state after:
x y : ℝ
⊢ Ico ↑↑x ↑↑y = Ico ↑x ↑y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x✝ : ↑{⊥, ⊤}ᶜ
x : EReal
hx : x ∈ {⊥, ⊤}ᶜ
⊢ (fun x ↦ ⟨↑x, ⋯⟩) ((fun x ↦ (↑x).toReal) ⟨x, hx⟩) = ⟨x, hx⟩

Tactic:
lift x to ℝ
    · simpa [not_or, and_comm] using hx
    · simp

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

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

Tactic:
rw [inv_le_iff_inv_le, inv_one]

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

Goal state before:
pp: x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ∃ n, ↑x ∈ Ico (↑y ^ n) (↑y ^ (n + 1))

Tactic:
obtain ⟨n, hn, h'n⟩ : ∃ n : ℤ, y ^ n ≤ x ∧ x < y ^ (n + 1) := by
    refine NNReal.exists_mem_Ico_zpow ?_ (one_lt_coe_iff.1 hy)
    simpa only [Ne, coe_eq_zero] using hx

Goal state after:
x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ ∃ n, ↑x ∈ Ico (↑y ^ n) (↑y ^ (n + 1))
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
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
q : HeightOneSpectrum R
hq : q ∈ s
hqp : ¬q = p'
⊢ q ∈ s \ {p'}

Tactic:
simpa [hq] using hqp

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

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
inst✝ : PseudoMetricSpace α✝
α : Type ?u.13
β : Type ?u.11
f : α → β
m : PseudoMetricSpace β
s : Set α
⊢ (f '' sᶜ)ᶜ ∈ cobounded β ↔ s ∈ {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist (f x) (f y) ≤ C}

Tactic:
by
    simp only [← isBounded_def, isBounded_iff, forall_mem_image, mem_ofPred]

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

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
s : Set α
a : α
hsa : a ∈ upperBounds s
hsf : a ∈ closure[inst✝²] s
⊢ IsLUB s a

Tactic:
rw [mem_closure_iff_clusterPt, ClusterPt, inf_comm] at hsf

Goal state after:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
s : Set α
a : α
hsa : a ∈ upperBounds s
hsf : (𝓟 s ⊓ 𝓝 a).NeBot
⊢ IsLUB s a
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)) ↔ BddBelow s ∧ BddAbove s

Tactic:
bddBelow_pi,

Goal state after:
α✝ : 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)) ↔ (∀ (a : ι), BddBelow (Function.eval a '' s)) ∧ BddAbove s
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: case h'
α : 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 α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
⊢ x c < y (f (x c))

Tactic:
hfx _ hc

Goal state after:
case h'
α : 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 α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
⊢ x c < y c
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
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
H : c < d
a : α
xca : x c < a
ayc : a < y (f (x c))
xda : x d < a
ayd : a < y (f (x d))
⊢ False

Tactic:
hfx _ hc

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 α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c ≠ x d
H : c < d
a : α
xca : x c < a
ayc : a < y c
xda : x d < a
ayd : a < y (f (x d))
⊢ False
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : CompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
ι : Sort u_3
f : α → β
g : ι → α
Cf : ContinuousAt f (iSup g)
Mf : Monotone f
fbot : f ⊥ = ⊥
⊢ f (⨆ i, g i) = ⨆ i, f (g i)

Tactic:
by
  rw [iSup, Mf.map_sSup_of_continuousAt Cf fbot, ← range_comp, iSup, comp_def]

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
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
⊢ J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J

Tactic:
by
    have := FractionalIdeal.sup_mul_inf J' (spanSingleton R⁰ (I'.divMod I J') * I)
    rwa [FractionalIdeal.sup_eq_add, divMod_spec h' hJ' hI, mul_left_comm, mul_comm J' I, H,
      mul_comm I' J, ← mul_assoc, (mul_left_injective₀ _).eq_iff] at this
    rintro rfl
    exact hJ' (by simpa using h')

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

Goal state before:
pp: α : Type v
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
s : Set α
hs : IsPreconnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s = univ

Tactic:
refine eq_univ_of_forall fun x => ?_
  obtain ⟨y, ys, hy⟩ : ∃ y ∈ s, y < x := not_bddBelow_iff.1 hb x
  obtain ⟨z, zs, hz⟩ : ∃ z ∈ s, x < z := not_bddAbove_iff.1 ha x
  exact hs.Icc_subset ys zs ⟨le_of_lt hy, le_of_lt hz⟩

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ Inseparable a 1 ↔ ‖a‖ = 0

Tactic:
Metric.inseparable_iff,

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ dist a 1 = 0 ↔ ‖a‖ = 0
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
r : ℝ≥0∞
⊢ edist a 1 < r ↔ ‖a‖ₑ < r

Tactic:
edist_one_right

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
r : ℝ≥0∞
⊢ ‖a‖ₑ < r ↔ ‖a‖ₑ < r