mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Extension R A
inst✝ : FormallySmooth R P.Ring
⊢ FormallySmooth R A ↔ ∃ l, l ∘ₗ P.cotangentComplex = LinearMap.id

Tactic:
refine (Algebra.FormallySmooth.iff_split_injection P.algebraMap_surjective).trans ?_
  let e : P.ker.Cotangent ≃ₗ[P.Ring] P.Cotangent :=
    { __ := AddEquiv.refl _, map_smul' r m := by ext1; simp; rfl }
  constructor
  · intro ⟨l, hl⟩
    exact ⟨(e.comp l).extendScalarsOfSurjective P.algebraMap_surjective,
      LinearMap.ext (DFunLike.congr_fun hl : _)⟩
  · intro ⟨l, hl⟩
    exact ⟨e.symm.toLinearMap ∘ₗ l.restrictScalars P.Ring,
      LinearMap.ext (DFunLike.congr_fun hl : _)⟩

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

Goal state before:
pp: case add
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
Q : Generators S T ι
y : Q.Ring
x₁ x₂ : MvPolynomial ι S
hx₁ : (δAux R Q) (x₁ * y) = x₁ • (δAux R Q) y + y • (δAux R Q) x₁
hx₂ : (δAux R Q) (x₂ * y) = x₂ • (δAux R Q) y + y • (δAux R Q) x₂
⊢ (δAux R Q) ((x₁ + x₂) * y) = (x₁ + x₂) • (δAux R Q) y + y • (δAux R Q) (x₁ + x₂)

Tactic:
simp only [add_mul, map_add, hx₁, hx₂, add_smul, smul_add]; abel

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
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
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
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
x : ↥Q.ker
hx : x ∈ (Q.ker • ⊤).toAddSubgroup
⊢ ∀ r ∈ Q.ker, ∀ n ∈ ⊤, r • n ∈ (↑f').ker

Tactic:
clear x hx

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
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
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
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
⊢ ∀ r ∈ Q.ker, ∀ n ∈ ⊤, r • n ∈ (↑f').ker
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case tmul.tmul
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
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
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
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
a : Q.Ring
b : ↥P.ker
c : Q.Ring
d : ↥P.ker
h₂ : ↑b • Cotangent.mk d = 0
⊢ a • (c • 1) ⊗ₜ[S] 0 = 0

Tactic:
tmul_zero,

Goal state after:
case tmul.tmul
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
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
H : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
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
e : Q.Ring ⊗[P.Ring] ↥P.ker ≃ₗ[Q.Ring] ↥Q.ker :=
  LinearEquiv.ofBijective (LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) H
f' : ↥Q.ker →ₗ[Q.Ring] T ⊗[S] P.Cotangent :=
  LinearMap.liftBaseChange Q.Ring (↑P.Ring ((TensorProduct.mk S T P.Cotangent) 1) ∘ₗ Cotangent.mk) ∘ₗ ↑e.symm
a : Q.Ring
b : ↥P.ker
c : Q.Ring
d : ↥P.ker
h₂ : ↑b • Cotangent.mk d = 0
⊢ a • 0 = 0
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: case left
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
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : T ⊗[S] P.H1Cotangent
hx : (LinearMap.liftBaseChange T (H1Cotangent.map f)) x = 0
⊢ (tensorCotangent f halg H₂) ((LinearMap.lTensor T h1Cotangentι) x) = 0

Tactic:
← h1Cotangentι.map_zero,

Goal state after:
case left
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
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
x : T ⊗[S] P.H1Cotangent
hx : (LinearMap.liftBaseChange T (H1Cotangent.map f)) x = 0
⊢ (tensorCotangent f halg H₂) ((LinearMap.lTensor T h1Cotangentι) x) = h1Cotangentι 0
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
x✝ : ↥M'
y : P.Ring
hy : y ∈ M'
⊢ IsUnit (((IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) ↑⟨y, hy⟩)

Tactic:
by simpa using IsLocalization.map_units T ⟨algebraMap P.Ring S y, hy⟩

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
x : H1Cotangent R S
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
x✝ : ↥M'
y : P.Ring
hy : y ∈ M'
⊢ IsUnit (((IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) ↑⟨y, hy⟩)

Tactic:
by simpa using IsLocalization.map_units T ⟨algebraMap P.Ring S y, hy⟩

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 : α
ha' : a ∈ ⋃ i ∈ s, S i
i : ι
hi : i ∈ s
ha : a ∈ S i
⊢ (⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a = 0

Tactic:
by simp [ha, ha']

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

Tactic:
symm

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
⊢ ∑ x ∈ s.powerset with x.Nonempty, -((-1) ^ #x • (⋂ i ∈ x, S i).indicator f a) = 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
h₁ : s.Nonempty
h₂ : BddBelow s
⊢ IsGLB s (sInf s)

Tactic:
sInf_def,

Goal state after:
s : Set ℝ
h₁ : s.Nonempty
h₂ : BddBelow s
⊢ IsGLB s (-sSup (-s))
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ι : Sort u_2
s : ι → ℝ≥0
⊢ ↑(sSup (Set.range fun i ↦ s i)) = sSup (Set.range fun i ↦ ↑(s i))

Tactic:
coe_sSup,

Goal state after:
ι : Sort u_2
s : ι → ℝ≥0
⊢ sSup (toReal '' Set.range fun i ↦ s i) = sSup (Set.range fun i ↦ ↑(s i))
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r p : ℝ
hr : 0 ≤ r
hp : 0 ≤ p
⊢ ↑(r + p).toNNReal = ↑(r.toNNReal + p.toNNReal)

Tactic:
by simp [hr, hp, add_nonneg]

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

Goal state before:
pp: n : ℤ
⊢ ↑↑n.natAbs = ↑(nnabs ↑n)

Tactic:
NNReal.coe_natCast,

Goal state after:
n : ℤ
⊢ ↑n.natAbs = ↑(nnabs ↑n)
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: b : ℝ
hb : 0 < b
⊢ ∃ n, 0 < n ∧ (↑n)⁻¹ < b

Tactic:
refine (exists_nat_gt b⁻¹).imp fun k hk ↦ ?_
  have := (inv_pos_of_pos hb).trans hk
  refine ⟨Nat.cast_pos.mp this, ?_⟩
  rwa [inv_lt_comm₀ this hb]

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✝² : Group E
inst✝¹ : Group F
inst✝ : Group G
p✝ q : GroupSeminorm E
f✝ : F →* E
p : GroupSeminorm E
f : F →* E
⊢ p (f 1) = 0

Tactic:
f.map_one,

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 : GroupSeminorm E
f : F →* E
⊢ p 1 = 0
Module: Mathlib.Data.ENNReal.Operations

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

Tactic:
rintro (⟨ha, hb⟩ | rfl | rfl)

Goal state after:
case mpr.inl
a b : ℝ≥0∞
ha : a < ∞
hb : b < ∞
⊢ a * b < ∞

case mpr.inr.inl
b : ℝ≥0∞
⊢ 0 * b < ∞

case mpr.inr.inr
a : ℝ≥0∞
⊢ a * 0 < ∞
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: p q : ℝ
hq : 0 ≤ q
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

Tactic:
obtain h | h := le_total p q

Goal state after:
case inl
p q : ℝ
hq : 0 ≤ q
h : p ≤ q
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q

case inr
p q : ℝ
hq : 0 ≤ q
h : q ≤ p
⊢ ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
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 I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
⊢ spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * (↑J' * ↑J) =
    spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')

Tactic:
spanSingleton_mul_spanSingleton,

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
v : HeightOneSpectrum R
I I' : FractionalIdeal R⁰ K
hI : I ≠ 0
hI' : I' ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
a : R
J : Ideal R
ha : a ≠ 0
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
ha_ne_zero : Associates.mk (Ideal.span {a}) ≠ 0
hJ_ne_zero : Associates.mk J ≠ 0
a' : R
J' : Ideal R
ha' : a' ≠ 0
haJ' : I' = spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J'
ha'_ne_zero : Associates.mk (Ideal.span {a'}) ≠ 0
hJ'_ne_zero : Associates.mk J' ≠ 0
⊢ spanSingleton R⁰ (((algebraMap R K) a)⁻¹ * ((algebraMap R K) a')⁻¹) * (↑J' * ↑J) =
    spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')
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
x✝ : r > 0
x : X × X
hx : x ∈ {x | d x.1 x.2 < r}
⊢ d x.swap.1 x.swap.2 < r

Tactic:
symm

Goal state after:
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
x✝ : r > 0
x : X × X
hx : x ∈ {x | d x.1 x.2 < r}
⊢ d x.swap.2 x.swap.1 < r
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case mp
x : EReal
⊢ x = ⊥ → ∀ (y : ℝ), x < ↑y

pp: case mpr
x : EReal
⊢ (∀ (y : ℝ), x < ↑y) → x = ⊥

Tactic:
· rintro rfl
    exact bot_lt_coe

Goal state after:
case mpr
x : EReal
⊢ (∀ (y : ℝ), x < ↑y) → x = ⊥
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
⊢ count K v (∏ i ∈ insert i s, I i) = ∑ i ∈ insert i s, count K v (I i)

Tactic:
have hS' : ∀ i ∈ s, I i ≠ 0 := fun j hj => hS j (Finset.mem_insert_of_mem hj)

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
⊢ 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 : ℝ
⊢ WithBot.some ∘ WithTop.some ⁻¹' Ici ↑↑x = Ici x

Tactic:
refine preimage_comp.trans ?_

Goal state after:
x : ℝ
⊢ WithTop.some ⁻¹' WithBot.some ⁻¹' Ici ↑↑x = Ici x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ
⊢ WithBot.some ∘ WithTop.some ⁻¹' Ioi ↑↑x = Ioi x

Tactic:
refine preimage_comp.trans ?_

Goal state after:
x : ℝ
⊢ WithTop.some ⁻¹' WithBot.some ⁻¹' Ioi ↑↑x = Ioi x
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: ⊢ WithBot.some ∘ WithTop.some ⁻¹' Ioi ⊥ = univ

Tactic:
refine preimage_comp.trans ?_

Goal state after:
⊢ WithTop.some ⁻¹' WithBot.some ⁻¹' Ioi ⊥ = univ
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: y : ℝ
⊢ WithBot.some ∘ WithTop.some ⁻¹' Iic ↑↑y = Iic y

Tactic:
refine preimage_comp.trans ?_

Goal state after:
y : ℝ
⊢ WithTop.some ⁻¹' WithBot.some ⁻¹' Iic ↑↑y = Iic y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: y : ℝ
⊢ WithBot.some ∘ WithTop.some ⁻¹' Iio ↑↑y = Iio y

Tactic:
refine preimage_comp.trans ?_

Goal state after:
y : ℝ
⊢ WithTop.some ⁻¹' WithBot.some ⁻¹' Iio ↑↑y = Iio y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: ⊢ WithBot.some ∘ WithTop.some ⁻¹' Iio ↑⊤ = univ

Tactic:
refine preimage_comp.trans ?_

Goal state after:
⊢ WithTop.some ⁻¹' WithBot.some ⁻¹' Iio ↑⊤ = univ
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ≥0
⊢ ↑(∞ * ↑x) = ⊤ * ↑↑x

Tactic:
rcases eq_or_ne x 0 with (rfl | h0)
  · simp
  · rw [ENNReal.top_mul (ENNReal.coe_ne_zero.2 h0)]
    exact Eq.symm <| if_pos <| NNReal.coe_pos.2 h0.bot_lt

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

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

Tactic:
rw [lt_inv_iff_lt_inv, inv_one]

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
I : FractionalIdeal R⁰ K
hI : ¬I = 0
x✝ : HeightOneSpectrum R
⊢ count K x✝ I =
    ↑((Associates.mk x✝.asIdeal).count (Associates.mk (choose ⋯)).factors) -
      ↑((Associates.mk x✝.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors)

Tactic:
rw [count_ne_zero K _ hI]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ x ∈ closedBall y ε ↔ y ∈ closedBall x ε

Tactic:
mem_closedBall',

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ dist y x ≤ ε ↔ y ∈ closedBall x ε
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
inst✝ : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ iInf g * h

Tactic:
rw [iInf_mul]

Goal state after:
ι : Sort u_3
inst✝ : Nonempty ι
a : ℝ≥0
g : ι → ℝ≥0
h : ℝ≥0
H : ∀ (i : ι), a ≤ g i * h
⊢ a ≤ ⨅ i, g i * h
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
a✝ b✝ : α
s✝ : Set α
x : α
inst✝ : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
u : Set α
u_open : IsOpen[inst✝⁴] u
xu : x ∈ u
us : u ∩ {x}ᶜ ⊆ s
a b : α
a_lt_b : a < b
hab : Ioo a b ⊆ u
hy : a < x ∧ x < b
⊢ s.Nonempty

Tactic:
obtain ⟨z, hz⟩ : ∃ z, a < z ∧ z < x := exists_between hy.1

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
a✝ b✝ : α
s✝ : Set α
x : α
inst✝ : Nontrivial α
s : Set α
hs : s ∈ 𝓝[≠] x
u : Set α
u_open : IsOpen[inst✝⁴] u
xu : x ∈ u
us : u ∩ {x}ᶜ ⊆ s
a b : α
a_lt_b : a < b
hab : Ioo a b ⊆ u
hy : a < x ∧ x < b
z : α
hz : a < z ∧ z < x
⊢ s.Nonempty
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: case refine_2
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : NoMinOrder α
inst✝ : ClosedIicTopology α
s : Set α
hs : s ∈ cocompact α
t : Set α
ht : IsCompact t
hts : tᶜ ⊆ s
h_nonempty : t.Nonempty
⊢ s ∈ atBot

Tactic:
have := h_nonempty.nonempty
    obtain ⟨a, ha⟩ := ht.exists_isLeast h_nonempty
    obtain ⟨b, hb⟩ := exists_lt a
    exact Filter.mem_atBot_sets.mpr ⟨b, fun b' hb' ↦ hts <| Classical.byContradiction
      fun hc ↦ LT.lt.false <| hb'.trans_lt <| hb.trans_le <| ha.2 (not_notMem.mp hc)⟩

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

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : NoMaxOrder α
f : β → α
a : α
hs : IsCompact ∅
hf : ContinuousOn f ∅
hf' : ∀ b ∈ ∅, a < f b
a' : α
ha' : a < a'
⊢ ∃ a', a < a' ∧ ∀ b ∈ ∅, a' ≤ f b

Tactic:
exact ⟨a', ha', fun _ a ↦ a.elim⟩

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

Goal state before:
pp: case inl
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : NoMaxOrder α
f : β → α
a : α
hs : IsCompact ∅
hf : ContinuousOn f ∅
hf' : ∀ b ∈ ∅, a < f b
⊢ ∃ a', a < a' ∧ ∀ b ∈ ∅, a' ≤ f b

Tactic:
obtain ⟨a', ha'⟩ := exists_gt a
    exact ⟨a', ha', fun _ a ↦ a.elim⟩

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

Goal state before:
pp: case neg
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : BddBelow s
ha : ¬BddAbove s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}

pp: case pos
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}

pp: case neg
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}

Tactic:
· refine Or.inr <| Or.inr <| Or.inr <| Or.inr ?_
    rcases mem_Ici_Ioi_of_subset_of_subset (hs.Ioi_csInf_subset hb ha) fun x hx ↦
      csInf_le hb hx with hs | hs
    · exact Or.inl hs
    · exact Or.inr (Or.inl hs)

Goal state after:
case pos
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : BddAbove s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}

case neg
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected s
hne : s.Nonempty
hs' : IsConnected s
hb : ¬BddBelow s
ha : ¬BddAbove s
⊢ s ∈
    {Icc (sInf s) (sSup s), Ico (sInf s) (sSup s), Ioc (sInf s) (sSup s), Ioo (sInf s) (sSup s), Ici (sInf s),
      Ioi (sInf s), Iic (sSup s), Iio (sSup s), univ, ∅}
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ b ∈ closedBall a r ↔ ‖a⁻¹ * b‖ ≤ r

Tactic:
mem_closedBall',

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
r : ℝ
⊢ dist a b ≤ r ↔ ‖a⁻¹ * b‖ ≤ r
Module: Mathlib.Analysis.Normed.Group.Basic

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

Tactic:
simp [nndist_eq_nnnorm_inv_mul]

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

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

Tactic:
simp [nndist_eq_nnnorm_inv_mul]

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ b ∈ closedBall a r ↔ ‖a / b‖ ≤ r

Tactic:
mem_closedBall',

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ dist a b ≤ r ↔ ‖a / b‖ ≤ r
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoMetricSpace α
f : β → α
hf : Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (𝓤 α)
⊢ Bornology.IsBounded (range f)

Tactic:
by
  rcases (hasBasis_cofinite.prod_self.tendsto_iff uniformity_basis_dist).1 hf 1 zero_lt_one with
    ⟨s, hsf, hs1⟩
  rw [← image_union_image_compl_eq_range]
  refine (hsf.image f).isBounded.union (isBounded_image_iff.2 ⟨1, fun x hx y hy ↦ ?_⟩)
  exact le_of_lt (hs1 (x, y) ⟨hx, hy⟩)

Goal state after: