mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : (Generators.self R T).toExtension.Hom Q :=
  { toRingHom := (MvPolynomial.aeval Q.σ).toRingHom, toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
⊢ (Extension.H1Cotangent.equivOfFormallySmooth (Generators.self R T).toExtension
          (Extension.ofSurjective (IsLocalization.liftAlgHom ⋯) ⋯)).symm
      ((Extension.H1Cotangent.map
          {
            toRingHom :=
              algebraMap (Generators.self R S).toExtension.Ring
                (Localization (Submonoid.comap (algebraMap (Generators.self R S).toExtension.Ring S) M)),
            toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ })
        x) =
    (H1Cotangent.map R R S T) x

Tactic:
LinearEquiv.symm_apply_eq,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
x : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : (Generators.self R T).toExtension.Hom Q :=
  { toRingHom := (MvPolynomial.aeval Q.σ).toRingHom, toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
⊢ (Extension.H1Cotangent.map
        {
          toRingHom :=
            algebraMap (Generators.self R S).toExtension.Ring
              (Localization (Submonoid.comap (algebraMap (Generators.self R S).toExtension.Ring S) M)),
          toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ })
      x =
    (Extension.H1Cotangent.equivOfFormallySmooth (Generators.self R T).toExtension
        (Extension.ofSurjective (IsLocalization.liftAlgHom ⋯) ⋯))
      ((H1Cotangent.map R R S T) x)
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 ↑(factors' I) = v.asIdeal ^ Multiset.count v.asIdeal (normalizedFactors I)

Tactic:
count_some (irreducible_mk.mpr v.irreducible),

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
⊢ v.asIdeal ^ Multiset.count ⟨Associates.mk v.asIdeal, ⋯⟩ (factors' I) =
    v.asIdeal ^ Multiset.count v.asIdeal (normalizedFactors I)
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
hf : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ (Finite.toFinset hf).erase v, i.maxPowDividing I
hv_prime : Prime v.asIdeal
⊢ False

Tactic:
obtain ⟨w, hw, hvw'⟩ :=
    Prime.exists_mem_finset_dvd hv_prime ((mul_dvd_mul_iff_left h_ne_zero).mp h_contr)

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ (Finite.toFinset hf).erase v, i.maxPowDividing I
hv_prime : Prime v.asIdeal
w : HeightOneSpectrum R
hw : w ∈ (Finite.toFinset hf).erase v
hvw' : v.asIdeal ∣ w.maxPowDividing I
⊢ False
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℤ
⊢ ↑(x ^ n).toNNReal = ↑x.toNNReal ^ n

Tactic:
Real.coe_toNNReal _ (zpow_nonneg hx _),

Goal state after:
x : ℝ
hx : 0 ≤ x
n : ℤ
⊢ x ^ n = ↑x.toNNReal ^ n
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: E : Type u_3
inst✝ : Group E
ι : Type u_6
f : ι → GroupSeminorm E
h : BddAbove (range f)
x : E
⊢ (⨆ i, f i) x = ⨆ i, (f i) x

Tactic:
rw [← sSup_range, coe_sSup_apply h]
  exact (Set.rangeFactorization_surjective.iSup_congr _ (by simp)) |>.symm

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✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ : E
p q : GroupSeminorm E
x : E
⊢ ⨅ x_1, p x_1 + q (x⁻¹ / x_1⁻¹) = ⨅ y, p y + q (x / y)

Tactic:
← inv_div',

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
⊢ ⨅ x_1, p x_1 + q (x / x_1)⁻¹ = ⨅ y, p y + q (x / y)
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: E : Type u_3
inst✝ : AddGroup E
ι : Type u_6
f : ι → NonarchAddGroupSeminorm E
h : BddAbove (range f)
x : E
⊢ (⨆ i, f i) x = ⨆ i, (f i) x

Tactic:
rw [← sSup_range, coe_sSup_apply h]
  exact (Set.rangeFactorization_surjective.iSup_congr _ (by simp)) |>.symm

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s : Set X
⊢ s.ordConnectedComponent a ∈ 𝓝 a ↔ s ∈ 𝓝 a

Tactic:
refine ⟨fun h => mem_of_superset h ordConnectedComponent_subset, fun h => ?_⟩
  rcases exists_Icc_mem_subset_of_mem_nhds h with ⟨b, c, ha, ha', hs⟩
  exact mem_of_superset ha' (subset_ordConnectedComponent ha hs)

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

Goal state before:
pp: case inl
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
i : ι
hi : f i ≤ 0
⊢ ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)

Tactic:
rw [iInf_eq_bot.2 fun _ _ ↦ ⟨i, by simpa [ofReal_of_nonpos hi]⟩]
    simp [Real.iInf_nonpos' ⟨i, hi⟩]

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

Goal state before:
pp: case bot.bot
⊢ ⊥ * ⊥ = ⊥ * ⊥

Tactic:
{ rfl }

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

Goal state before:
pp: case bot.coe
a✝ : ℝ
⊢ ⊥ * ↑a✝ = ↑a✝ * ⊥

Tactic:
{ rfl }

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

Goal state before:
pp: case bot.top
⊢ ⊥ * ⊤ = ⊤ * ⊥

Tactic:
{ rfl }

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

Goal state before:
pp: case coe.bot
a✝ : ℝ
⊢ ↑a✝ * ⊥ = ⊥ * ↑a✝

Tactic:
{ rfl }

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

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
⊢ ↑a✝¹ * ↑a✝ = ↑a✝ * ↑a✝¹

Tactic:
{ rfl }

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
⊢ ↑a✝¹ * ↑a✝ = ↑a✝ * ↑a✝¹
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case coe.top
a✝ : ℝ
⊢ ↑a✝ * ⊤ = ⊤ * ↑a✝

Tactic:
{ rfl }

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

Goal state before:
pp: case top.bot
⊢ ⊤ * ⊥ = ⊥ * ⊤

Tactic:
{ rfl }

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

Goal state before:
pp: case top.coe
a✝ : ℝ
⊢ ⊤ * ↑a✝ = ↑a✝ * ⊤

Tactic:
{ rfl }

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

Goal state before:
pp: case top.top
⊢ ⊤ * ⊤ = ⊤ * ⊤

Tactic:
{ rfl }

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

Goal state before:
pp: case mp
x : ℝ
⊢ x ∈ toReal '' Ioo ⊥ 0 → x ∈ Iio 0

Tactic:
rintro ⟨y, ⟨_, hy0⟩, rfl⟩
    lift y to ℝ using by aesop
    simpa using hy0

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

Goal state before:
pp: case insert
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
ι : Type u_3
I : ι → FractionalIdeal R⁰ K
i : ι
s : Finset ι
hi : i ∉ s
hrec : (∀ i ∈ s, I i ≠ 0) → count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)
hS : ∀ i_1 ∈ insert i s, I i_1 ≠ 0
hS' : ∀ i ∈ s, I i ≠ 0
hS0 : ∏ i ∈ s, I i ≠ 0
⊢ count K v (∏ i ∈ insert i s, I i) = ∑ i ∈ insert i s, count K v (I i)

Tactic:
have hi0 : I i ≠ 0 := hS i (Finset.mem_insert_self i s)

Goal state after:
case insert
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
ι : Type u_3
I : ι → FractionalIdeal R⁰ K
i : ι
s : Finset ι
hi : i ∉ s
hrec : (∀ i ∈ s, I i ≠ 0) → count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)
hS : ∀ i_1 ∈ insert i s, I i_1 ≠ 0
hS' : ∀ i ∈ s, I i ≠ 0
hS0 : ∏ i ∈ s, I i ≠ 0
hi0 : I i ≠ 0
⊢ count K v (∏ i ∈ insert i s, I i) = ∑ i ∈ insert i s, count K v (I i)
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal ⁻¹' Icc ↑x ↑y = Icc x y

Tactic:
simp_rw [← Ici_inter_Iic]

Goal state after:
x y : ℝ
⊢ Real.toEReal ⁻¹' (Ici ↑x ∩ Iic ↑y) = Ici x ∩ Iic y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal ⁻¹' Ico ↑x ↑y = Ico x y

Tactic:
simp_rw [← Ici_inter_Iio]
  simp

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ 0 < a / b ↔ a ≠ 0 ∧ b ≠ ∞

Tactic:
by simp [pos_iff_ne_zero, not_or]

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

Goal state before:
pp: r : ℝ≥0
hr : r ≠ 0
n : ℤ
⊢ ↑(r ^ n) = ↑r ^ n

Tactic:
by
  rcases n with n | n
  · simp only [Int.ofNat_eq_natCast, coe_pow, zpow_natCast]
  · have : r ^ n.succ ≠ 0 := pow_ne_zero (n + 1) hr
    simp only [zpow_negSucc, coe_inv this, coe_pow]

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

Goal state before:
pp: case mpr.right
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ x < ∞

Tactic:
apply lt_trans h'n _

Goal state after:
y : ℝ≥0∞
hy : 1 < y
h'y : y ≠ ∞
x : ℝ≥0∞
n : ℤ
hn : y ^ n ≤ x
h'n : x < y ^ (n + 1)
⊢ y ^ (n + 1) < ∞
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
c : α → Set α
hs : IsCompact s
hc : ∀ x ∈ s, c x ∈ 𝓝 x
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ y, eball x δ ⊆ c y

Tactic:
simpa only [eball, UniformSpace.ball, preimage_ofPred_eq, edist_comm]
    using uniformity_basis_edist.lebesgue_number_lemma_nhds hs hc

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

Goal state before:
pp: α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : CompactIccSpace α
⊢ cocompact α ≤ atBot ⊔ atTop

Tactic:
refine fun s hs ↦ mem_cocompact.mpr <| (isEmpty_or_nonempty α).casesOn ?_ ?_ <;> intro
  · exact ⟨∅, isCompact_empty, fun x _ ↦ (IsEmpty.false x).elim⟩
  · obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs.1
    obtain ⟨u, hu⟩ := mem_atTop_sets.mp hs.2
    refine ⟨Icc t u, isCompact_Icc, fun x hx ↦ ?_⟩
    exact (not_and_or.mp hx).casesOn (fun h ↦ ht x (le_of_not_ge h)) fun h ↦ hu x (le_of_not_ge h)

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

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

Tactic:
rw [dist_eq_norm_inv_mul', inv_one, one_mul]

Goal state after:
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' ⊓ I = J
H' : ¬I'.divMod I J' = 0
⊢ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ⊓ ↑I ≤ ↑((spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I)

Tactic:
coe_inf

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' ⊓ I = J
H' : ¬I'.divMod I J' = 0
⊢ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ⊓ ↑I ≤ ↑((spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J') ⊓ ↑I
Module: Mathlib.Order.Filter.AtTopBot.Archimedean

Goal state before:

Tactic:
b ≤ max b 0 * 1 := by
    { rw [mul_one]
      exact le_max_left _ _ }
    _ ≤ max b 0 * (n * r) := by gcongr
    _ = max b 0 * n * r := by rw [mul_assoc]
    _ ≤ f x * r := by gcongr

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

Goal state before:
pp: α : Type u
s : Set α
inst✝ : PseudoMetricSpace α
h : ¬Bornology.IsBounded s
⊢ diam s = 0

Tactic:
by
  rw [diam, ediam_of_unbounded h, ENNReal.toReal_top]

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Archimedean

Goal state before:
pp: G : Type u_1
inst✝⁷ : CommGroup G
inst✝⁶ : LinearOrder G
inst✝⁵ : IsOrderedMonoid G
inst✝⁴ : TopologicalSpace G
inst✝³ : OrderTopology G
inst✝² : MulArchimedean G
inst✝¹ : Nontrivial G
inst✝ : DenselyOrdered G
s : Subgroup G
hd : Dense ↑s
⊢ Xor (Dense ↑s) (∃ a, s = zpowers a)

Tactic:
then

Goal state after:
G : Type u_1
inst✝⁷ : CommGroup G
inst✝⁶ : LinearOrder G
inst✝⁵ : IsOrderedMonoid G
inst✝⁴ : TopologicalSpace G
inst✝³ : OrderTopology G
inst✝² : MulArchimedean G
inst✝¹ : Nontrivial G
inst✝ : DenselyOrdered G
s : Subgroup G
hd : Dense ↑s
⊢ Xor (Dense ↑s) (∃ a, s = zpowers a)
Module: Mathlib.Topology.Algebra.Order.Archimedean

Goal state before:
pp: G : Type u_1
inst✝⁷ : CommGroup G
inst✝⁶ : LinearOrder G
inst✝⁵ : IsOrderedMonoid G
inst✝⁴ : TopologicalSpace G
inst✝³ : OrderTopology G
inst✝² : MulArchimedean G
inst✝¹ : Nontrivial G
inst✝ : DenselyOrdered G
a : G
hd : Dense ↑(zpowers a)
⊢ False

Tactic:
exact not_denseRange_zpow hd

Goal state after:
Module: Mathlib.Topology.Instances.Nat

Goal state before:
pp: case inl
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ closedBall x r = Icc ⌈↑x - r⌉₊ ⌊↑x + r⌋₊

Tactic:
rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]
    positivity

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

Goal state before:
pp: m : ℤ
⊢ ‖↑m‖ = ‖m‖

Tactic:
by
  rw [← Rat.norm_cast_real, ← Int.norm_cast_real]; congr 1

Goal state after:
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun x1 x2 ↦ x1 ≤ x2) x (m i)
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f fun a ↦ s.sup' hs fun i ↦ F i a

Tactic:
use sup' s hs m

Goal state after:
case h
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : LinearOrder β
inst✝ : Nonempty β
f : Filter α
F : ι → α → β
s : Finset ι
hs : s.Nonempty
m : ι → β
hm : ∀ i ∈ s, ∀ᶠ (x : β) in Filter.map (F i) f, (fun x1 x2 ↦ x1 ≤ x2) x (m i)
⊢ ∀ᶠ (x : β) in Filter.map (fun a ↦ s.sup' hs fun i ↦ F i a) f, (fun x1 x2 ↦ x1 ≤ x2) x (s.sup' hs m)
Module: Mathlib.Order.Filter.IsBounded

Goal state before:
pp: R : Type u_5
S : Type u_6
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, x < f l
⊢ ∀ᶠ (x : R) in F, x < l

Tactic:
filter_upwards [ev] with z hz

Goal state after:
R : Type u_5
S : Type u_6
F : Filter R
inst✝¹ : LinearOrder R
inst✝ : LinearOrder S
f : R → S
f_incr : Monotone f
l : R
freq_ge : ∃ᶠ (x : R) in F, l ≤ x
ev : ∀ᶠ (x : S) in map f F, x < f l
z : R
hz : z ∈ f ⁻¹' {x | x < f l}
⊢ z < l
Module: Mathlib.Topology.Order.MonotoneConvergence

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), SupConvergenceClass (α i)
⊢ SupConvergenceClass ((i : ι) → α i)

Tactic:
refine ⟨fun f s h => ?_⟩

Goal state after:
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), SupConvergenceClass (α i)
f : (i : ι) → α i
s : Set ((i : ι) → α i)
h : IsLUB s f
⊢ Tendsto Subtype.val atTop (𝓝 f)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℝ
h1 : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ ↑(-(a✝¹ + a✝)) = ↑(-a✝¹) - ↑a✝

Tactic:
← coe_sub,

Goal state after:
case coe.coe
a✝¹ a✝ : ℝ
h1 : ↑a✝¹ ≠ ⊥ ∨ ↑a✝ ≠ ⊤
h2 : ↑a✝¹ ≠ ⊤ ∨ ↑a✝ ≠ ⊥
⊢ ↑(-(a✝¹ + a✝)) = ↑(-a✝¹ - a✝)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case neg
x y : ℝ
hy : 0 ≤ ↑y
hxy : ¬x ≤ y
⊢ ENNReal.ofReal (↑x - ↑y).toReal = (↑x).toENNReal - (↑y).toENNReal

Tactic:
← coe_sub,

Goal state after:
case neg
x y : ℝ
hy : 0 ≤ ↑y
hxy : ¬x ≤ y
⊢ ENNReal.ofReal (↑(x - y)).toReal = (↑x).toENNReal - (↑y).toENNReal
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b c : EReal
hc : c < a + b
⊢ ∃ b' < b, c < a + b'

Tactic:
add_comm a

Goal state after:
a b c : EReal
hc : c < b + a
⊢ ∃ b' < b, c < b' + a
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
⊢ x ≤ limsup u f

Tactic:
by_cases h' : ∀ y < x, ∃ z, y < z ∧ z < x

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ∀ y < x, ∃ z, y < z ∧ z < x
⊢ x ≤ limsup u f

case neg
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h : ∀ y < x, ∃ᶠ (a : α) in f, y < u a
h' : ¬∀ y < x, ∃ z, y < z ∧ z < x
⊢ x ≤ limsup u f
Module: Mathlib.Topology.Order.LiminfLimsup

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : CompleteLattice β
f : α → β
hf : Antitone f
a : α
hb : ∃ b, a < b
⊢ liminf f (𝓝[>] a) = ⨆ r, ⨆ (_ : r > a), f r

Tactic:
rw [(nhdsGT_basis_of_exists_gt hb).liminf_eq_iSup_iInf]
  refine le_antisymm (iSup₂_mono' fun r hr ↦ ?_)
    (iSup₂_mono' fun r hr ↦ ⟨r, hr, le_iInf₂ fun i hi ↦ hf (Set.mem_Ioo.1 hi).2.le⟩)
  obtain ⟨b, hb⟩ := exists_between hr
  exact ⟨b, hb.1, iInf₂_le b hb⟩

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.BigOperators

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
t : Finset α
ht : s.preimage g ⋯ ⊆ t
y : β
hy : (∃ a ∈ t, g a = y) ∨ y ∈ s
hyt : ¬∃ a ∈ t, g a = y
⊢ y ∈ Set.range g → ∃ a ∈ t, g a = y

Tactic:
rintro ⟨x, rfl⟩

Goal state after:
case a
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : CommMonoid M
g : α → β
hg : Injective g
f : β → M
hf : ∀ x ∉ Set.range g, f x = 1
this : DecidableEq β
s : Finset β
t : Finset α
ht : s.preimage g ⋯ ⊆ t
x : α
hy : (∃ a ∈ t, g a = g x) ∨ g x ∈ s
hyt : ¬∃ a ∈ t, g a = g x
⊢ ∃ a ∈ t, g a = g x
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case pos
ι : Type u_4
α : Type u_5
α' : Type u_6
G : Type u_7
inst✝⁶ : CommMonoid α
inst✝⁵ : CommMonoid α'
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : T2Space α'
f : ι → α
L : SummationFilter ι
g : G
inst✝¹ : FunLike G α α'
inst✝ : MonoidHomClass G α α'
hge : IsClosedEmbedding ⇑g
hL : L.NeBot
⊢ g (∏'[L] (i : ι), f i) = ∏'[L] (i : ι), g (f i)

Tactic:
by_cases h : Multipliable f L
    · exact h.map_tprod g hge.continuous
    · rw [tprod_eq_one_of_not_multipliable h, tprod_eq_one_of_not_multipliable, map_one]
      contrapose h
      -- need to show `g ∘ f` multipliable implies `g` multipliable
      simp only [Multipliable, HasProd] at h ⊢
      obtain ⟨b, hb⟩ := h
      obtain ⟨a, ha⟩ : b ∈ Set.range g :=
        hge.isClosed_range.mem_of_tendsto hb (.of_forall <| by simp [← _root_.map_prod])
      use a
      simp [hge.tendsto_nhds_iff, Function.comp_def, ha, hb]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Group

Goal state before:
pp: α : Type u_1
G : Type u_4
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : IsTopologicalGroup G
f : α → G
inst✝¹ : FirstCountableTopology G
inst✝ : T1Space G
hf : Multipliable f
⊢ (mulSupport f).Countable

Tactic:
by
  simpa only [ker_nhds] using! hf.tendsto_cofinite_one.countable_compl_preimage_ker

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
⊢ ∃ u', u ⊆ u' ∧ (∏ x ∈ u', f x * if x = 0 then f 0 else 1) = ∏ b ∈ v', f ↑b * f (-↑b)

Tactic:
let u1 := v'.image fun x : ℕ ↦ (x : ℤ)

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m : M
inst✝ : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun x ↦ ↑x) v'
⊢ ∃ u', u ⊆ u' ∧ (∏ x ∈ u', f x * if x = 0 then f 0 else 1) = ∏ b ∈ v', f ↑b * f (-↑b)
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoid α
inst✝² : TopologicalSpace α
ι : Type u_4
S : Type u_5
s : S
inst✝¹ : SetLike S α
inst✝ : SubmonoidClass S α
h_closed : IsClosed[inst✝²] ↑s
f : ι → α
h : ∀ (i : ι), f i ∈ s
⊢ ∏' (i : ι), f i ∈ s

Tactic:
by
  by_cases hf : Multipliable f
  · exact h_closed.mem_of_tendsto hf.hasProd <| .of_forall fun _ => prod_mem fun i _ => h i
  · simp [tprod_eq_one_of_not_multipliable hf, one_mem]

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Ring

Goal state before:
pp: α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : IsTopologicalSemiring α
h : Summable fun x ↦ f x.1 * g x.2
⊢ Summable fun n ↦ ∑ ij ∈ antidiagonal n, f ij.1 * g ij.2

Tactic:
exact summable_sum_mul_antidiagonal_of_summable_mul h

Goal state after:
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case neg
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0
n : ℕ
hn : ¬n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
· exact iSup_pow_of_ne_zero hn _

Goal state after:
Module: Mathlib.Topology.Instances.NNReal.Lemmas

Goal state before:
pp: case neg
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
hn : ¬n = 0
⊢ (⨆ i, f i) ^ n = ⨆ i, f i ^ n

Tactic:
· exact iSup_pow_of_ne_zero hn _

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

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝¹ : EMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
h : f x = f y
⊢ x = y

Tactic:
simpa only [h, edist_self, mul_zero, edist_le_zero] using hf x y

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

Goal state before:
pp: α : Type u
β : Type v
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
f : α → β
inst✝ : Subsingleton α
x y : α
⊢ edist (f x) (f y) = edist x y

Tactic:
Subsingleton.elim x y

Goal state after:
α : Type u
β : Type v
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
f : α → β
inst✝ : Subsingleton α
x y : α
⊢ edist (f y) (f y) = edist y y
Module: Mathlib.Topology.Metrizable.Uniformity

Goal state before:
pp: X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
⊢ ↑(d x y) ≤ ↑2 * ↑(⨅ l, (zipWith d (x :: l) (l ++ [y])).sum)

Tactic:
← NNReal.coe_mul,

Goal state after:
X : Type u_1
d : X → X → ℝ≥0
dist_self : ∀ (x : X), d x x = 0
dist_comm : ∀ (x y : X), d x y = d y x
hd : ∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))
x y : X
⊢ ↑(d x y) ≤ ↑(2 * ⨅ l, (zipWith d (x :: l) (l ++ [y])).sum)