mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Norm.Basic

Goal state before:
pp: K : Type u_4
L : Type u_5
F : Type u_6
inst✝¹¹ : Field K
inst✝¹⁰ : Field L
inst✝⁹ : Field F
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra K F
E : Type u_7
inst✝⁶ : Field E
inst✝⁵ : Algebra K E
inst✝⁴ : Algebra L F
inst✝³ : IsScalarTower K L F
inst✝² : IsAlgClosed E
inst✝¹ : Algebra.IsSeparable K F
inst✝ : FiniteDimensional K F
pb : PowerBasis K L
this✝¹ : FiniteDimensional L F
this✝ : Algebra.IsSeparable L F
this : Fintype (L →ₐ[K] E) := PowerBasis.AlgHom.fintype pb
σ : F →ₐ[K] E
⊢ σ ((algebraMap L F) pb.gen) = (algHomEquivSigma σ).fst pb.gen

Tactic:
simp only [algHomEquivSigma, Equiv.coe_fn_mk, AlgHom.domRestrict, AlgHom.comp_apply,
      IsScalarTower.coe_toAlgHom']

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Noetherian

Goal state before:
pp: case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this✝¹ : (algebraMap R (Localization p.primeCompl)) r = 1
q : Ideal R
hq : q.IsPrime
e : q ≠ p
this✝ : { asIdeal := q, isPrime := ⋯ } ≠ { asIdeal := p, isPrime := ⋯ }
this : (algebraMap R (Localization.AtPrime q)) r = 0
⊢ r ∈ q

Tactic:
← IsLocalization.AtPrime.to_map_mem_maximal_iff (Localization.AtPrime q) q,

Goal state after:
case refine_3
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
p : Ideal R
inst✝ : p.IsPrime
r : R
hr : (toPiLocalization R) r = Pi.single { asIdeal := p, isPrime := ⋯ } 1
this✝¹ : (algebraMap R (Localization p.primeCompl)) r = 1
q : Ideal R
hq : q.IsPrime
e : q ≠ p
this✝ : { asIdeal := q, isPrime := ⋯ } ≠ { asIdeal := p, isPrime := ⋯ }
this : (algebraMap R (Localization.AtPrime q)) r = 0
⊢ (algebraMap R (Localization.AtPrime q)) r ∈ IsLocalRing.maximalIdeal (Localization.AtPrime q)
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case succ.refine_2.h
S : Type u_1
inst✝¹ : CommRing S
P : Ideal S
P_prime : P.IsPrime
inst✝ : IsDedekindDomain S
hP : P ≠ ⊥
i : ℕ
ih : cardQuot (P ^ i) = cardQuot P ^ i
this : P ^ (i + 1) < P ^ i
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
f g : (c : S) → c ∈ P ^ i → S
hg : ∀ (c : S) (hc : c ∈ P ^ i), g c hc ∈ P ^ (i + 1)
hf : ∀ (c : S) (hc : c ∈ P ^ i), a * f c hc + g c hc = c
k : (c' : S ⧸ P ^ i.succ) → c' ∈ map (mkQ (P ^ i.succ)) (P ^ i) → S
hk_mem : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), k c' hc' ∈ P ^ i
hk_eq : ∀ (c' : S ⧸ P ^ i.succ) (hc' : c' ∈ map (mkQ (P ^ i.succ)) (P ^ i)), (mkQ (P ^ i.succ)) (k c' hc') = c'
d : S
hd' : (mkQ (P ^ i.succ)) (a * d) ∈ map (mkQ (P ^ i.succ)) (P ^ i)
⊢ k ((mkQ (P ^ i.succ)) (a * d)) ⋯ - a * d ∈ P ^ (i + 1)

Tactic:
exact (Submodule.Quotient.eq _).mp (hk_eq _ hd')

Goal state after:
Module: Mathlib.RingTheory.Ideal.Norm.AbsNorm

Goal state before:
pp: case intro
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
P : Ideal S
inst✝ : P.IsMaximal
this✝¹ : IsAddTorsionFree S
this✝ : CharZero S
this : Finite (S ⧸ P)
val✝ : Fintype (S ⧸ P)
⊢ ∃ p n, 0 < n ∧ ↑p ∈ P ∧ Nat.Prime p ∧ absNorm P = p ^ n

Tactic:
let := Ideal.Quotient.field P

Goal state after:
case intro
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : IsDedekindDomain S
inst✝² : Free ℤ S
inst✝¹ : Module.Finite ℤ S
P : Ideal S
inst✝ : P.IsMaximal
this✝² : IsAddTorsionFree S
this✝¹ : CharZero S
this✝ : Finite (S ⧸ P)
val✝ : Fintype (S ⧸ P)
this : Field (S ⧸ P) := Quotient.field P
⊢ ∃ p n, 0 < n ∧ ↑p ∈ P ∧ Nat.Prime p ∧ absNorm P = p ^ n
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed[inst✝] Z
⊢ Z ⊆ closure[inst✝] (Z ∩ closedPoints X)

Tactic:
rw [← Set.disjoint_compl_left_iff_subset, Set.disjoint_iff_inter_eq_empty,
      ← Set.not_nonempty_iff_eq_empty]

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
Z : Set X
hZ : IsClosed[inst✝] Z
⊢ ¬((closure[inst✝] (Z ∩ closedPoints X))ᶜ ∩ Z).Nonempty
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
h : ∀ (n : ℕ), ∃ k, map f p ≤ P ^ k ∧ n < k
⊢ ¬∃ n, ∀ a ∈ {n | map f p ≤ P ^ n}, a ≤ n

Tactic:
by push Not; exact h

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
A : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
B : Type u_3
inst✝⁴ : CommRing B
inst✝³ : Algebra R B
inst✝² : Algebra A B
inst✝¹ : IsScalarTower R A B
inst✝ : FormallyUnramified R B
⊢ FormallyUnramified A B

Tactic:
by
  rw [iff_comp_injective]
  intro Q _ _ I e f₁ f₂ e'
  let := ((algebraMap A Q).comp (algebraMap R A)).toAlgebra
  let : IsScalarTower R A Q := IsScalarTower.of_algebraMap_eq' rfl
  refine AlgHom.restrictScalars_injective R ?_
  refine FormallyUnramified.ext I ⟨2, e⟩ ?_
  intro x
  exact AlgHom.congr_fun e' x

Goal state after:
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 Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : QuasiFiniteAt R Q
this : (Ideal.map (algebraMap S (Localization.AtPrime Q)) P).IsPrime
H : Ideal.map (algebraMap S (Localization.AtPrime Q)) P = IsLocalRing.maximalIdeal (Localization.AtPrime Q)
⊢ P = Ideal.under S (IsLocalRing.maximalIdeal (Localization Q.primeCompl))

Tactic:
← H,

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
P Q : Ideal S
inst✝² : P.IsPrime
inst✝¹ : Q.IsPrime
h₁ : P ≤ Q
h₂ : Ideal.under R P = Ideal.under R Q
inst✝ : QuasiFiniteAt R Q
this : (Ideal.map (algebraMap S (Localization.AtPrime Q)) P).IsPrime
H : Ideal.map (algebraMap S (Localization.AtPrime Q)) P = IsLocalRing.maximalIdeal (Localization.AtPrime Q)
⊢ P = Ideal.under S (Ideal.map (algebraMap S (Localization.AtPrime Q)) P)
Module: Mathlib.RingTheory.Unramified.Finite

Goal state before:
pp: case add
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
r : S
m : M
x✝ y✝ : S ⊗[R] S
a✝¹ :
  (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip (r • m))) x✝ =
    (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (1 ⊗ₜ[R] r * x✝)
a✝ :
  (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip (r • m))) y✝ =
    (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (1 ⊗ₜ[R] r * y✝)
⊢ (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip (r • m))) (x✝ + y✝) =
    (TensorProduct.AlgebraTensorModule.map LinearMap.id ((lsmul R R M).toLinearMap.flip m)) (1 ⊗ₜ[R] r * (x✝ + y✝))

Tactic:
· simp only [map_add, mul_add, *]

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

Goal state before:
pp: case h2.refine_2
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
w : P.Ring
hw : w ∈ P.ker
⊢ (Extension.Cotangent.map (Q.toComp P).toExtensionHom) (Extension.Cotangent.mk ⟨w, hw⟩) =
    Extension.Cotangent.mk ⟨(Q.toComp P).toAlgHom w, ⋯⟩

Tactic:
rw [map_mk]
      rfl

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

Goal state before:
pp: case refine_1.refine_2
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
this : Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker →
  P ⧸ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) →ₗ[R] S ⊗[P] Ω[P⁄R] :=
  (Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)).liftQ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P))
x : P
hx : x ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
⊢ ∀ (x y : P), 1 ⊗ₜ[P] (D R P) x = 0 → 1 ⊗ₜ[P] (D R P) y = 0 → 1 ⊗ₜ[P] (D R P) (x + y) = 0

Tactic:
intro x y hx hy

Goal state after:
case refine_1.refine_2
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
this : Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker →
  P ⧸ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) →ₗ[R] S ⊗[P] Ω[P⁄R] :=
  (Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)).liftQ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P))
x✝ : P
hx✝ : x✝ ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
x y : P
hx : 1 ⊗ₜ[P] (D R P) x = 0
hy : 1 ⊗ₜ[P] (D R P) y = 0
⊢ 1 ⊗ₜ[P] (D R P) (x + y) = 0
Module: Mathlib.RingTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsPrime
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.QuasiFinite R S
inst✝ : Fintype ↑(p.primesOver S)
this✝ : Fintype (PrimeSpectrum (p.Fiber S)) := Fintype.ofFinite (PrimeSpectrum (p.Fiber S))
q : PrimeSpectrum (p.Fiber S)
a✝ : q ∈ Finset.univ
r : Ideal S := comap Algebra.TensorProduct.includeRight q.asIdeal
this : Algebra (Localization.AtPrime p) (Localization.AtPrime r) := Localization.AtPrime.algebraOfLiesOver p r
⊢ r.ramificationIdx R * r.inertiaDeg R = finrank p.ResidueField (Localization.AtPrime q.asIdeal)

Tactic:
rw [ramificationIdx_eq p r, inertiaDeg_eq p r]

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
p : Ideal R
inst✝⁴ : p.IsPrime
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.QuasiFinite R S
inst✝ : Fintype ↑(p.primesOver S)
this✝ : Fintype (PrimeSpectrum (p.Fiber S)) := Fintype.ofFinite (PrimeSpectrum (p.Fiber S))
q : PrimeSpectrum (p.Fiber S)
a✝ : q ∈ Finset.univ
r : Ideal S := comap Algebra.TensorProduct.includeRight q.asIdeal
this : Algebra (Localization.AtPrime p) (Localization.AtPrime r) := Localization.AtPrime.algebraOfLiesOver p r
⊢ (length (Localization.AtPrime r) (Localization.AtPrime r ⧸ map (algebraMap R (Localization.AtPrime r)) p)).toNat *
      finrank p.ResidueField r.ResidueField =
    finrank p.ResidueField (Localization.AtPrime q.asIdeal)
Module: Mathlib.Algebra.Module.Torsion.PrimaryComponent

Goal state before:
pp: case mp.refine_2
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₂
w : ℕ
y : M
hy : y ∈ N₁
z : M
hz : z ∈ N₂
h : ∀ a ∈ I ^ w, a • (y + z) = 0
a : A
ha : a ∈ I ^ w
⊢ a • z = 0

Tactic:
· 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:
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case neg
ι : 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
t : Finset ι
hts : t ⊆ s
⊢ t.Nonempty → (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a = 0

Tactic:
ht

Goal state after:
case neg
ι : 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
t : Finset ι
hts : t ⊆ s
ht : t.Nonempty
⊢ (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a = 0
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case a
ι : 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
t : Finset ι
a✝ : t ∈ s.powerset
⊢ (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a = ((-1) ^ #t * ∏ i ∈ t, (S i).indicator 1 a) • f a

Tactic:
simp only [prod_const_one, prod_indicator_apply]

Goal state after:
case a
ι : 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
t : Finset ι
a✝ : t ∈ s.powerset
⊢ (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a = ((-1) ^ #t * (⋂ i ∈ t, S i).indicator 1 a) • f a
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: case pos
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
i : ι
hi : i ∈ t
⊢ (-1) ^ #t • ∑ a ∈ t.inf' ⋯ S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x

Tactic:
simp only [prod_const_one, prod_indicator_apply]

Goal state after:
case pos
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : AddCommGroup G
inst✝ : DecidableEq α
s : Finset ι
S : ι → Finset α
f : α → G
t : Finset ι
a✝ : t ∈ s.powerset
i : ι
hi : i ∈ t
⊢ (-1) ^ #t • ∑ a ∈ t.inf' ⋯ S, f a = ∑ x ∈ s.biUnion S, ((-1) ^ #t * (1 * (⋂ x ∈ t, ↑(S x)).indicator 1 x)) • f x
Module: Mathlib.Algebra.Order.Archimedean.Real.Basic

Goal state before:
pp: s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
hbdd' : BddAbove (-s)
⊢ ∃ x, IsGLB s x

Tactic:
use -Classical.choose (Real.exists_isLUB hne' hbdd')

Goal state after:
case h
s : Set ℝ
hne : s.Nonempty
hbdd : BddBelow s
hne' : (-s).Nonempty
hbdd' : BddAbove (-s)
⊢ IsGLB s (-Classical.choose ⋯)
Module: Mathlib.Data.NNReal.Defs

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

Tactic:
NNReal.coe_zpow,

Goal state after:
x : ℝ
hx : 0 ≤ x
n : ℤ
⊢ ↑(x ^ n).toNNReal = ↑x.toNNReal ^ n
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 : Ideal R
hI : I ≠ 0
| ↑I

Tactic:
rw [← Ideal.finprod_heightOneSpectrum_factorization hI]

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 : Ideal R
hI : I ≠ 0
| ↑(∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)
Module: Mathlib.Data.ENNReal.Basic

Goal state before:
pp: a : ℝ≥0∞
h : ENNReal.ofReal a.toReal = a
⊢ a ≠ ∞

Tactic:
rw [← h]
    exact ofReal_ne_top

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:
simp only [hb, add_top, toReal_top, add_zero, toReal_nonneg]

Goal state after:
Module: Mathlib.Algebra.Order.Module.Field

Goal state before:
pp: 𝕜 : Type u_1
G : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup G
inst✝³ : PartialOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : Module 𝕜 G
a : 𝕜
b₁ b₂ : G
inst✝ : PosSMulStrictMono 𝕜 G
h : a < 0
⊢ a⁻¹ • b₁ < b₂ ↔ a • b₂ < b₁

Tactic:
by
  rw [← smul_lt_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]

Goal state after:
Module: Mathlib.Algebra.Order.Module.Field

Goal state before:
pp: 𝕜 : Type u_1
G : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : LinearOrder 𝕜
inst✝⁵ : IsStrictOrderedRing 𝕜
inst✝⁴ : AddCommGroup G
inst✝³ : PartialOrder G
inst✝² : IsOrderedAddMonoid G
inst✝¹ : Module 𝕜 G
a : 𝕜
b₁ b₂ : G
inst✝ : PosSMulStrictMono 𝕜 G
h : a < 0
⊢ b₁ < a⁻¹ • b₂ ↔ b₂ < a • b₁

Tactic:
by
  rw [← smul_lt_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]

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

Goal state before:
pp: x y : EReal
h : x ≤ y
hx : x ≠ ⊥
hy : y ≠ ⊤
⊢ x.toReal ≤ y.toReal

Tactic:
lift x to ℝ using ⟨ne_top_of_le_ne_top hy h, hx⟩
  lift y to ℝ using ⟨hy, ne_bot_of_le_ne_bot hx h⟩
  simpa using h

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

Goal state before:
pp: x y : ℝ
⊢ Real.toEReal ⁻¹' Ioo ↑x ↑y = Ioo x y

Tactic:
← Ioi_inter_Iio

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

Goal state before:
pp: x : ℝ
⊢ Real.toEReal ⁻¹' Ioo ↑x ⊤ = Ioi x

Tactic:
← Ioi_inter_Iio

Goal state after:
x : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ↑x ∩ Iio ⊤) = Ioi x
Module: Mathlib.Data.EReal.Basic

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

Tactic:
← Ioi_inter_Iio

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

Goal state before:
pp: ⊢ Real.toEReal ⁻¹' Ioo ⊥ ⊤ = univ

Tactic:
← Ioi_inter_Iio

Goal state after:
⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iio ⊤) = univ
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: a b : ℝ≥0∞
h : a < b
⊢ b⁻¹ < a⁻¹

Tactic:
lift a to ℝ≥0 using h.ne_top

Goal state after:
b : ℝ≥0∞
a : ℝ≥0
h : ↑a < b
⊢ b⁻¹ < (↑a)⁻¹
Module: Mathlib.Topology.EMetricSpace.Defs

Goal state before:
pp: case mp
α : Type u
inst✝ : PseudoEMetricSpace α
β : Type u_2
p : β → Prop
f : β → ℝ≥0∞
hf₀ : ∀ (x : β), p x → 0 < f x
hf : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ x, p x ∧ f x ≤ ε
s : Set (α × α)
⊢ (∃ i, 0 < i ∧ {p | edist p.1 p.2 < i} ⊆ s) → ∃ i, p i ∧ {p | edist p.1 p.2 < f i} ⊆ s

Tactic:
rintro ⟨ε, ε₀, hε⟩
    rcases hf ε ε₀ with ⟨i, hi, H⟩
    exact ⟨i, hi, fun x hx => hε <| lt_of_lt_of_le hx.out H⟩

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

Goal state before:
pp: x : ℝ≥0
hx : ↑x ≠ 0
y : ℝ≥0
hy : 1 < ↑y
A : y ≠ 0
⊢ ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)

Tactic:
by
    refine NNReal.exists_mem_Ico_zpow ?_ (one_lt_coe_iff.1 hy)
    simpa only [Ne, coe_eq_zero] using hx

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

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

Tactic:
rw [edist_dist, ENNReal.toReal_ofReal dist_nonneg]

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

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

Tactic:
rw [mem_sphere', mem_sphere]

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ≥0
⊢ closedEBall x ↑ε = closedBall x ↑ε

Tactic:
by
  rw [← closedEBall_ofReal ε.coe_nonneg, ENNReal.ofReal_coe_nnreal]

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

Goal state before:
pp: α : Type u
β : Type v
X✝ : Type u_1
ι : Type u_2
inst✝ : PseudoMetricSpace α
X : Type u_3
e : PseudoEMetricSpace X
dist : X → X → ℝ
dist_nonneg : ∀ (x y : X), 0 ≤ dist x y
h : ∀ (x y : X), edist x y = ENNReal.ofReal (dist x y)
x y z : X
⊢ dist x z ≤ dist x y + dist y z

Tactic:
by
    simpa [h, dist_nonneg, add_nonneg, ← ENNReal.ofReal_add] using edist_triangle x y z

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

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
f : ℕ → α
m n : ℕ
h : m ≤ n
⊢ dist (f m) (f n) ≤ ∑ i ∈ Finset.Ico m n, dist (f i) (f (i + 1))

Tactic:
by
  induction n, h using Nat.le_induction with
  | base => rw [Finset.Ico_self, Finset.sum_empty, dist_self]
  | succ n hle ihn =>
    calc
      dist (f m) (f (n + 1)) ≤ dist (f m) (f n) + dist (f n) (f (n + 1)) := dist_triangle _ _ _
      _ ≤ (∑ i ∈ Finset.Ico m n, _) + _ := add_le_add ihn le_rfl
      _ = ∑ i ∈ Finset.Ico m (n + 1), _ := by
        rw [← Finset.insert_Ico_right_eq_Ico_add_one hle, Finset.sum_insert, add_comm]; simp

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

Goal state before:
pp: case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
x' : ↑s := Finv (F ⟨x, xs⟩)
⊢ x ∈ ⋃ y ∈ range (Subtype.val ∘ Finv), ball y ε

Tactic:
have : F x' = F ⟨x, xs⟩ := Function.invFun_eq ⟨⟨x, xs⟩, rfl⟩

Goal state after:
case inr
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
x0 : α
hx0 : x0 ∈ s
this✝ : Inhabited ↑s
ε : ℝ
ε0 : ε > 0
β : Type u
fβ : Fintype β
F : ↑s → β
hF : ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε
Finv : β → ↑s := Function.invFun F
x : α
xs : x ∈ s
x' : ↑s := Finv (F ⟨x, xs⟩)
this : F x' = F ⟨x, xs⟩
⊢ x ∈ ⋃ y ∈ range (Subtype.val ∘ Finv), ball y ε
Module: Mathlib.Topology.Order.DenselyOrdered

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
⊢ IsClosed[inst✝³] (Ioo a b) ↔ b ≤ a

Tactic:
refine ⟨fun h => le_of_not_gt fun hab => ?_, by simp_all⟩
  have := h.closure_eq
  rw [closure_Ioo hab.ne, Icc_eq_Ioo_same_iff] at this
  exact this hab.le

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

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this✝¹ : ∀ i < c, Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this✝ : Icc a c ∉ f
this : x ∈ Icc a b
⊢ False

Tactic:
have : Icc a x ∈ f := by simpa [s, this.1, this.2] using notMem_of_csSup_lt hx ⟨b, hsb⟩

Goal state after:
α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this✝² : ∀ i < c, Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this✝¹ : Icc a c ∉ f
this✝ : x ∈ Icc a b
this : Icc a x ∈ f
⊢ False
Module: Mathlib.Topology.Order.IsLUB

Goal state before:
pp: α : Type u_3
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
x✝ : a ≤ b
f : Ultrafilter α
hfab : Icc a b ∈ ↑f
hf : ∀ x ∈ Icc a b, ¬↑f ≤ 𝓝 x
hpt : ∀ x ∈ Icc a b, {x} ∉ f
s : Set α := {x | x ∈ Icc a b ∧ Icc a x ∉ f}
hsb : b ∈ upperBounds s
ha : a ∈ s
c : α := sSup s
hsc : IsLUB s c
hc : c ∈ Icc a b
this✝² : ∀ i < c, Ioi i ∈ f
x : α
hx : c < x
hxf : Iio x ∉ f
this✝¹ : Icc a c ∉ f
this✝ : x ∈ Icc a b
this : Icc a x ∈ f
⊢ {x} ∈ f

Tactic:
by filter_upwards [f.compl_mem_iff_notMem.mpr hxf, this]; grind

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

Goal state before:
pp: 𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
r _r _y : ℝ
⊢ |_y + -_r| = ‖_y + -_r‖

Tactic:
norm_eq_abs

Goal state after:
𝓕 : Type u_1
α : Type u_2
ι : Type u_3
κ : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
r _r _y : ℝ
⊢ |_y + -_r| = |_y + -_r|
Module: Mathlib.Topology.Order.Bornology

Goal state before:
pp: α : Type u_1
s✝ t : Set α
inst✝⁵ : Bornology α
inst✝⁴ : Preorder α
inst✝³ : IsOrderBornology α
β : Type u_2
inst✝² : Preorder β
inst✝¹ : Bornology β
inst✝ : IsOrderBornology β
s : Set (α × β)
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
by
    rw [← isBounded_image_fst_and_snd, bddBelow_prod, bddAbove_prod, and_and_and_comm,
      isBounded_iff_bddBelow_bddAbove, isBounded_iff_bddBelow_bddAbove]

Goal state after: