harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Archimedean/IndicatorCard.lean
lemma limsup_eq_tendsto_sum_indicator_atTop {α R : Type*} [OrderedAddCommMonoid R]
    [AddLeftStrictMono R] [Archimedean R] {r : R} (h : 0 < r) (s : ℕ → Set α) :
    atTop.limsup s = { ω | atTop.Tendsto
      (fun n ↦ ∑ k ∈ Finset.range n, (s k).indicator (fun _ ↦ r) ω) atTop }

Proof state:
case h
α : Type u_1
R : Type u_2
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : ℕ → Set α
ω : α
⊢ Tendsto (fun n => ∑ k ∈ Finset.range n, {n | ω ∈ s n}.indicator (fun x => r) k) atTop atTop =
    Tendsto (fun n => ∑ k ∈ Finset.range n, (s k).indicator (fun x => r) ω) atTop atTop

Tactic:
congr

Result:
no goals

Proof state:
case h
α : Type u_1
R : Type u_2
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : ℕ → Set α
ω : α
⊢ ω ∈ {x | {n | x ∈ s n}.Infinite} ↔
    ω ∈ {ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (s k).indicator (fun x => r) ω) atTop atTop}

Tactic:
rw [mem_setOf_eq, mem_setOf_eq, infinite_iff_tendsto_sum_indicator_atTop h, iff_eq_eq]

Result:
case h
α : Type u_1
R : Type u_2
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : ℕ → Set α
ω : α
⊢ Tendsto (fun n => ∑ k ∈ Finset.range n, {n | ω ∈ s n}.indicator (fun x => r) k) atTop atTop =
    Tendsto (fun n => ∑ k ∈ Finset.range n, (s k).indicator (fun x => r) ω) atTop atTop

Proof state:
α : Type u_1
R : Type u_2
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : ℕ → Set α
⊢ {x | {n | x ∈ s n}.Infinite} =
    {ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (s k).indicator (fun x => r) ω) atTop atTop}

Tactic:
ext ω

Result:
case h
α : Type u_1
R : Type u_2
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : ℕ → Set α
ω : α
⊢ ω ∈ {x | {n | x ∈ s n}.Infinite} ↔
    ω ∈ {ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (s k).indicator (fun x => r) ω) atTop atTop}

Proof state:
α : Type u_1
R : Type u_2
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : ℕ → Set α
⊢ limsup s atTop = {ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (s k).indicator (fun x => r) ω) atTop atTop}

Tactic:
nth_rw 1 [← Nat.cofinite_eq_atTop, cofinite.limsup_set_eq]

Result:
α : Type u_1
R : Type u_2
inst✝² : OrderedAddCommMonoid R
inst✝¹ : AddLeftStrictMono R
inst✝ : Archimedean R
r : R
h : 0 < r
s : ℕ → Set α
⊢ {x | {n | x ∈ s n}.Infinite} =
    {ω | Tendsto (fun n => ∑ k ∈ Finset.range n, (s k).indicator (fun x => r) ω) atTop atTop}
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem limit.lift_pre (c : Cone F) :
    limit.lift F c ≫ limit.pre F E = limit.lift (E ⋙ F) (c.whisker E)

Proof state:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
c : Cone F
j✝ : K
⊢ (lift F c ≫ pre F E) ≫ π (E ⋙ F) j✝ = lift (E ⋙ F) (Cone.whisker E c) ≫ π (E ⋙ F) j✝

Tactic:
simp

Result:
no goals

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
c : Cone F
⊢ lift F c ≫ pre F E = lift (E ⋙ F) (Cone.whisker E c)

Tactic:
ext

Result:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J ⥤ C
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
c : Cone F
j✝ : K
⊢ (lift F c ≫ pre F E) ≫ π (E ⋙ F) j✝ = lift (E ⋙ F) (Cone.whisker E c) ≫ π (E ⋙ F) j✝
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem div_eq_zero_iff (hq0 : q ≠ 0) : p / q = 0 ↔ degree p < degree q :=
  ⟨fun h => by
    have := EuclideanDomain.div_add_mod p q
    rwa [h, mul_zero, zero_add, mod_eq_self_iff hq0] at this,
  fun h => by
    have hlt : degree p < degree (q * C (leadingCoeff q)⁻¹)

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
this : q * (p / q) + p % q = p
⊢ p.degree < q.degree

Tactic:
rwa [h, mul_zero, zero_add, mod_eq_self_iff hq0] at this

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
⊢ p.degree < (q * C q.leadingCoeff⁻¹).degree

Tactic:
rwa [degree_mul_leadingCoeff_inv q hq0]

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
hlt : p.degree < (q * C q.leadingCoeff⁻¹).degree
⊢ p / q = 0

Tactic:
have hm : Monic (q * C (leadingCoeff q)⁻¹) := monic_mul_leadingCoeff_inv hq0

Result:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
hlt : p.degree < (q * C q.leadingCoeff⁻¹).degree
hm : (q * C q.leadingCoeff⁻¹).Monic
⊢ p / q = 0

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
⊢ p.degree < q.degree

Tactic:
have := EuclideanDomain.div_add_mod p q

Result:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p / q = 0
this : q * (p / q) + p % q = p
⊢ p.degree < q.degree

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
hlt : p.degree < (q * C q.leadingCoeff⁻¹).degree
hm : (q * C q.leadingCoeff⁻¹).Monic
⊢ p / q = 0

Tactic:
rw [div_def, (divByMonic_eq_zero_iff hm).2 hlt, mul_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
⊢ p / q = 0

Tactic:
have hlt : degree p < degree (q * C (leadingCoeff q)⁻¹) := by
  rwa [degree_mul_leadingCoeff_inv q hq0]

Result:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
hlt : p.degree < (q * C q.leadingCoeff⁻¹).degree
⊢ p / q = 0
-- Mathlib/Order/CompleteLattice.lean
lemma Equiv.biSup_comp {ι ι' : Type*} {g : ι' → α} (e : ι ≃ ι') (s : Set ι') :
    ⨆ i ∈ e.symm '' s, g (e i) = ⨆ i ∈ s, g i

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
ι : Type u_8
ι' : Type u_9
g : ι' → α
e : ι ≃ ι'
s : Set ι'
⊢ ⨆ i ∈ ⇑e.symm '' s, g (e i) = ⨆ i ∈ s, g i

Tactic:
simpa only [iSup_subtype'] using (image e.symm s).symm.iSup_comp (g := g ∘ (↑))

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean
theorem IsSRGWith.top :
    (⊤ : SimpleGraph V).IsSRGWith (Fintype.card V) (Fintype.card V - 1) (Fintype.card V - 2) μ where
  card := rfl
  regular := IsRegularOfDegree.top
  of_adj := fun v w h => by
    rw [card_commonNeighbors_top]
    exact h
  of_not_adj := fun v w h h' => False.elim (h' ((top_adj v w).2 h))

Proof state:
V : Type u
inst✝¹ : Fintype V
μ : ℕ
inst✝ : DecidableEq V
v w : V
h : ⊤.Adj v w
⊢ v ≠ w

Tactic:
exact h

Result:
no goals

Proof state:
V : Type u
inst✝¹ : Fintype V
μ : ℕ
inst✝ : DecidableEq V
v w : V
h : ⊤.Adj v w
⊢ Fintype.card ↑(⊤.commonNeighbors v w) = Fintype.card V - 2

Tactic:
rw [card_commonNeighbors_top]

Result:
V : Type u
inst✝¹ : Fintype V
μ : ℕ
inst✝ : DecidableEq V
v w : V
h : ⊤.Adj v w
⊢ v ≠ w
-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem neZero [h : IsCyclotomicExtension {n} A B] [IsDomain B] : NeZero ((n : ℕ) : B)

Proof state:
case intro.intro
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
h : IsCyclotomicExtension {n} A B
inst✝ : IsDomain B
r : B
hr : IsPrimitiveRoot r ↑n
⊢ NeZero ↑↑n

Tactic:
exact hr.neZero'

Result:
no goals

Proof state:
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
h : IsCyclotomicExtension {n} A B
inst✝ : IsDomain B
⊢ NeZero ↑↑n

Tactic:
obtain ⟨⟨r, hr⟩, -⟩ := (iff_singleton n A B).1 h

Result:
case intro.intro
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
h : IsCyclotomicExtension {n} A B
inst✝ : IsDomain B
r : B
hr : IsPrimitiveRoot r ↑n
⊢ NeZero ↑↑n
-- Mathlib/Data/Set/Pointwise/SMul.lean
@[simp] lemma inv_smul_set_distrib₀ (a : α) (s : Set α) : (a • s)⁻¹ = op a⁻¹ • s⁻¹

Proof state:
case inr
α : Type u_2
inst✝ : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
⊢ (a • s)⁻¹ = op a⁻¹ • s⁻¹

Tactic:
ext

Result:
case inr.h
α : Type u_2
inst✝ : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
x✝ : α
⊢ x✝ ∈ (a • s)⁻¹ ↔ x✝ ∈ op a⁻¹ • s⁻¹

Proof state:
case inl
α : Type u_2
inst✝ : GroupWithZero α
s : Set α
⊢ (0 • s)⁻¹ = op 0⁻¹ • s⁻¹

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty <;> simp [*]

Result:
no goals

Proof state:
case inr.h
α : Type u_2
inst✝ : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
x✝ : α
⊢ x✝ ∈ (a • s)⁻¹ ↔ x✝ ∈ op a⁻¹ • s⁻¹

Tactic:
simp [mem_smul_set_iff_inv_smul_mem₀, *]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : GroupWithZero α
a : α
s : Set α
⊢ (a • s)⁻¹ = op a⁻¹ • s⁻¹

Tactic:
obtain rfl | ha := eq_or_ne a 0

Result:
case inl
α : Type u_2
inst✝ : GroupWithZero α
s : Set α
⊢ (0 • s)⁻¹ = op 0⁻¹ • s⁻¹

case inr
α : Type u_2
inst✝ : GroupWithZero α
a : α
s : Set α
ha : a ≠ 0
⊢ (a • s)⁻¹ = op a⁻¹ • s⁻¹
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.inner_right_sum {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι → 𝕜) {s : Finset ι}
    {i : ι} (hi : i ∈ s) : ⟪v i, ∑ i ∈ s, l i • v i⟫ = l i

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι → 𝕜
s : Finset ι
i : ι
hi : i ∈ s
⊢ inner (v i) (∑ i ∈ s, l i • v i) = l i

Tactic:
simp [inner_sum, inner_smul_right, orthonormal_iff_ite.mp hv, hi]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι → 𝕜
s : Finset ι
i : ι
hi : i ∈ s
⊢ inner (v i) (∑ i ∈ s, l i • v i) = l i

Tactic:
classical
simp [inner_sum, inner_smul_right, orthonormal_iff_ite.mp hv, hi]

Result:
no goals
-- Mathlib/Data/Nat/Factorial/SuperFactorial.lean
theorem prod_range_succ_factorial : ∀ n : ℕ, ∏ x ∈ range (n + 1), x ! = sf n
  | 0 => rfl
  | n + 1 => by
    rw [prod_range_succ, prod_range_succ_factorial n, mul_comm, superFactorial]

Proof state:
n : ℕ
⊢ ∏ x ∈ range (n + 1 + 1), x ! = sf n + 1

Tactic:
rw [prod_range_succ, prod_range_succ_factorial n, mul_comm, superFactorial]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Pow.lean
theorem HasDerivAt.pow (hc : HasDerivAt c c' x) :
    HasDerivAt (fun y => c y ^ n) ((n : 𝕜) * c x ^ (n - 1) * c') x

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
n : ℕ
hc : HasDerivWithinAt c c' Set.univ x
⊢ HasDerivWithinAt (fun y => c y ^ n) (↑n * c x ^ (n - 1) * c') Set.univ x

Tactic:
exact hc.pow n

Result:
no goals

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
n : ℕ
hc : HasDerivAt c c' x
⊢ HasDerivAt (fun y => c y ^ n) (↑n * c x ^ (n - 1) * c') x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Result:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
c : 𝕜 → 𝕜
c' : 𝕜
n : ℕ
hc : HasDerivWithinAt c c' Set.univ x
⊢ HasDerivWithinAt (fun y => c y ^ n) (↑n * c x ^ (n - 1) * c') Set.univ x
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma preimage_coe_Ioi (x : ℝ) : Real.toEReal ⁻¹' Ioi x = Ioi x

Proof state:
x : ℝ
⊢ WithBot.some ∘ WithTop.some ⁻¹' Ioi ↑↑x = Ioi x

Tactic:
refine preimage_comp.trans ?_

Result:
x : ℝ
⊢ WithTop.some ⁻¹' (WithBot.some ⁻¹' Ioi ↑↑x) = Ioi x

Proof state:
x : ℝ
⊢ Real.toEReal ⁻¹' Ioi ↑x = Ioi x

Tactic:
change (WithBot.some ∘ WithTop.some) ⁻¹' (Ioi (WithBot.some (WithTop.some x))) = _

Result:
x : ℝ
⊢ WithBot.some ∘ WithTop.some ⁻¹' Ioi ↑↑x = Ioi x

Proof state:
x : ℝ
⊢ WithTop.some ⁻¹' (WithBot.some ⁻¹' Ioi ↑↑x) = Ioi x

Tactic:
simp only [WithBot.preimage_coe_Ioi, WithTop.preimage_coe_Ioi]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem val_sub {n : ℕ} [NeZero n] {a b : ZMod n} (h : b.val ≤ a.val) :
    (a - b).val = a.val - b.val

Proof state:
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
⊢ (a - b).val = a.val - b.val

Tactic:
by_cases hb : b = 0

Result:
case pos
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : b = 0
⊢ (a - b).val = a.val - b.val

case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
⊢ (a - b).val = a.val - b.val

Proof state:
case pos.refl
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : val 0 ≤ a.val
⊢ (a - 0).val = a.val - val 0

Tactic:
simp

Result:
no goals

Proof state:
case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
⊢ (a - b).val = a.val - b.val

Tactic:
have : NeZero b := ⟨hb⟩

Result:
case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (a - b).val = a.val - b.val

Proof state:
case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (a.val - b.val) % n = a.val - b.val

Tactic:
apply Nat.mod_eq_of_lt (tsub_lt_of_lt (val_lt _))

Result:
no goals

Proof state:
case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (a - b).val = a.val - b.val

Tactic:
rw [sub_eq_add_neg, val_add, val_neg_of_ne_zero, ← Nat.add_sub_assoc (le_of_lt (val_lt _)),
  add_comm, Nat.add_sub_assoc h, Nat.add_mod_left]

Result:
case neg
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : ¬b = 0
this : NeZero b
⊢ (a.val - b.val) % n = a.val - b.val

Proof state:
case pos
n : ℕ
inst✝ : NeZero n
a b : ZMod n
h : b.val ≤ a.val
hb : b = 0
⊢ (a - b).val = a.val - b.val

Tactic:
cases hb

Result:
case pos.refl
n : ℕ
inst✝ : NeZero n
a : ZMod n
h : val 0 ≤ a.val
⊢ (a - 0).val = a.val - val 0
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem comap_bracket_incl_of_le {I₁ I₂ : LieIdeal R L} (h₁ : I₁ ≤ I) (h₂ : I₂ ≤ I) :
    ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I₁, I₂⁆

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I₁ ≤ I
h₂ : I₂ ≤ I
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I₁, I₂⁆

Tactic:
rw [comap_bracket_incl]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I₁ ≤ I
h₂ : I₂ ≤ I
⊢ comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I₁ ≤ I
h₂ : I₂ ≤ I
⊢ comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆

Tactic:
rw [← inf_eq_right] at h₁ h₂

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I ⊓ I₁ = I₁
h₂ : I ⊓ I₂ = I₂
⊢ comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
h₁ : I ⊓ I₁ = I₁
h₂ : I ⊓ I₂ = I₂
⊢ comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆ = comap I.incl ⁅I₁, I₂⁆

Tactic:
rw [h₁, h₂]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem inj_on_iUnion_of_directed {s : ι → Set α} (hs : Directed (· ⊆ ·) s) {f : α → β}
    (hf : ∀ i, InjOn f (s i)) : InjOn f (⋃ i, s i)

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ i, s i
y : α
hy✝ : y ∈ ⋃ i, s i
hxy : f x = f y
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
k : ι
hi : s i ⊆ s k
hj : s j ⊆ s k
⊢ x = y

Tactic:
exact hf k (hi hx) (hj hy) hxy

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ i, s i
y : α
hy✝ : y ∈ ⋃ i, s i
hxy : f x = f y
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
⊢ x = y

Tactic:
rcases hs i j with ⟨k, hi, hj⟩

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ i, s i
y : α
hy✝ : y ∈ ⋃ i, s i
hxy : f x = f y
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
k : ι
hi : s i ⊆ s k
hj : s j ⊆ s k
⊢ x = y

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx : x ∈ ⋃ i, s i
y : α
hy : y ∈ ⋃ i, s i
hxy : f x = f y
⊢ x = y

Tactic:
rcases mem_iUnion.1 hx with ⟨i, hx⟩

Result:
case intro
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ i, s i
y : α
hy : y ∈ ⋃ i, s i
hxy : f x = f y
i : ι
hx : x ∈ s i
⊢ x = y

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
⊢ InjOn f (⋃ i, s i)

Tactic:
intro x hx y hy hxy

Result:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx : x ∈ ⋃ i, s i
y : α
hy : y ∈ ⋃ i, s i
hxy : f x = f y
⊢ x = y

Proof state:
case intro
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ i, s i
y : α
hy : y ∈ ⋃ i, s i
hxy : f x = f y
i : ι
hx : x ∈ s i
⊢ x = y

Tactic:
rcases mem_iUnion.1 hy with ⟨j, hy⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun x1 x2 => x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx✝ : x ∈ ⋃ i, s i
y : α
hy✝ : y ∈ ⋃ i, s i
hxy : f x = f y
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
⊢ x = y
-- Mathlib/Data/ENat/Basic.lean
lemma toNat_le_of_le_coe {m : ℕ∞} {n : ℕ} (h : m ≤ n) : toNat m ≤ n

Proof state:
case intro
n m : ℕ
h : ↑m ≤ ↑n
⊢ (↑m).toNat ≤ n

Tactic:
simpa using h

Result:
no goals

Proof state:
m : ℕ∞
n : ℕ
h : m ≤ ↑n
⊢ m.toNat ≤ n

Tactic:
lift m to ℕ using ne_top_of_le_ne_top (coe_ne_top n) h

Result:
case intro
n m : ℕ
h : ↑m ≤ ↑n
⊢ (↑m).toNat ≤ n
-- Mathlib/MeasureTheory/Covering/Besicovitch.lean
theorem exist_disjoint_covering_families {N : ℕ} {τ : ℝ} (hτ : 1 < τ)
    (hN : IsEmpty (SatelliteConfig α N τ)) (q : BallPackage β α) :
    ∃ s : Fin N → Set β,
      (∀ i : Fin N, (s i).PairwiseDisjoint fun j => closedBall (q.c j) (q.r j)) ∧
        range q.c ⊆ ⋃ i : Fin N, ⋃ j ∈ s i, ball (q.c j) (q.r j)

Proof state:
case inr
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
⊢ ∃ s,
    (∀ (i : Fin N), (s i).PairwiseDisjoint fun j => closedBall (q.c j) (q.r j)) ∧
      range q.c ⊆ ⋃ i, ⋃ j ∈ s i, ball (q.c j) (q.r j)

Tactic:
let s := fun i : Fin N =>
  ⋃ (k : Ordinal.{u}) (_ : k < p.lastStep) (_ : p.color k = i), ({p.index k} : Set β)

Result:
case inr
α : Type u_1
inst✝ : MetricSpace α
β : Type u
N : ℕ
τ : ℝ
hτ : 1 < τ
hN : IsEmpty (SatelliteConfig α N τ)
q : BallPackage β α
h✝ : Nonempty β
p : TauPackage β α := { toBallPackage := q, τ := τ, one_lt_tau := hτ }
s : Fin N → Set β := fun i => ⋃ k, ⋃ (_ : k < p.lastStep), ⋃ (_ : p.color k = ↑i), {p.index k}
⊢ ∃ s,
    (∀ (i : Fin N), (s i).PairwiseDisjoint fun j => closedBall (q.c j) (q.r j)) ∧
      range q.c ⊆ ⋃ i, ⋃ j ∈ s i, ball (q.c j) (q.r j)
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem biproduct.map_matrix {f : J → C} {g : J → C} {h : K → C} (m : ∀ k, f k ⟶ g k)
    (n : ∀ j k, g j ⟶ h k) :
    biproduct.map m ≫ biproduct.matrix n = biproduct.matrix fun j k => m j ≫ n j k

Proof state:
case w.w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
J K : Type
inst✝² : Finite J
inst✝¹ : HasFiniteBiproducts C
inst✝ : Finite K
f g : J → C
h : K → C
m : (k : J) → f k ⟶ g k
n : (j : J) → (k : K) → g j ⟶ h k
j✝¹ : K
j✝ : J
⊢ ι f j✝ ≫ (map m ≫ matrix n) ≫ π h j✝¹ = ι f j✝ ≫ (matrix fun j k => m j ≫ n j k) ≫ π h j✝¹

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
J K : Type
inst✝² : Finite J
inst✝¹ : HasFiniteBiproducts C
inst✝ : Finite K
f g : J → C
h : K → C
m : (k : J) → f k ⟶ g k
n : (j : J) → (k : K) → g j ⟶ h k
⊢ map m ≫ matrix n = matrix fun j k => m j ≫ n j k

Tactic:
ext

Result:
case w.w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
J K : Type
inst✝² : Finite J
inst✝¹ : HasFiniteBiproducts C
inst✝ : Finite K
f g : J → C
h : K → C
m : (k : J) → f k ⟶ g k
n : (j : J) → (k : K) → g j ⟶ h k
j✝¹ : K
j✝ : J
⊢ ι f j✝ ≫ (map m ≫ matrix n) ≫ π h j✝¹ = ι f j✝ ≫ (matrix fun j k => m j ≫ n j k) ≫ π h j✝¹
-- Mathlib/RingTheory/RingHom/FiniteType.lean
theorem finiteType_ofLocalizationSpan : RingHom.OfLocalizationSpan @RingHom.FiniteType

Proof state:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), (Localization.awayMap f ↑r).FiniteType
this✝ : Algebra R S := f.toAlgebra
this : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r => (Localization.awayMap f ↑r).toAlgebra
⊢ ∀ (r : { x // x ∈ s }),
    IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))

Tactic:
intro r

Result:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), (Localization.awayMap f ↑r).FiniteType
this✝ : Algebra R S := f.toAlgebra
this : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r => (Localization.awayMap f ↑r).toAlgebra
r : { x // x ∈ s }
⊢ IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))

Proof state:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), (Localization.awayMap f ↑r).FiniteType
this : Algebra R S := f.toAlgebra
⊢ f.FiniteType

Tactic:
letI := fun r : s => (Localization.awayMap f r).toAlgebra

Result:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), (Localization.awayMap f ↑r).FiniteType
this✝ : Algebra R S := f.toAlgebra
this : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r => (Localization.awayMap f ↑r).toAlgebra
⊢ f.FiniteType

Proof state:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), (Localization.awayMap f ↑r).FiniteType
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r => (Localization.awayMap f ↑r).toAlgebra
this✝ :
  ∀ (r : { x // x ∈ s }),
    IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
⊢ f.FiniteType

Tactic:
constructor

Result:
case out
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Finset R
hs : Ideal.span ↑s = ⊤
H : ∀ (r : { x // x ∈ s }), (Localization.awayMap f ↑r).FiniteType
this✝² : Algebra R S := f.toAlgebra
this✝¹ : (r : { x // x ∈ s }) → Algebra (Localization.Away ↑r) (Localization.Away (f ↑r)) :=
  fun r => (Localization.awayMap f ↑r).toAlgebra
this✝ :
  ∀ (r : { x // x ∈ s }),
    IsLocalization (Submonoid.map (algebraMap R S) (Submonoid.powers ↑r)) (Localization.Away (f ↑r))
this : ∀ (r : { x // x ∈ s }), IsScalarTower R (Localization.Away ↑r) (Localization.Away (f ↑r))
⊢ ⊤.FG