mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case inr
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 S T
inst✝⁹ : Algebra R T
inst✝⁸ : IsScalarTower R S T
inst✝⁷ : IsDedekindDomain S
inst✝⁶ : IsDedekindDomain T
inst✝⁵ : IsDomain R
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : P.LiesOver p
hp : p ≠ ⊥
⊢ p.ramificationIdx' Q = p.ramificationIdx' P * P.ramificationIdx' Q

Tactic:
have : P.IsPrime := isPrime_of_liesOver Q P

Goal state after:
case inr
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 S T
inst✝⁹ : Algebra R T
inst✝⁸ : IsScalarTower R S T
inst✝⁷ : IsDedekindDomain S
inst✝⁶ : IsDedekindDomain T
inst✝⁵ : IsDomain R
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : P.LiesOver p
hp : p ≠ ⊥
this : P.IsPrime
⊢ p.ramificationIdx' Q = p.ramificationIdx' P * P.ramificationIdx' Q
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
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := fun i ↦ b.repr (b i * x)
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (b.repr (b i * x)) k • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b k) =
      f.sum fun i y ↦ (b.repr y).sum fun j z ↦ (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
i : I
hi : i ∈ f.support
⊢ ∑ x ∈ (a i).support, ((a i) x • f i) ⊗ₜ[R] b x =
    ∑ x_1 ∈ f.support.biUnion fun i ↦ (b.repr (b i * x)).support, ((b.repr (b i * x)) x_1 • f i) ⊗ₜ[R] b x_1

Tactic:
apply Finset.sum_subset_zero_on_sdiff

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := ⋯
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (b.repr (b i * x)) k • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b k) =
      f.sum fun i y ↦ (b.repr y).sum fun j z ↦ (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
i : I
hi : i ∈ f.support
⊢ (a i).support ⊆ f.support.biUnion fun i ↦ (b.repr (b i * x)).support

case hg
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := ⋯
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (b.repr (b i * x)) k • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b k) =
      f.sum fun i y ↦ (b.repr y).sum fun j z ↦ (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
i : I
hi : i ∈ f.support
⊢ ∀ x_1 ∈ (f.support.biUnion fun i ↦ (b.repr (b i * x)).support) \ (a i).support,
    ((b.repr (b i * x)) x_1 • f i) ⊗ₜ[R] b x_1 = 0

case hfg
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
I : Type u_4
inst✝ : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : I → I →₀ R := ⋯
h₁ :
  ∀ (k : I),
    ((f.sum fun i y ↦ (b.repr (b i * x)) k • b.repr y).sum fun j z ↦ z • b j ⊗ₜ[R] b k) =
      f.sum fun i y ↦ (b.repr y).sum fun j z ↦ (b.repr (b i * x)) k • z • b j ⊗ₜ[R] b k
h₂ : ∀ (x : S), ∑ a ∈ (b.repr x).support, (b.repr x) a • b a = x
i : I
hi : i ∈ f.support
⊢ ∀ x_1 ∈ (a i).support, ((a i) x_1 • f i) ⊗ₜ[R] b x_1 = ((b.repr (b i * x)) x_1 • f i) ⊗ₜ[R] b x_1
Module: Mathlib.RingTheory.QuasiFinite.Basic

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
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R q
e : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
qF : PrimeSpectrum (p.Fiber S) := e ⟨{ asIdeal := q, isPrime := inst✝³ }, ⋯⟩
this : QuasiFiniteAt p.ResidueField qF.asIdeal
r : p.Fiber S
hr : r ∉ qF.asIdeal
hrq : ↑(PrimeSpectrum.basicOpen r) = {{ asIdeal := qF.asIdeal, isPrime := ⋯ }}
s : R
hs : s ∉ p
x : S
hsx : s • r = 1 ⊗ₜ[R] x
⊢ x ∉ q

Tactic:
have : r ∉ _ := hrq.ge rfl

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
p : Ideal R
inst✝⁴ : p.IsPrime
q : Ideal S
inst✝³ : q.IsPrime
inst✝² : q.LiesOver p
inst✝¹ : EssFiniteType R S
inst✝ : QuasiFiniteAt R q
e : ↑(PrimeSpectrum.comap (algebraMap R S) ⁻¹' {{ asIdeal := p, isPrime := ⋯ }}) ≃ₜ
  PrimeSpectrum ({ asIdeal := p, isPrime := ⋯ }.asIdeal.Fiber S) :=
  PrimeSpectrum.preimageHomeomorphFiber R S { asIdeal := p, isPrime := ⋯ }
qF : PrimeSpectrum (p.Fiber S) := e ⟨{ asIdeal := q, isPrime := inst✝³ }, ⋯⟩
this✝ : QuasiFiniteAt p.ResidueField qF.asIdeal
r : p.Fiber S
hr : r ∉ qF.asIdeal
hrq : ↑(PrimeSpectrum.basicOpen r) = {{ asIdeal := qF.asIdeal, isPrime := ⋯ }}
s : R
hs : s ∉ p
x : S
hsx : s • r = 1 ⊗ₜ[R] x
this : r ∉ { asIdeal := qF.asIdeal, isPrime := ⋯ }.asIdeal
⊢ x ∉ q
Module: Mathlib.RingTheory.Etale.Basic

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ FormallyUnramified R S ∧ FormallySmooth R S ↔ FormallySmooth R S

Tactic:
and_iff_right (FormallyUnramified.of_surjective (Algebra.ofId R S) h)

Goal state after:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ FormallySmooth R S ↔ FormallySmooth R S
Module: Mathlib.RingTheory.Etale.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (algebraMap R S).FormallyEtale ↔ Algebra.FormallyEtale R S

Tactic:
by
  rw [FormallyEtale, toAlgebra_algebraMap]

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

Goal state before:
pp: R : Type u_4
inst✝⁸ : CommRing R
A : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallySmooth R A
inst✝ : FormallySmooth A B
⊢ FormallySmooth R B

Tactic:
refine .of_comp_surjective fun C _ _ I hI f ↦ ?_

Goal state after:
R : Type u_4
inst✝⁸ : CommRing R
A : Type u_5
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
B : Type u_6
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FormallySmooth R A
inst✝ : FormallySmooth A B
C : Type (max u_4 u_6)
x✝¹ : CommRing C
x✝ : Algebra R C
I : Ideal C
hI : I ^ 2 = ⊥
f : B →ₐ[R] C ⧸ I
⊢ ∃ a, (Ideal.Quotient.mkₐ R I).comp a = f
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
R : Type u_4
inst✝⁵ : CommRing R
A : Type u_5
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_6
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
⊢ FormallySmooth B (B ⊗[R] A)

Tactic:
refine .of_comp_surjective fun C _ _ I hI f ↦ ?_

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
R : Type u_4
inst✝⁵ : CommRing R
A : Type u_5
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type u_6
inst✝² : CommRing B
inst✝¹ : Algebra R B
inst✝ : FormallySmooth R A
C : Type (max u_5 u_6)
x✝¹ : CommRing C
x✝ : Algebra B C
I : Ideal C
hI : I ^ 2 = ⊥
f : B ⊗[R] A →ₐ[B] C ⧸ I
⊢ ∃ a, (Ideal.Quotient.mkₐ B I).comp a = f
Module: Mathlib.RingTheory.Unramified.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : EssFiniteType R A
⊢ IsOpen (PrimeSpectrum.zeroLocus ↑(Module.annihilator A Ω[A⁄R]))ᶜ

Tactic:
exact (PrimeSpectrum.isClosed_zeroLocus _).isOpen_compl

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

Goal state before:
pp: R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
⊢ Derivation R (P ⧸ RingHom.ker (algebraMap P S) ^ 2) (S ⊗[P] Ω[P⁄R])

Tactic:
by
  letI := Submodule.liftQ ((RingHom.ker (algebraMap P S) ^ 2).restrictScalars R)
    (((mk P S _ 1).restrictScalars R).comp (KaehlerDifferential.D R P).toLinearMap)
  refine ⟨this ?_, ?_, ?_⟩
  · rintro x hx
    simp only [Submodule.restrictScalars_mem, pow_two] at hx
    simp only [LinearMap.mem_ker, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
      Derivation.coeFn_coe, Function.comp_apply, mk_apply]
    refine Submodule.smul_induction_on hx ?_ ?_
    · intro x hx y hy
      simp only [smul_eq_mul, Derivation.leibniz, tmul_add, ← smul_tmul, Algebra.smul_def,
        mul_one, RingHom.mem_ker.mp hx, RingHom.mem_ker.mp hy, zero_tmul, zero_add]
    · intro x y hx hy; simp only [map_add, hx, hy, tmul_add, zero_add]
  · change (1 : S) ⊗ₜ[P] KaehlerDifferential.D R P 1 = 0; simp
  · intro a b
    obtain ⟨a, rfl⟩ := Submodule.Quotient.mk_surjective _ a
    obtain ⟨b, rfl⟩ := Submodule.Quotient.mk_surjective _ b
    change (1 : S) ⊗ₜ[P] KaehlerDifferential.D R P (a * b) =
      Ideal.Quotient.mk _ a • ((1 : S) ⊗ₜ[P] KaehlerDifferential.D R P b) +
      Ideal.Quotient.mk _ b • ((1 : S) ⊗ₜ[P] KaehlerDifferential.D R P a)
    simp only [← Ideal.Quotient.algebraMap_eq, IsScalarTower.algebraMap_smul,
      Derivation.leibniz, tmul_add, tmul_smul]

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

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

Tactic:
rw [H]

Goal state after:
case refine_3
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 ∘ₗ kerToTensor R P' S = LinearMap.id }
l : S ⊗[P'] Ω[P'⁄R] →ₗ[P'] ↥(RingHom.ker (algebraMap P' S))
hl : l ∘ₗ kerToTensor R P' S = LinearMap.id
x : (RingHom.ker (algebraMap P S)).Cotangent
⊢ ((↑e₁.symm ∘ₗ ↑P l ∘ₗ ↑e₂.symm) ∘ₗ ↑e₂ ∘ₗ ↑P (kerToTensor R P' S) ∘ₗ ↑e₁) x = LinearMap.id x
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
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
⊢ ¬minpoly K ((algebraMap A Q.ResidueField) x) ^ 2 ∣ p

Tactic:
have : Algebra.FiniteType K A := .of_surjective _ hp₂

Goal state after:
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
Q : Ideal A
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt K Q
x : A
p : K[X]
hp₁ : Ideal.span {p} = RingHom.ker (aeval x).toRingHom
hp₂ : Function.Surjective ⇑(aeval x)
this : FiniteType K A
⊢ ¬minpoly K ((algebraMap A Q.ResidueField) x) ^ 2 ∣ p
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

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

Tactic:
· use y, hymem, z, hzmem

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case neg.h
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
ha : a ∈ ⋂ i ∈ t, S i
⊢ a ∈ ⋃ i ∈ s, S i

Tactic:
simp only [Set.mem_iInter] at ha

Goal state after:
case neg.h
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
ha : ∀ i ∈ t, a ∈ S i
⊢ a ∈ ⋃ i ∈ s, S i
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

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun z xz => ?_

Goal state after:
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
z : ℝ
xz : z < x
⊢ z ≤ mk g
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: ⊢ sInf ∅ = 0

Tactic:
← coe_eq_zero,

Goal state after:
⊢ ↑(sInf ∅) = 0
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this : a * x⁻¹ < 1
⊢ a ≤ y

Tactic:
have : a * x⁻¹ * x ≤ y := h _ this

Goal state after:
x y : ℝ≥0
h : ∀ a < 1, a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this✝ : a * x⁻¹ < 1
this : a * x⁻¹ * x ≤ y
⊢ a ≤ 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✝² : FunLike F E ℝ
inst✝¹ : AddGroup E
inst✝ : NonarchAddGroupSeminormClass F E
f : F
x✝¹ x✝ a : E
⊢ max (f a) (f a) ≤ f a

Tactic:
max_self (f a)

Goal state after:
R : Type u_1
R' : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝² : FunLike F E ℝ
inst✝¹ : AddGroup E
inst✝ : NonarchAddGroupSeminormClass F E
f : F
x✝¹ x✝ a : E
⊢ f a ≤ f a
Module: Mathlib.Data.ENNReal.Real

Goal state before:
pp: a : ℝ≥0
b : ℝ
⊢ ↑a < ENNReal.ofReal b ↔ ↑a < b

Tactic:
by
  simp [ENNReal.ofReal, Real.lt_toNNReal_iff_coe_lt]

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

Goal state before:
pp: p : ℝ
hp : 0 ≤ p
n : ℕ
⊢ ENNReal.ofReal (p ^ n) = ↑(NNReal.mk p hp) ^ n

Tactic:
← coe_pow,

Goal state after:
p : ℝ
hp : 0 ≤ p
n : ℕ
⊢ ENNReal.ofReal (p ^ n) = ↑(NNReal.mk p hp ^ n)
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✝³ : AddGroup E
inst✝² : SMul R ℝ
inst✝¹ : SMul R ℝ≥0
inst✝ : IsScalarTower R ℝ≥0 ℝ
r : R
p : NonarchAddGroupSeminorm E
x y : E
⊢ r • p (x + y) ≤ max (r • p x) (r • p y)

Tactic:
simp only [← smul_one_smul ℝ≥0 r (_ : ℝ), NNReal.smul_def, smul_eq_mul, ←
          mul_max_of_nonneg _ _ NNReal.zero_le_coe]
        gcongr
        apply map_add_le_max

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

Goal state before:
pp: case pos
ι : Sort u_1
f : ι → ℝ≥0
h : BddAbove (range f)
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, f i

pp: case neg
ι : Sort u_1
f : ι → ℝ≥0
h : ¬BddAbove (range f)
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, f i

Tactic:
· rw [← coe_iSup h, toNNReal_coe]

Goal state after:
case neg
ι : Sort u_1
f : ι → ℝ≥0
h : ¬BddAbove (range f)
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, 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
⊢ count K v (I * I') = count K v I + count K v I'

Tactic:
have hv : Irreducible (Associates.mk v.asIdeal) := by apply v.associates_irreducible
  obtain ⟨a, J, ha, haJ⟩ := exists_eq_spanSingleton_mul I
  have ha_ne_zero : Associates.mk (Ideal.span {a} : Ideal R) ≠ 0 := by
    rw [ne_eq, Associates.mk_eq_zero, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]; exact ha
  have hJ_ne_zero : Associates.mk J ≠ 0 := Associates.mk_ne_zero.mpr (ideal_factor_ne_zero hI haJ)
  obtain ⟨a', J', ha', haJ'⟩ := exists_eq_spanSingleton_mul I'
  have ha'_ne_zero : Associates.mk (Ideal.span {a'} : Ideal R) ≠ 0 := by
    rw [ne_eq, Associates.mk_eq_zero, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]; exact ha'
  have hJ'_ne_zero : Associates.mk J' ≠ 0 :=
    Associates.mk_ne_zero.mpr (ideal_factor_ne_zero hI' haJ')
  have h_prod : I * I' = spanSingleton R⁰ ((algebraMap R K) (a * a'))⁻¹ * ↑(J * J') := by
    rw [haJ, haJ', mul_assoc, mul_comm (J : FractionalIdeal R⁰ K), mul_assoc, ← mul_assoc,
      spanSingleton_mul_spanSingleton, coeIdeal_mul, map_mul, mul_inv,
      mul_comm (J : FractionalIdeal R⁰ K)]
  rw [count_well_defined K v hI haJ, count_well_defined K v hI' haJ',
    count_well_defined K v (mul_ne_zero hI hI') h_prod, ← Associates.mk_mul_mk,
    Associates.count_mul hJ_ne_zero hJ'_ne_zero hv, ← Ideal.span_singleton_mul_span_singleton,
    ← Associates.mk_mul_mk, Associates.count_mul ha_ne_zero ha'_ne_zero hv]
  push_cast
  ring

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

Goal state before:
pp: a : ℝ≥0∞
⊢ a * (3⁻¹ + 3⁻¹ + 3⁻¹) = a

Tactic:
inv_three_add_inv_three,

Goal state after:
a : ℝ≥0∞
⊢ a * 1 = a
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: case inl.inl
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
hm : m < 0
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
simp_all [zero_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]

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

Goal state before:
pp: case inl.inr.inl
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
hm : m = 0
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
simp_all [zero_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]

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

Goal state before:
pp: case inl.inr.inr
x : ℝ≥0∞
m : ℤ
hx₀ : x = 0
hm : 0 < m
⊢ x ^ (-m) = (x ^ m)⁻¹

Tactic:
simp_all [zero_zpow_def, ne_of_lt, ne_of_gt, lt_asymm]

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

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

Tactic:
by
  rw [ENNReal.zpow_neg, ENNReal.inv_zpow]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
⊢ Function.swap dist = dist

Tactic:
funext x y; exact dist_comm _ _

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

Goal state before:
pp: α : Type u
inst✝ : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ ⋃ x ∈ t, closedEBall x ε = univ
⊢ SecondCountableTopology α

Tactic:
by
  suffices SeparableSpace α from UniformSpace.secondCountable_of_separable α
  have : ∀ ε > 0, ∃ t : Set α, Set.Countable t ∧ univ ⊆ ⋃ x ∈ t, closedEBall x ε := by
    simpa only [univ_subset_iff] using hs
  rcases subset_countable_closure_of_almost_dense_set (univ : Set α) this with ⟨t, -, htc, ht⟩
  exact ⟨⟨t, htc, fun x => ht (mem_univ x)⟩⟩

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

Goal state before:
pp: case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ Ici a \ Ioi a ⊆ closure[inst✝³] (Ioi a)

Tactic:
Ici_sdiff_Ioi_same,

Goal state after:
case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
h : (Ioi a).Nonempty
⊢ {a} ⊆ closure[inst✝³] (Ioi a)
Module: Mathlib.Topology.MetricSpace.Basic

Goal state before:
pp: γ : Type w
inst✝² : MetricSpace γ
α : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : DiscreteTopology α
ε : ℝ
hε : 0 < ε
f : α → γ
hf : Pairwise fun x y ↦ ε ≤ dist (f x) (f y)
⊢ Pairwise fun x y ↦ (f x, f y) ∉ {p | dist p.1 p.2 < ε}

Tactic:
by simpa using hf

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

Goal state before:
pp: α : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : DenselyOrdered α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
x y : α
hy : y < x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x) ∧ Tendsto u atTop (𝓝 x)

Tactic:
have hx : x ∉ Ioo y x := fun h => (lt_irrefl x h.2).elim
  have ht : Set.Nonempty (Ioo y x) := nonempty_Ioo.2 hy
  rcases (isLUB_Ioo hy).exists_seq_strictMono_tendsto_of_notMem hx ht with ⟨u, hu⟩
  exact ⟨u, hu.1, hu.2.2.symm⟩

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
β : Type u_2
ε : ℝ
hε : 0 < ε
f : β → α
hf : Pairwise fun x y ↦ ε ≤ dist (f x) (f y)
⊢ Pairwise fun x y ↦ (f x, f y) ∉ {p | dist p.1 p.2 < ε}

Tactic:
by simpa using hf

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : FirstCountableTopology α
s : Set α
hs : Dense s
x y : α
hy : y < x
⊢ ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n ∈ Ioo y x ∩ s) ∧ Tendsto u atTop (𝓝 x)

Tactic:
have hnonempty : (Ioo y x ∩ s).Nonempty := by
    obtain ⟨z, hyz, hzx⟩ := hs.exists_between hy
    exact ⟨z, mem_inter hzx hyz⟩
  have hx : IsLUB (Ioo y x ∩ s) x := hs.isLUB_inter_iff isOpen_Ioo |>.mpr <| isLUB_Ioo hy
  apply hx.exists_seq_strictMono_tendsto_of_notMem (by simp) hnonempty |>.imp
  simp_all

Goal state after: