harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem find?_iota_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
    (iota n).find? p = some i ↔ p i ∧ i ∈ iota n ∧ ∀ j, i < j → j ≤ n → !p j

Proof state:
case mpr.intro.intro.refine_1.right
n i : Nat
p : Nat → Bool
h✝ : p i = true
h : ∀ (j : Nat), i < j → j ≤ n → p j = false
i₁ : 1 ≤ i
i₂ : i < 1 + n
⊢ range' 1 (i - 1) = range' 1 (i - 1) ∧ range' i (n - i + 1) = range' (1 + (i - 1)) (n - (i - 1))

Tactic:
simp

Result:
case mpr.intro.intro.refine_1.right
n i : Nat
p : Nat → Bool
h✝ : p i = true
h : ∀ (j : Nat), i < j → j ≤ n → p j = false
i₁ : 1 ≤ i
i₂ : i < 1 + n
⊢ n - i + 1 = n - (i - 1) ∧ i = 1 + (i - 1)

Proof state:
case mp.intro.intro.intro.right.intro.intro.intro.intro.intro.a
n : Nat
p : Nat → Bool
k : Nat
h₁ : k ≤ n
h : p (1 + k) = true
h' : ∀ (a : Nat), a ∈ (range' (1 + k + 1) (n - k - 1)).reverse → p a = false
j : Nat
j₁ : 1 + k < j
j₂ : j ≤ n
⊢ 1 + k + 1 ≤ j ∧ j < 1 + k + 1 + (n - k - 1)

Tactic:
omega

Result:
no goals
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem card_ofPermHom_support :
    (ofPermHom a τ).support.card =
      ∑ c ∈ (τ : Perm g.cycleFactorsFinset).support,  c.val.support.card

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ ∀ x ∈ (↑τ).support, ∀ y ∈ (↑τ).support, x ≠ y → _root_.Disjoint (↑x).support (↑y).support

Tactic:
intro c _ d _ h

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
c : { x // x ∈ g.cycleFactorsFinset }
a✝¹ : c ∈ (↑τ).support
d : { x // x ∈ g.cycleFactorsFinset }
a✝ : d ∈ (↑τ).support
h : c ≠ d
⊢ _root_.Disjoint (↑c).support (↑d).support

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
c : { x // x ∈ g.cycleFactorsFinset }
a✝¹ : c ∈ (↑τ).support
d : { x // x ∈ g.cycleFactorsFinset }
a✝ : d ∈ (↑τ).support
h : c ≠ d
⊢ (↑c).Disjoint ↑d

Tactic:
apply g.cycleFactorsFinset_pairwise_disjoint c.prop d.prop (Subtype.coe_ne_coe.mpr h)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ (a.ofPermHom τ).support.card = ∑ c ∈ (↑τ).support, (↑c).support.card

Tactic:
rw [ofPermHom_support, Finset.card_biUnion]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
⊢ ∀ x ∈ (↑τ).support, ∀ y ∈ (↑τ).support, x ≠ y → _root_.Disjoint (↑x).support (↑y).support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
c : { x // x ∈ g.cycleFactorsFinset }
a✝¹ : c ∈ (↑τ).support
d : { x // x ∈ g.cycleFactorsFinset }
a✝ : d ∈ (↑τ).support
h : c ≠ d
⊢ _root_.Disjoint (↑c).support (↑d).support

Tactic:
apply Equiv.Perm.Disjoint.disjoint_support

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
c : { x // x ∈ g.cycleFactorsFinset }
a✝¹ : c ∈ (↑τ).support
d : { x // x ∈ g.cycleFactorsFinset }
a✝ : d ∈ (↑τ).support
h : c ≠ d
⊢ (↑c).Disjoint ↑d
-- Mathlib/CategoryTheory/ComposableArrows.lean
@[simp]
lemma map_zero_one' : map F f 0 ⟨0 + 1, by simp⟩ (by simp) = f := rfl

Proof state:
C : Type u_1
inst✝ : Category.{?u.86214, u_1} C
n m : ℕ
F G : ComposableArrows C n
X : C
f : X ⟶ F.left
⊢ 0 ≤ ⟨0 + 1, ⋯⟩

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{?u.86214, u_1} C
n m : ℕ
F G : ComposableArrows C n
X : C
f : X ⟶ F.left
⊢ 0 + 1 < n + 1 + 1

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem natDegree_cyclotomic (n : ℕ) (R : Type*) [Ring R] [Nontrivial R] :
    (cyclotomic n R).natDegree = Nat.totient n

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ (cyclotomic n R).natDegree = n.totient

Tactic:
rw [natDegree, degree_cyclotomic]

Result:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ WithBot.unbotD 0 ↑n.totient = n.totient

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ WithBot.unbotD 0 ↑n.totient = n.totient

Tactic:
norm_cast

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem add_sub_assoc {m k : Nat} (h : k ≤ m) (n : Nat) : n + m - k = n + (m - k)

Proof state:
case intro
m k : Nat
h : k ≤ m
n w✝ : Nat
h✝ : k + w✝ = m
⊢ n + m - k = n + (m - k)

Tactic:
rename_i l hl

Result:
case intro
m k : Nat
h : k ≤ m
n l : Nat
hl : k + l = m
⊢ n + m - k = n + (m - k)

Proof state:
case intro
m k : Nat
h : k ≤ m
n l : Nat
hl : k + l = m
⊢ n + m - k = n + (m - k)

Tactic:
rw [← hl, Nat.add_sub_cancel_left, Nat.add_comm k, ← Nat.add_assoc, Nat.add_sub_cancel]

Result:
no goals

Proof state:
m k : Nat
h : k ≤ m
n : Nat
⊢ n + m - k = n + (m - k)

Tactic:
cases Nat.le.dest h

Result:
case intro
m k : Nat
h : k ≤ m
n w✝ : Nat
h✝ : k + w✝ = m
⊢ n + m - k = n + (m - k)
-- Mathlib/Data/Set/Prod.lean
theorem prod_inter_prod : s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)

Proof state:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
⊢ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
x : α
y : β
⊢ (x, y) ∈ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ ↔ (x, y) ∈ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)

Proof state:
case h.mk
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
x : α
y : β
⊢ (x, y) ∈ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ ↔ (x, y) ∈ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)

Tactic:
simp [and_assoc, and_left_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem pmap_eq_map_attach {p : α → Prop} (f : ∀ a, p a → β) (l H) :
    pmap f l H = l.attach.map fun x => f x.1 (H _ x.2)

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
⊢ pmap f l H = map (fun x => f x.val ⋯) l.attach

Tactic:
rw [attach, attachWith, map_pmap]

Result:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
⊢ pmap f l H = pmap (fun a h => f ⟨a, h⟩.val ⋯) l ⋯

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
⊢ pmap f l H = pmap (fun a h => f ⟨a, h⟩.val ⋯) l ⋯

Tactic:
exact pmap_congr_left l fun _ _ _ _ => rfl

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem forall_eq_apply_imp_iff' {f : α → β} {p : β → Prop} :
    (∀ a b, b = f a → p b) ↔ ∀ a, p (f a)

Proof state:
α : Sort u_1
β : Sort u_2
f : α → β
p : β → Prop
⊢ (∀ (a : α) (b : β), b = f a → p b) ↔ ∀ (a : α), p (f a)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma isStableUnderBaseChange_iff_pullbacks_le :
    P.IsStableUnderBaseChange ↔ P.pullbacks ≤ P

Proof state:
case mpr.of_isPullback
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
⊢ ∀ {X Y Y' S : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X}, IsPullback f' g' g f → P g → P g'

Tactic:
intro _ _ _ _ _ _ _ _ h₁ h₂

Result:
case mpr.of_isPullback
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
X✝ Y✝ Y'✝ S✝ : C
f✝ : X✝ ⟶ S✝
g✝ : Y✝ ⟶ S✝
f'✝ : Y'✝ ⟶ Y✝
g'✝ : Y'✝ ⟶ X✝
h₁ : IsPullback f'✝ g'✝ g✝ f✝
h₂ : P g✝
⊢ P g'✝

Proof state:
case mpr.of_isPullback
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
X✝ Y✝ Y'✝ S✝ : C
f✝ : X✝ ⟶ S✝
g✝ : Y✝ ⟶ S✝
f'✝ : Y'✝ ⟶ Y✝
g'✝ : Y'✝ ⟶ X✝
h₁ : IsPullback f'✝ g'✝ g✝ f✝
h₂ : P g✝
⊢ P g'✝

Tactic:
exact h _ ⟨_, _, _, _, _, h₂, h₁⟩

Result:
no goals

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.IsStableUnderBaseChange → P.pullbacks ≤ P

Tactic:
intro h _ _ _ ⟨_, _, _, _, _, h₁, h₂⟩

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderBaseChange
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
w✝⁴ w✝³ : C
w✝² : w✝⁴ ⟶ w✝³
w✝¹ : X✝ ⟶ w✝⁴
w✝ : Y✝ ⟶ w✝³
h₁ : P w✝²
h₂ : IsPullback w✝¹ f✝ w✝² w✝
⊢ P f✝

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
⊢ P.IsStableUnderBaseChange

Tactic:
constructor

Result:
case mpr.of_isPullback
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
⊢ ∀ {X Y Y' S : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X}, IsPullback f' g' g f → P g → P g'

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.IsStableUnderBaseChange ↔ P.pullbacks ≤ P

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.IsStableUnderBaseChange → P.pullbacks ≤ P

case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.pullbacks ≤ P → P.IsStableUnderBaseChange

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.IsStableUnderBaseChange
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
w✝⁴ w✝³ : C
w✝² : w✝⁴ ⟶ w✝³
w✝¹ : X✝ ⟶ w✝⁴
w✝ : Y✝ ⟶ w✝³
h₁ : P w✝²
h₂ : IsPullback w✝¹ f✝ w✝² w✝
⊢ P f✝

Tactic:
exact of_isPullback h₂ h₁

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.pullbacks ≤ P → P.IsStableUnderBaseChange

Tactic:
intro h

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h : P.pullbacks ≤ P
⊢ P.IsStableUnderBaseChange
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean
/-- The power series expansion of `Complex.cosh`. -/
lemma hasSum_cosh (z : ℂ) : HasSum (fun n ↦ z ^ (2 * n) / ↑(2 * n)!) (cosh z)

Proof state:
z : ℂ
⊢ HasSum (fun n => z ^ (2 * n) / ↑(2 * n)!) (cosh z)

Tactic:
simpa [mul_assoc, cos_mul_I] using hasSum_cos' (z * I)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_mul_dvd_mul_gcd (k m n : Nat) : gcd k (m * n) ∣ gcd k m * gcd k n

Proof state:
k m n m' : Nat
hm' : m' ∣ m
n' : Nat
hn' : n' ∣ n
h : k.gcd (m * n) = m' * n'
⊢ m' * n' ∣ k.gcd m * k.gcd n

Tactic:
have h' : m' * n' ∣ k := h ▸ gcd_dvd_left ..

Result:
k m n m' : Nat
hm' : m' ∣ m
n' : Nat
hn' : n' ∣ n
h : k.gcd (m * n) = m' * n'
h' : m' * n' ∣ k
⊢ m' * n' ∣ k.gcd m * k.gcd n

Proof state:
k m n m' : Nat
hm' : m' ∣ m
n' : Nat
hn' : n' ∣ n
h : k.gcd (m * n) = m' * n'
⊢ k.gcd (m * n) ∣ k.gcd m * k.gcd n

Tactic:
rw [h]

Result:
k m n m' : Nat
hm' : m' ∣ m
n' : Nat
hn' : n' ∣ n
h : k.gcd (m * n) = m' * n'
⊢ m' * n' ∣ k.gcd m * k.gcd n

Proof state:
k m n m' : Nat
hm' : m' ∣ m
n' : Nat
hn' : n' ∣ n
h : k.gcd (m * n) = m' * n'
h' : m' * n' ∣ k
⊢ m' * n' ∣ k.gcd m * k.gcd n

Tactic:
exact Nat.mul_dvd_mul
  (dvd_gcd (Nat.dvd_trans (Nat.dvd_mul_right m' n') h') hm')
  (dvd_gcd (Nat.dvd_trans (Nat.dvd_mul_left n' m') h') hn')

Result:
no goals

Proof state:
k m n : Nat
⊢ k.gcd (m * n) ∣ k.gcd m * k.gcd n

Tactic:
let ⟨⟨⟨m', hm'⟩, ⟨n', hn'⟩⟩, (h : gcd k (m * n) = m' * n')⟩ :=
  prod_dvd_and_dvd_of_dvd_prod <| gcd_dvd_right k (m * n)

Result:
k m n m' : Nat
hm' : m' ∣ m
n' : Nat
hn' : n' ∣ n
h : k.gcd (m * n) = m' * n'
⊢ k.gcd (m * n) ∣ k.gcd m * k.gcd n
-- Mathlib/NumberTheory/Divisors.lean
theorem map_div_right_divisors :
    n.divisors.map ⟨fun d => (d, n / d), fun _ _ => congr_arg Prod.fst⟩ =
      n.divisorsAntidiagonal

Proof state:
case h.mk.mp
n d nd : ℕ
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd → d * nd = n ∧ n ≠ 0

Tactic:
rintro ⟨⟨⟨k, rfl⟩, hn⟩, rfl⟩

Result:
case h.mk.mp.intro.intro.intro
d k : ℕ
hn : d * k ≠ 0
⊢ d * (d * k / d) = d * k ∧ d * k ≠ 0

Proof state:
case h.mk.mp.intro.intro.intro
d k : ℕ
hn : d * k ≠ 0
⊢ d * k = d * k ∧ d * k ≠ 0

Tactic:
exact ⟨rfl, hn⟩

Result:
no goals

Proof state:
case h.mk
n d nd : ℕ
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd ↔ d * nd = n ∧ n ≠ 0

Tactic:
constructor

Result:
case h.mk.mp
n d nd : ℕ
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd → d * nd = n ∧ n ≠ 0

case h.mk.mpr
n d nd : ℕ
⊢ d * nd = n ∧ n ≠ 0 → (d ∣ n ∧ n ≠ 0) ∧ n / d = nd

Proof state:
n : ℕ
⊢ map { toFun := fun d => (d, n / d), inj' := ⋯ } n.divisors = n.divisorsAntidiagonal

Tactic:
ext ⟨d, nd⟩

Result:
case h.mk
n d nd : ℕ
⊢ (d, nd) ∈ map { toFun := fun d => (d, n / d), inj' := ⋯ } n.divisors ↔ (d, nd) ∈ n.divisorsAntidiagonal

Proof state:
case h.mk.mpr.intro
d nd : ℕ
hn : d * nd ≠ 0
⊢ (d ∣ d * nd ∧ d * nd ≠ 0) ∧ d * nd / d = nd

Tactic:
exact ⟨⟨dvd_mul_right _ _, hn⟩, Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt⟩

Result:
no goals

Proof state:
case h.mk
n d nd : ℕ
⊢ (d, nd) ∈ map { toFun := fun d => (d, n / d), inj' := ⋯ } n.divisors ↔ (d, nd) ∈ n.divisorsAntidiagonal

Tactic:
simp only [mem_map, mem_divisorsAntidiagonal, Function.Embedding.coeFn_mk, mem_divisors,
  Prod.ext_iff, exists_prop, and_left_comm, exists_eq_left]

Result:
case h.mk
n d nd : ℕ
⊢ (d ∣ n ∧ n ≠ 0) ∧ n / d = nd ↔ d * nd = n ∧ n ≠ 0

Proof state:
case h.mk.mpr
n d nd : ℕ
⊢ d * nd = n ∧ n ≠ 0 → (d ∣ n ∧ n ≠ 0) ∧ n / d = nd

Tactic:
rintro ⟨rfl, hn⟩

Result:
case h.mk.mpr.intro
d nd : ℕ
hn : d * nd ≠ 0
⊢ (d ∣ d * nd ∧ d * nd ≠ 0) ∧ d * nd / d = nd

Proof state:
case h.mk.mp.intro.intro.intro
d k : ℕ
hn : d * k ≠ 0
⊢ d * (d * k / d) = d * k ∧ d * k ≠ 0

Tactic:
rw [Nat.mul_div_cancel_left _ (left_ne_zero_of_mul hn).bot_lt]

Result:
case h.mk.mp.intro.intro.intro
d k : ℕ
hn : d * k ≠ 0
⊢ d * k = d * k ∧ d * k ≠ 0
-- Mathlib/Topology/MetricSpace/CantorScheme.lean
theorem ClosureAntitone.map_of_vanishingDiam [CompleteSpace α] (hdiam : VanishingDiam A)
    (hanti : ClosureAntitone A) (hnonempty : ∀ l, (A l).Nonempty) : (inducedMap A).1 = univ

Proof state:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
⊢ x ∈ (inducedMap A).fst

Tactic:
obtain ⟨y, hy⟩ := cauchySeq_tendsto_of_complete this

Result:
case intro
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
⊢ x ∈ (inducedMap A).fst

Proof state:
case h
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
n : ℕ
⊢ y ∈ A (res x n)

Tactic:
apply hanti _ (x n)

Result:
case h.a
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
umem : ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
this : CauchySeq u
y : α
hy : Tendsto u atTop (𝓝 y)
n : ℕ
⊢ y ∈ closure (A (x n :: res x n))

Proof state:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
n : ℕ
⊢ A (res x (n + 1)) ≤ A (res x n)

Tactic:
apply hanti.antitone

Result:
no goals

Proof state:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
⊢ ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)

Tactic:
have : Antitone fun n : ℕ => A (res x n) := by
  refine antitone_nat_of_succ_le ?_
  intro n
  apply hanti.antitone

Result:
β : Type u_1
α : Type u_2
A : List β → Set α
inst✝¹ : PseudoMetricSpace α
inst✝ : CompleteSpace α
hdiam : VanishingDiam A
hanti : ClosureAntitone A
hnonempty : ∀ (l : List β), (A l).Nonempty
x : ℕ → β
u : ℕ → α
hu : ∀ (n : ℕ), u n ∈ A (res x n)
this : Antitone fun n => A (res x n)
⊢ ∀ (n m : ℕ), n ≤ m → u m ∈ A (res x n)
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem addHaar_parallelepiped (b : Basis ι ℝ G) (v : ι → G) :
    b.addHaar (parallelepiped v) = ENNReal.ofReal |b.det v|

Proof state:
ι : Type u_2
G : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
⊢ b.addHaar (parallelepiped v) = ENNReal.ofReal |b.det v|

Tactic:
have A : parallelepiped v = b.constr ℕ v '' parallelepiped b := by
  rw [image_parallelepiped]
  exact congr_arg _ <| funext fun i ↦ (b.constr_basis ℕ v i).symm

Result:
ι : Type u_2
G : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A : parallelepiped v = ⇑((b.constr ℕ) v) '' parallelepiped ⇑b
⊢ b.addHaar (parallelepiped v) = ENNReal.ofReal |b.det v|

Proof state:
ι : Type u_2
G : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
A : parallelepiped v = ⇑((b.constr ℕ) v) '' parallelepiped ⇑b
⊢ b.addHaar (parallelepiped v) = ENNReal.ofReal |b.det v|

Tactic:
rw [A, addHaar_image_linearMap, b.addHaar_self, mul_one, ← LinearMap.det_toMatrix b,
  ← Basis.toMatrix_eq_toMatrix_constr, Basis.det_apply]

Result:
no goals

Proof state:
ι : Type u_2
G : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
⊢ parallelepiped v = ⇑((b.constr ℕ) v) '' parallelepiped ⇑b

Tactic:
rw [image_parallelepiped]

Result:
ι : Type u_2
G : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
⊢ parallelepiped v = parallelepiped (⇑((b.constr ℕ) v) ∘ ⇑b)

Proof state:
ι : Type u_2
G : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
⊢ b.addHaar (parallelepiped v) = ENNReal.ofReal |b.det v|

Tactic:
have : FiniteDimensional ℝ G := FiniteDimensional.of_fintype_basis b

Result:
ι : Type u_2
G : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
⊢ b.addHaar (parallelepiped v) = ENNReal.ofReal |b.det v|

Proof state:
ι : Type u_2
G : Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
b : Basis ι ℝ G
v : ι → G
this : FiniteDimensional ℝ G
⊢ parallelepiped v = parallelepiped (⇑((b.constr ℕ) v) ∘ ⇑b)

Tactic:
exact congr_arg _ <| funext fun i ↦ (b.constr_basis ℕ v i).symm

Result:
no goals
-- Mathlib/Order/SupClosed.lean
lemma SupClosed.biSup_mem_of_nonempty {ι : Type*} {t : Set ι} {f : ι → α} (hs : SupClosed s)
    (ht : t.Finite) (ht' : t.Nonempty) (hf : ∀ i ∈ t, f i ∈ s) : ⨆ i ∈ t, f i ∈ s

Proof state:
α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hf : ∀ i ∈ t, f i ∈ s
⊢ f '' t ⊆ s

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hf : ∀ i ∈ t, f i ∈ s
⊢ (f '' t).Nonempty

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hf : ∀ i ∈ t, f i ∈ s
⊢ ⨆ i ∈ t, f i ∈ s

Tactic:
rw [← sSup_image]

Result:
α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hf : ∀ i ∈ t, f i ∈ s
⊢ sSup (f '' t) ∈ s

Proof state:
α : Type u_3
inst✝ : CompleteLattice α
s : Set α
ι : Type u_5
t : Set ι
f : ι → α
hs : SupClosed s
ht : t.Finite
ht' : t.Nonempty
hf : ∀ i ∈ t, f i ∈ s
⊢ sSup (f '' t) ∈ s

Tactic:
exact hs.sSup_mem_of_nonempty (ht.image _) (by simpa) (by simpa)

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Card.lean
theorem cardinal_generateMeasurableRec_le (s : Set (Set α)) (i : Ordinal.{v}) :
    #(generateMeasurableRec s i) ≤ max #s 2 ^ ℵ₀

Proof state:
case h1.h1.h2
α : Type u
s : Set (Set α)
i✝¹ i✝ i : Ordinal.{v}
IH : ∀ y < i, y ≤ ω_ 1 → #↑(generateMeasurableRec s y) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : i ≤ ω_ 1
A : 𝔠 ≤ (#↑s ⊔ 2) ^ ℵ₀
B : ℵ₀ ≤ (#↑s ⊔ 2) ^ ℵ₀
C : #↑(⋃ j, ⋃ (_ : j < i), generateMeasurableRec s j) ≤ (#↑s ⊔ 2) ^ ℵ₀
⊢ 1 ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
exact one_lt_aleph0.le.trans B

Result:
no goals

Proof state:
case inr
α : Type u
s : Set (Set α)
i : Ordinal.{v}
this : ∀ i ≤ ω_ 1, #↑(generateMeasurableRec s i) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : ω_ 1 < i
⊢ #↑(generateMeasurableRec s i) ≤ (#↑s ⊔ 2) ^ ℵ₀

Tactic:
rw [generateMeasurableRec_of_omega1_le s hi.le]

Result:
case inr
α : Type u
s : Set (Set α)
i : Ordinal.{v}
this : ∀ i ≤ ω_ 1, #↑(generateMeasurableRec s i) ≤ (#↑s ⊔ 2) ^ ℵ₀
hi : ω_ 1 < i
⊢ #↑(generateMeasurableRec s (ω_ 1)) ≤ (#↑s ⊔ 2) ^ ℵ₀