mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FormallyUnramified R S
inst✝¹ : EssFiniteType R S
inst✝ : Free R S
I : Type u_2 := ⋯
b : Basis I R S := ⋯
f : I →₀ S
hf : elem R S = f.sum fun i x ↦ x ⊗ₜ[R] b i
x : S
a : I → I →₀ R := ⋯
F : I →₀ I →₀ R := ⋯
j : I
hj : ∀ (x : I), ¬f x = 0 → (a x) j = 0
⊢ b.repr (∑ x ∈ f.support, (a x) j • f x) = b.repr (∑ x ∈ f.support, 0)

Tactic:
refine congr_arg b.repr (Finset.sum_congr rfl ?_)
      simp only [Finsupp.mem_support_iff]
      intro i hi
      rw [hj i hi, zero_smul]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
B : Type u_1
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
C : Type u_4
inst✝² : CommRing C
inst✝¹ : Algebra R C
inst✝ : FormallySmooth R A
f : A →ₐ[R] C
g : B →ₐ[R] C
hg : Function.Surjective ⇑g
hg' : IsNilpotent (RingHom.ker g)
x : A
⊢ g ((liftOfSurjective f g hg hg') x) =
    (↑g).kerLift
      ((Ideal.Quotient.mk (RingHom.ker g))
        ((lift (RingHom.ker g) hg' ((↑(Ideal.quotientKerAlgEquivOfSurjective hg).symm).comp f)) x))

Tactic:
simp only [liftOfSurjective, ← RingHom.ker_coe_toRingHom g, RingHom.kerLift_mk, RingHom.coe_coe]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_1
P : Type u_2
C : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : CommRing C
inst✝³ : Algebra R C
inst✝² : CommRing P
inst✝¹ : Algebra R P
P₁ : Extension R A
P₂ : Extension R A
inst✝ : FormallySmooth R P₁.Ring
⊢ P₂.infinitesimal.ker ^ 2 = ⊥

Tactic:
rw [ker_infinitesimal]

Goal state after:
R : Type u
A : Type v
inst✝⁹ : CommRing R
inst✝⁸ : CommRing A
inst✝⁷ : Algebra R A
B : Type u_1
P : Type u_2
C : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R B
inst✝⁴ : CommRing C
inst✝³ : Algebra R C
inst✝² : CommRing P
inst✝¹ : Algebra R P
P₁ : Extension R A
P₂ : Extension R A
inst✝ : FormallySmooth R P₁.Ring
⊢ P₂.ker.cotangentIdeal ^ 2 = ⊥
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case mp
R : Type u_4
inst✝² : CommRing R
A : Type u_6
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Function.Surjective ⇑(algebraMap R A)
g : A →ₐ[R] R ⧸ RingHom.ker (ofId R A).toRingHom ^ 2
hg : (ofId R A).kerSquareLift.comp g = AlgHom.id R A
e : A ≃ₐ[R] R ⧸ RingHom.ker (algebraMap R A) ^ 2 := AlgEquiv.ofAlgHom g (ofId R A).kerSquareLift ⋯ hg
⊢ IsIdempotentElem (RingHom.ker (algebraMap R A))

Tactic:
rw [IsIdempotentElem, ← pow_two, ← Ideal.mk_ker (I := _ ^ 2), ← Ideal.Quotient.algebraMap_eq,
      ← e.toAlgHom.comp_algebraMap, RingHom.ker_comp_of_injective _ (by exact e.injective)]

Goal state after:
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
⊢ ∀ ⦃B : Type u_3⦄ [inst : CommRing B] [inst_1 : Algebra K B] (I : Ideal B),
    I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ K I).comp

Tactic:
intro B _ _ I hI f₁ f₂ e

Goal state after:
K : Type u_1
L : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra.IsSeparable K L
B : Type u_3
inst✝¹ : CommRing B
inst✝ : Algebra K B
I : Ideal B
hI : I ^ 2 = ⊥
f₁ f₂ : L →ₐ[K] B
e : (Ideal.Quotient.mkₐ K I).comp f₁ = (Ideal.Quotient.mkₐ K I).comp f₂
⊢ f₁ = f₂
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A :=
  let __spread.0 := ofId K (A ⧸ IsLocalRing.maximalIdeal A);
  let __spread.1 := Equiv.ofBijective ⇑(algebraMap K (A ⧸ IsLocalRing.maximalIdeal A)) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  (TensorProduct.congr AlgEquiv.refl e.symm).trans (TensorProduct.rid K A A)
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := e'.toLinearMap ∘ₗ sec K A (A ⧸ IsLocalRing.maximalIdeal A)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A
hf₃ : IsIdempotentElem (1 - f 1)
n : ℕ
hn : IsLocalRing.maximalIdeal A ^ n = 0
⊢ (1 - f 1) ^ n ∈ 0

Tactic:
← hn

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
this✝ : Module.Finite K A
this : IsArtinianRing A
e : K ≃ₐ[K] A ⧸ IsLocalRing.maximalIdeal A :=
  let __spread.0 := ofId K (A ⧸ IsLocalRing.maximalIdeal A);
  let __spread.1 := Equiv.ofBijective ⇑(algebraMap K (A ⧸ IsLocalRing.maximalIdeal A)) ⋯;
  { toFun := (↑↑__spread.0.toRingHom).toFun, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯,
    map_add' := ⋯, commutes' := ⋯ }
e' : A ⊗[K] (A ⧸ IsLocalRing.maximalIdeal A) ≃ₐ[A] A :=
  (TensorProduct.congr AlgEquiv.refl e.symm).trans (TensorProduct.rid K A A)
f : A ⧸ IsLocalRing.maximalIdeal A →ₗ[A] A := e'.toLinearMap ∘ₗ sec K A (A ⧸ IsLocalRing.maximalIdeal A)
hf : (ofId A (A ⧸ IsLocalRing.maximalIdeal A)).toLinearMap ∘ₗ f = LinearMap.id
hf₁ : f 1 • 1 = 1
hf₂ : 1 - f 1 ∈ IsLocalRing.maximalIdeal A
hf₃ : IsIdempotentElem (1 - f 1)
n : ℕ
hn : IsLocalRing.maximalIdeal A ^ n = 0
⊢ (1 - f 1) ^ n ∈ IsLocalRing.maximalIdeal A ^ n
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 : ℕ
hn : x ^ ringExpChar K ^ n ∈ (algebraMap K L).range
this : ExpChar (L ⊗[K] L) (ringExpChar K)
⊢ x ∈ (algebraMap K L).range

Tactic:
have : (1 ⊗ₜ x - x ⊗ₜ 1 : L ⊗[K] L) ^ (ringExpChar K) ^ n = 0 := by
    rw [sub_pow_expChar_pow, TensorProduct.tmul_pow, one_pow, TensorProduct.tmul_pow, one_pow]
    obtain ⟨r, hr⟩ := hn
    rw [← hr, algebraMap_eq_smul_one, TensorProduct.smul_tmul, sub_self]

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 : ℕ
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
⊢ x ∈ (algebraMap K L).range
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: case h
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
a b : K
e : a • 1 + b • x = 0
hab : a = 0 → ¬b = 0
this : IsUnit b
⊢ -↑this.unit⁻¹ • a • 1 = x

Tactic:
eq_neg_iff_add_eq_zero.mpr e,

Goal state after:
case h
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
a b : K
e : a • 1 + b • x = 0
hab : a = 0 → ¬b = 0
this : IsUnit b
⊢ -↑this.unit⁻¹ • -(b • x) = x
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
x : M
a : A
ha : a ∈ A⁰
hmem : x ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
⊢ x ∈ ⨆ P, primaryComponent M P.asIdeal

Tactic:
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]

Goal state after:
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
x : M
a : A
ha : a ∈ A⁰
hmem : x ∈ torsionBySet A M ↑(⨅ i, i.maxPowDividing (span {a}))
ha0 : span {a} ≠ ⊥
this✝ : Fintype ↑(mulSupport fun v ↦ v.maxPowDividing (span {a})) := Finite.fintype ⋯
S : Finset (HeightOneSpectrum A) := (mulSupport fun v ↦ v.maxPowDividing (span {a})).toFinset
this : ⨅ i, i.maxPowDividing (span {a}) = ⨅ i ∈ S, i.maxPowDividing (span {a})
⊢ x ∈ ⨆ P, primaryComponent M P.asIdeal
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, (∏ i ∈ s, (1 - (↑(S i)).indicator 1 a)) • f a =
    ∑ a ∈ s.biUnion S, (∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a)) • f a

Tactic:
by
      congr! with t; rw [Set.indicator_of_mem ‹_›, Pi.one_apply]

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

Goal state before:
pp: ⊢ sInf Set.univ = 0

Tactic:
by
  simp [sInf_def]

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

Goal state before:
pp: s : Set ℝ
⊢ sSup (-s) = -sInf s

Tactic:
obtain rfl | hn := s.eq_empty_or_nonempty; · simp
  by_cases hb : BddBelow s
  · rw [csSup_neg hn hb]
  · rw [csInf_of_not_bddBelow hb, Real.sInf_empty, csSup_of_not_bddAbove (bddAbove_neg.not.2 hb),
      Real.sSup_empty, neg_zero]

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

Goal state before:
pp: s : Set ℝ
hs : ∀ x ∈ s, 0 ≤ x
⊢ 0 ≤ sSup s

Tactic:
by
  obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty
  · exact sSup_empty.ge
  · exact sSup_nonneg' ⟨x, hx, hs _ hx⟩

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

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
⊢ (a + b).toReal = a.toReal + b.toReal

Tactic:
lift a to ℝ≥0 using ha

Goal state after:
b : ℝ≥0∞
hb : b ≠ ∞
a : ℝ≥0
⊢ (↑a + b).toReal = (↑a).toReal + b.toReal
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
⊢ a.toReal ≤ b.toReal ↔ a ≤ b

Tactic:
lift a to ℝ≥0 using ha

Goal state after:
b : ℝ≥0∞
hb : b ≠ ∞
a : ℝ≥0
⊢ (↑a).toReal ≤ b.toReal ↔ ↑a ≤ b
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a b : ℝ≥0∞
ha : a ≠ ∞
hb : b ≠ ∞
⊢ a.toReal < b.toReal ↔ a < b

Tactic:
lift a to ℝ≥0 using ha

Goal state after:
b : ℝ≥0∞
hb : b ≠ ∞
a : ℝ≥0
⊢ (↑a).toReal < b.toReal ↔ ↑a < b
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a : ℝ≥0∞
b : ℝ
ha : a ≠ ∞
hb : 0 ≤ b
⊢ a ≤ ENNReal.ofReal b ↔ a.toReal ≤ b

Tactic:
lift a to ℝ≥0 using ha

Goal state after:
b : ℝ
hb : 0 ≤ b
a : ℝ≥0
⊢ ↑a ≤ ENNReal.ofReal b ↔ (↑a).toReal ≤ b
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a : ℝ≥0∞
b : ℝ
ha : a ≠ ∞
⊢ a < ENNReal.ofReal b ↔ a.toReal < b

Tactic:
lift a to ℝ≥0 using ha

Goal state after:
b : ℝ
a : ℝ≥0
⊢ ↑a < ENNReal.ofReal b ↔ (↑a).toReal < b
Module: Mathlib.Analysis.Normed.Group.Seminorm

Goal state before:
pp: case pos
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁴ : AddGroup E
inst✝³ : SMul R ℝ
inst✝² : SMul R ℝ≥0
inst✝¹ : IsScalarTower R ℝ≥0 ℝ
inst✝ : DecidableEq E
x y : E
hx : x = 0
⊢ (if y = 0 then 0 else 1) ≤ max 0 (if y = 0 then 0 else 1)

Tactic:
exact le_max_of_le_right (le_refl _)

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

Goal state before:
pp: a b : ℝ≥0∞
⊢ a + b ≠ ∞ ↔ a ≠ ∞ ∧ b ≠ ∞

Tactic:
by simpa only [lt_top_iff_ne_top] using add_lt_top

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

Goal state before:
pp: a : ℝ≥0∞
ha : a ≠ ∞
⊢ ∞ - a = ∞

Tactic:
lift a to ℝ≥0 using ha

Goal state after:
a : ℝ≥0
⊢ ∞ - ↑a = ∞
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: a b c : ℝ≥0∞
ha : a ≠ ∞
h : b ≤ a
hb : b ≠ ∞
⊢ a - c - (a - b) = b - c

Tactic:
lift a to ℝ≥0 using ha

Goal state after:
b c : ℝ≥0∞
hb : b ≠ ∞
a : ℝ≥0
h : b ≤ ↑a
⊢ ↑a - c - (↑a - b) = b - c
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 : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
a₁ : R := choose ⋯
J₁ : Ideal R := choose ⋯
h_aJ : ↑(J₁ * Ideal.span {a}) = ↑(J * Ideal.span {a₁})
h_a₁J₁ : I = spanSingleton R⁰ ((algebraMap R K) a₁)⁻¹ * ↑J₁
h_a₁_ne_zero : a₁ ≠ 0
h_J₁_ne_zero : J₁ ≠ 0
h_a_ne_zero : Ideal.span {a} ≠ 0
h_J_ne_zero : J ≠ 0
h_a₁' : spanSingleton R⁰ ((algebraMap R K) a₁) ≠ 0
h_a' : spanSingleton R⁰ ((algebraMap R K) a) ≠ 0
hv : Irreducible (Associates.mk v.asIdeal)
⊢ Associates.mk J ≠ 0

Tactic:
rw [ne_eq, Associates.mk_eq_zero]; exact h_J_ne_zero

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

Goal state before:
pp: y : ℝ
⊢ Real.toEReal ⁻¹' Ioc ⊥ ↑y = Iic y

Tactic:
rw [← Ioi_inter_Iic]

Goal state after:
y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iic ↑y) = Iic y
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: a b : ℝ
h : ↑a < ↑b
⊢ ∃ x, ↑a < ↑↑x ∧ ↑↑x < ↑b

Tactic:
by simp [exists_rat_btwn (EReal.coe_lt_coe_iff.1 h)]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
⊢ edist x y ≤ edist x z + edist y z

Tactic:
rw [edist_comm y]; apply edist_triangle

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:
rw [two_mul, dist_comm]

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

Goal state after:
x : ℝ≥0∞
hx : 1 ≤ x
a b : ℕ
h : Int.ofNat a ≤ Int.negSucc b
⊢ Int.negSucc b < Int.ofNat a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: x y : ℝ
hy : 0 < y
⊢ ENNReal.ofReal (x / y) = ENNReal.ofReal x / ENNReal.ofReal y

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ofReal_mul' (inv_nonneg.2 hy.le), ofReal_inv_of_pos hy]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ dist x y = (ENNReal.ofReal (dist x y)).toReal

Tactic:
ENNReal.toReal_ofReal dist_nonneg

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ dist x y = dist x y
Module: Mathlib.Topology.MetricSpace.Pseudo.Lemmas

Goal state before:
pp: α : Type u_2
inst✝ : PseudoMetricSpace α
x : α
r : ℝ
x✝ : α
⊢ x✝ ∉ ⋃ r', ⋃ (_ : r' < r), ball x r' ↔ x✝ ∉ ball x r

Tactic:
simp [forall_lt_imp_le_iff_le_of_dense]

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

Goal state before:
pp: case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x✝ : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
x : (x : β) → X x
hx : x ∈ sphere x✝ 0
⊢ x ∈ Function.eval default ⁻¹' sphere (x✝ default) 0

Tactic:
replace hx := hx.le

Goal state after:
case inr.inl
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x✝ : (b : β) → X b
h : 0 < 0 ∨ Nonempty β
this : Nonempty β := Or.resolve_left h (lt_irrefl 0)
inhabited_h : Inhabited β
x : (x : β) → X x
hx : dist x x✝ ≤ 0
⊢ x ∈ Function.eval default ⁻¹' sphere (x✝ default) 0
Module: Mathlib.Topology.MetricSpace.Pseudo.Pi

Goal state before:
pp: case inr.inr
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
h : 0 < r ∨ Nonempty β
hr : 0 < r
⊢ sphere x r = (⋃ i, Function.eval i ⁻¹' sphere (x i) r) ∩ closedBall x r

Tactic:
· ext
    simp [dist_pi_eq_iff hr, dist_pi_le_iff hr.le]

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

Goal state before:
pp: case refine_3
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
⊢ Submodule.map (↑I).subtype
      (Submodule.comap (↑I).subtype (Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J')) ≤
    ↑J

Tactic:
Submodule.map_comap_eq,

Goal state after:
case refine_3
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
⊢ (↑I).subtype.range ⊓ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ≤ ↑J
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
⊢ (↑I').subtype.range ≤
    Submodule.map (↑I').subtype (Submodule.comap (↑I').subtype (↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I)) ⊔
      Submodule.map (↑I').subtype (Submodule.comap (↑I').subtype ↑J')

Tactic:
Submodule.map_comap_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
⊢ (↑I').subtype.range ≤
    (↑I').subtype.range ⊓ ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I ⊔
      Submodule.map (↑I').subtype (Submodule.comap (↑I').subtype ↑J')
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
⊢ (↑I').subtype.range ≤
    (↑I').subtype.range ⊓ ↑(spanSingleton R⁰ (I'.divMod I J')) * ↑I ⊔
      Submodule.map (↑I').subtype (Submodule.comap (↑I').subtype ↑J')

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

Goal state before:
pp: E : Type u_8
inst✝ : SeminormedGroup E
a b : E
⊢ ‖a / b‖ₑ = ‖b / a‖ₑ

Tactic:
← enorm_inv',

Goal state after:
E : Type u_8
inst✝ : SeminormedGroup E
a b : E
⊢ ‖(a / b)⁻¹‖ₑ = ‖b / a‖ₑ
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
f : Filter E
⊢ Disjoint (𝓝 1) f ↔ ∃ δ > 0, ∀ᶠ (y : E) in f, δ ≤ ‖y‖

Tactic:
by
  simpa using disjoint_nhds 1 f

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
⊢ Disjoint (𝓝ˢ k) (comap f (cobounded α) ⊓ 𝓟 s)

Tactic:
hk.disjoint_nhdsSet_left

Goal state after:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
k s : Set β
f : β → α
hk : IsCompact k
hf : ∀ x ∈ k, ContinuousWithinAt f s x
⊢ ∀ x ∈ k, Disjoint (𝓝 x) (comap f (cobounded α) ⊓ 𝓟 s)
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 δ
a b : α
f : α → δ
hab : a < b
hf_c : ContinuousOn f (Ioo a b)
hf_i : InjOn f (Ioo a b)
this : Inhabited ↑(Ioo a b)
⊢ StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)

Tactic:
let g : Ioo a b → δ := Set.domRestrict (Ioo a b) f

Goal state after:
α : Type u
inst✝⁶ : TopologicalSpace α
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : OrderTopology α
inst✝³ : DenselyOrdered α
δ : Type u_1
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderClosedTopology δ
a b : α
f : α → δ
hab : a < b
hf_c : ContinuousOn f (Ioo a b)
hf_i : InjOn f (Ioo a b)
this : Inhabited ↑(Ioo a b)
g : ↑(Ioo a b) → δ := (Ioo a b).domRestrict f
⊢ StrictMonoOn f (Ioo a b) ∨ StrictAntiOn f (Ioo a b)
Module: Mathlib.Data.ENNReal.BigOperators

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℝ≥0∞
Hle : ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i
⊢ ∃ i ∈ s, f i ≤ g i

Tactic:
contrapose! Hle

Goal state after:
α : Type u_1
s : Finset α
hs : s.Nonempty
f g : α → ℝ≥0∞
Hle : ∀ i ∈ s, g i < f i
⊢ ∑ i ∈ s, g i < ∑ i ∈ s, f i
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : 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
⊢ limsup u f ≤ x

Tactic:
by_cases h' : ∀ y > x, ∃ z, x < z ∧ z < y

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

case neg
α : 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
Module: Mathlib.Order.Filter.AtTopBot.Finset

Goal state before:
pp: α : Type u_3
β : Type u_4
s : Set (Finset α)
t : Finset α
H : ∀ (b : Finset α), t ⊆ b → b ∈ s
⊢ ∃ a, ∀ (b : Finset (α ⊕ β)), a ⊆ b → b.toLeft ∈ s

Tactic:
exact ⟨t.disjSum ∅, fun b hb ↦ H _ (by simpa [← Finset.coe_subset, Set.subset_def] using hb)⟩

Goal state after: