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
P : Extension R S
Q : Extension R T
f : P.Hom Q
H : f.toRingHom.FormallyEtale
this✝⁴ : Algebra P.Ring Q.Ring := f.toRingHom.toAlgebra
this✝³ : IsScalarTower R P.Ring Q.Ring
this✝² : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝¹ : IsScalarTower P.Ring S T
this✝ : IsScalarTower P.Ring Q.Ring T
this : FormallyEtale P.Ring Q.Ring
⊢ Ω[P.Ring⁄R] →ₗ[P.Ring] T ⊗[S] P.CotangentSpace

Tactic:
exact (TensorProduct.mk _ _ _ 1).restrictScalars P.Ring ∘ₗ
        (TensorProduct.mk _ _ _ 1).restrictScalars P.Ring

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

Goal state before:
pp: case left
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Function.Injective ⇑(map P.toInfinitesimal)

pp: case right
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Surjective ⇑(map P.toInfinitesimal)

Tactic:
· intro x y e
    ext1
    exact (Cotangent.map_toInfinitesimal_bijective P).1 (congr_arg Subtype.val e)

Goal state after:
case right
R : Type u_1
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ Surjective ⇑(map P.toInfinitesimal)
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 ⋯
s : S
hs : s ∈ M
x : P.Ring
⊢ ∃ a, fQ a = IsLocalization.mk' T ((algebraMap P.Ring S) x) ⟨s, hs⟩

Tactic:
obtain ⟨s, rfl⟩ := P.algebraMap_surjective s

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 ⋯
x s : P.Ring
hs : (algebraMap P.Ring S) s ∈ M
⊢ ∃ a, fQ a = IsLocalization.mk' T ((algebraMap P.Ring S) x) ⟨(algebraMap P.Ring S) s, hs⟩
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
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
r' : R
x : S
hxs : x ∈ ↑s
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
⊢ (awayMapₐ (Algebra.ofId R S) r').toRingHom
      (IsLocalization.mk' (Away r') ((r'' * r * ∏ i ∈ s.erase x, b i) * a x) ⟨(fun x ↦ r' ^ x) 1, ⋯⟩) =
    ↑(IsScalarTower.toAlgHom R S (Away ((Algebra.ofId R S) r'))) x

Tactic:
dsimp [awayMapₐ, IsLocalization.Away.map]

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
hRS : (RingHom.ker (algebraMap R S)).FG
H : Function.Bijective ⇑(localRingHom p q (algebraMap R S) ⋯)
s : Finset S
hs : Algebra.adjoin R ↑s = ⊤
a b : S → R
hbp : ∀ (x : S), b x ∉ p
e : ∀ (x : S), (algebraMap R S) (a x) = x * (algebraMap R S) (b x)
r : R
hrp : r ∉ p
hr : ∀ (r' : R), r ∣ r' → Function.Injective ⇑(awayMap (algebraMap R S) r')
r' : R
x : S
hxs : x ∈ ↑s
r'' : R
hr' : r' = (r * ∏ i ∈ s, b i) * r''
⊢ (IsLocalization.map (Away ((algebraMap R S) r')) (algebraMap R S) ⋯)
      (IsLocalization.mk' (Away r') ((r'' * r * ∏ i ∈ s.erase x, b i) * a x) ⟨r' ^ 1, ⋯⟩) =
    (algebraMap S (Away ((algebraMap R S) r'))) x
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 ⋯
s : S
hs : s ∈ M
x : P.Ring
⊢ ∃ a, fQ a = IsLocalization.mk' T ((algebraMap P.Ring S) x) ⟨s, hs⟩

Tactic:
obtain ⟨s, rfl⟩ := P.algebraMap_surjective s

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 ⋯
x s : P.Ring
hs : (algebraMap P.Ring S) s ∈ M
⊢ ∃ a, fQ a = IsLocalization.mk' T ((algebraMap P.Ring S) x) ⟨(algebraMap P.Ring S) s, hs⟩
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:
classical
    let _ := Encodable.ofCountable ι
    let _ := fun i ↦ Encodable.ofCountable (α i)
    infer_instance

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0

Tactic:
by_cases ha : a ∈ ⋃ i ∈ s, S i

Goal state after:
case pos
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha : a ∈ ⋃ i ∈ s, S i
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0

case neg
ι : Type u_1
α : Type u_2
s : Finset ι
hs : s.Nonempty
S : ι → Set α
a : α
ha : a ∉ ⋃ i ∈ s, S i
⊢ ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
⊢ (⋃ i ∈ s, S i).indicator f a = ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (#t + 1) • (⋂ i ∈ t, S i).indicator f a

Tactic:
by_cases ha : a ∈ ⋃ i ∈ s, S i

Goal state after:
case pos
ι : 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
⊢ (⋃ i ∈ s, S i).indicator f a = ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (#t + 1) • (⋂ i ∈ t, S i).indicator f a

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
⊢ (⋃ i ∈ s, S i).indicator f a = ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (#t + 1) • (⋂ i ∈ t, S i).indicator f a
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:
by
  classical
  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: x y : ℝ
hx : 0 ≤ x
⊢ (x / y).toNNReal = x.toNNReal / y.toNNReal

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ← Real.toNNReal_inv, ← Real.toNNReal_mul hx]

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

Goal state before:
pp: r : ℝ
⊢ 0 ≤ r ∨ 0 ≤ -r

Tactic:
simpa using le_total ..

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
h0 : I ≠ 0
⊢ (↑(Finite.toFinset ⋯)).Pairwise (IsCoprime on fun i ↦ i.maxPowDividing I)

Tactic:
· intro x hx y hy hxy
    apply IsDedekindDomain.HeightOneSpectrum.isCoprime_pow_of_ne _ _ hxy

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
⊢ ∀ (s : Finset (HeightOneSpectrum A)) (v : HeightOneSpectrum A → M),
    (∀ i ∈ s, v i ∈ primaryComponent M i.asIdeal) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0

Tactic:
intro s

Goal state after:
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
s : Finset (HeightOneSpectrum A)
⊢ ∀ (v : HeightOneSpectrum A → M), (∀ i ∈ s, v i ∈ primaryComponent M i.asIdeal) → ∑ i ∈ s, v i = 0 → ∀ i ∈ s, v i = 0
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
s : Finset (HeightOneSpectrum A)
p : HeightOneSpectrum A → M
hsum : ∑ i ∈ s, p i = 0
f : HeightOneSpectrum A → ℕ
hmem : ∀ i ∈ s, p i ∈ torsionBySet A M ↑(i.asIdeal ^ f i)
m : ℕ := s.sup f
⊢ iSupIndep fun i ↦ torsionBySet A M ↑(i.asIdeal ^ m)

Tactic:
iSupIndep_iff_supIndep

Goal state after:
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
s : Finset (HeightOneSpectrum A)
p : HeightOneSpectrum A → M
hsum : ∑ i ∈ s, p i = 0
f : HeightOneSpectrum A → ℕ
hmem : ∀ i ∈ s, p i ∈ torsionBySet A M ↑(i.asIdeal ^ f i)
m : ℕ := s.sup f
⊢ ∀ (s : Finset (HeightOneSpectrum A)), s.SupIndep fun i ↦ torsionBySet A M ↑(i.asIdeal ^ m)
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
⊢ φ ↑(f P) = φ b

Tactic:
rw [eq_comm, ← sub_eq_zero]

Goal state after:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
⊢ φ b - φ ↑(f P) = 0
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case pos
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 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1

Tactic:
rw [if_pos hx, hx, zero_add, zero_add]

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ a * b < ∞ ↔ a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0

Tactic:
constructor
  · intro h
    rw [← or_assoc, or_iff_not_imp_right, or_iff_not_imp_right]
    intro hb ha
    exact ⟨lt_top_of_mul_ne_top_left h.ne hb, lt_top_of_mul_ne_top_right h.ne ha⟩
  · rintro (⟨ha, hb⟩ | rfl | rfl) <;> [exact mul_lt_top ha hb; simp; simp]

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

Goal state before:
pp: a b c : ℝ≥0∞
hc : c ≠ ∞
⊢ c + a - (c + b) = a - b

Tactic:
simp_rw [add_comm c]

Goal state after:
a b c : ℝ≥0∞
hc : c ≠ ∞
⊢ a + c - (b + c) = a - b
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inl
a c : ℝ≥0∞
h : a ≠ ∞ ∨ ∞ ≠ ∞
⊢ a - ∞ < c → a < ∞ + c

Tactic:
rw [top_add, lt_top_iff_ne_top]

Goal state after:
case inl
a c : ℝ≥0∞
h : a ≠ ∞ ∨ ∞ ≠ ∞
⊢ a - ∞ < c → a ≠ ∞
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
⊢ (iSup f).toNNReal = ⨆ i, (f i).toNNReal

Tactic:
by
  lift f to ι → ℝ≥0 using hf
  simp_rw [toNNReal_coe]
  by_cases h : BddAbove (range f)
  · rw [← coe_iSup h, toNNReal_coe]
  · rw [NNReal.iSup_of_not_bddAbove h, iSup_coe_eq_top.2 h, toNNReal_top]

Goal state after:
Module: Mathlib.Topology.UniformSpace.OfFun

Goal state before:
pp: X : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : PartialOrder M
d : X → X → M
refl : ∀ (x : X), d x x = 0
symm : ∀ (x y : X), d x y = d y x
triangle : ∀ (x y z : X), d x z ≤ d x y + d y z
half : ∀ ε > 0, ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε
r : M
hr : r > 0
⊢ SetRel.id ⊆ {x | d x.1 x.2 < r}

Tactic:
simp [Set.subset_def, *]

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

Goal state before:
pp: x : ℝ
⊢ Real.toEReal '' Ioi x = Ioo ↑x ⊤

Tactic:
refine (image_comp WithBot.some WithTop.some _).trans ?_
  rw [WithTop.image_coe_Ioi, WithBot.image_coe_Ioo]
  rfl

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ a < b⁻¹ ↔ b < a⁻¹

Tactic:
simpa only [inv_inv] using @ENNReal.inv_lt_inv a⁻¹ b

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

Goal state before:
pp: case hp₁
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
exps : HeightOneSpectrum R → ℤ
⊢ ∀ (x y : FractionalIdeal R⁰ K), count K v x = 0 → count K v y = 0 → count K v (x * y) = 0

Tactic:
intro I

Goal state after:
case hp₁
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
exps : HeightOneSpectrum R → ℤ
I : FractionalIdeal R⁰ K
⊢ ∀ (y : FractionalIdeal R⁰ K), count K v I = 0 → count K v y = 0 → count K v (I * y) = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0
hz : a ≠ 0
⊢ ↑a / 2 < ↑a

Tactic:
rw [← coe_two, ← coe_div, coe_lt_coe]

Goal state after:
a : ℝ≥0
hz : a ≠ 0
⊢ a / 2 < a

a : ℝ≥0
hz : a ≠ 0
⊢ 2 ≠ 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x : ℝ≥0∞
n : ℤ
⊢ x⁻¹ ^ n = (x ^ n)⁻¹

Tactic:
cases n <;> simp [ENNReal.inv_pow]

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

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

Tactic:
rintro ⟨i, hi⟩

Goal state after:
ι : Sort u_1
κ : Sort u_2
f : ι → ℝ≥0∞
a : ℝ≥0∞
g : κ → ℝ≥0∞
hf : ∃ i, f i ≠ ∞
ha : ∀ (i : ι) (j : κ), a ≤ f i * g j
this✝ : Nonempty { a // f a ≠ ∞ }
this : Nonempty κ
hg : ⨅ j, g j ≠ ∞
i : ι
hi : f i ≠ ∞
⊢ a ≤ f ↑⟨i, hi⟩ * ⨅ j, g j
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 z : E
⊢ f (x⁻¹ * z) ≤ f (x⁻¹ * y) + f (y⁻¹ * z)

Tactic:
convert! map_mul_le_add f (x⁻¹ * y) (y⁻¹ * z) using 2

Goal state after:
case e'_3
𝓕 : 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 z : E
⊢ x⁻¹ * z = x⁻¹ * y * (y⁻¹ * z)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y ≤ ε₂
z : α
hz : z ∈ ball x ε₁
⊢ dist z x + dist x y < ε₁ + dist x y

Tactic:
by gcongr; exact hz

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y ≤ ε₂
z : α
hz : z ∈ closedBall x ε₁
⊢ dist z x + dist x y ≤ ε₁ + dist x y

Tactic:
by gcongr; exact hz

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : ε₁ + dist x y < ε₂
z : α
hz : z ∈ closedBall x ε₁
⊢ dist z x + dist x y ≤ ε₁ + dist x y

Tactic:
by gcongr; exact hz

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

Goal state before:
pp: ι : Sort u_1
r : ℝ
ha : 0 ≤ r
f : ι → ℝ
⊢ (⨆ i, f i) * r = ⨆ i, f i * r

Tactic:
by
  simp only [Real.mul_iSup_of_nonneg ha, mul_comm]

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

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝ : Bornology β
f : α → β
⊢ Bornology.IsBounded (f '' univ) ↔ Bornology.IsBounded (range f)

Tactic:
image_univ

Goal state after:
α : Type u_5
β : Type u_6
inst✝ : Bornology β
f : α → β
⊢ Bornology.IsBounded (range f) ↔ Bornology.IsBounded (range f)
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
⊢ TotallyBounded s

Tactic:
rcases s.eq_empty_or_nonempty with hs | hs
  · rw [hs]
    exact totallyBounded_empty
  rcases hs with ⟨x0, hx0⟩
  have : Inhabited s := ⟨⟨x0, hx0⟩⟩
  refine totallyBounded_iff.2 fun ε ε0 => ?_
  rcases H ε ε0 with ⟨β, fβ, F, hF⟩
  let Finv := Function.invFun F
  refine ⟨range (Subtype.val ∘ Finv), finite_range _, fun x xs => ?_⟩
  let x' := Finv (F ⟨x, xs⟩)
  have : F x' = F ⟨x, xs⟩ := Function.invFun_eq ⟨⟨x, xs⟩, rfl⟩
  simp only [Set.mem_iUnion, Set.mem_range]
  exact ⟨_, ⟨F ⟨x, xs⟩, rfl⟩, hF _ _ this.symm⟩

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
f : Filter α
⊢ Cauchy f ↔ f.NeBot ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε

Tactic:
exact uniformity_basis_edist.cauchy_iff

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
ι : Type u_2
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
rcases mem_uniformity_edist.1 hu with ⟨ε, εpos, hε⟩

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
ι : Type u_2
inst✝ : TopologicalSpace β
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
x : β
hx : x ∈ s
ε : ℝ≥0∞
εpos : ε > 0
hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
Module: Mathlib.Topology.EMetricSpace.Basic

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

Tactic:
rcases mem_uniformity_edist.1 hu with ⟨ε, εpos, hε⟩

Goal state after:
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
s : Set β
H : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, edist (f x) (F n x) < ε
u : Set (α × α)
hu : u ∈ 𝓤 α
ε : ℝ≥0∞
εpos : ε > 0
hε : ∀ {a b : α}, edist a b < ε → (a, b) ∈ u
⊢ ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < r
h : ∀ (b : β), nndist (f b) (g b) ≤ r
b : β
⊢ r ≤ nndist (f b) (g b) ↔ nndist (f b) (g b) ≤ r ∧ r ≤ nndist (f b) (g b)

Tactic:
apply (and_iff_right <| h _).symm

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

Goal state before:
pp: X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ edist = edist

Tactic:
exact hd

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

Goal state before:
pp: X : Type u_2
m : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ dist = dist

Tactic:
exact hd

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

Goal state before:
pp: X : Type u_2
m : EMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ edist = edist

Tactic:
exact hd

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

Goal state before:
pp: X : Type u_2
m : MetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ dist = dist

Tactic:
exact hd

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

Goal state before:
pp: α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
⊢ Filter.atTop ≤ cobounded α

Tactic:
intro s

Goal state after:
α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
s : Set α
⊢ s ∈ cobounded α → s ∈ Filter.atTop
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
s : Set α
hs : BddBelow sᶜ ∧ BddAbove sᶜ
b : α
hb : b ∈ upperBounds sᶜ
c : α
hbc : b < c
x : α
hx : x ∈ {b | c ≤ b}
⊢ x ∈ s

Tactic:
by_contra hx'

Goal state after:
α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
s : Set α
hs : BddBelow sᶜ ∧ BddAbove sᶜ
b : α
hb : b ∈ upperBounds sᶜ
c : α
hbc : b < c
x : α
hx : x ∈ {b | c ≤ b}
hx' : x ∉ s
⊢ False
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
⊢ Filter.atTop ≤ cobounded α

Tactic:
intro s hs
  rw [← compl_compl s, ← isBounded_def, isBounded_iff_bddBelow_bddAbove] at hs
  obtain ⟨b, hb⟩ := hs.2
  obtain ⟨c, hbc⟩ := exists_gt b
  refine Filter.mem_of_superset (Filter.mem_atTop c) fun x hx ↦ ?_
  by_contra hx'
  exact hbc.not_ge <| hx.trans <| hb <| mem_compl hx'

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

Goal state before:
pp: α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
⊢ cobounded α ≤ Filter.atBot ⊔ Filter.atTop

Tactic:
intro s

Goal state after:
α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
⊢ s ∈ Filter.atBot ⊔ Filter.atTop → s ∈ cobounded α
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
⊢ {s | IsPreconnected s} ⊆
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Tactic:
intro s

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
⊢ s ∈ {s | IsPreconnected s} →
    s ∈
      range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
        (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})