mathlib-initiative/mathlib-tactics huggingface dataset:
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 : α
ha : a ∈ ⋃ i ∈ s, S i
this : (⋃ i ∈ s, S i).indicator 1 a = 1
⊢ (∏ i ∈ s, (1 - (S i).indicator 1 a)) • f a = 0

Tactic:
rw [← this, prod_indicator_biUnion_sub_indicator, zero_smul]

Goal state after:
case hs
ι : 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
this : (⋃ i ∈ s, S i).indicator 1 a = 1
⊢ s.Nonempty
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case hbc
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
k : ℤ
hk : U < ↑k
d : ℕ
z : ℤ
y : ℝ
yS : y ∈ s
hy : ↑z ≤ y * ↑d
⊢ y ≤ ↑k

Tactic:
exact (hU yS).trans hk.le

Goal state after:
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
⊢ ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I

Tactic:
have h_ne_zero : v.maxPowDividing I ≠ 0 := pow_ne_zero _ v.ne_bot

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
⊢ ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
      ∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: α : Sort u_2
⊢ ↑(⨅ x, 0) = ↑0

Tactic:
coe_iInf

Goal state after:
α : Sort u_2
⊢ ⨅ i, ↑0 = ↑0
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 : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
⊢ ¬(algebraMap R K) a₁ = 0

Tactic:
← (algebraMap R K).map_zero,

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 : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
⊢ ¬(algebraMap R K) a₁ = (algebraMap R K) 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) ≤ max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)

pp: case neg
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) ≤ max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)

Tactic:
· simp_rw [if_pos hx, hx, zero_add]
          exact le_max_of_le_right (le_refl _)

Goal state after:
case neg
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) ≤ max (if x = 0 then 0 else 1) (if y = 0 then 0 else 1)
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 : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
⊢ ¬(algebraMap R K) a = 0

Tactic:
← (algebraMap R K).map_zero,

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 : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
h_aJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
⊢ ¬(algebraMap R K) a = (algebraMap R K) 0
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case pos
x : EReal
h : x ≠ ⊤
h' : x = ⊥
⊢ x ≤ ↑x.toReal

Tactic:
simp only [h', bot_le]

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

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

Tactic:
by
  rw [← Ici_inter_Iio]
  simp

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

Goal state before:
pp: x : EReal
⊢ x.toENNReal = ∞ ↔ x = ⊤

Tactic:
by_cases h : x = ⊤
  · simp [h]
  · simp [h, toENNReal]

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

Goal state before:
pp: m n : ℕ
⊢ ↑m = ↑n ↔ m = n

Tactic:
by
  rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_eq_coe_iff, Nat.cast_inj]

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
hv : ↑v.asIdeal ≠ 0
h_self : ↑v.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑v.asIdeal
hv_irred : Irreducible (Associates.mk v.asIdeal)
⊢ ↑1 = 1

Tactic:
ofNat_one

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
hv : ↑v.asIdeal ≠ 0
h_self : ↑v.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑v.asIdeal
hv_irred : Irreducible (Associates.mk v.asIdeal)
⊢ 1 = 1
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
n : ℤ
⊢ count K v (↑v.asIdeal ^ n) = n

Tactic:
by
  rw [count_zpow, count_self, mul_one]

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

Goal state before:
pp: a b c : ℝ≥0∞
h₁ : a ≠ 0 ∨ b ≠ ∞
h₂ : a ≠ ∞ ∨ b ≠ 0
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ c ≤ a * b

Tactic:
rw [← ENNReal.inv_le_inv, ENNReal.mul_inv h₁ h₂]

Goal state after:
a b c : ℝ≥0∞
h₁ : a ≠ 0 ∨ b ≠ ∞
h₂ : a ≠ ∞ ∨ b ≠ 0
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ a⁻¹ * b⁻¹ ≤ c⁻¹
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case hI
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
J : Ideal R
hJ : J ≠ 0
⊢ ↑J ≠ 0

Tactic:
simpa only [ne_eq, coeIdeal_eq_zero]

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

Goal state before:
pp: ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Tactic:
by_cases hf : ∀ i, f i = 0

Goal state after:
case pos
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i = 0
⊢ a * ⨆ i, f i = ⨆ i, a * f i

case neg
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
⊢ a * ⨆ i, f i = ⨆ i, a * f i
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
s : Set ℝ≥0∞
c : R
⊢ c • 1 * sSup s = ⨆ a ∈ s, c • a

Tactic:
ENNReal.mul_sSup,

Goal state after:
R : Type u_3
inst✝¹ : SMul R ℝ≥0∞
inst✝ : IsScalarTower R ℝ≥0∞ ℝ≥0∞
s : Set ℝ≥0∞
c : R
⊢ ⨆ b ∈ s, c • 1 * b = ⨆ a ∈ s, c • a
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ edist x y = ↑(nndist x y)

Tactic:
edist_dist,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ ENNReal.ofReal (dist x y) = ↑(nndist x y)
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
r : ℝ
⊢ edist x y < ENNReal.ofReal r ↔ dist x y < r

Tactic:
edist_dist,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
r : ℝ
⊢ ENNReal.ofReal (dist x y) < ENNReal.ofReal r ↔ dist x y < r
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
r : ℝ
hr : 0 ≤ r
⊢ edist x y ≤ ENNReal.ofReal r ↔ dist x y ≤ r

Tactic:
edist_dist,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
r : ℝ
hr : 0 ≤ r
⊢ ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal r ↔ dist x y ≤ r
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ dist x y = (edist x y).toReal

Tactic:
edist_dist,

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ dist x y = (ENNReal.ofReal (dist x y)).toReal
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

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

Tactic:
by rw [dist_comm, mem_ball]

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

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

Tactic:
rw [dist_comm, mem_sphere]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ PseudoMetricSpace.toUniformSpace = ⊥ ↔ ∃ r, 0 < r ∧ Pairwise fun x1 x2 ↦ r ≤ dist x1 x2

Tactic:
by
  simp only [uniformity_basis_dist.uniformSpace_eq_bot, mem_ofPred_eq, not_lt]

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

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
⊢ ENNReal.ofReal (dist x z) ≤ ENNReal.ofReal (dist x y + dist y z)

Tactic:
rw [ENNReal.ofReal_le_ofReal_iff _]

Goal state after:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
⊢ dist x z ≤ dist x y + dist y z

α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
x y z : α
⊢ 0 ≤ dist x y + dist y z
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
ι' : Sort u_4
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
f : ι → ℝ≥0
g : ι' → ℝ≥0
a : ℝ≥0
h : ∀ (i : ι) (j : ι'), a ≤ f i + g j
⊢ ↑a ≤ (⨅ i, ↑(f i)) + ↑(⨅ j, g j)

Tactic:
coe_iInf

Goal state after:
ι : Sort u_3
ι' : Sort u_4
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
f : ι → ℝ≥0
g : ι' → ℝ≥0
a : ℝ≥0
h : ∀ (i : ι) (j : ι'), a ≤ f i + g j
⊢ ↑a ≤ (⨅ i, ↑(f i)) + ⨅ i, ↑(g i)
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨅ i, ↑(f i)) * ↑a = ↑(⨅ i, f i * a)

Tactic:
coe_iInf

Goal state after:
ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ (⨅ i, ↑(f i)) * ↑a = ⨅ i, ↑(f i * a)
Module: Mathlib.Topology.Metrizable.Basic

Goal state before:
pp: ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : LindelofSpace X
inst✝ : PseudoMetrizableSpace X
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
V : ℕ → SetRel X X
hVb : (𝓤 X).HasAntitoneBasis V
hVs : ∀ (n : ℕ), (V n).IsSymm
U : ℕ → Set X
hUc : ∀ (n : ℕ), (U n).Countable
hUu : ∀ (n : ℕ), ⋃ x ∈ U n, ball x (V n) = univ
x : X
n : ℕ
a✝ : True
i : X
hi : i ∈ U n
hx : x ∈ {y | (y, i) ∈ V n}
⊢ ∃ x_1 ∈ V n, ∃ a, (x, a) = x_1 ∧ a ∈ iUnion U

Tactic:
exact ⟨(x, i), hx, i, rfl, Set.mem_iUnion_of_mem n hi⟩

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝² : PseudoEMetricSpace α
X : β → Type u_2
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
⊢ 𝓤 ((b : β) → X b) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | edist p.1 p.2 < ε}

Tactic:
by
    simp only [Pi.uniformity, PseudoEMetricSpace.uniformity_edist, comap_iInf, gt_iff_lt,
      preimage_ofPred_eq, comap_principal, edist_pi_def]
    rw [iInf_comm]; congr; funext ε
    rw [iInf_comm]; congr; funext εpos
    simp [ofPred_forall, εpos]

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

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
ha : IsLUB s a
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
⊢ f x ≤ b

Tactic:
replace ha := ha.inter_Ici_of_mem hx

Goal state after:
α : Type u_1
γ : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderClosedTopology γ
f : α → γ
s : Set α
a : α
b : γ
hf : MonotoneOn f s
hb : Tendsto f (𝓝[s] a) (𝓝 b)
x : α
hx : x ∈ s
ha : IsLUB (s ∩ Ici x) a
⊢ f x ≤ b
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: case refine_1
β : Type u_2
inst✝³ : Fintype β
Y : Type u_4
inst✝² : PseudoMetricSpace Y
inst✝¹ : Zero Y
inst✝ : DecidableEq β
i j : β
a b : Y
h : i ≠ j
k : β
⊢ nndist (Pi.single i a k) (Pi.single j b k) ≤ max (nndist a 0) (nndist b 0)

Tactic:
simp only [Pi.single_apply]
    by_cases hki : k = i <;> by_cases hkj : k = j <;> simp_all [nndist_comm]

Goal state after:
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)
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
← forall_isBounded_image_eval_iff,

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)) ↔ BddBelow s ∧ BddAbove s
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)
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
simp_rw [← forall_isBounded_image_eval_iff, bddBelow_pi, bddAbove_pi, ← forall_and,
      isBounded_iff_bddBelow_bddAbove]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
b : α
left✝¹ : True
hb : Iic b ⊆ s
a : α
left✝ : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
⊢ b ≤ x

Tactic:
by_contra! hx'

Goal state after:
case refine_1
α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
b : α
left✝¹ : True
hb : Iic b ⊆ s
a : α
left✝ : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
hx' : x < b
⊢ False
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
b : α
left✝¹ : True
hb : Iic b ⊆ s
a : α
left✝ : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
⊢ x ≤ a

Tactic:
by_contra! hx'

Goal state after:
case refine_2
α : Type u_1
inst✝² : Bornology α
inst✝¹ : LinearOrder α
inst✝ : IsOrderBornology α
this : Nonempty α
s : Set α
b : α
left✝¹ : True
hb : Iic b ⊆ s
a : α
left✝ : True
ha : Ici a ⊆ s
x : α
hx : x ∈ sᶜ
hx' : a < x
⊢ False
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝⁴ : Bornology α
inst✝³ : LinearOrder α
inst✝² : IsOrderBornology α
inst✝¹ : NoMaxOrder α
inst✝ : OrderBot α
s : Set α
x✝ : ∃ i, True ∧ Ici i ⊆ s
b : α
left✝ : True
hb : Ici b ⊆ s
x : α
hx : x ∈ sᶜ
⊢ x ≤ b

Tactic:
by_contra! hx'

Goal state after:
α : Type u_1
inst✝⁴ : Bornology α
inst✝³ : LinearOrder α
inst✝² : IsOrderBornology α
inst✝¹ : NoMaxOrder α
inst✝ : OrderBot α
s : Set α
x✝ : ∃ i, True ∧ Ici i ⊆ s
b : α
left✝ : True
hb : Ici b ⊆ s
x : α
hx : x ∈ sᶜ
hx' : b < x
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case refine_2
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 : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
⊢ Submodule.comap (↑I).subtype ↑J ≤
    Submodule.comap ((↑I').subtype ∘ₗ LinearMap.restrict ((Algebra.lsmul R R K) (I'.divMod I J')) ⋯) ↑J'

Tactic:
LinearMap.subtype_comp_restrict,

Goal state after:
case refine_2
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 : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
⊢ Submodule.comap (↑I).subtype ↑J ≤
    Submodule.comap (LinearMap.domRestrict ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I) ↑J'
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : CompactIccSpace α
a b : αᵒᵈ
⊢ IsCompact (Icc a b)

Tactic:
convert! isCompact_Icc (α := α) (a := b) (b := a) using 1

Goal state after:
case e'_3
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : CompactIccSpace α
a b : αᵒᵈ
e_1✝ : αᵒᵈ = α
⊢ Icc a b = Icc b a
Module: Mathlib.Topology.Order.Compact

Goal state before:
pp: α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
H : ¬(s ∩ ⋂ x, Iic ↑x).Nonempty
⊢ False

Tactic:
not_nonempty_iff_eq_empty

Goal state after:
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : s.Nonempty
this : Nonempty ↑s
H : s ∩ ⋂ x, Iic ↑x = ∅
⊢ False
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: case refine_3
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 : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
⊢ Submodule.map (Submodule.comap (↑I).subtype ↑J).mkQ
      (Submodule.comap ((↑I').subtype ∘ₗ LinearMap.restrict ((Algebra.lsmul R R K) (I'.divMod I J')) ⋯) ↑J') =
    ⊥

Tactic:
LinearMap.subtype_comp_restrict,

Goal state after:
case refine_3
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 : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J
⊢ Submodule.map (Submodule.comap (↑I).subtype ↑J).mkQ
      (Submodule.comap (LinearMap.domRestrict ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I) ↑J') =
    ⊥
Module: Mathlib.RingTheory.DedekindDomain.Factorization

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

Tactic:
obtain rfl : J' = I' := by simpa [H'] using divMod_spec h' hJ' hI
      obtain rfl : I = J := mul_left_injective₀ hJ' (H.trans (mul_comm _ _))
      exact inf_le_left

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
r : ℝ
hpos : 0 < r
hr : ∀ (x : E), x ≠ 1 → r ≤ ‖x‖
x y : E
hne : x ≠ y
⊢ (fun x1 x2 ↦ r ≤ dist x1 x2) x y

Tactic:
simp only [dist_eq_norm_inv_mul]

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
r : ℝ
hpos : 0 < r
hr : ∀ (x : E), x ≠ 1 → r ≤ ‖x‖
x y : E
hne : x ≠ y
⊢ r ≤ ‖x⁻¹ * y‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ edist a b = ‖a⁻¹ * b‖ₑ

Tactic:
edist_dist,

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a b : E
⊢ ENNReal.ofReal (dist a b) = ‖a⁻¹ * b‖ₑ
Module: Mathlib.Topology.EMetricSpace.Diam

Goal state before:
pp: X : Type u_2
s t : Set X
inst✝ : PseudoEMetricSpace X
h : (s ∩ t).Nonempty
x : X
xs : x ∈ s
xt : x ∈ t
⊢ ediam (s ∪ t) ≤ ediam s + ediam t

Tactic:
simpa using ediam_union_le_add_edist xs xt

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist a b = ‖a / b‖

Tactic:
dist_eq_norm_div

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ ‖a / b‖ = ‖a / b‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ edist a b = ‖a / b‖ₑ

Tactic:
edist_dist,

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ ENNReal.ofReal (dist a b) = ‖a / b‖ₑ
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ dist b a < r ↔ ‖b / a‖ < r

Tactic:
dist_eq_norm_div

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ ‖b / a‖ < r ↔ ‖b / a‖ < r
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ dist a b < r ↔ ‖a / b‖ < r

Tactic:
dist_eq_norm_div

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ ‖a / b‖ < r ↔ ‖a / b‖ < r
Module: Mathlib.Analysis.Normed.Group.Basic

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

Tactic:
dist_eq_norm_div

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ ‖b / a‖ ≤ r ↔ ‖b / a‖ ≤ r
Module: Mathlib.Analysis.Normed.Group.Basic

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

Tactic:
dist_eq_norm_div

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ ‖a / b‖ ≤ r ↔ ‖a / b‖ ≤ r
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
r : ℝ
⊢ a • closedBall b r = closedBall (a • b) r

Tactic:
by
  ext
  simp [mem_closedBall, Set.mem_smul_set, dist_eq_norm_inv_mul, ← eq_inv_mul_iff_mul_eq, mul_assoc]

Goal state after: