harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem cons_isTrail_iff {u v w : V} (h : G.Adj u v) (p : G.Walk v w) :
    (cons h p).IsTrail ↔ p.IsTrail ∧ s(u, v) ∉ p.edges

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).IsTrail ↔ p.IsTrail ∧ s(u, v) ∉ p.edges

Tactic:
simp [isTrail_def, and_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
@[reassoc]
lemma pullback.map_comp {X Y Z X' Y' Z' X'' Y'' Z'' : C}
    {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'} {f'' : X'' ⟶ Z''} {g'' : Y'' ⟶ Z''}
    (i₁ : X ⟶ X') (j₁ : X' ⟶ X'') (i₂ : Y ⟶ Y') (j₂ : Y' ⟶ Y'') (i₃ : Z ⟶ Z') (j₃ : Z' ⟶ Z'')
    [HasPullback f g] [HasPullback f' g'] [HasPullback f'' g'']
    (e₁ e₂ e₃ e₄) :
    pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂ ≫ pullback.map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄ =
      pullback.map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃)
        (by rw [reassoc_of% e₁, e₃, Category.assoc])
        (by rw [reassoc_of% e₂, e₄, Category.assoc])

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPullback f g
inst✝¹ : HasPullback f' g'
inst✝ : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
⊢ map f g f' g' i₁ i₂ i₃ e₁ e₂ ≫ map f' g' f'' g'' j₁ j₂ j₃ e₃ e₄ = map f g f'' g'' (i₁ ≫ j₁) (i₂ ≫ j₂) (i₃ ≫ j₃) ⋯ ⋯

Tactic:
ext <;> simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPullback f g
inst✝¹ : HasPullback f' g'
inst✝ : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
⊢ f ≫ i₃ ≫ j₃ = (i₁ ≫ j₁) ≫ f''

Tactic:
rw [reassoc_of% e₁, e₃, Category.assoc]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W X✝ Y✝ Z✝ X Y Z X' Y' Z' X'' Y'' Z'' : C
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f'' : X'' ⟶ Z''
g'' : Y'' ⟶ Z''
i₁ : X ⟶ X'
j₁ : X' ⟶ X''
i₂ : Y ⟶ Y'
j₂ : Y' ⟶ Y''
i₃ : Z ⟶ Z'
j₃ : Z' ⟶ Z''
inst✝² : HasPullback f g
inst✝¹ : HasPullback f' g'
inst✝ : HasPullback f'' g''
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
e₃ : f' ≫ j₃ = j₁ ≫ f''
e₄ : g' ≫ j₃ = j₂ ≫ g''
⊢ g ≫ i₃ ≫ j₃ = (i₂ ≫ j₂) ≫ g''

Tactic:
rw [reassoc_of% e₂, e₄, Category.assoc]

Result:
no goals
-- Mathlib/Dynamics/Flow.lean
theorem isInvariant_iff_image_eq (s : Set α) : IsInvariant ϕ s ↔ ∀ t, ϕ t '' s = s :=
  (isInvariant_iff_image _ _).trans
    (Iff.intro
      (fun h t => Subset.antisymm (h t) fun _ hx => ⟨_, h (-t) ⟨_, hx, rfl⟩, by simp [← map_add]⟩)
      fun h t => by rw [h t])

Proof state:
τ : Type u_1
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : IsTopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
s : Set α
h : ∀ (t : τ), ϕ.toFun t '' s = s
t : τ
⊢ ϕ.toFun t '' s ⊆ s

Tactic:
rw [h t]

Result:
no goals

Proof state:
τ : Type u_1
inst✝³ : AddCommGroup τ
inst✝² : TopologicalSpace τ
inst✝¹ : IsTopologicalAddGroup τ
α : Type u_2
inst✝ : TopologicalSpace α
ϕ : Flow τ α
s : Set α
h : ∀ (t : τ), ϕ.toFun t '' s ⊆ s
t : τ
x✝ : α
hx : x✝ ∈ s
⊢ ϕ.toFun t (ϕ.toFun (-t) x✝) = x✝

Tactic:
simp [← map_add]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem LinearIndepOn.union_of_quotient {M' : Submodule R M}
    {s : Set M} (hs : s ⊆ M') (hs' : LinearIndepOn R id s) {t : Set M}
    (ht : LinearIndepOn R (Submodule.Quotient.mk (p := M')) t) : LinearIndepOn R id (s ∪ t) :=
  have h := (LinearIndependent.sumElim_of_quotient (f := Set.embeddingOfSubset s M' hs)
    (LinearIndependent.of_comp M'.subtype (by simpa using hs')) Subtype.val ht)
  h.linearIndepOn_id' <| by
    simp only [embeddingOfSubset_apply_coe, Sum.elim_range, Subtype.range_val]

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
s : Set M
hs : s ⊆ ↑M'
hs' : LinearIndepOn R id s
t : Set M
ht : LinearIndepOn R Submodule.Quotient.mk t
h : LinearIndependent R (Sum.elim (fun x => ↑((s.embeddingOfSubset (↑M') hs) x)) Subtype.val)
⊢ range (Sum.elim (fun x => ↑((s.embeddingOfSubset (↑M') hs) x)) Subtype.val) = s ∪ t

Tactic:
simp only [embeddingOfSubset_apply_coe, Sum.elim_range, Subtype.range_val]

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
M' : Submodule R M
s : Set M
hs : s ⊆ ↑M'
hs' : LinearIndepOn R id s
t : Set M
ht : LinearIndepOn R Submodule.Quotient.mk t
⊢ LinearIndependent (ι := ↑s) R (⇑M'.subtype ∘ ⇑(s.embeddingOfSubset (↑M') hs))

Tactic:
simpa using hs'

Result:
no goals
-- Mathlib/Computability/DFA.lean
theorem comap_reindex (f : α' → α) (g : σ ≃ σ') :
    (reindex g M).comap f = reindex g (M.comap f)

Proof state:
α : Type u
σ : Type v
M : DFA α σ
α' : Type u_1
σ' : Type u_2
f : α' → α
g : σ ≃ σ'
⊢ comap f ((reindex g) M) = (reindex g) (comap f M)

Tactic:
simp [comap, reindex]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Field.lean
lemma cast_div_div_div_cancel_right (hn : d ∣ n) (hm : d ∣ m) :
    (↑(m / d) : K) / (↑(n / d) : K) = (m : K) / n

Proof state:
case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n

Tactic:
replace hd : (d : K) ≠ 0 := by norm_cast

Result:
case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n

Proof state:
case inl
K : Type u_1
inst✝¹ : DivisionSemiring K
m n : ℕ
inst✝ : CharZero K
hn : 0 ∣ n
hm : 0 ∣ m
⊢ ↑(m / 0) / ↑(n / 0) = ↑m / ↑n

Tactic:
simp [Nat.zero_dvd.1 hm]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
⊢ ↑d ≠ 0

Tactic:
norm_cast

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n

Tactic:
rcases eq_or_ne d 0 with (rfl | hd)

Result:
case inl
K : Type u_1
inst✝¹ : DivisionSemiring K
m n : ℕ
inst✝ : CharZero K
hn : 0 ∣ n
hm : 0 ∣ m
⊢ ↑(m / 0) / ↑(n / 0) = ↑m / ↑n

case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : d ≠ 0
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n

Proof state:
case inr
K : Type u_1
inst✝¹ : DivisionSemiring K
d m n : ℕ
inst✝ : CharZero K
hn : d ∣ n
hm : d ∣ m
hd : ↑d ≠ 0
⊢ ↑(m / d) / ↑(n / d) = ↑m / ↑n

Tactic:
rw [cast_div hm, cast_div hn, div_div_div_cancel_right₀ hd] <;> exact hd

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.eq [AddZeroClass α] (h : Periodic f c) : f c = f 0

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddZeroClass α
h : Periodic f c
⊢ f c = f 0

Tactic:
simpa only [zero_add] using h 0

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem AECover.integral_tendsto_of_countably_generated [l.IsCountablyGenerated] {φ : ι → Set α}
    (hφ : AECover μ l φ) {f : α → E} (hfi : Integrable f μ) :
    Tendsto (fun i => ∫ x in φ i, f x ∂μ) l (𝓝 <| ∫ x, f x ∂μ) :=
  suffices h : Tendsto (fun i => ∫ x : α, (φ i).indicator f x ∂μ) l (𝓝 (∫ x : α, f x ∂μ)) from by
    convert h using 2; rw [integral_indicator (hφ.measurableSet _)]
  tendsto_integral_filter_of_dominated_convergence (fun x => ‖f x‖)
    (Eventually.of_forall fun i => hfi.aestronglyMeasurable.indicator <| hφ.measurableSet i)
    (Eventually.of_forall fun _ => ae_of_all _ fun _ => norm_indicator_le_norm_self _ _) hfi.norm
    (hφ.ae_tendsto_indicator f)

Proof state:
case h.e'_3.h
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
hfi : Integrable f μ
h : Tendsto (fun i => ∫ (x : α), (φ i).indicator f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
x✝ : ι
⊢ ∫ (x : α) in φ x✝, f x ∂μ = ∫ (x : α), (φ x✝).indicator f x ∂μ

Tactic:
rw [integral_indicator (hφ.measurableSet _)]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
hfi : Integrable f μ
h : Tendsto (fun i => ∫ (x : α), (φ i).indicator f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
⊢ Tendsto (fun i => ∫ (x : α) in φ i, f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
convert h using 2

Result:
case h.e'_3.h
α : Type u_1
ι : Type u_2
E : Type u_3
inst✝³ : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : l.IsCountablyGenerated
φ : ι → Set α
hφ : AECover μ l φ
f : α → E
hfi : Integrable f μ
h : Tendsto (fun i => ∫ (x : α), (φ i).indicator f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
x✝ : ι
⊢ ∫ (x : α) in φ x✝, f x ∂μ = ∫ (x : α), (φ x✝).indicator f x ∂μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem attach_cons {x : α} {xs : List α} :
    (x :: xs).attach =
      ⟨x, mem_cons_self x xs⟩ :: xs.attach.map fun ⟨y, h⟩ => ⟨y, mem_cons_of_mem x h⟩

Proof state:
α : Type u_1
x : α
xs : List α
⊢ (x :: xs).attach =
    ⟨x, ⋯⟩ ::
      map
        (fun x_1 =>
          match x_1 with
          | ⟨y, h⟩ => ⟨y, ⋯⟩)
        xs.attach

Tactic:
simp only [attach, attachWith, pmap, map_pmap, cons.injEq, true_and]

Result:
α : Type u_1
x : α
xs : List α
⊢ pmap Subtype.mk xs ⋯ = pmap (fun a h => ⟨a, ⋯⟩) xs ⋯

Proof state:
case h
α : Type u_1
x : α
xs : List α
⊢ ∀ (a : α), a ∈ xs → ∀ (h₁ : a ∈ x :: xs) (h₂ : a ∈ xs), ⟨a, h₁⟩ = ⟨a, ⋯⟩

Tactic:
intros a _ m' _

Result:
case h
α : Type u_1
x : α
xs : List α
a : α
a✝ : a ∈ xs
m' : a ∈ x :: xs
h₂✝ : a ∈ xs
⊢ ⟨a, m'⟩ = ⟨a, ⋯⟩

Proof state:
α : Type u_1
x : α
xs : List α
⊢ pmap Subtype.mk xs ⋯ = pmap (fun a h => ⟨a, ⋯⟩) xs ⋯

Tactic:
apply pmap_congr_left

Result:
case h
α : Type u_1
x : α
xs : List α
⊢ ∀ (a : α), a ∈ xs → ∀ (h₁ : a ∈ x :: xs) (h₂ : a ∈ xs), ⟨a, h₁⟩ = ⟨a, ⋯⟩

Proof state:
case h
α : Type u_1
x : α
xs : List α
a : α
a✝ : a ∈ xs
m' : a ∈ x :: xs
h₂✝ : a ∈ xs
⊢ ⟨a, m'⟩ = ⟨a, ⋯⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem readyForRatAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))) :
    ReadyForRatAdd (ofArray arr)

Proof state:
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).ReadyForRatAdd

Tactic:
constructor

Result:
case left
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).ratUnits = #[]

case right
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).ReadyForRupAdd

Proof state:
case left
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).ratUnits = #[]

Tactic:
simp only [ofArray]

Result:
no goals

Proof state:
case right
n : Nat
arr : Array (Option (DefaultClause n))
⊢ (ofArray arr).ReadyForRupAdd

Tactic:
exact readyForRupAdd_ofArray arr

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_eq_two_iff : #α = 2 ↔ ∃ x y : α, x ≠ y ∧ ({x, y} : Set α) = univ

Proof state:
α : Type u
x y : α
hne : x ≠ y
h : {x, y} = univ
⊢ ↑{x, y} = univ

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u
⊢ (∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}) ↔ ∃ x y, x ≠ y ∧ {x, y} = univ

Tactic:
constructor

Result:
case mp
α : Type u
⊢ (∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}) → ∃ x y, x ≠ y ∧ {x, y} = univ

case mpr
α : Type u
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}

Proof state:
case mpr.intro.intro.intro
α : Type u
x y : α
hne : x ≠ y
h : {x, y} = univ
⊢ ∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}

Tactic:
exact ⟨{x, y}, by simpa using h, x, y, hne, rfl⟩

Result:
no goals

Proof state:
case mp
α : Type u
⊢ (∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}) → ∃ x y, x ≠ y ∧ {x, y} = univ

Tactic:
rintro ⟨t, ht, x, y, hne, rfl⟩

Result:
case mp.intro.intro.intro.intro.intro
α : Type u
x y : α
hne : x ≠ y
ht : ↑{x, y} = univ
⊢ ∃ x y, x ≠ y ∧ {x, y} = univ

Proof state:
case mpr
α : Type u
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}

Tactic:
rintro ⟨x, y, hne, h⟩

Result:
case mpr.intro.intro.intro
α : Type u
x y : α
hne : x ≠ y
h : {x, y} = univ
⊢ ∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}

Proof state:
α : Type u
⊢ #α = 2 ↔ ∃ x y, x ≠ y ∧ {x, y} = univ

Tactic:
simp only [← @Nat.cast_two Cardinal, mk_eq_nat_iff_finset, Finset.card_eq_two]

Result:
α : Type u
⊢ (∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}) ↔ ∃ x y, x ≠ y ∧ {x, y} = univ

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u
x y : α
hne : x ≠ y
ht : ↑{x, y} = univ
⊢ ∃ x y, x ≠ y ∧ {x, y} = univ

Tactic:
exact ⟨x, y, hne, by simpa using ht⟩

Result:
no goals

Proof state:
α : Type u
x y : α
hne : x ≠ y
ht : ↑{x, y} = univ
⊢ {x, y} = univ

Tactic:
simpa using ht

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_range_add (f : ℕ → β) (n m : ℕ) :
    (∏ x ∈ range (n + m), f x) = (∏ x ∈ range n, f x) * ∏ x ∈ range m, f (n + x)

Proof state:
β : Type u_4
inst✝ : CommMonoid β
f : ℕ → β
n m : ℕ
⊢ ∏ x ∈ range (n + m), f x = (∏ x ∈ range n, f x) * ∏ x ∈ range m, f (n + x)

Tactic:
induction m with
| zero => simp
| succ m hm => rw [Nat.add_succ, prod_range_succ, prod_range_succ, hm, mul_assoc]

Result:
no goals

Proof state:
case zero
β : Type u_4
inst✝ : CommMonoid β
f : ℕ → β
n : ℕ
⊢ ∏ x ∈ range (n + 0), f x = (∏ x ∈ range n, f x) * ∏ x ∈ range 0, f (n + x)

Tactic:
simp

Result:
no goals

Proof state:
case succ
β : Type u_4
inst✝ : CommMonoid β
f : ℕ → β
n m : ℕ
hm : ∏ x ∈ range (n + m), f x = (∏ x ∈ range n, f x) * ∏ x ∈ range m, f (n + x)
⊢ ∏ x ∈ range (n + (m + 1)), f x = (∏ x ∈ range n, f x) * ∏ x ∈ range (m + 1), f (n + x)

Tactic:
rw [Nat.add_succ, prod_range_succ, prod_range_succ, hm, mul_assoc]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Cover/Open.lean
theorem OpenCover.compactSpace {X : Scheme.{u}} (𝒰 : X.OpenCover) [Finite 𝒰.J]
    [H : ∀ i, CompactSpace (𝒰.obj i)] : CompactSpace X

Proof state:
case intro.h
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace
val✝ : Fintype 𝒰.J
⊢ ∀ (i : 𝒰.J), IsCompact (Set.range ⇑(ConcreteCategory.hom (𝒰.map i).base))

Tactic:
intro i

Result:
case intro.h
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace
val✝ : Fintype 𝒰.J
i : 𝒰.J
⊢ IsCompact (Set.range ⇑(ConcreteCategory.hom (𝒰.map i).base))

Proof state:
case intro.h
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace
val✝ : Fintype 𝒰.J
i : 𝒰.J
⊢ CompactSpace ↑(Set.range ⇑(ConcreteCategory.hom (𝒰.map i).base))

Tactic:
exact
  @Homeomorph.compactSpace _ _ _ _ (H i)
    (TopCat.homeoOfIso
      (asIso
        (IsOpenImmersion.isoOfRangeEq (𝒰.map i)
          (X.ofRestrict (Opens.isOpenEmbedding ⟨_, (𝒰.map_prop i).base_open.isOpen_range⟩))
          Subtype.range_coe.symm).hom.base))

Result:
no goals

Proof state:
case intro
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace
val✝ : Fintype 𝒰.J
⊢ IsCompact (⋃ i, Set.range ⇑(ConcreteCategory.hom (𝒰.map i).base))

Tactic:
apply isCompact_iUnion

Result:
case intro.h
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace
val✝ : Fintype 𝒰.J
⊢ ∀ (i : 𝒰.J), IsCompact (Set.range ⇑(ConcreteCategory.hom (𝒰.map i).base))

Proof state:
case intro.h
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace
val✝ : Fintype 𝒰.J
i : 𝒰.J
⊢ IsCompact (Set.range ⇑(ConcreteCategory.hom (𝒰.map i).base))

Tactic:
rw [isCompact_iff_compactSpace]

Result:
case intro.h
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace
val✝ : Fintype 𝒰.J
i : 𝒰.J
⊢ CompactSpace ↑(Set.range ⇑(ConcreteCategory.hom (𝒰.map i).base))

Proof state:
case intro
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace
val✝ : Fintype 𝒰.J
⊢ CompactSpace ↑↑X.toPresheafedSpace

Tactic:
rw [← isCompact_univ_iff, ← 𝒰.iUnion_range]

Result:
case intro
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace
val✝ : Fintype 𝒰.J
⊢ IsCompact (⋃ i, Set.range ⇑(ConcreteCategory.hom (𝒰.map i).base))

Proof state:
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace
⊢ CompactSpace ↑↑X.toPresheafedSpace

Tactic:
cases nonempty_fintype 𝒰.J

Result:
case intro
X : Scheme
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.J
H : ∀ (i : 𝒰.J), CompactSpace ↑↑(𝒰.obj i).toPresheafedSpace
val✝ : Fintype 𝒰.J
⊢ CompactSpace ↑↑X.toPresheafedSpace
-- Mathlib/MeasureTheory/Measure/Doubling.lean
theorem eventually_measure_le_scaling_constant_mul' (K : ℝ) (hK : 0 < K) :
    ∀ᶠ r in 𝓝[>] 0, ∀ x,
      μ (closedBall x r) ≤ scalingConstantOf μ K⁻¹ * μ (closedBall x (K * r))

Proof state:
case h.e'_2.h.h.h.e'_3.h.e'_6.h.e'_4
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
hK : 0 < K
x✝ : ℝ
a✝ : α
⊢ x✝ = K⁻¹ * (K * x✝)

Tactic:
simp [inv_mul_cancel_left₀ hK.ne']

Result:
no goals

Proof state:
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
hK : 0 < K
⊢ ∀ᶠ (r : ℝ) in 𝓝[>] 0, ∀ (x : α), μ (closedBall x r) ≤ ↑(scalingConstantOf μ K⁻¹) * μ (closedBall x (K * r))

Tactic:
convert eventually_nhdsGT_zero_mul_left hK (eventually_measure_le_scaling_constant_mul μ K⁻¹)

Result:
case h.e'_2.h.h.h.e'_3.h.e'_6.h.e'_4
α : Type u_1
inst✝² : PseudoMetricSpace α
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : IsUnifLocDoublingMeasure μ
K : ℝ
hK : 0 < K
x✝ : ℝ
a✝ : α
⊢ x✝ = K⁻¹ * (K * x✝)
-- Mathlib/Analysis/Calculus/VectorField.lean
theorem _root_.Filter.EventuallyEq.lieBracket_vectorField_eq
    (hV : V₁ =ᶠ[𝓝 x] V) (hW : W₁ =ᶠ[𝓝 x] W) :
    lieBracket 𝕜 V₁ W₁ x = lieBracket 𝕜 V W x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W V₁ W₁ : E → E
x : E
hV : V₁ =ᶠ[𝓝 x] V
hW : W₁ =ᶠ[𝓝 x] W
⊢ lieBracket 𝕜 V₁ W₁ x = lieBracket 𝕜 V W x

Tactic:
rw [← lieBracketWithin_univ, ← lieBracketWithin_univ, hV.lieBracketWithin_vectorField_eq_nhds hW]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_mkPiRing (z : G) : ‖ContinuousMultilinearMap.mkPiRing 𝕜 ι z‖ = ‖z‖

Proof state:
𝕜 : Type u
ι : Type v
G : Type wG
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
z : G
⊢ ‖ContinuousMultilinearMap.mkPiRing 𝕜 ι z‖ = ‖z‖

Tactic:
rw [ContinuousMultilinearMap.mkPiRing, norm_smulRight, norm_mkPiAlgebra, one_mul]

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Ring.lean
theorem isMaximal_comap_C_of_isJacobsonRing : (P.comap (C : R →+* R[X])).IsMaximal

Proof state:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
this : ⊥.IsMaximal
⊢ (comap ((Ideal.Quotient.mk P).comp C) ⊥).IsMaximal

Tactic:
exact isMaximal_comap_of_isIntegral_of_isMaximal' _
  (quotient_mk_comp_C_isIntegral_of_isJacobsonRing P) ⊥

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
⊢ (comap C P).IsMaximal

Tactic:
rw [← @mk_ker _ _ P, RingHom.ker_eq_comap_bot, comap_comap]

Result:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
⊢ (comap ((Ideal.Quotient.mk P).comp C) ⊥).IsMaximal

Proof state:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
⊢ (comap ((Ideal.Quotient.mk P).comp C) ⊥).IsMaximal

Tactic:
have := (bot_quotient_isMaximal_iff _).mpr hP

Result:
R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
hP : P.IsMaximal
inst✝ : IsJacobsonRing R
this : ⊥.IsMaximal
⊢ (comap ((Ideal.Quotient.mk P).comp C) ⊥).IsMaximal
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_left [NeBot g] : map₂ (fun x _ => x) f g = f

Proof state:
α : Type u_1
β : Type u_3
f : Filter α
g : Filter β
inst✝ : g.NeBot
⊢ map₂ (fun x x_1 => x) f g = f

Tactic:
rw [← map_prod_eq_map₂, map_fst_prod]

Result:
no goals
-- Mathlib/Data/Nat/ModEq.lean
lemma eq_of_abs_lt (h : a ≡ b [MOD m]) (h2 : |(b : ℤ) - a| < m) : a = b

Proof state:
case x
m a b : ℕ
h : a ≡ b [MOD m]
h2 : |↑b - ↑a| < ↑m
⊢ Int.ofNat b - Int.ofNat a = 0

Tactic:
exact Int.eq_zero_of_abs_lt_dvd h.dvd h2

Result:
no goals

Proof state:
case x
m a b : ℕ
h : a ≡ b [MOD m]
h2 : |↑b - ↑a| < ↑m
⊢ Int.ofNat a = Int.ofNat b

Tactic:
rw [eq_comm, ← sub_eq_zero]

Result:
case x
m a b : ℕ
h : a ≡ b [MOD m]
h2 : |↑b - ↑a| < ↑m
⊢ Int.ofNat b - Int.ofNat a = 0

Proof state:
m a b : ℕ
h : a ≡ b [MOD m]
h2 : |↑b - ↑a| < ↑m
⊢ a = b

Tactic:
apply Int.ofNat.inj

Result:
case x
m a b : ℕ
h : a ≡ b [MOD m]
h2 : |↑b - ↑a| < ↑m
⊢ Int.ofNat a = Int.ofNat b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_toArray {α n} (xs : Vector α n) (i : Nat) (h : i < xs.toArray.size) :
    xs.toArray[i] = xs[i]'(by simpa using h)

Proof state:
α : Type u_1
n : Nat
xs : Vector α n
i : Nat
h : i < xs.size
⊢ xs.toArray[i] = xs[i]

Tactic:
cases xs

Result:
case mk
α : Type u_1
n i : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : i < { toArray := toArray✝, size_toArray := size_toArray✝ }.size
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray[i] =
    { toArray := toArray✝, size_toArray := size_toArray✝ }[i]

Proof state:
α : Type ?u.20071
n : Nat
xs : Vector α n
i : Nat
h : i < xs.size
⊢ i < n

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
n i : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : i < { toArray := toArray✝, size_toArray := size_toArray✝ }.size
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray[i] =
    { toArray := toArray✝, size_toArray := size_toArray✝ }[i]

Tactic:
simp

Result:
no goals