mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case pos
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
m : ι
hm : P.root m = P.root ↑i + P.root ↑j
⊢ ((if ↑i = ↑i then ↑|b.cartanMatrix i j| else 0) -
      ∑ x,
        if P.root x = P.root ↑i + P.root ↑j ∧ P.root ↑i = P.root x - P.root ↑j then ↑(chainTopCoeff (↑j) x) + 1
        else 0) =
    0

Tactic:
rw [Finset.sum_eq_single_of_mem m (Finset.mem_univ _) (by rintro x - hx; simp [← hm, hx]),
        b.abs_cartanMatrix_apply, Base.cartanMatrix, Base.cartanMatrixIn_def]

Goal state after:
case pos
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Finite ι
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
inst✝⁶ : CharZero R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsCrystallographic
b : P.Base
inst✝ : Fintype ι
i j : ↥b.support
hij : i ≠ j
hij' : ↑i ≠ ↑j
this : InvolutiveNeg ι := P.indexNeg
m : ι
hm : P.root m = P.root ↑i + P.root ↑j
⊢ ((if ↑i = ↑i then ↑((if i = j then 4 else 0) - P.pairingIn ℤ ↑i ↑j) else 0) -
      if P.root m = P.root ↑i + P.root ↑j ∧ P.root ↑i = P.root m - P.root ↑j then ↑(chainTopCoeff (↑j) m) + 1 else 0) =
    0
Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular 2
x y : ↑{x | B.IsReflective x}
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 : ∀ (z : M), (IsReflective.coroot B ⋯) z = (IsReflective.coroot B ⋯) z
h2x : ∀ (z : M), 2 * (B ↑x) z = (B ↑x) ↑x * (IsReflective.coroot B ⋯) z
h2y : ∀ (z : M), (B ↑y) ↑y * (IsReflective.coroot B ⋯) z = 2 * (B ↑y) z
h2xy : (B ↑x) ↑x = (B ↑y) ↑y
⊢ ↑x - ↑y = 0

Tactic:
refine hNB.1 _ (fun z => ?_)

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular 2
x y : ↑{x | B.IsReflective x}
hxy : IsReflective.coroot B ⋯ = IsReflective.coroot B ⋯
h1 : ∀ (z : M), (IsReflective.coroot B ⋯) z = (IsReflective.coroot B ⋯) z
h2x : ∀ (z : M), 2 * (B ↑x) z = (B ↑x) ↑x * (IsReflective.coroot B ⋯) z
h2y : ∀ (z : M), (B ↑y) ↑y * (IsReflective.coroot B ⋯) z = 2 * (B ↑y) z
h2xy : (B ↑x) ↑x = (B ↑y) ↑y
z : M
⊢ (B (↑x - ↑y)) z = 0
Module: Mathlib.LinearAlgebra.SModEq.Pow

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
p : ℕ
hpI : ↑p ∈ I
x y : R
h : x ≡ y [SMOD I]
m : ℕ
⊢ x ^ p ^ m ≡ y ^ p ^ m [SMOD I ^ (m + 1)]

Tactic:
by
  induction m with
  | zero => simpa
  | succ m ih =>
    simp_rw [pow_succ _ m, pow_mul]
    exact ih.pow_add_one hpI m.succ_ne_zero

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case refine_2
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsCrystallographic
b : P.Base
⊢ span K (range u) ≤ ↑(genWeightSpace (↥b.support ⊕ ι → K) 0)

Tactic:
span_le

Goal state after:
case refine_2
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : Field K
inst✝⁷ : CharZero K
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
P : RootPairing ι K M N
inst✝ : P.IsCrystallographic
b : P.Base
⊢ range u ⊆ ↑↑(genWeightSpace (↥b.support ⊕ ι → K) 0)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : P.root k + P.root i - P.root j ∈ range ⇑P.root
this✝ : P.IsNotG2
this : InvolutiveNeg ι := P.indexNeg
him_mem : P.root i + P.root m ∈ range ⇑P.root
hik_mem : P.root k + P.root i ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
⊢ P.root j + P.root (-l) ∈ range ⇑P.root

Tactic:
rw [h₁, ← neg_mem_range_root_iff] at h₃

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
h₂ : P.root k - P.root j = P.root m
h₃ : -(P.root l - P.root j) ∈ range ⇑P.root
this✝ : P.IsNotG2
this : InvolutiveNeg ι := P.indexNeg
him_mem : P.root i + P.root m ∈ range ⇑P.root
hik_mem : P.root k + P.root i ∈ range ⇑P.root
hjk_mem : P.root j + P.root (-k) ∈ range ⇑P.root
⊢ P.root j + P.root (-l) ∈ range ⇑P.root
Module: Mathlib.LinearAlgebra.SymmetricAlgebra.Basis

Goal state before:
pp: R : Type uR
M : Type uM
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial M
inst✝ : Free R M
⊢ Module.rank R (SymmetricAlgebra R M) = Cardinal.lift.{uR, uM} (max (Module.rank R M) ℵ₀)

Tactic:
by
  let ⟨⟨κ, b⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
  have : Nonempty κ := Basis.index_nonempty b
  have : Nontrivial R := Module.nontrivial R M
  rw [(equivMvPolynomial b).toLinearEquiv.rank_eq, MvPolynomial.rank_eq_lift,
    Cardinal.mk_finsupp_nat, Basis.mk_eq_rank'' b]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Matrix

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_7
κ : Type u_8
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
bM : Basis ι R M
bN : Basis κ R N
⊢ (toMatrix (bM.tensorProduct bN) (bN.tensorProduct bM)) ↑(TensorProduct.comm R M N) = submatrix 1 Prod.swap _root_.id

Tactic:
by
  ext ⟨i, j⟩ ⟨i', j'⟩
  simp only [toMatrix_apply, Basis.tensorProduct_apply, LinearEquiv.coe_coe, comm_tmul,
    Basis.tensorProduct_repr_tmul_apply, Basis.repr_self, Finsupp.single_apply, @eq_comm _ i',
    @eq_comm _ j', smul_eq_mul, mul_ite, mul_one, mul_zero, ← ite_and, and_comm, submatrix_apply,
    Matrix.one_apply, Prod.swap_prod_mk, id_eq, Prod.mk.injEq]

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Projective

Goal state before:
pp: case inl
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : ↥J) → α ↑j)
I J : Finset ι
hP : IsProjectiveMeasureFamily P
S : Set ((i : ↥I) → α ↑i)
T : Set ((i : ↥J) → α ↑i)
hT : MeasurableSet T
h_eq : cylinder I S = cylinder J T
hJI : J ⊆ I
h : IsEmpty ((i : ι) → α i)
⊢ (P I) S = (P J) T

Tactic:
suffices ∀ I, P I univ = 0 by
      simp only [Measure.measure_univ_eq_zero] at this
      simp [this]
    simpa using eq_zero_of_isEmpty hP

Goal state after:
Module: Mathlib.MeasureTheory.Constructions.Cylinders

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
S T : Set ((i : ↥s) → α ↑i)
⊢ cylinder s S \ cylinder s T = cylinder s (S \ T)

Tactic:
by
  ext1 f; simp only [mem_sdiff, mem_cylinder]

Goal state after:
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: case insert
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
a✝ : s ∉ S
ih : ↑S ⊆ C → ∃ P, ↑P.parts ⊆ C
hsC : s ∈ C
hSC : ↑S ⊆ C
P : Finpartition (S.sup id)
hP : ↑P.parts ⊆ C
⊢ ∃ P, ↑P.parts ⊆ C

Tactic:
id

Goal state after:
case insert
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
S : Finset (Set α)
a✝ : s ∉ S
ih : ↑S ⊆ C → ∃ P, ↑P.parts ⊆ C
hsC : s ∈ C
hSC : ↑S ⊆ C
P : Finpartition (S.sup id)
hP : ↑P.parts ⊆ C
⊢ ∃ P, ↑P.parts ⊆ C
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑(hC.disjointOfDiff hs ht)
⊢ Disjoint (id t) (id u)

Tactic:
id

Goal state after:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff hs ht)).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑(hC.disjointOfDiff hs ht)
⊢ Disjoint t u
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI) ⊆ s \ ⋃₀ ↑I

Tactic:
hC.sdiff_sUnion_eq_sUnion_disjointOfDiffUnion hs hI

Goal state after:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI) ⊆ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI)
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑I
v : Set α
hv : v ∈ ↑(hC.disjointOfDiffUnion hs hI)
x✝ : u ≠ v
⊢ Disjoint (id u) (id v)

Tactic:
id

Goal state after:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
h_dis : (↑I).PairwiseDisjoint id
u : Set α
hu : u ∈ ↑I
v : Set α
hv : v ∈ ↑(hC.disjointOfDiffUnion hs hI)
x✝ : u ≠ v
⊢ Disjoint u v
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
| ⋃₀ ↑I ∪ s \ ⋃₀ ↑I

Tactic:
hC.sdiff_sUnion_eq_sUnion_disjointOfDiffUnion hs hI

Goal state after:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
| ⋃₀ ↑I ∪ ⋃₀ ↑(hC.disjointOfDiffUnion hs hI)
Module: Mathlib.MeasureTheory.SetSemiring

Goal state before:
pp: α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
hJ : ↑J ⊆ C
⊢ ⨆ i ∈ J, i = ⨆ a ∈ J, id a

Tactic:
id

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

Goal state before:
pp: case a.inl.coe.coe.refine_2.hs
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (⋂ z ∈ f, Ioi ↑z)

Tactic:
apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})

Goal state after:
case a.inl.coe.coe.refine_2.hs.hs
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ f.Finite

case a.inl.coe.coe.refine_2.hs.h
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ ∀ i ∈ f, IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Ioi ↑i)
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inl.coe.coe.refine_2.ht
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (⋂ z ∈ g, Iio ↑z)

Tactic:
apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})

Goal state after:
case a.inl.coe.coe.refine_2.ht.hs
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ g.Finite

case a.inl.coe.coe.refine_2.ht.h
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ ∀ i ∈ g, IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio ↑i)
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inr.coe.coe.refine_2.hs.hs
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (⋂ z ∈ f, Ioi ↑z)

Tactic:
apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})

Goal state after:
case a.inr.coe.coe.refine_2.hs.hs.hs
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
⊢ f.Finite

case a.inr.coe.coe.refine_2.hs.hs.h
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
⊢ ∀ i ∈ f, IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Ioi ↑i)
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case a.inr.coe.coe.refine_2.hs.ht
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
⊢ IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (⋂ z ∈ g, Iio ↑z)

Tactic:
apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})

Goal state after:
case a.inr.coe.coe.refine_2.hs.ht.hs
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
⊢ g.Finite

case a.inr.coe.coe.refine_2.hs.ht.h
ι : Type u_1
inst✝¹ : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst✝ : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := ⋯
d : Set (WithTop ι) := ⋯
basis : Set (Set ι) := ⋯
h_basis : IsTopologicalBasis basis
a b : ι
hb✝ : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : b ∈ (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
⊢ ∀ i ∈ g, IsOpen[generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio ↑i)
Module: Mathlib.MeasureTheory.Covering.LiminfLimsup

Goal state before:
pp: α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun i ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun i ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun i ↦ ⋃ j, ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬μ W = 0
d : α
hd' :
  ∀ {ι : Type ?u.192} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (fun j ↦ μ (W ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : ℕ → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
⊢ False

Tactic:
let C := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹

Goal state after:
α : Type u_1
inst✝⁵ : PseudoMetricSpace α
inst✝⁴ : SecondCountableTopology α
inst✝³ : MeasurableSpace α
inst✝² : BorelSpace α
μ : Measure α
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : IsUnifLocDoublingMeasure μ
p : ℕ → Prop
s : ℕ → Set α
hs : ∀ (i : ℕ), IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s i)
r₁ r₂ : ℕ → ℝ
hrp : 0 ≤ r₁
M : ℝ
hM : 0 < M
hM' : M < 1
Y₁ : ℕ → Set α := fun i ↦ cthickening (r₁ i) (s i)
Y₂ : ℕ → Set α := fun i ↦ cthickening (r₂ i) (s i)
Z : ℕ → Set α := fun i ↦ ⋃ j, ⋃ (_ : p j ∧ i ≤ j), Y₂ j
i : ℕ
W : Set α := blimsup Y₁ atTop p \ Z i
contra : ¬μ W = 0
d : α
hd' :
  ∀ {ι : Type ?u.192} {l : Filter ι} (w : ι → α) (δ : ι → ℝ),
    Tendsto δ l (𝓝[>] 0) →
      (∀ᶠ (j : ι) in l, d ∈ closedBall (w j) (2 * δ j)) →
        Tendsto (fun j ↦ μ (W ∩ closedBall (w j) (δ j)) / μ (closedBall (w j) (δ j))) l (𝓝 1)
hd : d ∈ blimsup Y₁ atTop p
f : ℕ → ℕ
hf₁ : ∀ (x : ℕ), p (f x)
hf₂ : ∀ (j : ℕ), j ≤ f j
hf₃ : Tendsto f atTop atTop
hr : Tendsto (r₁ ∘ f) atTop (𝓝[>] 0)
hMr : ∀ᶠ (j : ℕ) in atTop, M * r₁ (f j) ≤ r₂ (f j)
w : ℕ → α
hw : ∀ (j : ℕ), w j ∈ s (f j)
hw' : ∀ (j : ℕ), d ∈ closedBall (w j) (2 * r₁ (f j))
C : ℝ≥0 := IsUnifLocDoublingMeasure.scalingConstantOf μ M⁻¹
⊢ False
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
⊢ (range fun a ↦ ↑a).OrdConnected

Tactic:
WithTop.range_coe

Goal state after:
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
⊢ (Iio ⊤).OrdConnected
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
⊢ IsOpen[TopologicalSpace.instWithTopOfOrderTopology] (range some)

Tactic:
WithTop.range_coe

Goal state after:
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
⊢ IsOpen[TopologicalSpace.instWithTopOfOrderTopology] (Iio ⊤)
Module: Mathlib.Topology.Order.WithTop

Goal state before:
pp: case inr
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
α : Type u_2
f : Filter α
x : α → WithTop ι
h : Nonempty ι
⊢ (∀ i < ⊤, ∀ᶠ (x_1 : α) in f, x x_1 ∈ Ioi i) ↔ ∀ a ∈ range some, ∀ᶠ (a_2 : α) in f, a < x a_2

Tactic:
WithTop.range_coe

Goal state after:
case inr
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
α : Type u_2
f : Filter α
x : α → WithTop ι
h : Nonempty ι
⊢ (∀ i < ⊤, ∀ᶠ (x_1 : α) in f, x x_1 ∈ Ioi i) ↔ ∀ a ∈ Iio ⊤, ∀ᶠ (a_2 : α) in f, a < x a_2