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

Goal state before:
pp: 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 : P.Ring
x_in : x ∈ P.toExtension.ker
property✝ : Extension.Cotangent.mk ⟨x, x_in⟩ ∈ P.toExtension.cotangentComplex.ker
⊢ (↑((Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom)
          ((Extension.H1Cotangent.map (Q.toComp P).toExtensionHom)
            ⟨Extension.Cotangent.mk ⟨x, x_in⟩, property✝⟩))).val =
    (↑0).val

Tactic:
suffices (Q.ofComp P).toAlgHom ((Q.toComp P).toAlgHom x) ∈ Q.toExtension.ker ^ 2 by
    simpa [Ideal.toCotangent_eq_zero]

Goal state after:
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 : P.Ring
x_in : x ∈ P.toExtension.ker
property✝ : Extension.Cotangent.mk ⟨x, x_in⟩ ∈ P.toExtension.cotangentComplex.ker
⊢ (Q.ofComp P).toAlgHom ((Q.toComp P).toAlgHom x) ∈ Q.toExtension.ker ^ 2
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝⁷ : FormallySmooth R P.Ring
this✝⁶ : FormallySmooth P.Ring (Localization M')
this✝⁵ : FormallySmooth R Q.Ring
this✝⁴ : Module.Flat S T
this✝³ : Algebra P.Ring Q.Ring := inferInstance
this✝² : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝¹ : Algebra (Localization M') T := fQ.toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring (Localization M') T
⊢ IsLocalization (algebraMapSubmonoid S M') T

Tactic:
convert! ‹IsLocalization M T› using 1

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
fQ : Localization M' →ₐ[R] T := IsLocalization.liftAlgHom ⋯
Q : Extension R T := Extension.ofSurjective fQ ⋯
f : P.Hom Q :=
  { toRingHom := algebraMap P.Ring (Localization M'), toRingHom_algebraMap := ⋯, algebraMap_toRingHom := ⋯ }
this✝⁷ : FormallySmooth R P.Ring
this✝⁶ : FormallySmooth P.Ring (Localization M')
this✝⁵ : FormallySmooth R Q.Ring
this✝⁴ : Module.Flat S T
this✝³ : Algebra P.Ring Q.Ring := inferInstance
this✝² : Algebra P.Ring T := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
this✝¹ : Algebra (Localization M') T := fQ.toAlgebra
this✝ : IsScalarTower P.Ring S T
this : IsScalarTower P.Ring (Localization M') T
⊢ algebraMapSubmonoid S M' = M
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
⊢ IsBaseChange T (map R R S T)

Tactic:
change Function.Bijective ((Algebra.H1Cotangent.map R R S T).liftBaseChange T)

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
⊢ Function.Bijective ⇑(LinearMap.liftBaseChange T (map R R S T))
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
⊢ (⋃ i ∈ s, S i).indicator f a = ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (#t + 1) • (⋂ i ∈ t, S i).indicator f a

pp: case pos
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∈ ⋃ i ∈ s, S i
⊢ (⋃ i ∈ s, S i).indicator f a = ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (#t + 1) • (⋂ i ∈ t, S i).indicator f a

Tactic:
· simp only [ha, not_false_eq_true, Set.indicator_of_notMem, Int.reduceNeg, pow_succ, mul_neg,
      mul_one, neg_smul]
    symm
    apply sum_eq_zero
    simp only [Int.reduceNeg, neg_eq_zero, mem_filter, mem_powerset, and_imp]
    intro t hts ht
    rw [Set.indicator_of_notMem]
    · simp
    · contrapose ha
      simp only [Set.mem_iInter] at ha
      rcases ht with ⟨i, hi⟩
      simp only [Set.mem_iUnion, exists_prop]
      exact ⟨i, hts hi, ha _ hi⟩

Goal state after:
case pos
ι : Type u_1
α : Type u_2
G : Type u_3
inst✝ : AddCommGroup G
s : Finset ι
S : ι → Set α
f : α → G
a : α
ha : a ∈ ⋃ i ∈ s, S i
⊢ (⋃ i ∈ s, S i).indicator f a = ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (#t + 1) • (⋂ i ∈ t, S i).indicator f a
Module: Mathlib.Combinatorics.Enumerative.InclusionExclusion

Goal state before:
pp: ι : 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 ∈ s.powerset with t.Nonempty, (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a +
      ∑ t ∈ s.powerset with ¬t.Nonempty, (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a =
    ∑ t ∈ s.powerset, (-1) ^ #t • (⋂ i ∈ t, S i).indicator f a

Tactic:
rw [sum_filter_add_sum_filter_not]

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

Goal state before:
pp: case a
ι : 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
⊢ ((-1) ^ #t • if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a) =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x

Tactic:
split_ifs with ht

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
ht : t.Nonempty
⊢ (-1) ^ #t • ∑ a ∈ t.inf' ht S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x

case neg
ι : 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
ht : ¬t.Nonempty
⊢ (-1) ^ #t • ∑ a ∈ s.biUnion S, f a =
    ∑ x ∈ s.biUnion S, ((-1) ^ #t * ((∏ i ∈ s \ t, 1) * ∏ i ∈ t, (↑(S i)).indicator 1 x)) • f x
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:
by rw [max_self (f a)]

Goal state after:
Module: Mathlib.Data.NNReal.Defs

Goal state before:
pp: case neg
Γ₀ : Type u_1
inst✝ : LinearOrderedCommGroupWithZero Γ₀
h : Nontrivial Γ₀ˣ
f : Γ₀ →*₀ ℝ≥0
hf : StrictMono ⇑f
r : ℝ≥0
hr : 0 < r
g : Γ₀ˣ
hg1 : g ≠ 1
u : Γ₀ˣ := if g < 1 then g else g⁻¹
hu : u = if g < 1 then g else g⁻¹
hu1 : ¬g < 1
hfg0 : f ↑g ≠ 0
hg1' : 1 < g
⊢ f 1 < f ↑g

Tactic:
exact hf hg1'

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

Goal state after:
α : Type u_1
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
n : ℕ
a : AddUnits ℝ≥0∞
⊢ ↑a ≤ ↑a + ↑(-a)
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
s : Finset (HeightOneSpectrum A)
p : HeightOneSpectrum A → M
hmem : ∀ i ∈ s, p i ∈ primaryComponent M i.asIdeal
⊢ ∑ i ∈ s, p i = 0 → ∀ i ∈ s, p i = 0

Tactic:
hsum

Goal state after:
A : Type u_1
M : Type u_2
inst✝³ : CommRing A
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsDedekindDomain A
s : Finset (HeightOneSpectrum A)
p : HeightOneSpectrum A → M
hmem : ∀ i ∈ s, p i ∈ primaryComponent M i.asIdeal
hsum : ∑ i ∈ s, p i = 0
⊢ ∀ i ∈ s, p i = 0
Module: Mathlib.Data.ENNReal.Operations

Goal state before:
pp: case coe
b x✝ : ℝ≥0
⊢ (↑x✝).toReal - (↑b).toReal ≤ (↑x✝ - ↑b).toReal

Tactic:
· simp only [← coe_sub, NNReal.sub_def, Real.coe_toNNReal', coe_toReal]
    exact le_max_left _ _

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

Goal state before:
pp: ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
inst✝ : Nonempty ι
ha : a ≠ ∞
i : ι
hi : a < f i
x : ℝ≥0∞
hx : ⊥ < x
⊢ a - f i < x

Tactic:
simpa [hi.le, tsub_eq_zero_of_le]

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

Goal state before:
pp: case insert
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
ι : Type u_3
I : ι → FractionalIdeal R⁰ K
i : ι
s : Finset ι
hi : i ∉ s
hrec : (∀ i ∈ s, I i ≠ 0) → count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)
hS : ∀ i_1 ∈ insert i s, I i_1 ≠ 0
hS' : ∀ i ∈ s, I i ≠ 0
hS0 : ∏ i ∈ s, I i ≠ 0
hi0 : I i ≠ 0
⊢ count K v (I i) + count K v (∏ i ∈ s, I i) = count K v (I i) + ∑ x ∈ s, count K v (I x)

Tactic:
hrec hS'

Goal state after:
case insert
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
ι : Type u_3
I : ι → FractionalIdeal R⁰ K
i : ι
s : Finset ι
hi : i ∉ s
hrec : (∀ i ∈ s, I i ≠ 0) → count K v (∏ i ∈ s, I i) = ∑ i ∈ s, count K v (I i)
hS : ∀ i_1 ∈ insert i s, I i_1 ≠ 0
hS' : ∀ i ∈ s, I i ≠ 0
hS0 : ∏ i ∈ s, I i ≠ 0
hi0 : I i ≠ 0
⊢ count K v (I i) + ∑ i ∈ s, count K v (I i) = count K v (I i) + ∑ x ∈ s, count K v (I x)
Module: Mathlib.Data.EReal.Basic

Goal state before:
pp: case neg
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
⊢ ↑(if x = ⊤ then ∞ else ENNReal.ofReal x.toReal) = x

Tactic:
if_neg h_top

Goal state after:
case neg
x : EReal
hx : 0 ≤ x
h_top : ¬x = ⊤
⊢ ↑(ENNReal.ofReal x.toReal) = x
Module: Mathlib.Data.ENNReal.Inv

Goal state before:
pp: ⊢ 2 * 2⁻¹ = 1

Tactic:
← div_eq_mul_inv,

Goal state after:
⊢ 2 / 2 = 1
Module: Mathlib.Topology.MetricSpace.Pseudo.Defs

Goal state before:
pp: α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ ball x ε ∪ sphere x ε = closedBall x ε

Tactic:
ball_union_sphere

Goal state after:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ closedBall x ε = closedBall x ε
Module: Mathlib.Topology.Metrizable.Basic

Goal state before:
pp: ι : Type u_1
X✝ : Type u_2
Y : Type u_3
A : ι → Type u_4
inst✝⁶ : TopologicalSpace X✝
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → TopologicalSpace (A i)
X : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : LindelofSpace X
inst✝ : PseudoMetrizableSpace X
⊢ SecondCountableTopology X

Tactic:
by
  let := pseudoMetrizableSpaceUniformity X
  have := pseudoMetrizableSpaceUniformity_countably_generated X
  suffices _ : SeparableSpace X from secondCountable_of_separable X
  obtain ⟨V, hVb, hVs⟩ := has_seq_basis X
  choose U hUc hUu using fun n =>
    LindelofSpace.elim_nhds_subcover (fun x => ball x (V n))
      (fun x => ball_mem_nhds x (hVb.mem n))
  refine ⟨Set.iUnion U, Set.countable_iUnion hUc, fun x => ?_⟩
  rw [mem_closure_iff_frequently, nhds_eq_comap_uniformity, frequently_comap, hVb.frequently_iff]
  intro n _
  obtain ⟨i, hi, hx⟩ := Set.mem_iUnion₂.1 (Set.eq_univ_iff_forall.1 (hUu n) x)
  rw [ball_eq_of_symmetry] at hx
  exact ⟨(x, i), hx, i, rfl, Set.mem_iUnion_of_mem n hi⟩

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

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

Tactic:
| base =>

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

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

Tactic:
| base =>

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 b : α
hab : a ≠ b
⊢ closure[inst✝³] (Ioo a b) ⊆ Icc a b

pp: case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure[inst✝³] (Ioo a b)

Tactic:
· exact closure_minimal Ioo_subset_Icc_self isClosed_Icc

Goal state after:
case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure[inst✝³] (Ioo a b)
Module: Mathlib.Topology.MetricSpace.Pseudo.Constructions

Goal state before:
pp: case inr.inr
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
x : α × β
r : ℝ
hr : 0 < r
⊢ sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r

Tactic:
ext ⟨x', y'⟩
    simp_rw [Set.mem_union, Set.mem_prod, Metric.mem_closedBall, Metric.mem_sphere, Prod.dist_eq,
      max_eq_iff]
    refine or_congr (and_congr_right ?_) (and_comm.trans (and_congr_left ?_))
    all_goals rintro rfl; rfl

Goal state after:
Module: Mathlib.Topology.Instances.Discrete

Goal state before:
pp: α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
⊢ ⊥ = Preorder.topology α

Tactic:
let _ := Preorder.topology α
  have : OrderTopology α := ⟨rfl⟩
  exact DiscreteTopology.of_predOrder_succOrder.eq_bot.symm

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

Goal state before:
pp: α : Type u_1
inst✝² : Bornology α
inst✝¹ : Lattice α
inst✝ : Nonempty α
h : IsOrderBornology α
s : Set α
⊢ s ∈ cobounded α ↔ s ∈ cobounded α

Tactic:
exact isBounded_compl_iff.symm.trans (h.1 _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : ConditionallyCompleteLinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderClosedTopology β
ι : Sort u_3
inst✝ : Nonempty ι
f : α → β
g : ι → α
Cf : ContinuousAt f (iInf g)
Mf : Monotone f
bdd : BddBelow (range g)
⊢ f (⨅ i, g i) = ⨅ i, f (g i)

Tactic:
rw [iInf, Monotone.map_csInf_of_continuousAt Cf Mf (range_nonempty g) bdd, ← range_comp, iInf,
    comp_def]

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

Goal state before:
pp: case refine_2
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTop α
inst✝ : CompactIccSpace α
x✝¹ : Set α
hs : x✝¹ ∈ atBot
h✝ : Nonempty α
t : α
ht : ∀ b ≤ t, b ∈ x✝¹
x✝ : α
hx : x✝ ∈ (Icc t ⊤)ᶜ
⊢ x✝ ∈ x✝¹

Tactic:
exact (not_and_or.mp hx).casesOn (fun h ↦ ht _ (le_of_not_ge h)) (fun h ↦ (h le_top).elim)

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

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

Tactic:
by
  rw [← dist_one, dist_eq_norm_inv_mul, dist_eq_norm_inv_mul']
  simp

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

Goal state before:
pp: case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
⊢ ↑I ⊓ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ≤ ↑J

Tactic:
rw [← this, inf_comm, coe_inf]

Goal state after:
case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
I J I' J' : FractionalIdeal R⁰ K
H : I * J' = I' * J
h : J ≤ I
h' : J' ≤ I'
hJ' : J' ≠ 0
hI : I ≠ 0
this : (spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J' ⊓ I = J
H' : ¬I'.divMod I J' = 0
⊢ Submodule.comap ((Algebra.lsmul R R K) (I'.divMod I J')) ↑J' ⊓ ↑I ≤ ↑((spanSingleton R⁰ (I'.divMod I J'))⁻¹ * J') ⊓ ↑I
Module: Mathlib.Analysis.Normed.Group.Basic

Goal state before:
pp: E : Type u_5
inst✝ : SeminormedGroup E
⊢ NontrivialTopology E ↔ ∃ x, ‖x‖ ≠ 0

Tactic:
by
  simp [nontrivialTopology_iff_exists_nnnorm_ne_zero', ← NNReal.ne_iff]

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

Goal state before:
pp: R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)

Tactic:
rcases eq_or_ne I ⊥ with rfl | hI

Goal state after:
case inl
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
J : Ideal R
⊢ emultiplicity p.asIdeal (⊥ ⊔ J) = min (emultiplicity p.asIdeal ⊥) (emultiplicity p.asIdeal J)

case inr
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : HeightOneSpectrum R
I J : Ideal R
hI : I ≠ ⊥
⊢ emultiplicity p.asIdeal (I ⊔ J) = min (emultiplicity p.asIdeal I) (emultiplicity p.asIdeal J)
Module: Mathlib.GroupTheory.Archimedean

Goal state before:
pp: G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
⊢ ∃ b, H = closure {b}

Tactic:
rcases eq_or_ne H ⊥ with rfl | hbot

Goal state after:
case inl
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
a : G
h₀ : 1 < a
hd : Disjoint (↑⊥) (Ioo 1 a)
⊢ ∃ b, ⊥ = closure {b}

case inr
G : Type u_1
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : MulArchimedean G
H : Subgroup G
a : G
h₀ : 1 < a
hd : Disjoint (↑H) (Ioo 1 a)
hbot : H ≠ ⊥
⊢ ∃ b, H = closure {b}
Module: Mathlib.Topology.Algebra.Ring.Real

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
⊢ ContinuousAdd ℝ≥0∞

Tactic:
by
  refine ⟨continuous_iff_continuousAt.2 ?_⟩
  rintro ⟨_ | a, b⟩
  · exact tendsto_nhds_top_mono' continuousAt_fst fun p => le_add_right le_rfl
  rcases b with (_ | b)
  · exact tendsto_nhds_top_mono' continuousAt_snd fun p => le_add_left le_rfl
  simp only [ContinuousAt, some_eq_coe, nhds_coe_coe, ← coe_add, tendsto_map'_iff,
    Function.comp_def, tendsto_coe, tendsto_add]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
⊢ ∀ᶠ (b_1 : { x // x ∈ s }) in atTop, b < ↑b_1

Tactic:
rcases ha.exists_between hb with ⟨c, hcs, bc, bca⟩
    lift c to s using hcs
    exact (eventually_ge_atTop c).mono fun x hx => bc.trans_le hx

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ limsup u atTop = ⨅ n, ⨆ i, u (i + n)

Tactic:
simp only [limsup_eq_iInf_iSup_of_nat, iSup_ge_eq_iSup_nat_add]

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

Goal state before:
pp: case neg
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ x, f.limsSup < x
hbot : ∃ x, x < f.limsSup
⊢ ClusterPt f.limsSup f

Tactic:
refine (nhds_basis_Ioo' hbot htop).clusterPt_iff_frequently |>.mpr fun a ⟨hl, hg⟩ => ?_

Goal state after:
case neg
α : Type u_2
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
f : Filter α
inst✝ : f.NeBot
hc : IsCobounded (fun x1 x2 ↦ x1 ≤ x2) f
hb : IsBounded (fun x1 x2 ↦ x1 ≤ x2) f
hn : Nontrivial α
htop : ∃ x, f.limsSup < x
hbot : ∃ x, x < f.limsSup
a : α × α
x✝ : a.1 < f.limsSup ∧ f.limsSup < a.2
hl : a.1 < f.limsSup
hg : f.limsSup < a.2
⊢ ∃ᶠ (x : α) in f, x ∈ Set.Ioo a.1 a.2
Module: Mathlib.Data.EReal.Operations

Goal state before:
pp: a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
⊢ -(a + b) ≤ -c

Tactic:
neg_add h₁ h₂

Goal state after:
a b c : EReal
h₁ : a ≠ ⊥ ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ ⊥
h : ∀ a' > a, ∀ b' > b, c ≤ a' + b'
⊢ -a - b ≤ -c
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
⊢ x ≤ limsup u f ↔ ∀ y < x, ∃ᶠ (a : α) in f, y < u a

Tactic:
refine ⟨fun h _ h' ↦ frequently_lt_of_lt_limsup h₁ (h'.trans_le h), fun h ↦ ?_⟩
  --Two cases: Either `x` is a cluster point from below, or it is not.
  --In the first case, we use `forall_lt_iff_le` and split an interval.
  --In the second case, the function `u` must frequently be larger or equal to `x`.
  by_cases h' : ∀ y < x, ∃ z, y < z ∧ z < x
  · rw [← forall_lt_iff_le]
    intro y y_x
    obtain ⟨z, y_z, z_x⟩ := h' y y_x
    exact y_z.trans_le (le_limsup_of_frequently_le ((h z z_x).mono (fun _ ↦ le_of_lt)) h₂)
  · apply le_limsup_of_frequently_le _ h₂
    push +distrib Not at h'
    rcases h' with ⟨z, z_x, hz⟩
    exact (h z z_x).mono <| fun w hw ↦ (or_iff_right (not_le_of_gt hw)).1 (hz (u w))

Goal state after:
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst✝ : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ x ≤ limsup u f ↔ ∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a

Tactic:
refine ⟨fun h _ h' ↦ (frequently_lt_of_lt_limsup h₁ (h'.trans_le h)).mono fun _ ↦ le_of_lt, ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
inst✝ : DenselyOrdered β
x : β
h₁ : IsCoboundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) f u
⊢ (∀ y < x, ∃ᶠ (a : α) in f, y ≤ u a) → x ≤ limsup u f
Module: Mathlib.Order.LiminfLimsup

Goal state before:
pp: case neg
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
j : Subtype p
hj : j ∉ m
⊢ ⋂ i, Iic (f ↑i) ⊆ ⋃ j, ⋂ i, Iic (f ↑i)

Tactic:
simp only [m, mem_ofPred_eq, ← nonempty_iInter_Iic_iff, not_nonempty_iff_eq_empty] at hj

Goal state after:
case neg
α : Type u_1
ι : Type u_4
ι' : Type u_5
inst✝² : ConditionallyCompleteLinearOrder α
v : Filter ι
p : ι' → Prop
s : ι' → Set ι
inst✝¹ : Countable (Subtype p)
inst✝ : Nonempty (Subtype p)
hv : v.HasBasis p s
f : ι → α
hs : ∀ (j : Subtype p), (s ↑j).Nonempty
j0 : Subtype p
hj0 : BddBelow (range fun i ↦ f ↑i)
m : Set (Subtype p) := {j | BddBelow (range fun i ↦ f ↑i)}
this : ∀ (j : Subtype p), Nonempty ↑(s ↑j)
j : Subtype p
hj : ⋂ i, Iic (f ↑i) = ∅
⊢ ⋂ i, Iic (f ↑i) ⊆ ⋃ j, ⋂ i, Iic (f ↑i)
Module: Mathlib.Topology.Algebra.InfiniteSum.SummationFilter

Goal state before:
pp: β : Type u_4
inst✝² : Finite β
L : SummationFilter β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
this : Fintype β
⊢ 𝓟 (Ici ⊤) = pure ⊤

Tactic:
Ici_top,

Goal state after:
β : Type u_4
inst✝² : Finite β
L : SummationFilter β
inst✝¹ : L.LeAtTop
inst✝ : L.NeBot
this : Fintype β
⊢ 𝓟 {⊤} = pure ⊤