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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
⊢ Set.range (⇑(map R R S T) ∘ ⇑(D R S)) = ⇑(map R R S T) '' Set.range ⇑(D R S)

Tactic:
rw [← Set.range_comp, Function.comp_def]

Goal state after:
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: case pos
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 : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this✝ : ExpChar (L ⊗[K] L) (ringExpChar K)
this : (1 ⊗ₜ[K] x - x ⊗ₜ[K] 1) ^ ringExpChar K ^ n = 0
H : 1 ⊗ₜ[K] x = x ⊗ₜ[K] 1
h' : LinearIndependent K ![1, x]
h : LinearIndepOn K _root_.id (Set.range ![1, x])
S : Set L := h.extend ⋯
a : ↑S := ⟨1, ⋯⟩
ha : (Basis.extend h) a = 1
b : ↑S := ⟨x, ⋯⟩
hb : (Basis.extend h) b = x
e : a = b
⊢ x ∈ (algebraMap K L).range

Tactic:
obtain rfl : 1 = x := congr_arg Subtype.val e
      exact ⟨1, map_one _⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
⊢ T ⊗[S] P.H1Cotangent ≃ₗ[T] Q.H1Cotangent

Tactic:
refine .ofBijective ((H1Cotangent.map f).liftBaseChange T) ?_

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
P : Extension R S
Q : Extension R T
f : P.Hom Q
alg : Algebra P.Ring Q.Ring
halg : algebraMap P.Ring Q.Ring = f.toRingHom
inst✝ : Module.Flat S T
H₁ : f.toRingHom.FormallyEtale
H₂ : Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg))
⊢ Function.Bijective ⇑(LinearMap.liftBaseChange T (H1Cotangent.map f))
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
M₁ : Type u_3
M₂ : Type u_4
inst✝⁴ : CommRing A
I : Ideal A
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
φ : M₁ →ₗ[A] M₂
c : ↥(primaryComponent M₁ I)
⊢ φ ↑c ∈ primaryComponent M₂ I

Tactic:
by
  obtain ⟨c, hc⟩ := c
  simp only [primaryComponent_mem, mem_torsionBySet_iff, SetLike.coe_sort_coe, Subtype.forall,
    ← map_smul] at ⊢ hc
  obtain ⟨n, hn⟩ := hc
  use n
  grind

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mp
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₂
x : M
⊢ ((∃ n, ∀ a ∈ I ^ n, a • x = 0) ∧ ∃ y ∈ N₁, ∃ z ∈ N₂, y + z = x) →
    ∃ y, ((∃ n, ∀ a ∈ I ^ n, a • y = 0) ∧ y ∈ N₁) ∧ ∃ z, ((∃ n, ∀ a ∈ I ^ n, a • z = 0) ∧ z ∈ N₂) ∧ y + z = x

pp: case mpr
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₂
x : M
⊢ (∃ y, ((∃ n, ∀ a ∈ I ^ n, a • y = 0) ∧ y ∈ N₁) ∧ ∃ z, ((∃ n, ∀ a ∈ I ^ n, a • z = 0) ∧ z ∈ N₂) ∧ y + z = x) →
    (∃ n, ∀ a ∈ I ^ n, a • x = 0) ∧ ∃ y ∈ N₁, ∃ z ∈ N₂, y + z = x

Tactic:
· rintro ⟨⟨w, h⟩, ⟨y, hy, z, hz, rfl⟩⟩
    refine ⟨y, ⟨⟨w, fun a ha ↦ ?_⟩, by simp [hy]⟩, z, ⟨⟨w, fun a ha ↦ ?_⟩, by simp [hz]⟩, rfl⟩
    · exact ((Submodule.disjoint_iff_add_eq_zero.mp hD) (Submodule.smul_mem N₁ a hy)
        (Submodule.smul_mem N₂ a hz) (h a ha ▸ (smul_add a y z).symm)).1
    · exact ((Submodule.disjoint_iff_add_eq_zero.mp hD) (Submodule.smul_mem N₁ a hy)
        (Submodule.smul_mem N₂ a hz) (h a ha ▸ (smul_add a y z).symm)).2

Goal state after:
case mpr
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₂
x : M
⊢ (∃ y, ((∃ n, ∀ a ∈ I ^ n, a • y = 0) ∧ y ∈ N₁) ∧ ∃ z, ((∃ n, ∀ a ∈ I ^ n, a • z = 0) ∧ z ∈ N₂) ∧ y + z = x) →
    (∃ n, ∀ a ∈ I ^ n, a • x = 0) ∧ ∃ y ∈ N₁, ∃ z ∈ N₂, y + z = x
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case pos
ι : 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, S i).indicator f a

Tactic:
← sub_eq_zero

Goal state after:
case pos
ι : 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, S i).indicator f a = 0
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ s.biUnion S, f a = ∑ t, (-1) ^ (#↑t + 1) • ∑ a ∈ (↑t).inf' ⋯ S, f a

Tactic:
← sub_eq_zero

Goal state after:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ a ∈ s.biUnion S, f a - ∑ t, (-1) ^ (#↑t + 1) • ∑ a ∈ (↑t).inf' ⋯ S, f a = 0
Module: Mathlib.Data.NNReal.Defs

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

Tactic:
rw [← coe_inj, coe_iInf]
  exact Real.iInf_const_zero

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

Goal state before:
pp: case hab
a : ℝ
ha : 1 < a
k : ℕ
posk : 0 < k
hk : 1 / ↑k + 1 < a
⊢ 1 / ↑k * ↑k + 1 ≤ (1 / ↑k + 1) ^ k

Tactic:
exact mul_add_one_le_add_one_pow (by simp) _

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
⊢ (↑(Finite.toFinset ⋯)).Pairwise (IsCoprime on fun i ↦ i.maxPowDividing I)

Tactic:
intro x hx y hy hxy

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
h0 : I ≠ 0
x : HeightOneSpectrum R
hx : x ∈ ↑(Finite.toFinset ⋯)
y : HeightOneSpectrum R
hy : y ∈ ↑(Finite.toFinset ⋯)
hxy : x ≠ y
⊢ (IsCoprime on fun i ↦ i.maxPowDividing I) x y
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✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ : E
p q : GroupSeminorm E
x y u v : E
⊢ p (u * v) + q (x * y / (u * v)) ≤ p u + q (x / u) + (p v + q (y / v))

Tactic:
mul_div_mul_comm,

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝¹ : CommGroup E
inst✝ : CommGroup F
p✝ q✝ : GroupSeminorm E
x✝ : E
p q : GroupSeminorm E
x y u v : E
⊢ p (u * v) + q (x / u * (y / v)) ≤ p u + q (x / u) + (p v + q (y / v))
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
⊢ φ b = φ ↑(f P)

Tactic:
← sub_eq_zero

Goal state after:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : IsDedekindDomain A
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
hM₁ : IsTorsion A M₁
P : HeightOneSpectrum A
φ : M₁ →ₗ[A] M₂
hf✝ : Surjective ⇑φ
b : M₁
hy : φ b ∈ primaryComponent M₂ P.asIdeal
f : Π₀ (i : HeightOneSpectrum A), ↥(primaryComponent M₁ i.asIdeal)
hf : ((DFinsupp.lsum ℕ) fun i ↦ (primaryComponent M₁ i.asIdeal).subtype) f = b
⊢ φ b - φ ↑(f P) = 0
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : AddGroupSeminorm E
x y : ℝ
⊢ r • max x y = max (r • x) (r • y)

Tactic:
simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
      mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg

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

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝³ : Group E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : GroupSeminorm E
x y : ℝ
⊢ r • max x y = max (r • x) (r • y)

Tactic:
simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
      mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg

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

Goal state before:
pp: R : Type u_1
E : Type u_3
inst✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p q : NonarchAddGroupSeminorm E
x y : ℝ
⊢ r • max x y = max (r • x) (r • y)

Tactic:
simpa only [← smul_eq_mul, ← NNReal.smul_def, smul_one_smul ℝ≥0 r (_ : ℝ)] using
      mul_max_of_nonneg x y (r • (1 : ℝ≥0) : ℝ≥0).coe_nonneg

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

Goal state before:
pp: case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ a ≤ ENNReal.ofReal (⨅ i, f i) ↔ a ≤ ⨅ i, ENNReal.ofReal (f i)

Tactic:
le_iInf_iff,

Goal state after:
case inr.inr
ι : Sort u_1
inst✝ : Nonempty ι
f : ι → ℝ
h : ∀ (i : ι), 0 ≤ f i
a : ℝ≥0∞
ha : a ≠ ∞
⊢ a ≤ ENNReal.ofReal (⨅ i, f i) ↔ ∀ (i : ι), a ≤ ENNReal.ofReal (f i)
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
h_prod : I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')
⊢ count K v (I * I') =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) +
      count K v I'

Tactic:
count_well_defined K v hI' 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
h_prod : I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J')
⊢ count K v (I * I') =
    ↑((Associates.mk v.asIdeal).count (Associates.mk J).factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a})).factors) +
      (↑((Associates.mk v.asIdeal).count (Associates.mk J').factors) -
        ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {a'})).factors))
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 w : HeightOneSpectrum R
hw : w ≠ v
⊢ count K v ↑w.asIdeal = 0

Tactic:
have hw_fact : (w.asIdeal : FractionalIdeal R⁰ K) =
      spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal := by
    rw [(algebraMap R K).map_one, inv_one, spanSingleton_one, one_mul]

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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
⊢ count K v ↑w.asIdeal = 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 w : HeightOneSpectrum R
hw : w ≠ v
hw_fact : ↑w.asIdeal = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑w.asIdeal
hw_ne_zero : ↑w.asIdeal ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
hw' : Irreducible (Associates.mk w.asIdeal)
⊢ ¬v = w

Tactic:
exact Ne.symm hw

Goal state after:
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

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
⊢ (w ∈ fun i ↦ i = v → False) → count K v (↑w.asIdeal ^ exps w) = 0
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ 0
⊢ ∃ n > 0, ↑n * a < b

Tactic:
rcases exists_nat_pos_inv_mul_lt ha hb with ⟨n, npos : 0 < n, hn⟩
  use (n : ℝ≥0)⁻¹
  simp [*, npos.ne']

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

Goal state before:
pp: case neg
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 : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
this : J⁻¹ * I ≤ J⁻¹ * J
⊢ count K v J ≤ count K v I

Tactic:
inv_mul_cancel₀ hJ,

Goal state after:
case neg
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 : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I ≤ J
hJ : ¬J = 0
this : J⁻¹ * I ≤ 1
⊢ count K v J ≤ count K v I
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
s : Set β
⊢ ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, edist (f x) (f b) < ε

Tactic:
by
  simp [ContinuousOn, continuousWithinAt_iff']

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
⊢ ∀ (x : HeightOneSpectrum R),
    ↑x.asIdeal ^ count K x I =
      ↑x.asIdeal ^
        (↑((Associates.mk x.asIdeal).count (Associates.mk (Classical.choose ⋯)).factors) -
          ↑((Associates.mk x.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors))

Tactic:
intro w

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
I : FractionalIdeal R⁰ K
hI : I ≠ 0
h : I = spanSingleton R⁰ ((algebraMap R K) (Classical.choose ⋯))⁻¹ * ↑(Classical.choose ⋯)
w : HeightOneSpectrum R
⊢ ↑w.asIdeal ^ count K w I =
    ↑w.asIdeal ^
      (↑((Associates.mk w.asIdeal).count (Associates.mk (Classical.choose ⋯)).factors) -
        ↑((Associates.mk w.asIdeal).count (Associates.mk (Ideal.span {Classical.choose ⋯})).factors))
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
s : Set β
⊢ ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ (x : β) in 𝓝[s] b, dist (f x) (f b) < ε

Tactic:
by
  simp [ContinuousOn, continuousWithinAt_iff']

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : Dense s
x : α
ε : ℝ
hε : 0 < ε
⊢ (ball x ε).Nonempty

Tactic:
simp [hε]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ 𝓤 α = comap (fun p ↦ dist p.1 p.2) (𝓝 0)

Tactic:
ext s

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set (α × α)
⊢ s ∈ 𝓤 α ↔ s ∈ comap (fun p ↦ dist p.1 p.2) (𝓝 0)
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: c : ℝ
⊢ ball 0 c = Ico 0 c.toNNReal

Tactic:
by
  by_cases! c_pos : 0 < c
  · convert! NNReal.ball_zero_eq_Ico' (NNReal.mk c c_pos.le)
    simp [Real.toNNReal, c_pos.le]
  simp [c_pos]

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

Goal state before:
pp: α : Type u_1
inst✝² : Bornology α
inst✝¹ : Lattice α
inst✝ : Nonempty α
h : IsOrderBornology α
⊢ inst✝² = orderBornology

Tactic:
ext s

Goal state after:
α : Type u_1
inst✝² : Bornology α
inst✝¹ : Lattice α
inst✝ : Nonempty α
h : IsOrderBornology α
s : Set α
⊢ s ∈ cobounded α ↔ s ∈ cobounded α
Module: Mathlib.Topology.Order.Compact

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

pp: case inr
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : NoMaxOrder α
f : β → α
s : Set β
hs : IsCompact s
hf : ContinuousOn f s
a : α
hf' : ∀ b ∈ s, a < f b
hs' : s.Nonempty
⊢ ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b

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

Goal state after:
case inr
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : ClosedIicTopology α
inst✝ : NoMaxOrder α
f : β → α
s : Set β
hs : IsCompact s
hf : ContinuousOn f s
a : α
hf' : ∀ b ∈ s, a < f b
hs' : s.Nonempty
⊢ ∃ a', a < a' ∧ ∀ b ∈ s, a' ≤ f b
Module: Mathlib.Topology.MetricSpace.ProperSpace

Goal state before:
pp: α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
⊢ SigmaCompactSpace α

Tactic:
rcases em (Nonempty α) with (⟨⟨x⟩⟩ | hn)

Goal state after:
case inl
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
⊢ SigmaCompactSpace α

case inr
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
hn : ¬Nonempty α
⊢ SigmaCompactSpace α
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
⊢ ⊤ ≤
    Submodule.comap (Submodule.comap (↑I').subtype ↑J').mkQ
      (Submodule.map (Submodule.comap (↑I').subtype ↑J').mkQ
        (Submodule.comap (↑I').subtype (↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I)))

Tactic:
Submodule.comap_map_eq,

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
⊢ ⊤ ≤
    Submodule.comap (↑I').subtype (↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I) ⊔
      (Submodule.comap (↑I').subtype ↑J').mkQ.ker
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x : E
y : F
⊢ ‖x‖ₑ = ‖y‖ₑ ↔ ‖x‖ = ‖y‖

Tactic:
simp only [← ofReal_norm']

Goal state after:
E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x : E
y : F
⊢ ENNReal.ofReal ‖x‖ = ENNReal.ofReal ‖y‖ ↔ ‖x‖ = ‖y‖
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x : E
y : F
⊢ ‖x‖ₑ ≤ ‖y‖ₑ ↔ ‖x‖ ≤ ‖y‖

Tactic:
simp only [← ofReal_norm']

Goal state after:
E : Type u_5
F : Type u_6
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
x : E
y : F
⊢ ENNReal.ofReal ‖x‖ ≤ ENNReal.ofReal ‖y‖ ↔ ‖x‖ ≤ ‖y‖
Module: Mathlib.Topology.Order.IntermediateValue

Goal state before:
pp: case refine_1
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
h : ∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
⊢ ∃ z ∉ s, z ∈ Ioo x y

Tactic:
simp_rw [← not_ordConnected_inter_Icc_iff hx hy]

Goal state after:
case refine_1
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
s : Set α
h : ∀ t ⊆ s, t.OrdConnected → ∀ x ∈ t, ∀ x_1 ∈ t, ¬x < x_1
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x < y
⊢ ¬(s ∩ Icc x y).OrdConnected
Module: Mathlib.Topology.MetricSpace.Bounded

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
c : α
⊢ (cobounded α).HasBasis (fun x ↦ True) fun i ↦ (fun x ↦ dist x c) ⁻¹' Ici i

Tactic:
simpa only [compl_def, mem_ball, not_lt] using! hasBasis_cobounded_compl_ball c

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

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

Tactic:
by rwa [Nat.cofinite_eq_atTop]

Goal state after:
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 δ
f : α → δ
hf_c : Continuous[inst✝⁶, inst✝¹] f
hf_i : Injective f
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
h : Subsingleton α
⊢ StrictMono f ∨ StrictAnti f

Tactic:
| inl h =>

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
H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f
x✝ : Subsingleton α ∨ Nontrivial α
⊢ StrictMono f ∨ StrictAnti f

Tactic:
cases subsingleton_or_nontrivial α with

Goal state after: