mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case refine_2
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₁
x✝ : { l // l ∘ₗ kerCotangentToTensor R P S = LinearMap.id }
l : S ⊗[P] Ω[P⁄R] →ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent
hl : l ∘ₗ kerCotangentToTensor R P S = LinearMap.id
⊢ { toAddHom := ↑(↑e₁ ∘ₗ l ∘ₗ ↑e₂), map_smul' := ⋯ } ∘ₗ kerToTensor R P' S = LinearMap.id

Tactic:
ext1 x

Goal state after:
case refine_2
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₁
x✝ : { l // l ∘ₗ kerCotangentToTensor R P S = LinearMap.id }
l : S ⊗[P] Ω[P⁄R] →ₗ[P] (RingHom.ker (algebraMap P S)).Cotangent
hl : l ∘ₗ kerCotangentToTensor R P S = LinearMap.id
x : ↥(RingHom.ker (algebraMap P' S))
⊢ ({ toAddHom := ↑(↑e₁ ∘ₗ l ∘ₗ ↑e₂), map_smul' := ⋯ } ∘ₗ kerToTensor R P' S) x = LinearMap.id x
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
this : ExpChar (L ⊗[K] L) (ringExpChar K)
r : K
hr : (algebraMap K L) r = x ^ ringExpChar K ^ n
⊢ 1 ⊗ₜ[K] (x ^ ringExpChar K ^ n) - (x ^ ringExpChar K ^ n) ⊗ₜ[K] 1 = 0

Tactic:
← hr,

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : FormallyUnramified K L
inst✝¹ : EssFiniteType K L
inst✝ : IsPurelyInseparable K L
this✝ : Nontrivial (L ⊗[K] L)
x : L
a✝ : x ∈ ⊤
n : ℕ
this : ExpChar (L ⊗[K] L) (ringExpChar K)
r : K
hr : (algebraMap K L) r = x ^ ringExpChar K ^ n
⊢ 1 ⊗ₜ[K] (algebraMap K L) r - (algebraMap K L) r ⊗ₜ[K] 1 = 0
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case hn0
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := under R q
Sq : Type u_1 := Localization.AtPrime q
⊢ map (algebraMap S (Localization.AtPrime q)) (map (algebraMap R S) (under R q)) < ⊤

Tactic:
grw [map_mono map_comap_le, Localization.AtPrime.map_eq_maximalIdeal]

Goal state after:
case hn0
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := under R q
Sq : Type u_1 := Localization.AtPrime q
⊢ IsLocalRing.maximalIdeal (Localization q.primeCompl) < ⊤
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: case hxt
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := ⋯
Sq : Type u_1 := ⋯
⊢ Module.length (Localization.AtPrime q)
      (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q)) ≠
    ⊤

Tactic:
let r := PrimeSpectrum.primesOverOrderIsoFiber R S p (primesOver.mk p q)

Goal state after:
case hxt
S : Type u_1
inst✝⁴ : CommRing S
q : Ideal S
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra R S
inst✝¹ : q.IsPrime
inst✝ : Module.Finite R S
p : Ideal R := under R q
Sq : Type u_1 := Localization.AtPrime q
r : PrimeSpectrum (p.Fiber S) := (PrimeSpectrum.primesOverOrderIsoFiber R S p) (primesOver.mk p q)
⊢ Module.length (Localization.AtPrime q)
      (Localization.AtPrime q ⧸ map (algebraMap R (Localization.AtPrime q)) (under R q)) ≠
    ⊤
Module: Mathlib.RingTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
q : Ideal S
G : Type u_4
inst✝² : Group G
inst✝¹ : MulSemiringAction G S
inst✝ : SMulCommClass G R S
g : G
hq : q.IsPrime
p : Ideal R := under R q
f₀ : S ≃ₐ[R] S := (MulSemiringAction.toAlgAut G R S) g
hg : g • q = map f₀ q
Sq : Type u_2 := Localization.AtPrime q
Sq' : Type u_2 := Localization.AtPrime (map f₀ q)
f : Sq ≃ₐ[R] Sq' := Localization.localAlgEquiv q (map f₀ q) f₀ ⋯
this✝ : Algebra Sq Sq' := f.toRingEquiv.toRingHom.toAlgebra
this : IsScalarTower R Sq Sq'
⊢ map (algebraMap R Sq') p = map (↑(AlgEquiv.ofBijective (Algebra.ofId Sq Sq') ⋯)) (map (algebraMap R Sq) p)

Tactic:
by rw [IsScalarTower.algebraMap_eq R Sq Sq', Ideal.map_map,
          ← AlgEquiv.toAlgHom_toRingHom, AlgEquiv.toAlgHom_ofBijective, Algebra.toRingHom_ofId]

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

Goal state before:
pp: r : ℝ
n : ℕ
⊢ ↑n < r.toNNReal ↔ ↑n < r

Tactic:
by
  simpa only [not_le] using toNNReal_le_natCast.not

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

Goal state before:
pp: r p : ℝ
⊢ ¬p.toNNReal < r.toNNReal ↔ ¬p < r ∨ ¬0 < r

Tactic:
toNNReal_lt_toNNReal_iff',

Goal state after:
r p : ℝ
⊢ ¬(p < r ∧ 0 < r) ↔ ¬p < r ∨ ¬0 < r
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ (x ^ n).toNNReal = x.toNNReal ^ n

Tactic:
← coe_inj,

Goal state after:
x : ℝ
hx : 0 ≤ x
n : ℕ
⊢ ↑(x ^ n).toNNReal = ↑(x.toNNReal ^ n)
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x : ℝ
hx : 0 ≤ x
n : ℤ
⊢ (x ^ n).toNNReal = x.toNNReal ^ n

Tactic:
← coe_inj,

Goal state after:
x : ℝ
hx : 0 ≤ x
n : ℤ
⊢ ↑(x ^ n).toNNReal = ↑(x.toNNReal ^ n)
Module: Mathlib.Data.NNReal.Defs

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

Tactic:
← coe_inj,

Goal state after:
α : Sort u_2
⊢ ↑(⨅ x, 0) = ↑0
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: ⊢ ¬BddBelow (range fun x ↦ ↑x)

Tactic:
dsimp only [BddBelow, lowerBounds]

Goal state after:
⊢ ¬{x | ∀ ⦃a : ℝ⦄, (a ∈ range fun x ↦ ↑x) → x ≤ a}.Nonempty
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
s : Set (GroupSeminorm E)
h : BddAbove s
x y : E
⊢ ⨆ p, ↑p (x * y) ≤ (⨆ p, ↑p x) + ⨆ p, ↑p y

Tactic:
obtain (rfl | hs) := eq_empty_or_nonempty s
          · simp
          · have : Nonempty s := hs.to_subtype
            refine ciSup_le fun p ↦ (map_mul_le_add p.1 x y).trans ?_
            gcongr
            all_goals
              apply le_ciSup (f := (DFunLike.coe · _) ∘ Subtype.val) ?_ p
              simpa [Set.range_comp] using Monotone.map_bddAbove (fun _ _ h' ↦ by exact h' _) h

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

Goal state before:
pp: b : ℝ≥0∞
p : ℝ≥0
right✝¹ h : ↑p < b
r : ℝ≥0
right✝ : ↑r < b
pc : ↑p < ↑r
cb : ↑r < b
q : ℚ
hq0 : 0 ≤ q
pq : p < (↑q).toNNReal
qr : (↑q).toNNReal < r
⊢ ∃ q, 0 ≤ q ∧ ↑p < ↑(↑q).toNNReal ∧ ↑(↑q).toNNReal < b

Tactic:
exact ⟨q, hq0, coe_lt_coe.2 pq, lt_trans (coe_lt_coe.2 qr) cb⟩

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

Goal state before:
pp: case neg
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
hac : a ≤ c
hcb : c ≤ b
hsub' : Icc a b ⊆ tᶜ.ordConnectedComponent a
hd : Disjoint s (s.ordSeparatingSet t).ordConnectedSection
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
replace hac : a < c := hac.lt_of_ne <| Ne.symm <| ne_of_mem_of_not_mem hc <|
      disjoint_left.1 hd ha

Goal state after:
case neg
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
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
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
  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.Data.ENNReal.Operations

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

Tactic:
cases a

Goal state after:
case top
b : ℝ≥0∞
c : ℝ≥0
⊢ ∞ + ↑c - (b + ↑c) = ∞ - b

case coe
b : ℝ≥0∞
c x✝ : ℝ≥0
⊢ ↑x✝ + ↑c - (b + ↑c) = ↑x✝ - b
Module: Mathlib.Data.ENNReal.Operations

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

Tactic:
exact fun _ => h.resolve_right (Classical.not_not.2 rfl)

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

Goal state before:
pp: case top
b : ℝ≥0
⊢ (∞ - ↑b).toNNReal = ∞.toNNReal - (↑b).toNNReal

Tactic:
simp [← coe_sub]

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

Goal state before:
pp: case coe
b x✝ : ℝ≥0
⊢ (↑x✝ - ↑b).toNNReal = (↑x✝).toNNReal - (↑b).toNNReal

Tactic:
simp [← coe_sub]

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

Goal state before:
pp: ⊢ range Real.toEReal = {⊥, ⊤}ᶜ

Tactic:
by
  ext x
  induction x <;> simp

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

Goal state before:
pp: ⊢ range Real.toEReal = Ioo ⊥ ⊤

Tactic:
by
  ext x
  induction x <;> simp

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

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

Tactic:
simp only [WithBot.preimage_coe_Iic, WithTop.preimage_coe_Iic]

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

Goal state before:
pp: case pos
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h✝ : a = 0
⊢ a⁻¹⁻¹ = a

Tactic:
cases a

Goal state after:
case pos.top
a b c d : ℝ≥0∞
r p q : ℝ≥0
h✝ : ∞ = 0
⊢ ∞⁻¹⁻¹ = ∞

case pos.coe
a b c d : ℝ≥0∞
r p q x✝ : ℝ≥0
h✝ : ↑x✝ = 0
⊢ (↑x✝)⁻¹⁻¹ = ↑x✝
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case neg
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
h✝ : ¬a = 0
⊢ a⁻¹⁻¹ = a

Tactic:
cases a

Goal state after:
case neg.top
a b c d : ℝ≥0∞
r p q : ℝ≥0
h✝ : ¬∞ = 0
⊢ ∞⁻¹⁻¹ = ∞

case neg.coe
a b c d : ℝ≥0∞
r p q x✝ : ℝ≥0
h✝ : ¬↑x✝ = 0
⊢ (↑x✝)⁻¹⁻¹ = ↑x✝
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case coe
a : ℝ≥0∞
x✝ : ℝ≥0
ha : a ≠ 0 ∨ ↑x✝ ≠ ∞
hb : a ≠ ∞ ∨ ↑x✝ ≠ 0
⊢ (a * ↑x✝)⁻¹ = a⁻¹ * (↑x✝)⁻¹

Tactic:
cases a

Goal state after:
case coe.top
x✝ : ℝ≥0
ha : ∞ ≠ 0 ∨ ↑x✝ ≠ ∞
hb : ∞ ≠ ∞ ∨ ↑x✝ ≠ 0
⊢ (∞ * ↑x✝)⁻¹ = ∞⁻¹ * (↑x✝)⁻¹

case coe.coe
x✝¹ x✝ : ℝ≥0
ha : ↑x✝ ≠ 0 ∨ ↑x✝¹ ≠ ∞
hb : ↑x✝ ≠ ∞ ∨ ↑x✝¹ ≠ 0
⊢ (↑x✝ * ↑x✝¹)⁻¹ = (↑x✝)⁻¹ * (↑x✝¹)⁻¹
Module: Mathlib.Data.ENNReal.Inv

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

Tactic:
← coe_div,

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

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

Goal state before:
pp: case ofNat.negSucc
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.negSucc b
⊢ x ^ Int.ofNat a ≤ x ^ Int.negSucc b

Tactic:
apply absurd h (not_le_of_gt _)
    exact lt_of_lt_of_le (Int.negSucc_lt_zero _) (Int.natCast_nonneg _)

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

Goal state before:
pp: x : ℝ≥0∞
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ∞
m n : ℤ
⊢ x ^ (m - n) = x ^ m * (x ^ n)⁻¹

Tactic:
by
  rw [sub_eq_add_neg, ENNReal.zpow_add x_ne_zero x_ne_top, ENNReal.zpow_neg]

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

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

Tactic:
by
  rw [edist_dist, dist_nndist, ENNReal.ofReal_coe_nnreal]

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

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

Tactic:
by rw [dist_comm, mem_closedBall]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall x R, p y
y : α
⊢ p y

Tactic:
obtain ⟨R, hR, h⟩ : ∃ R ≥ dist y x, ∀ z : α, z ∈ closedBall x R → p z :=
    frequently_iff.1 H (Ici_mem_atTop (dist y x))

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ y ∈ closedBall x R, p y
y : α
R : ℝ
hR : R ≥ dist y x
h : ∀ z ∈ closedBall x R, p z
⊢ p y
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ y ∈ eball x (ENNReal.ofReal ε) ↔ y ∈ ball x ε

Tactic:
simp only [mem_eball, mem_ball, edist_dist]

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ ENNReal.ofReal (dist y x) < ENNReal.ofReal ε ↔ dist y x < ε
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Type u_2
s : Finset ι
f : ι → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ (∑ a ∈ s, f a).toNNReal = ∑ a ∈ s, (f a).toNNReal

Tactic:
← coe_inj,

Goal state after:
ι : Type u_2
s : Finset ι
f : ι → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ↑(∑ a ∈ s, f a).toNNReal = ↑(∑ a ∈ s, (f a).toNNReal)
Module: Mathlib.Data.NNReal.Basic

Goal state before:
pp: ι : Type u_2
s : Finset ι
f : ι → ℝ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ (∏ a ∈ s, f a).toNNReal = ∏ a ∈ s, (f a).toNNReal

Tactic:
← coe_inj,

Goal state after:
ι : Type u_2
s : Finset ι
f : ι → ℝ
hf : ∀ a ∈ s, 0 ≤ f a
⊢ ↑(∏ a ∈ s, f a).toNNReal = ↑(∏ a ∈ s, (f a).toNNReal)
Module: Mathlib.Data.NNReal.Basic

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

Tactic:
← coe_inj,

Goal state after:
ι : Sort u_3
f : ι → ℝ≥0
a : ℝ≥0
⊢ ↑(iInf f * a) = ↑(⨅ i, f i * a)
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:
exact Real.iInf_mul_of_nonneg (NNReal.coe_nonneg _) _

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

Goal state before:
pp: x r y : ℝ
⊢ x - y ≤ r ∧ y - x ≤ r ↔ x - r ≤ y ∧ y - x ≤ r

Tactic:
sub_le_comm

Goal state after:
x r y : ℝ
⊢ x - r ≤ y ∧ y - x ≤ r ↔ x - r ≤ y ∧ y - x ≤ r
Module: Mathlib.Data.NNReal.Basic

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

Tactic:
← coe_inj,

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

Goal state before:
pp: case neg
γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
h : ¬BddAbove (range fun x ↦ f ↑x)
⊢ ¬BddAbove (range f)

Tactic:
contrapose h

Goal state after:
case neg
γ : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : ClosedIicTopology α
f : γ → α
inst✝ : TopologicalSpace γ
S : Set γ
hS : Dense S
hf : Continuous[inst✝, inst✝³] f
h : BddAbove (range f)
⊢ BddAbove (range fun x ↦ f ↑x)
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
b : β
⊢ dist (f b) (g b) ≤ dist f g

Tactic:
simp only [dist_nndist, NNReal.coe_le_coe, nndist_le_pi_nndist f g b]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
t : Set α
x : α
inst✝ : (𝓝 x).IsCountablyGenerated
htx : IsLUB t x
notMem : x ∉ t
ht : t.Nonempty
v : ℕ → α
hvt : ∀ (n : ℕ), v n ∈ t
hvx : Tendsto v atTop (𝓝 x)
hvx' : ∀ {n : ℕ}, v n < x
this : ∀ (k : ℕ), ∀ᶠ (l : ℕ) in atTop, v k < v l
N : ℕ → ℕ
hN : ∀ (k : ℕ), k < N k
hvN : ∀ (k : ℕ), v k < v (N k)
x✝ : ℕ
⊢ v (N^[x✝] 0) < v (N^[x✝ + 1] 0)

Tactic:
rw [iterate_succ_apply']; exact hvN _

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : ↑(range F) → α := rangeSplitting F
x : α
x' : α := Finv ⟨F x, ⋯⟩
⊢ ∃ y ∈ range Finv, dist x y ≤ ε

Tactic:
have : F x' = F x := apply_rangeSplitting F _

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : ↑(range F) → α := rangeSplitting F
x : α
x' : α := Finv ⟨F x, ⋯⟩
this : F x' = F x
⊢ ∃ y ∈ range Finv, dist x y ≤ ε
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 : PseudoMetricSpace X
d : X → X → ℝ
hd : d = dist
⊢ (cobounded X).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, d x y ≤ C}

Tactic:
by simp [hd, cobounded_sets]

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✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
H : (x '' t).Countable
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c = x d
this : f (x c) = f (x d)
⊢ c = d

Tactic:
hfx _ hc,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : LinearOrder β
s : Set α
f : α → β
inst✝ : SecondCountableTopology α
hf : MonotoneOn f s
a✝ : Nontrivial α
t : Set β := {c | ∃ x y, x ∈ s ∧ y ∈ s ∧ x < y ∧ f x = c ∧ f y = c}
x y : β → α
hxs : ∀ c ∈ t, x c ∈ s
hys : ∀ c ∈ t, y c ∈ s
hxy : ∀ c ∈ t, x c < y c
hfx : ∀ c ∈ t, f (x c) = c
hfy : ∀ c ∈ t, f (y c) = c
u : Set α := x '' t
H : (x '' t).Countable
c : β
hc : c ∈ t
d : β
hd : d ∈ t
hcd : x c = x d
this : c = f (x d)
⊢ c = d
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
a : E
n : ℕ
⊢ ‖a ^ (n + 1)‖ ≤ ↑(n + 1) * ‖a‖

Tactic:
simpa [pow_succ, add_mul] using norm_mul_le_of_le' norm_pow_le_mul_norm le_rfl

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

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ ENNReal.ofReal (dist a b) = ‖a / b‖ₑ

Tactic:
dist_eq_norm_div,

Goal state after:
E : Type u_5
inst✝ : SeminormedCommGroup E
a b : E
⊢ ENNReal.ofReal ‖a / b‖ = ‖a / b‖ₑ
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u_3
inst✝⁴ : AddCommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompactIccSpace α
C : α
⊢ {x | |x| ≤ C} = Icc (-C) C

Tactic:
ext1 x

Goal state after:
α : Type u_3
inst✝⁴ : AddCommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompactIccSpace α
C x : α
⊢ x ∈ {x | |x| ≤ C} ↔ x ∈ Icc (-C) C
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u_3
inst✝⁴ : AddCommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompactIccSpace α
C : α
⊢ {x | |x| < C} = Ioo (-C) C

Tactic:
ext1 x

Goal state after:
α : Type u_3
inst✝⁴ : AddCommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedAddMonoid α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompactIccSpace α
C x : α
⊢ x ∈ {x | |x| < C} ↔ x ∈ Ioo (-C) C
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case inl
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf : StrictMono f
hab : a ≤ b
⊢ f '' Ioo a b = Ioo (f a) (f b)

Tactic:
exact hf_c.continuousOn.image_Ioo_of_strictMonoOn hab (hf.strictMonoOn _)

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

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ (∑ a ∈ s, f a).toNNReal = ∑ a ∈ s, (f a).toNNReal

Tactic:
← coe_inj,

Goal state after:
α : Type u_1
s : Finset α
f : α → ℝ≥0∞
hf : ∀ a ∈ s, f a ≠ ∞
⊢ ↑(∑ a ∈ s, f a).toNNReal = ↑(∑ a ∈ s, (f a).toNNReal)
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: case inl.inr
x y : EReal
h : x < y
z : ℝ
h' : ↑z ≤ ↑z
hbot : ↑z ≠ ⊥
htop : ↑z = ⊤ → ↑z = ⊤ → x = ⊥
hz : ↑z ≠ ⊤
⊢ x + ↑z < y + ↑z

Tactic:
exact add_lt_add_right_coe h z

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
u : β → α
inst✝ : Nonempty β
hu : BddBelow (range u)
⊢ sInf (range u) = ⨅ i, u i

Tactic:
sInf_range

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLattice α
u : β → α
inst✝ : Nonempty β
hu : BddBelow (range u)
⊢ iInf u = ⨅ i, u i
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
s : Set α
⊢ (𝓟 s).limsInf = sInf s

Tactic:
simpa only [limsInf, eventually_principal] using! sSup_lowerBounds_eq_sInf s

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
u : β → α
⊢ sInf (range u) = ⨅ i, u i

Tactic:
sInf_range

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
u : β → α
⊢ iInf u = ⨅ i, u i
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a : EReal
b : ℝ
⊢ a + ↑b - ↑b = a

Tactic:
cases a

Goal state after:
case bot
b : ℝ
⊢ ⊥ + ↑b - ↑b = ⊥

case coe
b a✝ : ℝ
⊢ ↑a✝ + ↑b - ↑b = ↑a✝

case top
b : ℝ
⊢ ⊤ + ↑b - ↑b = ⊤
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a : EReal
b : ℝ
⊢ ↑b - (a + ↑b) = -a

Tactic:
cases a

Goal state after:
case bot
b : ℝ
⊢ ↑b - (⊥ + ↑b) = -⊥

case coe
b a✝ : ℝ
⊢ ↑b - (↑a✝ + ↑b) = -↑a✝

case top
b : ℝ
⊢ ↑b - (⊤ + ↑b) = -⊤
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case refine_1
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∈ ⋂₀ {a | {x | p x ∧ ¬s x ⊆ a}.Finite}
⊢ x ∈ {x | {n | p n ∧ x ∈ s n}.Infinite}

Tactic:
contrapose h

Goal state after:
case refine_1
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∉ {x | {n | p n ∧ x ∈ s n}.Infinite}
⊢ x ∉ ⋂₀ {a | {x | p x ∧ ¬s x ⊆ a}.Finite}