mathlib-initiative/mathlib-tactics huggingface dataset:
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
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
P' : Type u_2 := P ⧸ RingHom.ker (algebraMap P S) ^ 2
h₁ : Surjective ⇑(algebraMap P' S)
h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥
e₁ : (RingHom.ker (algebraMap P S)).Cotangent ≃ₗ[P] ↥(RingHom.ker (algebraMap P' S)) :=
  (RingHom.ker (algebraMap P S)).cotangentEquivIdeal ≪≫ₗ
    LinearEquiv.restrictScalars P
      (LinearEquiv.ofEq (RingHom.ker (IsScalarTower.toAlgHom R P S).toRingHom).cotangentIdeal
        (RingHom.ker (IsScalarTower.toAlgHom R P S).kerSquareLift.toRingHom) ⋯)
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)
H : kerCotangentToTensor R P S = ↑e₂ ∘ₗ ↑P (kerToTensor R P' S) ∘ₗ ↑e₁
⊢ { l // l ∘ₗ kerCotangentToTensor R P S = LinearMap.id } ≃
    { g // (IsScalarTower.toAlgHom R P S).kerSquareLift.comp g = AlgHom.id R S }

Tactic:
refine Equiv.trans ?_ (retractionKerToTensorEquivSection (R := R) h₂ h₁)

Goal state after:
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
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
P' : Type u_2 := P ⧸ RingHom.ker (algebraMap P S) ^ 2
h₁ : Surjective ⇑(algebraMap P' S)
h₂ : RingHom.ker (algebraMap P' S) ^ 2 = ⊥
e₁ : (RingHom.ker (algebraMap P S)).Cotangent ≃ₗ[P] ↥(RingHom.ker (algebraMap P' S)) :=
  (RingHom.ker (algebraMap P S)).cotangentEquivIdeal ≪≫ₗ
    LinearEquiv.restrictScalars P
      (LinearEquiv.ofEq (RingHom.ker (IsScalarTower.toAlgHom R P S).toRingHom).cotangentIdeal
        (RingHom.ker (IsScalarTower.toAlgHom R P S).kerSquareLift.toRingHom) ⋯)
e₂ : S ⊗[P'] Ω[P'⁄R] ≃ₗ[P] S ⊗[P] Ω[P⁄R] := LinearEquiv.restrictScalars P (tensorKaehlerQuotKerSqEquiv R P S)
H : kerCotangentToTensor R P S = ↑e₂ ∘ₗ ↑P (kerToTensor R P' S) ∘ₗ ↑e₁
⊢ { l // l ∘ₗ kerCotangentToTensor R P S = LinearMap.id } ≃ { l // l ∘ₗ kerToTensor R P' S = LinearMap.id }
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case h
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
hy : ∀ a ∈ I ^ n₁, a • y = 0
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ a ∈ I ^ n₂, a • z = 0
a : A
⊢ a ∈ I ^ max n₁ n₂ → a • (y + z) = 0

Tactic:
ha

Goal state after:
case h
A : Type u_1
M : Type u_2
inst✝² : CommRing A
I : Ideal A
inst✝¹ : AddCommGroup M
inst✝ : Module A M
N₁ N₂ : Submodule A M
hD : Disjoint N₁ N₂
y : M
hymem : y ∈ N₁
n₁ : ℕ
hy : ∀ a ∈ I ^ n₁, a • y = 0
z : M
hzmem : z ∈ N₂
n₂ : ℕ
hz : ∀ a ∈ I ^ n₂, a • z = 0
a : A
ha : a ∈ I ^ max n₁ n₂
⊢ a • (y + z) = 0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ
⊢ (Set.range fun i ↦ f i) = ∅

Tactic:
Set.range_eq_empty_iff

Goal state after:
ι : Sort u_1
inst✝ : IsEmpty ι
f : ι → ℝ
⊢ IsEmpty ι
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 q : GroupSeminorm E
⊢ (⇑p ⊔ ⇑q) 1 = 0

Tactic:
by
        rw [Pi.sup_apply, ← map_one_eq_zero p, sup_eq_left, map_one_eq_zero p, map_one_eq_zero q]

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

Goal state before:
pp: b a : ℝ≥0
h : ↑a = ∞ → ↑b = ∞
h_nnreal : ↑a ≠ ∞ → ↑b ≠ ∞ → (↑a).toNNReal ≤ (↑b).toNNReal
hlt : ↑b < ↑a
⊢ False

Tactic:
refine hlt.not_ge ?_

Goal state after:
b a : ℝ≥0
h : ↑a = ∞ → ↑b = ∞
h_nnreal : ↑a ≠ ∞ → ↑b ≠ ∞ → (↑a).toNNReal ≤ (↑b).toNNReal
hlt : ↑b < ↑a
⊢ ↑a ≤ ↑b
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a : ℝ≥0∞
⊢ a * ∞ = if a = 0 then 0 else ∞

Tactic:
by convert! WithTop.mul_top' a

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

Goal state before:
pp: case mp
a b : ℝ≥0∞
h : a * b < ∞
hb : ¬b = 0
⊢ ¬a = 0 → a < ∞ ∧ b < ∞

Tactic:
ha

Goal state after:
case mp
a b : ℝ≥0∞
h : a * b < ∞
hb : ¬b = 0
ha : ¬a = 0
⊢ a < ∞ ∧ b < ∞
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b c : ℝ≥0∞
hab : b ≤ a
b_ne_top : b ≠ ∞
⊢ a - b + c = a + c - b

Tactic:
by_cases c_top : c = ∞
  · simpa [c_top] using! ENNReal.eq_sub_of_add_eq b_ne_top rfl
  refine ENNReal.eq_sub_of_add_eq b_ne_top ?_
  simp only [add_assoc, add_comm c b]
  simpa only [← add_assoc] using! (add_left_inj c_top).mpr <| tsub_add_cancel_of_le hab

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

Goal state before:
pp: X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
s t : Set X
hd : Disjoint s (closure[inst✝¹] t)
x : X
hx : x ∈ s
⊢ tᶜ ∈ 𝓝 x

Tactic:
by
      rw [← mem_interior_iff_mem_nhds, interior_compl]
      exact disjoint_left.1 hd hx

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
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)⁻¹ * ↑J * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')

Tactic:
haJ',

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)⁻¹ * ↑J * (spanSingleton R⁰ ((algebraMap R K) a')⁻¹ * ↑J') =
    spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case inr
ι : Sort u_1
f g : ι → ℝ≥0∞
h : ∀ (i j : ι), ∃ k, f i + g j ≤ f k + g k
h✝ : Nonempty ι
⊢ iSup f + iSup g = ⨆ i, f i + g i

Tactic:
refine le_antisymm ?_ (iSup_le fun a => add_le_add (le_iSup _ _) (le_iSup _ _))
    refine iSup_add_iSup_le fun i j => ?_
    rcases h i j with ⟨k, hk⟩
    exact le_iSup_of_le k hk

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
x✝ : r > 0
x : X × X
hx : x ∈ {x | d x.1 x.2 < r}
⊢ x.swap ∈ {x | d x.1 x.2 < r}

Tactic:
by rwa [mem_ofPred, symm]

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

Goal state before:
pp: case inr
a : ℝ≥0
n : ℕ
ha : a ≠ 0
this : a ^ (n + 1) ≠ 0
⊢ (a ^ (n + 1))⁻¹ = a⁻¹ ^ (n + 1)

Tactic:
inv_pow

Goal state after:
case inr
a : ℝ≥0
n : ℕ
ha : a ≠ 0
this : a ^ (n + 1) ≠ 0
⊢ (a ^ (n + 1))⁻¹ = (a ^ (n + 1))⁻¹
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 ∈ fun i ↦ i = v → False, count K v (↑x.asIdeal ^ exps x) = 0

Tactic:
intro w hw

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 → ℤ
w : HeightOneSpectrum R
hw : w ∈ fun i ↦ i = v → False
⊢ count K v (↑w.asIdeal ^ exps w) = 0
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
⊢ y ∈ closedEBall x ε ↔ edist x y ≤ ε

Tactic:
by
  rw [edist_comm, mem_closedEBall]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x : α
ε : ℝ≥0∞
⊢ x ∈ closedEBall x ε

Tactic:
rw [mem_closedEBall, edist_self]; apply zero_le

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

Goal state before:
pp: α : Sort u_3
x y : α
dist : α → α → ℝ
dist_self : ∀ (x : α), dist x x = 0
dist_comm : ∀ (x y : α), dist x y = dist y x
dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
⊢ dist x y + dist y x = 2 * dist x y

Tactic:
by rw [two_mul, dist_comm]

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

Goal state before:
pp: 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
p : HeightOneSpectrum R
⊢ p ∈ s → J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal

Tactic:
hps

Goal state after:
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
p : HeightOneSpectrum R
hps : p ∈ s
⊢ J * ∏ q ∈ s, q.asIdeal < J * ∏ q ∈ s \ {p}, q.asIdeal
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure[inst✝³] (Ioc a b) = Icc a b

Tactic:
apply Subset.antisymm
  · exact closure_minimal Ioc_subset_Icc_self isClosed_Icc
  · apply Subset.trans _ (closure_mono Ioo_subset_Ioc_self)
    rw [closure_Ioo hab]

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
inst✝¹ : PseudoMetricSpace α
γ : Type w
inst✝ : MetricSpace γ
X : Type u_2
m : PseudoEMetricSpace X
d : X → X → ℝ≥0∞
hd : d = edist
⊢ 𝓤 X = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | d p.1 p.2 < ε}

Tactic:
by simp [hd, uniformity_edist]

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

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
h : DiscreteTopology α
⊢ inst✝³ = Preorder.topology α

Tactic:
h.eq_bot,

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
h : DiscreteTopology α
⊢ ⊥ = Preorder.topology α
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 α
x : α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hbx : b ≤ x
⊢ f b ≤ f x

pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
s : Set α
x : α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb : x ≤ b
⊢ f x ≤ f b

Tactic:
· rcases hbx.eq_or_lt with rfl | hbx
    · exact le_rfl
    simp only [ContinuousWithinAt] at h'x
    apply ge_of_tendsto h'x
    have : s ∩ Ioi b ∈ 𝓝[s] x := inter_mem_nhdsWithin _ (Ioi_mem_nhds hbx)
    filter_upwards [this] with y hy using hf hb hy.1 (le_of_lt hy.2)

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
s : Set α
x : α
f : α → β
inst✝¹ : TopologicalSpace β
inst✝ : OrderClosedTopology β
hf : MonotoneOn f s
hx : ClusterPt x (𝓟 s)
h'x : ContinuousWithinAt f s x
this : (𝓝[s] x).NeBot
b : α
hb : b ∈ s
hxb : x ≤ b
⊢ f x ≤ f b
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: case refine_1
α : 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
m : β
hm : m < f x
⊢ ∀ᶠ (b : α) in 𝓝[s ∩ Ioi x] x, m < f b

Tactic:
filter_upwards [@self_mem_nhdsWithin _ _ x (s ∩ Ioi x)] with y hy

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
m : β
hm : m < f x
y : α
hy : y ∈ s ∩ Ioi x
⊢ m < f y
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 | x ∈ s ∧ ¬ContinuousWithinAt f s x}.Countable

Tactic:
by
  apply (hf.countable_not_continuousWithinAt_Ioi.union hf.countable_not_continuousWithinAt_Iio).mono
  refine compl_subset_compl.1 ?_
  simp only [compl_union]
  rintro x ⟨hx, h'x⟩
  simp only [mem_compl_iff, mem_ofPred_eq, not_and, not_not] at hx h'x ⊢
  intro xs
  exact continuousWithinAt_iff_continuous_left'_right'.2 ⟨h'x xs, hx xs⟩

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : IsPreconnected 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:
by
  rcases s.eq_empty_or_nonempty with (rfl | hne)
  · apply_rules [Or.inr, mem_singleton]
  have hs' : IsConnected s := ⟨hne, hs⟩
  by_cases hb : BddBelow s <;> by_cases ha : BddAbove s
  · refine mem_of_subset_of_mem ?_ <| mem_Icc_Ico_Ioc_Ioo_of_subset_of_subset
      (hs'.Ioo_csInf_csSup_subset hb ha) (subset_Icc_csInf_csSup hb ha)
    simp only [insert_subset_iff, mem_insert_iff, mem_singleton_iff, true_or, or_true,
      singleton_subset_iff, and_self]
  · 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)
  · iterate 6 apply Or.inr
    rcases mem_Iic_Iio_of_subset_of_subset (hs.Iio_csSup_subset hb ha) fun x hx ↦
      le_csSup ha hx with hs | hs
    · exact Or.inl hs
    · exact Or.inr (Or.inl hs)
  · iterate 8 apply Or.inr
    exact Or.inl (hs.eq_univ_of_unbounded hb ha)

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℤ
⊢ ‖a ^ n.natAbs‖ = ‖a ^ n‖

Tactic:
← zpow_natCast,

Goal state after:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℤ
⊢ ‖a ^ ↑n.natAbs‖ = ‖a ^ n‖
Module: Mathlib.Topology.MetricSpace.Cauchy

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N ↦ (fun p ↦ dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
⊢ ∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)

Tactic:
have hS : ∀ N, ∃ x, ∀ y ∈ S N, y ≤ x := by
      rcases cauchySeq_bdd hs with ⟨R, -, hR⟩
      refine fun N => ⟨R, ?_⟩
      rintro _ ⟨⟨m, n⟩, _, rfl⟩
      exact le_of_lt (hR m n)

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : ℕ → α
hs : CauchySeq s
S : ℕ → Set ℝ := fun N ↦ (fun p ↦ dist (s p.1) (s p.2)) '' {p | p.1 ≥ N ∧ p.2 ≥ N}
hS : ∀ (N : ℕ), ∃ x, ∀ y ∈ S N, y ≤ x
⊢ ∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Tendsto b atTop (𝓝 0)
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : NormedGroup E
a : E
⊢ 0 < ‖a‖ ↔ a ≠ 1

Tactic:
by rw [← not_le, norm_le_zero_iff']

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

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

pp: case refine_4
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 : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ↑J' ≤ ↑I'

Tactic:
· exact le_trans (by simp) (divMod_spec h' hJ' hI).le

Goal state after:
case refine_4
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 : Submodule.map ((Algebra.lsmul R R K) (I'.divMod I J')) ↑I = ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I
⊢ ↑J' ≤ ↑I'
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
hf : CauchySeq f
⊢ Cauchy (map f Filter.cofinite)

Tactic:
rwa [Nat.cofinite_eq_atTop]

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

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

Tactic:
simp only [Int.cast_natCast, NNReal.coe_natCast]

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

Goal state before:
pp: case inl
y z t : EReal
h2 : z < t
h1 : ⊥ < y
⊢ ⊥ + z < y + t

Tactic:
simp [h1, bot_le.trans_lt h2]

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 : α✝ ≃ β✝
ih : ∀ (I : α✝ → Ideal R), emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)
I : β✝ → Ideal R
⊢ emultiplicity p.asIdeal (⨆ i, I i) = ⨅ i, emultiplicity p.asIdeal (I i)

Tactic:
specialize ih (I ∘ e)
    rw [← sSup_range, ← sInf_range] at ih ⊢
    rw [EquivLike.range_comp I e] at ih
    rw [ih]
    exact congrArg _ <| EquivLike.range_comp (emultiplicity p.asIdeal <| I ·) e

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
a : α
⊢ (∀ᶠ (n : β) in f, u n ≤ a) → ∀ (i : α), (∀ᶠ (n : β) in g, u n ≤ i) → sInf {a | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ a ⊔ i

Tactic:
ha

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
u : β → α
g : Filter β
a : α
ha : ∀ᶠ (n : β) in f, u n ≤ a
⊢ ∀ (i : α), (∀ᶠ (n : β) in g, u n ≤ i) → sInf {a | ∀ᶠ (n : β) in f ⊔ g, u n ≤ a} ≤ a ⊔ i
Module: Mathlib.Order.LiminfLimsup

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

Tactic:
rw [← forall_gt_iff_le]
    intro y x_y
    rcases h' y x_y with ⟨z, x_z, z_y⟩
    exact (limsup_le_of_le h₁ ((h z x_z).mono (fun _ ↦ le_of_lt))).trans_lt z_y

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

Goal state before:
pp: β : Type u_2
L : SummationFilter β
inst✝ : L.HasSupport
b : β
hb : ¬∀ᶠ (s : Finset β) in L.filter, b ∈ s
a : Finset β
⊢ ↑a ⊆ L.support → b ∉ a

Tactic:
ha

Goal state after:
β : Type u_2
L : SummationFilter β
inst✝ : L.HasSupport
b : β
hb : ¬∀ᶠ (s : Finset β) in L.filter, b ∈ s
a : Finset β
ha : ↑a ⊆ L.support
⊢ b ∉ a
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : ContinuousMul α
ι : Type u_4
s : Finset ι
t : ι → Set β
a : ι → α
hs : (↑s).Pairwise (Disjoint on t)
hf : ∀ i ∈ s, HasProd (f ∘ Subtype.val) (a i)
⊢ HasProd (f ∘ Subtype.val) (∏ i ∈ s, a i)

Tactic:
simp_rw [hasProd_subtype_iff_mulIndicator] at *

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
inst✝ : ContinuousMul α
ι : Type u_4
s : Finset ι
t : ι → Set β
a : ι → α
hs : (↑s).Pairwise (Disjoint on t)
hf : ∀ i ∈ s, HasProd ((t i).mulIndicator f) (a i)
⊢ HasProd ((⋃ i ∈ s, t i).mulIndicator f) (∏ i ∈ s, a i)
Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt

Goal state before:
pp: case refine_1
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
e : Set G
he : e ∈ 𝓝 1
⊢ ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e

pp: case refine_2
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
e : Set G
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e

Tactic:
· obtain ⟨s, hs⟩ := vanish e he
    refine ⟨if h : s.Nonempty then s.max' h + 1 else 0,
      fun t ht ↦ hs _ <| Set.disjoint_left.mpr ?_⟩
    split_ifs at ht with h
    · exact fun m hmt hms ↦ (s.le_max' _ hms).not_gt (Nat.succ_le_iff.mp <| ht hmt)
    · exact fun _ _ hs ↦ h ⟨_, hs⟩

Goal state after:
case refine_2
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : UniformSpace G
inst✝ : IsUniformGroup G
f : ℕ → G
vanish : ∀ e ∈ 𝓝 1, ∃ N, ∀ t ⊆ {n | N ≤ n}, ∏' (n : ↑t), f ↑n ∈ e
e : Set G
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Set ℕ), Disjoint t ↑s → ∏' (b : ↑t), f ↑b ∈ e
Module: Mathlib.Topology.Algebra.InfiniteSum.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
⊢ (if L.HasSupport ∧ ∅.Finite then 1 else if True then 1 else Exists.choose ⋯) = 1

Tactic:
if_true,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
L : SummationFilter β
⊢ (if L.HasSupport ∧ ∅.Finite then 1 else 1) = 1
Module: Mathlib.Topology.MetricSpace.Isometry

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : Unique ι
inst✝ : Fintype ι
x hx : ι → α
⊢ edist ((Equiv.funUnique ι α).toFun x) ((Equiv.funUnique ι α).toFun hx) = edist x hx

Tactic:
simp [edist_pi_def, Finset.univ_unique, Finset.sup_singleton]

Goal state after: