mathlib-initiative/mathlib-tactics huggingface dataset:
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₂
⊢ x₁ • (δAux R Q) y + y • (δAux R Q) x₁ + (x₂ • (δAux R Q) y + y • (δAux R Q) x₂) =
    x₁ • (δAux R Q) y + x₂ • (δAux R Q) y + (y • (δAux R Q) x₁ + y • (δAux R Q) x₂)

Tactic:
abel

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

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
l : S ⊗[P] Ω[P⁄R] →ₗ[P] ↥(RingHom.ker (algebraMap P S))
hl : l ∘ₗ kerToTensor R P S = LinearMap.id
σ : S → P
hσ : ∀ (x : S), (algebraMap P S) (σ x) = x
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
⊢ σ 1 - ↑(l (1 ⊗ₜ[P] (D R P) (σ 1))) = 1

Tactic:
by simp [sectionOfRetractionKerToTensorAux_prop l hl (σ 1) 1 (by simp [hσ])]

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

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
s : S
t : P
⊢ (tensorKaehlerQuotKerSqEquiv R P S).symm (s ⊗ₜ[P] (D R P) t) =
    s ⊗ₜ[P ⧸ RingHom.ker (algebraMap P S) ^ 2]
      (D R (P ⧸ RingHom.ker (algebraMap P S) ^ 2)) ((Ideal.Quotient.mk (RingHom.ker (algebraMap P S) ^ 2)) t)

Tactic:
apply (tensorKaehlerQuotKerSqEquiv R P S).injective
  simp

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

Tactic:
by
      simp [sub_eq_neg_add, ← sum_neg_distrib, filter_eq', pow_succ, ha]

Goal state after:
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ ↑j
ik : ε⁻¹ ≤ ↑k
j0 : 0 < j
k0 : 0 < k
y : ℝ
yS : y ∈ s
hy : ↑(↑(f j) / ↑j) ≤ y
⊢ ↑(f j) / ↑j - ↑(f k) / ↑k < ε

Tactic:
refine lt_of_lt_of_le ((Rat.cast_lt (K := ℝ)).1 ?_) ((inv_le_comm₀ ε0 (Nat.cast_pos.2 k0)).1 ik)

Goal state after:
s : Set ℝ
L : ℝ
hL : L ∈ s
U : ℝ
hU : U ∈ upperBounds s
this : ∀ (d : ℕ), BddAbove {m | ∃ y ∈ s, ↑m ≤ y * ↑d}
f : ℕ → ℤ
hf : ∀ (d : ℕ), f d ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d} ∧ ∀ z ∈ {m | ∃ y ∈ s, ↑m ≤ y * ↑d}, z ≤ f d
hf₁ : ∀ n > 0, ∃ y ∈ s, ↑(↑(f n) / ↑n) ≤ y
hf₂ : ∀ n > 0, ∀ y ∈ s, y - (↑n)⁻¹ < ↑(↑(f n) / ↑n)
ε : ℚ
ε0 : ε > 0
j k : ℕ
ij : ε⁻¹ ≤ ↑j
ik : ε⁻¹ ≤ ↑k
j0 : 0 < j
k0 : 0 < k
y : ℝ
yS : y ∈ s
hy : ↑(↑(f j) / ↑j) ≤ y
⊢ ↑(↑(f j) / ↑j - ↑(f k) / ↑k) < ↑(↑k)⁻¹
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
⊢ ∃ x, f ≈ const abs x

Tactic:
refine ⟨sSup s, ((lt_total _ _).resolve_left fun h => ?_).resolve_right fun h => ?_⟩

Goal state after:
case refine_1
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
h : f < const abs (sSup s)
⊢ False

case refine_2
f : CauSeq ℝ abs
s : Set ℝ := {x | const abs x < f}
lb : ∃ x, x ∈ s
ub' : ∀ (x : ℝ), f < const abs x → ∀ y ∈ s, y ≤ x
ub : ∃ x, ∀ y ∈ s, y ≤ x
h : const abs (sSup s) < f
⊢ False
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: r p : ℝ
hr : 0 ≤ r
hp : 0 ≤ p
⊢ r.toNNReal = p.toNNReal ↔ r = p

Tactic:
by simp [← coe_inj, hr, hp]

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

Goal state before:
pp: case inl
s : Set ℝ
h : s.OrdConnected
x : ℝ
hx : x ∈ s
y : ℝ
hy : y ∈ s
z : ℝ≥0
hz : x.toNNReal ≤ z ∧ z = 0
hy₀ : y ≤ 0
⊢ z ∈ toNNReal '' s

Tactic:
exact ⟨y, hy, (toNNReal_of_nonpos hy₀).trans hz.2.symm⟩

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

Goal state before:
pp: case inr
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ∞
h✝ : Nonempty ι
⊢ (iInf f).toNNReal = ⨅ i, (f i).toNNReal

Tactic:
· lift f to ι → ℝ≥0 using hf
    simp_rw [← coe_iInf, toNNReal_coe]

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

Goal state before:
pp: case refine_2
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd✝ : Disjoint s (closure[inst✝¹] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
b : X
hab : a ≤ b
hmem' : Icc a b ∈ 𝓝[≥] a
hsub : Icc a b ⊆ tᶜ
c : X
hc : c ∈ (s.ordSeparatingSet t).ordConnectedSection
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
hac : a < c
x : X
hx : x ∈ Ico a c
hx' : x ∈ (s.ordSeparatingSet t).ordConnectedSection
⊢ [[x, c]] ⊆ ⋃ x ∈ t, sᶜ.ordConnectedComponent x

Tactic:
rcases mem_iUnion₂.1 (ordConnectedSection_subset hx').2 with ⟨y, hyt, hxy⟩
      refine subset_iUnion₂_of_subset y hyt (OrdConnected.uIcc_subset inferInstance hxy ?_)
      refine subset_ordConnectedComponent left_mem_uIcc hxy ?_
      suffices c < y by
        rw [uIcc_of_ge (hx.2.trans this).le]
        exact ⟨hx.2.le, this.le⟩
      refine lt_of_not_ge fun hyc => ?_
      have hya : y < a := not_le.1 fun hay => hsub ⟨hay, hyc.trans hcb⟩ hyt
      exact hxy (Icc_subset_uIcc ⟨hya.le, hx.1⟩) ha

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
hi0 : I i ≠ 0
⊢ count K v (∏ i ∈ insert i s, I i) = ∑ i ∈ insert i s, count K v (I i)

Tactic:
Finset.prod_insert hi,

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 i * ∏ x ∈ s, I x) = ∑ i ∈ insert i s, count K v (I i)
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: x : ℝ≥0∞
⊢ 0 < x ↔ x ≠ 0

Tactic:
pos_iff_ne_zero

Goal state after:
x : ℝ≥0∞
⊢ x ≠ 0 ↔ x ≠ 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b ≠ 0 ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a

Tactic:
rw [← ENNReal.inv_ne_top] at hzero

Goal state after:
a b : ℝ≥0∞
htop : b⁻¹ ≠ 0 ∨ a ≠ ∞
hzero : b⁻¹ ≠ ∞ ∨ a ≠ 0
⊢ (a / b)⁻¹ = b / a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b c : ℝ≥0∞
h : a < b * c
⊢ a < b / c⁻¹

Tactic:
rwa [div_eq_mul_inv, inv_inv]

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

Goal state before:
pp: case inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
⊢ sInf (a • ∅) = a • sInf ∅

Tactic:
smul_set_empty,

Goal state after:
case inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
⊢ sInf ∅ = a • sInf ∅
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
⊢ sSup (a • ∅) = a • sSup ∅

Tactic:
smul_set_empty,

Goal state after:
case inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : MulActionWithZero α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : 0 ≤ a
⊢ sSup ∅ = a • sSup ∅
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
⊢ sInf (a • ∅) = a • sSup ∅

Tactic:
smul_set_empty,

Goal state after:
case inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
⊢ sInf ∅ = a • sSup ∅
Module: Mathlib.Data.Real.Pointwise

Goal state before:
pp: case inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
⊢ sSup (a • ∅) = a • sInf ∅

Tactic:
smul_set_empty,

Goal state after:
case inl
α : Type u_2
inst✝⁴ : Field α
inst✝³ : LinearOrder α
inst✝² : IsStrictOrderedRing α
inst✝¹ : Module α ℝ
inst✝ : IsOrderedModule α ℝ
a : α
ha : a ≤ 0
⊢ sSup ∅ = a • sInf ∅
Module: Mathlib.Data.NNReal.Basic

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

Tactic:
rw [iSup_mul]
  exact ciSup_le' H

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
X : ι → Type u_4
inst✝³ : Bornology α
inst✝² : Bornology β
inst✝¹ : (i : ι) → Bornology (X i)
inst✝ : ∀ (i : ι), BoundedSpace (X i)
⊢ BoundedSpace ((i : ι) → X i)

Tactic:
by
  simp [← cobounded_eq_bot_iff, cobounded_pi]

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
ι : Type u_2
F : ι → β → α
f : β → α
p : Filter ι
⊢ TendstoUniformly F f p ↔ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ (x : β), edist (f x) (F n x) < ε

Tactic:
simp only [← tendstoUniformlyOn_univ, tendstoUniformlyOn_iff, mem_univ, forall_const]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this✝ : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
q : HeightOneSpectrum R
hq : q ∈ s
hqp : ¬q = p'
⊢ a p' ∈ J * (↑⟨q, hq⟩).asIdeal

Tactic:
refine Ideal.mul_mono_right ?_ (ha p' hp's)

Goal state after:
case neg
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
J I : Ideal R
hIJ : J * I ≤ J
hJ : ¬J = 0
hI : ¬I = 0
s : Finset (HeightOneSpectrum R) := ⋯.toFinset
this✝ : ∀ p ∈ s, J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
a : HeightOneSpectrum R → R
ha : ∀ p ∈ s, a p ∈ J * ∏ q ∈ s \ {p}, q.asIdeal
ha' : ∀ p ∈ s, a p ∉ J * ∏ q ∈ s, q.asIdeal
K : Ideal R
hK : Ideal.span {∑ p ∈ s, a p} = J * K
H : ¬I + K = ⊤
p : Ideal R
hp : p.IsMaximal
h : I + K ≤ p
p' : HeightOneSpectrum R := { asIdeal := p, isPrime := ⋯, ne_bot := ⋯ }
hp's : p' ∈ s
H₁ : ∑ p ∈ s, a p ∈ J * p
H₂ : ∑ q ∈ s \ {p'}, a q ∈ J * p
this : (s.inf fun i ↦ i.asIdeal) = ∏ i ∈ s, i.asIdeal
inst : Nonempty ↥s
q : HeightOneSpectrum R
hq : q ∈ s
hqp : ¬q = p'
⊢ ∏ q ∈ s \ {p'}, q.asIdeal ≤ (↑⟨q, hq⟩).asIdeal
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: a b : ℝ≥0
⊢ a ≤ b + nndist a b

Tactic:
suffices (a : ℝ) ≤ (b : ℝ) + dist a b by
    rwa [← NNReal.coe_le_coe, NNReal.coe_add, coe_nndist]

Goal state after:
a b : ℝ≥0
⊢ ↑a ≤ ↑b + dist a b
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : α
⊢ interior (Ico a b) = Ioo a b

Tactic:
by
  rw [← Ici_inter_Iio, interior_inter, interior_Ici, interior_Iio, Ioi_inter_Iio]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
s : Set α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : ¬ContinuousWithinAt f (s ∩ Ioi x) x
⊢ x ∈ s ∧ ∃ z, f x < z ∧ ∀ y ∈ s, x < y → z ≤ f y

Tactic:
contrapose! hx

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
s : Set α
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : SecondCountableTopology β
hf : MonotoneOn f s
x : α
xs : x ∈ s
hx : x ∈ s → ∀ (z : β), f x < z → ∃ y ∈ s, x < y ∧ f y < z
⊢ ContinuousWithinAt f (s ∩ Ioi x) x
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: case h
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖y‖ = 0
⊢ ‖y⁻¹‖ = 0

Tactic:
rwa [norm_inv']

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
s : Set α
hs : IsClosed[inst✝³] (s ∩ Icc a b)
ha : a ∈ s
h : ∀ t ∈ Ico a b, Icc a t ⊆ s → s ∈ 𝓝[>] t
⊢ Icc a b ⊆ s

Tactic:
rcases lt_or_ge b a with hab | hab
  · simp_all
  set A := {t ∈ Icc a b | Icc a t ⊆ s}
  have a_mem : a ∈ A := ⟨left_mem_Icc.mpr hab, by simp [ha]⟩
  have bdd_A : BddAbove A := ⟨b, fun t ht ↦ ht.1.2⟩
  set t₁ := sSup A
  have t₁_mem : t₁ ∈ Icc a b := ⟨le_csSup bdd_A a_mem, csSup_le ⟨a, a_mem⟩ (fun t ht ↦ ht.1.2)⟩
  obtain ⟨⟨t₁a, t₁b⟩, ht₁⟩ : t₁ ∈ A := by
    refine ⟨t₁_mem, fun t ht ↦ ?_⟩
    rcases ht.2.eq_or_lt with rfl | h
    · have : closure A ⊆ s ∩ Icc a b := by
        apply (closure_subset_iff hs).2 (fun t ht ↦ ⟨?_, ht.1⟩)
        have : t ∈ Icc a t := ⟨ht.1.1, le_rfl⟩
        exact ht.2 this
      apply this.trans inter_subset_left
      exact csSup_mem_closure ⟨a, a_mem⟩ bdd_A
    · obtain ⟨c, cA, tc⟩ : ∃ c ∈ A, t < c := (lt_csSup_iff bdd_A ⟨a, a_mem⟩).1 h
      apply cA.2
      exact ⟨ht.1, tc.le⟩
  suffices t₁ = b by simpa [this] using ht₁
  apply eq_of_le_of_not_lt t₁b fun t₁b' ↦ ?_
  obtain ⟨m, t₁m, H⟩ : ∃ m > t₁, Ioo t₁ m ⊆ s :=
    (mem_nhdsGT_iff_exists_Ioo_subset' t₁b').mp (h t₁ ⟨t₁a, t₁b'⟩ (fun s hs ↦ ht₁ hs))
  obtain ⟨t, hat, ht⟩ : ∃ t, t₁ < t ∧ t < min m b := exists_between (lt_min t₁m t₁b')
  have : t ∈ A := by
    refine ⟨⟨by order, ht.le.trans (min_le_right _ _)⟩, fun t' ht' ↦ ?_⟩
    rcases le_or_gt t' t₁ with h't' | h't'
    · exact ht₁ ⟨ht'.1, h't'⟩
    · exact H ⟨h't', ht'.2.trans_lt <| ht.trans_le <| min_le_left ..⟩
  have : t ≤ t₁ := le_csSup bdd_A this
  order

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

Goal state before:
pp: case neg
α : Type u
inst✝⁷ : TopologicalSpace α
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : OrderTopology α
inst✝⁴ : DenselyOrdered α
δ : Type u_1
inst✝³ : LinearOrder δ
inst✝² : TopologicalSpace δ
inst✝¹ : OrderClosedTopology δ
inst✝ : BoundedOrder α
f : α → δ
hf_c : Continuous[inst✝⁷, inst✝²] f
hf : f ⊥ ≤ f ⊤
hf_i : Injective f
a b : α
hab : a < b
h : f b ≤ f a
H : f b < f a
ha : f ⊥ < f a
hb : f b ≤ f ⊥
⊢ False

Tactic:
· replace hb : f b < f ⊥ := lt_of_le_of_ne hb <| hf_i.ne (lt_of_lt_of_le' hab bot_le).ne'
      obtain ⟨u, hu⟩ := intermediate_value_Ioo' hab.le hf_c.continuousOn ⟨hb, ha⟩
      have : u = ⊥ := hf_i hu.2
      simp_all

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

Goal state before:
pp: α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
⊢ f x < f y

Tactic:
have hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t) := by
    have : Fact (s ≤ t) := ⟨hsa.trans <| hbt.trans' hab.le⟩
    have := Continuous.strictMono_of_inj_boundedOrder' (f := Set.domRestrict (Icc s t) f)
      hf_c.continuousOn.domRestrict hf_i.injOn.injective
    exact this.imp strictMono_domRestrict.mp strictAntiOn_iff_strictAnti.mpr

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
a b : α
hab : a < b
hf_mono : StrictMonoOn f (Icc a b)
x y : α
hxy : x < y
s : α := min a x
t : α := max b y
hsa : s ≤ a
hbt : b ≤ t
hf_mono_st : StrictMonoOn f (Icc s t) ∨ StrictAntiOn f (Icc s t)
⊢ f x < f y
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
U : Set β
hUo : IsOpen[inst✝] U
hkU : k ⊆ U
t : Set α
ht : t ∈ cobounded α
hd : Disjoint (U ∩ s) (f ⁻¹' id t)
⊢ U ∩ s ⊆ f ⁻¹' tᶜ

Tactic:
preimage_compl,

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
this : Disjoint (𝓝ˢ k ⊓ 𝓟 s) (comap f (cobounded α))
U : Set β
hUo : IsOpen[inst✝] U
hkU : k ⊆ U
t : Set α
ht : t ∈ cobounded α
hd : Disjoint (U ∩ s) (f ⁻¹' id t)
⊢ U ∩ s ⊆ (f ⁻¹' t)ᶜ
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
hbot : H ≠ ⊥
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
⊢ ∃ b, IsLeast {g | g ∈ H ∧ 1 < g} b

Tactic:
by
  -- todo: move to a lemma?
  have hex : ∀ g > 1, ∃ n : ℕ, g ∈ Ioc (a ^ n) (a ^ (n + 1)) := fun g hg => by
    rcases existsUnique_mul_zpow_mem_Ico h₀ 1 (g / a) with ⟨m, ⟨hm, hm'⟩, -⟩
    simp only [one_mul, div_le_iff_le_mul, div_mul_cancel, ← zpow_add_one] at hm hm'
    lift m to ℕ
    · rw [← Int.lt_add_one_iff, ← zpow_lt_zpow_iff_right h₀, zpow_zero]
      exact hg.trans_le hm
    · simp only [← Nat.cast_succ, zpow_natCast] at hm hm'
      exact ⟨m, hm', hm⟩
  have : ∃ n : ℕ, Set.Nonempty (H ∩ Ioc (a ^ n) (a ^ (n + 1))) := by
    rcases (bot_or_exists_ne_one H).resolve_left hbot with ⟨g, hgH, hg₀⟩
    rcases hex |g|ₘ (one_lt_mabs.2 hg₀) with ⟨n, hn⟩
    exact ⟨n, _, (@mabs_mem_iff (Subgroup G) G _ _).2 hgH, hn⟩
  classical rcases Nat.findX this with ⟨n, ⟨x, hxH, hnx, hxn⟩, hmin⟩
  by_contra hxmin
  simp only [IsLeast, not_and, mem_ofPred_eq, mem_lowerBounds, not_exists, not_forall,
    not_le] at hxmin
  rcases hxmin x ⟨hxH, (one_le_pow_of_one_le'  h₀.le _).trans_lt hnx⟩ with ⟨y, ⟨hyH, hy₀⟩, hxy⟩
  obtain ⟨m, hm, hya⟩ := hex y hy₀
  rcases lt_or_ge m n with hmn | hnm
  · exact hmin m hmn ⟨y, hyH, hm, hya⟩
  · refine disjoint_left.1 hd (div_mem hxH hyH) ⟨one_lt_div'.2 hxy, div_lt_iff_lt_mul'.2 ?_⟩
    calc x ≤ a ^ (n + 1) := hxn
    _ ≤ a ^ (m + 1) := by grw [hnm]; exact h₀.le
    _ = a ^ m * a := pow_succ _ _
    _ < y * a := by gcongr

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

Goal state before:
pp: r₁ r₂ : ℚ
⊢ dist r₁ r₂ = ‖↑(-r₁ + r₂)‖

Tactic:
simp only [dist_eq, norm, cast_add, cast_neg]
    rw [← abs_neg, neg_sub]
    abel_nf

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

Goal state before:
pp: case of_equiv
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
α✝ β✝ : Type u_4
e : α✝ ≃ β✝
I : β✝ → Ideal R
ih :
  emultiplicity p.asIdeal (sSup (range fun i ↦ (I ∘ ⇑e) i)) = sInf (range fun i ↦ emultiplicity p.asIdeal ((I ∘ ⇑e) i))
⊢ emultiplicity p.asIdeal (sSup (range fun i ↦ I i)) = sInf (range fun i ↦ emultiplicity p.asIdeal (I i))

Tactic:
EquivLike.range_comp I e

Goal state after:
case of_equiv
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDedekindDomain R
p : HeightOneSpectrum R
ι : Type u_4
inst✝ : Finite ι
α✝ β✝ : Type u_4
e : α✝ ≃ β✝
I : β✝ → Ideal R
ih : emultiplicity p.asIdeal (sSup (range I)) = sInf (range fun i ↦ emultiplicity p.asIdeal ((I ∘ ⇑e) i))
⊢ emultiplicity p.asIdeal (sSup (range fun i ↦ I i)) = sInf (range fun i ↦ emultiplicity p.asIdeal (I i))
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: motive : EReal → Sort u_1
coe : (x : ℝ≥0∞) → motive ↑x
neg_coe : (x : ℝ≥0∞) → 0 < x → motive (-↑x)
x : ℝ≥0∞
⊢ recENNReal coe neg_coe ↑x = coe x

Tactic:
suffices ∀ y : EReal, x = y → (recENNReal coe neg_coe y : motive y) ≍ coe x from
    heq_iff_eq.mp (this x rfl)
  intro y hy
  have H₁ : 0 ≤ y := hy ▸ coe_ennreal_nonneg x
  obtain rfl : y.toENNReal = x := by simp [← hy]
  simp [recENNReal, H₁]

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

Goal state before:
pp: case bot
a c : EReal
hb : ⊥ ≠ ⊥ ∨ c ≠ ⊥
ht : ⊥ ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c - ⊥ ↔ a + ⊥ ≤ c

Tactic:
simp only [ne_eq, not_true_eq_false, false_or] at hb

Goal state after:
case bot
a c : EReal
ht : ⊥ ≠ ⊤ ∨ c ≠ ⊤
hb : ¬c = ⊥
⊢ a ≤ c - ⊥ ↔ a + ⊥ ≤ c
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case coe
a b : EReal
c : ℝ
h : a ≤ b + ↑c
⊢ a - ↑c ≤ b

Tactic:
exact (sub_le_iff_le_add (.inl (coe_ne_bot c)) (.inl (coe_ne_top c))).2 h

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

Goal state before:
pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ (⊤ * ↑x✝).toReal = ⊤.toReal * (↑x✝).toReal

Tactic:
| top_pos _ h =>

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

Goal state before:
pp: case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ -⊤ * ↑x✝ = -(⊤ * ↑x✝)

Tactic:
| top_pos _ h =>

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

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : L.NeBot
hf : Multipliable f L
⊢ ∏'[L] (i : ι), f i ≤ a₂

pp: case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : L.NeBot
hf : ¬Multipliable f L
⊢ ∏'[L] (i : ι), f i ≤ a₂

Tactic:
· exact hf.tprod_le_of_prod_le h

Goal state after:
case neg
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst✝³ : CommMonoid α
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a₂ : α
ha₂ : 1 ≤ a₂
h : ∀ (s : Finset ι), ∏ i ∈ s, f i ≤ a₂
hL : L.NeBot
hf : ¬Multipliable f L
⊢ ∏'[L] (i : ι), f i ≤ a₂
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a : α
L : SummationFilter β
inst✝ : ContinuousMul α
hf : HasProd f a L
n : ℕ
hn : HasProd (fun x ↦ f x ^ n) (a ^ n) L
⊢ HasProd (fun x ↦ f x ^ (n + 1)) (a ^ (n + 1)) L

Tactic:
| succ n hn =>

Goal state after: