mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : Algebra.IsSeparable K L
⊢ FormallyUnramified K L

Tactic:
by
  rw [iff_comp_injective]
  intro B _ _ I hI f₁ f₂ e
  ext x
  have : f₁ x - f₂ x ∈ I := by
    simpa [Ideal.Quotient.mk_eq_mk_iff_sub_mem] using AlgHom.congr_fun e x
  have := Polynomial.eval_add_of_sq_eq_zero ((minpoly K x).map (algebraMap K B)) (f₂ x)
    (f₁ x - f₂ x) (show (f₁ x - f₂ x) ^ 2 ∈ ⊥ from hI ▸ Ideal.pow_mem_pow this 2)
  simp only [add_sub_cancel, eval_map_algebraMap, aeval_algHom_apply, minpoly.aeval, map_zero,
    derivative_map, zero_add] at this
  rwa [eq_comm, ((isUnit_iff_ne_zero.mpr
    ((Algebra.IsSeparable.isSeparable K x).aeval_derivative_ne_zero
      (minpoly.aeval K x))).map f₂).mul_right_eq_zero, sub_eq_zero] at this

Goal state after:
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
p : Ideal R
q : Ideal S
inst✝³ : IsDomain R
inst✝² : IsDedekindDomain S
inst✝¹ : Module.IsTorsionFree R S
inst✝ : q.LiesOver p
hq : q.IsPrime
hp : p ≠ ⊥
⊢ p.ramificationIdx' q = q.ramificationIdx R

Tactic:
by
  have hpS : p.map (algebraMap R S) ≠ ⊥ := map_ne_bot_of_ne_bot hp
  exact ramificationIdx'_eq_ramificationIdx' p q hpS

Goal state after:
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
p : Ideal R
q : Ideal S
inst✝¹ : IsDedekindDomain S
inst✝ : q.LiesOver p
hp0 : map (algebraMap R S) p ≠ ⊥
⊢ q.ramificationIdx R = Multiset.count q (factors (map (algebraMap R S) p))

Tactic:
by
  by_cases hq : q.IsPrime; swap
  · rw [ramificationIdx_of_not_isPrime q R hq, eq_comm, Multiset.count_eq_zero]
    contrapose! hq
    exact isPrime_of_prime (prime_of_factor q hq)
  have hq0 : q ≠ ⊥ := ne_bot_of_le_ne_bot hp0 (map_le_of_le_comap (q.over_def p).le)
  rw [← ramificationIdx'_eq_ramificationIdx' p q hp0, ramificationIdx'_eq_factors_count hp0 ‹_› hq0]

Goal state after:
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
p : Ideal R
q : Ideal S
inst✝² : IsDedekindDomain S
inst✝¹ : q.IsPrime
inst✝ : q.LiesOver p
hp : map (algebraMap R S) p ≠ ⊥
hq : q ≠ ⊥
⊢ q.ramificationIdx R = multiplicity q (map (algebraMap R S) p)

Tactic:
rw [ramificationIdx_eq_normalizedFactors_count p q hp,
    multiplicity_eq_of_emultiplicity_eq_some (emultiplicity_eq_count_normalizedFactors
      (prime_of_isPrime hq inferInstance).irreducible hp), normalize_eq]

Goal state after:
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:
IsScalarTower.algebraMap_eq R Sq Sq',

Goal state after:
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 Sq Sq').comp (algebraMap R Sq)) p =
    map (↑(AlgEquiv.ofBijective (Algebra.ofId Sq Sq') ⋯)) (map (algebraMap R Sq) p)
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
⊢ ∑ t, (-1) ^ #↑t • ∑ a ∈ (↑t).inf' ⋯ S, f a + ∑ t ∈ s.powerset with ¬t.Nonempty, (-1) ^ #t • ∑ a ∈ s.biUnion S, f a =
    ∑ t ∈ s.powerset, (-1) ^ #t • if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a

Tactic:
rw [← sum_attach (filter ..)]

Goal state after:
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
⊢ ∑ t, (-1) ^ #↑t • ∑ a ∈ (↑t).inf' ⋯ S, f a +
      ∑ x ∈ {x ∈ s.powerset | ¬x.Nonempty}.attach, (-1) ^ #↑x • ∑ a ∈ s.biUnion S, f a =
    ∑ t ∈ s.powerset, (-1) ^ #t • if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case refine_1
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)
hg : IsCauSeq abs fun n ↦ ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n ↦ ↑(f n) / ↑n, hg⟩
x : ℝ
xS : x ∈ s
⊢ x ≤ mk g

pp: case refine_2
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)
hg : IsCauSeq abs fun n ↦ ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n ↦ ↑(f n) / ↑n, hg⟩
y : ℝ
h : y ∈ upperBounds s
⊢ mk g ≤ y

Tactic:
· refine le_of_forall_lt_imp_le_of_dense fun z xz => ?_
    obtain ⟨K, hK⟩ := exists_nat_gt (x - z)⁻¹
    refine le_mk_of_forall_le ⟨K, fun n nK => ?_⟩
    replace xz := sub_pos.2 xz
    replace hK := hK.le.trans (Nat.cast_le.2 nK)
    have n0 : 0 < n := Nat.cast_pos.1 ((inv_pos.2 xz).trans_le hK)
    refine le_trans ?_ (hf₂ _ n0 _ xS).le
    rwa [le_sub_comm, inv_le_comm₀ (Nat.cast_pos.2 n0 : (_ : ℝ) < _) xz]

Goal state after:
case refine_2
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)
hg : IsCauSeq abs fun n ↦ ↑(f n) / ↑n
g : CauSeq ℚ abs := ⟨fun n ↦ ↑(f n) / ↑n, hg⟩
y : ℝ
h : y ∈ upperBounds s
⊢ mk g ≤ y
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case mp
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
⊢ (∀ (ε : ℝ), 0 < ε → sInf s < a + ε) → ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε

Tactic:
intro H ε ε_pos

Goal state after:
case mp
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → sInf s < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ x ∈ s, x < a + ε
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: case mpr
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
⊢ (∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε) → ∀ (ε : ℝ), 0 < ε → sInf s < a + ε

Tactic:
intro H ε ε_pos

Goal state after:
case mpr
s : Set ℝ
a : ℝ
h : BddBelow s
h' : s.Nonempty
H : ∀ (ε : ℝ), 0 < ε → ∃ x ∈ s, x < a + ε
ε : ℝ
ε_pos : 0 < ε
⊢ sInf s < a + ε
Module: Mathlib.RingTheory.DedekindDomain.Factorization

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ (Finite.toFinset hf).erase v, i.maxPowDividing I
⊢ False

Tactic:
have hv_prime : Prime v.asIdeal := Ideal.prime_of_isPrime v.ne_bot v.isPrime

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I : Ideal R
hI : I ≠ 0
hf : HasFiniteMulSupport fun v ↦ v.maxPowDividing I
h_ne_zero : v.maxPowDividing I ≠ 0
h_contr :
  v.asIdeal ^ (Associates.mk v.asIdeal).count (Associates.mk I).factors * v.asIdeal ∣
    v.maxPowDividing I * ∏ i ∈ (Finite.toFinset hf).erase v, i.maxPowDividing I
hv_prime : Prime v.asIdeal
⊢ False
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : ↑q.den < ↑q.num
⊢ 1 ≤ q * ↑q.den - ↑q.den

Tactic:
q.mul_den_eq_num

Goal state after:
a : ℝ
ha : ∀ (k : ℕ), 0 < k → a ≤ 1 / ↑k + 1
q : ℚ
hq : ↑q.den < ↑q.num
⊢ 1 ≤ ↑q.num - ↑q.den
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: α : Type u_1
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
a : AddUnits ℝ≥0∞
⊢ ↑a ≤ 0

Tactic:
rw [← a.add_neg]; exact le_self_add

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

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
h : IsTorsion A M
⊢ ⨆ P, primaryComponent M P.asIdeal = ⊤

Tactic:
rw [eq_top_iff']
  intro x
  obtain ⟨⟨a : A, ha : a ∈ A⁰⟩, hmem : a • x = 0⟩ := h (x := x)
  replace hmem : x ∈ torsionBySet A M (span {a}) := by
    simp_all [← torsionBySet_eq_torsionBySet_span {a}]
  have ha0 : span {a} ≠ ⊥ := by simpa using nonZeroDivisors.ne_zero ha
  rw [← iInf_maxPowDividing_eq ha0] at hmem
  let : Fintype (mulSupport fun v : HeightOneSpectrum A => v.maxPowDividing (span {a})) :=
    Finite.fintype (hasFiniteMulSupport ha0)
  let S := (mulSupport fun v : HeightOneSpectrum A => v.maxPowDividing (span {a})).toFinset
  have : (⨅ i : HeightOneSpectrum A, i.maxPowDividing (span {a})) =
      (⨅ i ∈ S, i.maxPowDividing (span {a})) := by
    ext x
    constructor
    · aesop
    · simp only [mem_iInf]
      intro h i
      by_cases htop : i.maxPowDividing (span {a}) = ⊤ <;> simp_all [S]
  have hPairwise : (S : Set (HeightOneSpectrum _)).Pairwise
      fun i j ↦ i.maxPowDividing (span {a}) ⊔ j.maxPowDividing (span {a}) = ⊤ :=
    fun r hr s hs hrs ↦ (isCoprime_pow_of_ne _ _ hrs _ _).sup_eq
  rw [this, ← iSup_torsionBySet_ideal_eq_torsionBySet_iInf hPairwise] at hmem
  revert x
  rw [← SetLike.le_def]
  refine iSup_mono (fun P x hxmem ↦ ?_)
  by_cases hPS : P ∈ S
  · simp_all only [mem_nonZeroDivisors_iff_ne_zero, ne_eq, mem_toFinset, mem_mulSupport,
      one_eq_top, primaryComponent_mem, mem_torsionBySet_iff, SetLike.coe_sort_coe,
      Subtype.forall, iSup_pos, S]
    exact ⟨(Associates.mk P.asIdeal).count (Associates.mk (span {a})).factors, fun _ b ↦ hxmem _ b⟩
  · simp_all

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

Goal state before:
pp: n : ℕ
⊢ (↑↑n).toNNReal = ↑n

Tactic:
ENNReal.toNNReal_coe

Goal state after:
n : ℕ
⊢ ↑n = ↑n
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: a : ℝ≥0∞
⊢ ⋃ n, Ioc a ↑n = Ioi a \ {∞}

Tactic:
by
  simp only [← Ioi_inter_Iic, ← inter_iUnion, iUnion_Iic_coe_nat, sdiff_eq]

Goal state after:
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 : E
⊢ p x + q (x / x) ≤ p x

Tactic:
div_self',

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 : E
⊢ p x + q 1 ≤ p x
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a : ℝ≥0∞
⊢ (a * ∞).toReal = 0

Tactic:
toReal_mul,

Goal state after:
a : ℝ≥0∞
⊢ a.toReal * ∞.toReal = 0
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
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
⊢ c ∈ [[y, x]]

Tactic:
suffices c < y by
        rw [uIcc_of_ge (hx.2.trans this).le]
        exact ⟨hx.2.le, this.le⟩

Goal state after:
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
y : X
hyt : y ∈ t
hxy : x ∈ sᶜ.ordConnectedComponent y
⊢ c < y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case neg
x : EReal
h : ¬x = ⊤
⊢ x.toENNReal = ∞ ↔ x = ⊤

Tactic:
· simp [h, toENNReal]

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 : FractionalIdeal R⁰ K
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : ¬I = 0
⊢ (if I ^ n ≠ 0 ∧ I ≠ 0 then count K v (I ^ n) + count K v I else 0) = ↑(n + 1) * count K v I

Tactic:
rw [if_pos (And.intro (pow_ne_zero n hI) hI), h, Nat.cast_add,
        Nat.cast_one]

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 : FractionalIdeal R⁰ K
n : ℕ
h : count K v (I ^ n) = ↑n * count K v I
hI : ¬I = 0
⊢ ↑n * count K v I + count K v I = (↑n + 1) * count K v I
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a : ℝ≥0∞
⊢ 1 < a⁻¹ ↔ a < 1

Tactic:
lt_inv_iff_lt_inv,

Goal state after:
a : ℝ≥0∞
⊢ a < 1⁻¹ ↔ a < 1
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
h : a * b = 1
⊢ a * 1 = b⁻¹

Tactic:
← ENNReal.mul_inv_cancel (right_ne_zero_of_mul_eq_one h),

Goal state after:
a b : ℝ≥0∞
h : a * b = 1
⊢ a * (b * b⁻¹) = b⁻¹

a b : ℝ≥0∞
h : a * b = 1
⊢ b ≠ ∞
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z = edist y z

Tactic:
apply le_antisymm
  · rw [← zero_add (edist y z), ← h]
    apply edist_triangle
  · rw [edist_comm] at h
    rw [← zero_add (edist x z), ← h]
    apply edist_triangle

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ (a * b⁻¹).toReal = a.toReal / b.toReal

Tactic:
toReal_mul,

Goal state after:
a b : ℝ≥0∞
⊢ a.toReal * b⁻¹.toReal = a.toReal / b.toReal
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
c : ℝ≥0
⊢ edist x y < ↑c ↔ nndist x y < c

Tactic:
by
  rw [edist_nndist, ENNReal.coe_lt_coe]

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

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
U : Set (X × X)
⊢ U ∈ 𝓤 X → ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U

Tactic:
hU

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : PseudoMetrizableSpace X
s : Set X
hs : IsSeparable s
this✝ : UniformSpace X := pseudoMetrizableSpaceUniformity X
this : (𝓤 X).IsCountablyGenerated
U : Set (X × X)
hU : U ∈ 𝓤 X
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, ball x U
Module: Mathlib.Topology.MetricSpace.Pseudo.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : ∀ d ∈ 𝓤 α, ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ d}
ε : ℝ
ε_pos : ε > 0
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, ball y ε

Tactic:
exact hs _ (dist_mem_uniformity ε_pos)

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
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
⊢ a p' ∈ ⨅ i, J * (↑i).asIdeal

Tactic:
Ideal.mem_iInf

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
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
⊢ ∀ (i : Subtype (Membership.mem s)), a p' ∈ J * (↑i).asIdeal
Module: Mathlib.Topology.EMetricSpace.Basic

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
U : Set (α × α)
⊢ U ∈ 𝓤 α → ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, UniformSpace.ball x U

Tactic:
hU

Goal state after:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedEBall x ε
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, UniformSpace.ball x U
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: case neg
c : ℝ
c_pos : c ≤ 0
⊢ ball 0 c = Ico 0 c.toNNReal

Tactic:
simp [c_pos]

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

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u

Tactic:
have : Iic ε ∈ 𝓝 (0 : ℝ) := Iic_mem_nhds εpos

Goal state after:
α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
this : Iic ε ∈ 𝓝 0
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ioi a ∩ Iio b = Ioo a b

Tactic:
Ioi_inter_Iio

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : OrderTopology α
inst✝² : DenselyOrdered α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ Ioo a b = Ioo 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 : α
⊢ Ioi a ∩ Iio b = Ioo a b

Tactic:
Ioi_inter_Iio

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : α
⊢ Ioo a b = Ioo a b
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b : α
⊢ Ioi a ∩ Iio b = Ioo a b

Tactic:
Ioi_inter_Iio

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
a b : α
⊢ Ioo a b = Ioo a b
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: n : ℕ
α : Fin (n + 1) → Type u_4
inst✝ : (i : Fin (n + 1)) → PseudoMetricSpace (α i)
i : Fin (n + 1)
x y : α i
f g : (j : Fin n) → α (i.succAbove j)
⊢ dist (i.insertNth x f) (i.insertNth y g) = max (dist x y) (dist f g)

Tactic:
by
  simp only [dist_nndist, Fin.nndist_insertNth_insertNth, NNReal.coe_max]

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

Goal state before:
pp: α : Type u_1
s✝ t : Set α
inst✝² : Bornology α
inst✝¹ : Preorder α
inst✝ : IsOrderBornology α
s : Set αᵒᵈ
⊢ IsBounded (⇑toDual ⁻¹' s) ↔ BddBelow s ∧ BddBelow (⇑toDual ⁻¹' s)

Tactic:
← bddAbove_preimage_toDual,

Goal state after:
α : Type u_1
s✝ t : Set α
inst✝² : Bornology α
inst✝¹ : Preorder α
inst✝ : IsOrderBornology α
s : Set αᵒᵈ
⊢ IsBounded (⇑toDual ⁻¹' s) ↔ BddAbove (⇑toDual ⁻¹' s) ∧ BddBelow (⇑toDual ⁻¹' s)
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
⊢ Filter.atTop ≤ cobounded α

Tactic:
intro s hs

Goal state after:
α : Type u_1
inst✝³ : Bornology α
inst✝² : Preorder α
inst✝¹ : IsOrderBornology α
inst✝ : NoMaxOrder α
s : Set α
hs : s ∈ cobounded α
⊢ s ∈ Filter.atTop
Module: Mathlib.Topology.Order.Monotone

Goal state before:
pp: case inr.refine_2
α : Type u_3
β : Type u_4
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
x : α
Mf : MonotoneOn f (Iio x)
h_bdd : BddAbove (f '' Iio x)
h : (Iio x).Nonempty
m : β
hm : m > sSup (f '' Iio x)
y : α
hy : y ∈ Iio x
⊢ f y ≤ sSup (f '' Iio x)

Tactic:
exact le_csSup h_bdd (mem_image_of_mem _ hy)

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
⊢ {s | IsPreconnected s} ⊆
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})

Tactic:
intro s hs

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : OrderTopology α
s : Set α
hs : s ∈ {s | IsPreconnected s}
⊢ s ∈
    range (uncurry Icc) ∪ range (uncurry Ico) ∪ range (uncurry Ioc) ∪ range (uncurry Ioo) ∪
      (range Ici ∪ range Ioi ∪ range Iic ∪ range Iio ∪ {univ, ∅})
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_8
inst✝ : SeminormedCommGroup E
u v : E
⊢ ‖u * v‖ - ‖u / v‖ ≤ 2 * min ‖u‖ ‖v‖

Tactic:
by
  rw [mul_min_of_nonneg _ _ (by positivity)]
  refine le_min ?_ (norm_mul_sub_norm_div_le_two_mul u v)
  rw [norm_div_rev, mul_comm]
  exact norm_mul_sub_norm_div_le_two_mul _ _

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

Goal state before:
pp: ι : Type u_3
X : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (X i)
s : (i : ι) → Set (X i)
c : ℝ≥0∞
h : ∀ (b : ι), ediam (s b) ≤ c
⊢ ediam (univ.pi s) ≤ c

Tactic:
refine ediam_le fun x hx y hy => edist_pi_le_iff.mpr ?_

Goal state after:
ι : Type u_3
X : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (X i)
s : (i : ι) → Set (X i)
c : ℝ≥0∞
h : ∀ (b : ι), ediam (s b) ≤ c
x : (i : ι) → X i
hx : x ∈ univ.pi s
y : (i : ι) → X i
hy : y ∈ univ.pi s
⊢ ∀ (b : ι), edist (x b) (y b) ≤ c
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedCommGroup E
m : Multiset E
⊢ ‖m.prod‖ ≤ (Multiset.map (toReal ∘ fun x ↦ ‖x‖₊) m).sum

Tactic:
exact norm_multiset_prod_le _

Goal state after: