harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean
private lemma card_bound (hP₁ : P.IsEquipartition) (hP₃ : #P.parts ≤ bound (ε / 8) ⌈4/ε⌉₊)
    (hX : s ∈ P.parts) : card α / (2 * bound (ε / 8) ⌈4 / ε⌉₊ : ℝ) ≤ #s

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
P : Finpartition univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
h✝ : Nonempty α
this : 0 < #P.parts
⊢ ↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑(Fintype.card α) / (2 * ↑(#P.parts))

Tactic:
gcongr

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
P : Finpartition univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
h✝ : Nonempty α
this : 0 < #P.parts
⊢ 0 < 2 * ↑(#P.parts)

Tactic:
positivity

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
P : Finpartition univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
h✝ : Nonempty α
⊢ ↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑(#s)

Tactic:
have := Finset.Nonempty.card_pos ⟨_, hX⟩

Result:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
P : Finpartition univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
h✝ : Nonempty α
this : 0 < #P.parts
⊢ ↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑(#s)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
P : Finpartition univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
⊢ ↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑(#s)

Tactic:
cases isEmpty_or_nonempty α

Result:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
P : Finpartition univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
h✝ : IsEmpty α
⊢ ↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑(#s)

case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
P : Finpartition univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
h✝ : Nonempty α
⊢ ↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑(#s)

Proof state:
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
P : Finpartition univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
h✝ : Nonempty α
this : 0 < #P.parts
⊢ ↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑(#s)

Tactic:
calc
  _ ≤ card α / (2 * #P.parts : ℝ) := by gcongr
  _ ≤ ↑(card α / #P.parts) :=
    (div_le_iff₀' (by positivity)).2 <| mod_cast (aux ‹_› P.card_parts_le_card).le
  _ ≤ (#s : ℝ) := mod_cast hP₁.average_le_card_part hX

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
P : Finpartition univ
ε : ℝ
hP₁ : P.IsEquipartition
hP₃ : #P.parts ≤ bound (ε / 8) ⌈4 / ε⌉₊
hX : s ∈ P.parts
h✝ : IsEmpty α
⊢ ↑(Fintype.card α) / (2 * ↑(bound (ε / 8) ⌈4 / ε⌉₊)) ≤ ↑(#s)

Tactic:
simp [Fintype.card_eq_zero]

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem preimage_closure_subset_closure_preimage (hf : IsOpenMap f) {s : Set Y} :
    f ⁻¹' closure s ⊆ closure (f ⁻¹' s)

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
s : Set Y
⊢ (closure (f ⁻¹' s))ᶜ ⊆ (f ⁻¹' closure s)ᶜ

Tactic:
simp only [← interior_compl, ← preimage_compl, hf.interior_preimage_subset_preimage_interior]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
s : Set Y
⊢ f ⁻¹' closure s ⊆ closure (f ⁻¹' s)

Tactic:
rw [← compl_subset_compl]

Result:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
s : Set Y
⊢ (closure (f ⁻¹' s))ᶜ ⊆ (f ⁻¹' closure s)ᶜ
-- Mathlib/Data/Fin/Basic.lean
theorem succ_ne_last_of_lt {p i : Fin n} (h : i < p) : succ i ≠ last n

Proof state:
case succ
n✝ : ℕ
p i : Fin (n✝ + 1)
h : i < p
⊢ ¬↑i = ↑(last n✝)

Tactic:
exact ((le_last _).trans_lt' h).ne

Result:
no goals

Proof state:
case succ
n✝ : ℕ
p i : Fin (n✝ + 1)
h : i < p
⊢ i.succ ≠ last (n✝ + 1)

Tactic:
rw [succ_ne_last_iff, Ne, Fin.ext_iff]

Result:
case succ
n✝ : ℕ
p i : Fin (n✝ + 1)
h : i < p
⊢ ¬↑i = ↑(last n✝)

Proof state:
case zero
p i : Fin 0
h : i < p
⊢ i.succ ≠ last 0

Tactic:
exact i.elim0

Result:
no goals

Proof state:
n : ℕ
p i : Fin n
h : i < p
⊢ i.succ ≠ last n

Tactic:
cases n

Result:
case zero
p i : Fin 0
h : i < p
⊢ i.succ ≠ last 0

case succ
n✝ : ℕ
p i : Fin (n✝ + 1)
h : i < p
⊢ i.succ ≠ last (n✝ + 1)
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
lemma comp_assoc (C C' C'' : VariableChange R) : comp (comp C C') C'' = comp C (comp C' C'')

Proof state:
R : Type u
inst✝ : CommRing R
C C' C'' : VariableChange R
⊢ (C.comp C').comp C'' = C.comp (C'.comp C'')

Tactic:
ext <;> simp only [comp, Units.val_mul] <;> ring1

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem coe_subtypeEquivCodomain_symm (f : { x' // x' ≠ x } → Y) :
    ((subtypeEquivCodomain f).symm : Y → _) = fun y =>
      ⟨fun x' => if h : x' ≠ x then f ⟨x', h⟩ else y, by
        funext x'
        simp only [ne_eq, dite_not, comp_apply, Subtype.coe_eta, dite_eq_ite, ite_eq_right_iff]
        intro w
        exfalso
        exact x'.property w⟩ :=
  rfl

Proof state:
case h
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
X : Sort u_9
Y : Sort u_10
inst✝ : DecidableEq X
x : X
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
⊢ ((fun x' => if h : x' ≠ x then f ⟨x', h⟩ else y) ∘ Subtype.val) x' = f x'

Tactic:
simp only [ne_eq, dite_not, comp_apply, Subtype.coe_eta, dite_eq_ite, ite_eq_right_iff]

Result:
case h
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
X : Sort u_9
Y : Sort u_10
inst✝ : DecidableEq X
x : X
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
⊢ ↑x' = x → y = f x'

Proof state:
case h
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
X : Sort u_9
Y : Sort u_10
inst✝ : DecidableEq X
x : X
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
w : ↑x' = x
⊢ y = f x'

Tactic:
exfalso

Result:
case h
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
X : Sort u_9
Y : Sort u_10
inst✝ : DecidableEq X
x : X
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
w : ↑x' = x
⊢ False

Proof state:
case h
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
X : Sort u_9
Y : Sort u_10
inst✝ : DecidableEq X
x : X
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
⊢ ↑x' = x → y = f x'

Tactic:
intro w

Result:
case h
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
X : Sort u_9
Y : Sort u_10
inst✝ : DecidableEq X
x : X
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
w : ↑x' = x
⊢ y = f x'

Proof state:
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
X : Sort u_9
Y : Sort u_10
inst✝ : DecidableEq X
x : X
f : { x' // x' ≠ x } → Y
y : Y
⊢ (fun x' => if h : x' ≠ x then f ⟨x', h⟩ else y) ∘ Subtype.val = f

Tactic:
funext x'

Result:
case h
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
X : Sort u_9
Y : Sort u_10
inst✝ : DecidableEq X
x : X
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
⊢ ((fun x' => if h : x' ≠ x then f ⟨x', h⟩ else y) ∘ Subtype.val) x' = f x'

Proof state:
case h
α : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
X : Sort u_9
Y : Sort u_10
inst✝ : DecidableEq X
x : X
f : { x' // x' ≠ x } → Y
y : Y
x' : { x' // x' ≠ x }
w : ↑x' = x
⊢ False

Tactic:
exact x'.property w

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma Exact.map_of_preservesRightHomologyOf (h : S.Exact) (F : C ⥤ D)
    [F.PreservesZeroMorphisms] [F.PreservesRightHomologyOf S]
    [(S.map F).HasHomology] : (S.map F).Exact

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : (S.map F).HasHomology
this : S.HasHomology
h : 𝟙 S.rightHomologyData.H = 0
⊢ (S.map F).Exact

Tactic:
rw [S.rightHomologyData.exact_map_iff F, IsZero.iff_id_eq_zero,
  ← F.map_id, h, F.map_zero]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : (S.map F).HasHomology
this : S.HasHomology
⊢ (S.map F).Exact

Tactic:
rw [S.rightHomologyData.exact_iff, IsZero.iff_id_eq_zero] at h

Result:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : (S.map F).HasHomology
this : S.HasHomology
h : 𝟙 S.rightHomologyData.H = 0
⊢ (S.map F).Exact

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : (S.map F).HasHomology
⊢ (S.map F).Exact

Tactic:
have : S.HasHomology := h.hasHomology

Result:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
h : S.Exact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : F.PreservesRightHomologyOf S
inst✝ : (S.map F).HasHomology
this : S.HasHomology
⊢ (S.map F).Exact
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma isSetSemiring (hC : IsSetRing C) : IsSetSemiring C where
  empty_mem := hC.empty_mem
  inter_mem := fun _ hs _ ht => hC.inter_mem hs ht
  diff_eq_sUnion'

Proof state:
case refine_3
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : Set α
hs : s ∈ C
t : Set α
ht : t ∈ C
⊢ s \ t = ⋃₀ ↑{s \ t}

Tactic:
simp only [coe_singleton, sUnion_singleton]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : Set α
hs : s ∈ C
t : Set α
ht : t ∈ C
⊢ s \ t ∈ C

Tactic:
exact hC.diff_mem hs ht

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
⊢ ∀ s ∈ C, ∀ t ∈ C, ∃ I, ↑I ⊆ C ∧ (↑I).PairwiseDisjoint id ∧ s \ t = ⋃₀ ↑I

Tactic:
refine fun s hs t ht => ⟨{s \ t}, ?_, ?_, ?_⟩

Result:
case refine_1
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : Set α
hs : s ∈ C
t : Set α
ht : t ∈ C
⊢ ↑{s \ t} ⊆ C

case refine_2
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : Set α
hs : s ∈ C
t : Set α
ht : t ∈ C
⊢ (↑{s \ t}).PairwiseDisjoint id

case refine_3
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : Set α
hs : s ∈ C
t : Set α
ht : t ∈ C
⊢ s \ t = ⋃₀ ↑{s \ t}

Proof state:
case refine_1
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : Set α
hs : s ∈ C
t : Set α
ht : t ∈ C
⊢ ↑{s \ t} ⊆ C

Tactic:
simp only [coe_singleton, Set.singleton_subset_iff]

Result:
case refine_1
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : Set α
hs : s ∈ C
t : Set α
ht : t ∈ C
⊢ s \ t ∈ C

Proof state:
case refine_2
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : Set α
hs : s ∈ C
t : Set α
ht : t ∈ C
⊢ (↑{s \ t}).PairwiseDisjoint id

Tactic:
simp only [coe_singleton, pairwiseDisjoint_singleton]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasFDerivAt.clm_comp (hc : HasFDerivAt c c' x) (hd : HasFDerivAt d d' x) :
    HasFDerivAt (fun y => (c y).comp (d y))
      ((compL 𝕜 F G H (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') x

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type u_4
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
x : E
H : Type u_5
inst✝¹ : NormedAddCommGroup H
inst✝ : NormedSpace 𝕜 H
c : E → G →L[𝕜] H
c' : E →L[𝕜] G →L[𝕜] H
d : E → F →L[𝕜] G
d' : E →L[𝕜] F →L[𝕜] G
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
⊢ HasFDerivAt (fun y => (c y).comp (d y)) (((compL 𝕜 F G H) (c x)).comp d' + ((compL 𝕜 F G H).flip (d x)).comp c') x

Tactic:
exact (isBoundedBilinearMap_comp.hasFDerivAt (c x, d x) :).comp x <| hc.prod hd

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
@[to_additive]
lemma closure_pow {n : ℕ} (hs : 1 ∈ s) (hn : n ≠ 0) : closure (s ^ n) = closure s :=
  (closure_pow_le hn).antisymm <| by gcongr; exact subset_pow hs hn

Proof state:
case h
M : Type u_3
inst✝ : Monoid M
s : Set M
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ s ⊆ s ^ n

Tactic:
exact subset_pow hs hn

Result:
no goals

Proof state:
M : Type u_3
inst✝ : Monoid M
s : Set M
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ closure s ≤ closure (s ^ n)

Tactic:
gcongr

Result:
case h
M : Type u_3
inst✝ : Monoid M
s : Set M
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ s ⊆ s ^ n
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Alter.lean
theorem Ordered.modify {t : RBNode α}
    (H : (t.zoom cut).1.OnRoot fun x => cmpEq cmp (f x) x)
    (h : t.Ordered cmp) : (modify cut f t).Ordered cmp :=
  modify_eq_alter _ ▸ h.alter @fun
    | _, .node .., _, eq, rfl => by
      rw [eq] at H; exact ⟨H.RootOrdered_congr.2 (h.zoom eq).2.2.1.1, H⟩

Proof state:
α : Type u_1
cut : α → Ordering
cmp : α → α → Ordering
f : α → α
t : RBNode α
h : Ordered cmp t
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝ : Path α
H : OnRoot (fun x => cmpEq cmp (f x) x) (node c✝ l✝ v✝ r✝, x✝).fst
eq : RBNode.zoom cut t = (node c✝ l✝ v✝ r✝, x✝)
⊢ Path.RootOrdered cmp x✝ (f v✝) ∧ OnRoot (cmpEq cmp (f v✝)) (node c✝ l✝ v✝ r✝)

Tactic:
exact ⟨H.RootOrdered_congr.2 (h.zoom eq).2.2.1.1, H⟩

Result:
no goals

Proof state:
α : Type u_1
cut : α → Ordering
cmp : α → α → Ordering
f : α → α
t : RBNode α
H : OnRoot (fun x => cmpEq cmp (f x) x) (RBNode.zoom cut t).fst
h : Ordered cmp t
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝ : Path α
eq : RBNode.zoom cut t = (node c✝ l✝ v✝ r✝, x✝)
⊢ Path.RootOrdered cmp x✝ (f v✝) ∧ OnRoot (cmpEq cmp (f v✝)) (node c✝ l✝ v✝ r✝)

Tactic:
rw [eq] at H

Result:
α : Type u_1
cut : α → Ordering
cmp : α → α → Ordering
f : α → α
t : RBNode α
h : Ordered cmp t
c✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝ : Path α
H : OnRoot (fun x => cmpEq cmp (f x) x) (node c✝ l✝ v✝ r✝, x✝).fst
eq : RBNode.zoom cut t = (node c✝ l✝ v✝ r✝, x✝)
⊢ Path.RootOrdered cmp x✝ (f v✝) ∧ OnRoot (cmpEq cmp (f v✝)) (node c✝ l✝ v✝ r✝)
-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
/-- `s ↦ (s - 1) * L χ s` is an entire function when `χ` is a trivial Dirichlet character. -/
lemma differentiable_LFunctionTrivChar₁ : Differentiable ℂ (LFunctionTrivChar₁ n)

Proof state:
case funProp.discharger
n : ℕ
inst✝ : NeZero n
x✝ : ℂ
hs : x✝ ∈ Set.univ \ {1}
⊢ x✝ ≠ 1 ∨ 1 ≠ 1

Tactic:
simp_all [hs]

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
x✝ : ℂ
hs : x✝ ∈ Set.univ \ {1}
⊢ DifferentiableAt ℂ (fun s => (s - 1) * LFunctionTrivChar n s) x✝

Tactic:
fun_prop (disch := simp_all [hs])

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ Differentiable ℂ (LFunctionTrivChar₁ n)

Tactic:
rw [← differentiableOn_univ,
  ← differentiableOn_compl_singleton_and_continuousAt_iff (c := 1) Filter.univ_mem]

Result:
n : ℕ
inst✝ : NeZero n
⊢ DifferentiableOn ℂ (LFunctionTrivChar₁ n) (Set.univ \ {1}) ∧ ContinuousAt (LFunctionTrivChar₁ n) 1

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ ContinuousWithinAt (LFunctionTrivChar₁ n) {1}ᶜ 1

Tactic:
simpa using LFunctionTrivChar_residue_one

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ DifferentiableOn ℂ (LFunctionTrivChar₁ n) (Set.univ \ {1}) ∧ ContinuousAt (LFunctionTrivChar₁ n) 1

Tactic:
refine ⟨DifferentiableOn.congr (f := fun s ↦ (s - 1) * LFunctionTrivChar n s)
  (fun _ hs ↦ DifferentiableAt.differentiableWithinAt <| by fun_prop (disch := simp_all [hs]))
 fun _ hs ↦ Function.update_of_ne (Set.mem_diff_singleton.mp hs).2 ..,
  continuousWithinAt_compl_self.mp ?_⟩

Result:
n : ℕ
inst✝ : NeZero n
⊢ ContinuousWithinAt (LFunctionTrivChar₁ n) {1}ᶜ 1
-- Mathlib/Data/Nat/BitIndices.lean
theorem twoPowSum_bitIndices (n : ℕ) : (n.bitIndices.map (fun i ↦ 2 ^ i)).sum = n

Proof state:
case h
b : Bool
n : ℕ
hs : (map (fun i => 2 ^ i) n.bitIndices).sum = n
i : ℕ
⊢ ((fun i => 2 ^ i) ∘ fun x => x + 1) i = 2 * 2 ^ i

Tactic:
simp [pow_add, mul_comm]

Result:
no goals

Proof state:
b : Bool
n : ℕ
hs : (map (fun i => 2 ^ i) n.bitIndices).sum = n
⊢ ((fun i => 2 ^ i) ∘ fun x => x + 1) = fun i => 2 * 2 ^ i

Tactic:
ext i

Result:
case h
b : Bool
n : ℕ
hs : (map (fun i => 2 ^ i) n.bitIndices).sum = n
i : ℕ
⊢ ((fun i => 2 ^ i) ∘ fun x => x + 1) i = 2 * 2 ^ i

Proof state:
case f.false
n : ℕ
hs : (map (fun i => 2 ^ i) n.bitIndices).sum = n
hrw : ((fun i => 2 ^ i) ∘ fun x => x + 1) = fun i => 2 * 2 ^ i
⊢ (map (fun i => 2 ^ i) (bit false n).bitIndices).sum = bit false n

Tactic:
simpa [hrw, List.sum_map_mul_left]

Result:
no goals

Proof state:
n : ℕ
⊢ (map (fun i => 2 ^ i) n.bitIndices).sum = n

Tactic:
induction' n using binaryRec with b n hs

Result:
case z

⊢ (map (fun i => 2 ^ i) (bitIndices 0)).sum = 0

case f
b : Bool
n : ℕ
hs : (map (fun i => 2 ^ i) n.bitIndices).sum = n
⊢ (map (fun i => 2 ^ i) (bit b n).bitIndices).sum = bit b n

Proof state:
case z

⊢ (map (fun i => 2 ^ i) (bitIndices 0)).sum = 0

Tactic:
simp

Result:
no goals

Proof state:
case f
b : Bool
n : ℕ
hs : (map (fun i => 2 ^ i) n.bitIndices).sum = n
hrw : ((fun i => 2 ^ i) ∘ fun x => x + 1) = fun i => 2 * 2 ^ i
⊢ (map (fun i => 2 ^ i) (bit b n).bitIndices).sum = bit b n

Tactic:
cases b

Result:
case f.false
n : ℕ
hs : (map (fun i => 2 ^ i) n.bitIndices).sum = n
hrw : ((fun i => 2 ^ i) ∘ fun x => x + 1) = fun i => 2 * 2 ^ i
⊢ (map (fun i => 2 ^ i) (bit false n).bitIndices).sum = bit false n

case f.true
n : ℕ
hs : (map (fun i => 2 ^ i) n.bitIndices).sum = n
hrw : ((fun i => 2 ^ i) ∘ fun x => x + 1) = fun i => 2 * 2 ^ i
⊢ (map (fun i => 2 ^ i) (bit true n).bitIndices).sum = bit true n

Proof state:
case f
b : Bool
n : ℕ
hs : (map (fun i => 2 ^ i) n.bitIndices).sum = n
⊢ (map (fun i => 2 ^ i) (bit b n).bitIndices).sum = bit b n

Tactic:
have hrw : (fun i ↦ 2^i) ∘ (fun x ↦ x+1) = fun i ↦ 2 * 2 ^ i := by
  ext i; simp [pow_add, mul_comm]

Result:
case f
b : Bool
n : ℕ
hs : (map (fun i => 2 ^ i) n.bitIndices).sum = n
hrw : ((fun i => 2 ^ i) ∘ fun x => x + 1) = fun i => 2 * 2 ^ i
⊢ (map (fun i => 2 ^ i) (bit b n).bitIndices).sum = bit b n

Proof state:
case f.true
n : ℕ
hs : (map (fun i => 2 ^ i) n.bitIndices).sum = n
hrw : ((fun i => 2 ^ i) ∘ fun x => x + 1) = fun i => 2 * 2 ^ i
⊢ (map (fun i => 2 ^ i) (bit true n).bitIndices).sum = bit true n

Tactic:
simp [hrw, List.sum_map_mul_left, hs, add_comm (a := 1)]

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem IsClosedMap.lift'_closure_map_eq
    (f_closed : IsClosedMap f) (f_cont : Continuous f) (F : Filter X) :
    (map f F).lift' closure = map f (F.lift' closure)

Proof state:
case e_h.h
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous f
F : Filter X
s : Set X
⊢ (closure ∘ image f) s = (image f ∘ closure) s

Tactic:
exact f_closed.closure_image_eq_of_continuous f_cont s

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous f
F : Filter X
⊢ F.lift' (closure ∘ image f) = F.lift' (image f ∘ closure)

Tactic:
congr

Result:
case e_h
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous f
F : Filter X
⊢ closure ∘ image f = image f ∘ closure

Proof state:
case e_h
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous f
F : Filter X
⊢ closure ∘ image f = image f ∘ closure

Tactic:
ext s : 1

Result:
case e_h.h
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous f
F : Filter X
s : Set X
⊢ (closure ∘ image f) s = (image f ∘ closure) s

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous f
F : Filter X
⊢ (map f F).lift' closure = map f (F.lift' closure)

Tactic:
rw [map_lift'_eq2 (monotone_closure Y), map_lift'_eq (monotone_closure X)]

Result:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f_closed : IsClosedMap f
f_cont : Continuous f
F : Filter X
⊢ F.lift' (closure ∘ image f) = F.lift' (image f ∘ closure)
-- Mathlib/Logic/Relation.lean
theorem head'_iff : TransGen r a c ↔ ∃ b, r a b ∧ ReflTransGen r b c

Proof state:
case single
α : Type u_1
r : α → α → Prop
a c b✝ : α
hac : r a b✝
⊢ ∃ b, r a b ∧ ReflTransGen r b b✝

Tactic:
exact ⟨_, hac, by rfl⟩

Result:
no goals

Proof state:
case tail
α : Type u_1
r : α → α → Prop
a c b✝ c✝ : α
a✝ : TransGen r a b✝
hbc : r b✝ c✝
IH : ∃ b, r a b ∧ ReflTransGen r b b✝
⊢ ∃ b, r a b ∧ ReflTransGen r b c✝

Tactic:
rcases IH with ⟨d, had, hdb⟩

Result:
case tail.intro.intro
α : Type u_1
r : α → α → Prop
a c b✝ c✝ : α
a✝ : TransGen r a b✝
hbc : r b✝ c✝
d : α
had : r a d
hdb : ReflTransGen r d b✝
⊢ ∃ b, r a b ∧ ReflTransGen r b c✝

Proof state:
α : Type u_1
r : α → α → Prop
a c b✝ : α
hac : r a b✝
⊢ ReflTransGen r b✝ b✝

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
a c : α
⊢ TransGen r a c ↔ ∃ b, r a b ∧ ReflTransGen r b c

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨b, hab, hbc⟩ ↦ head' hab hbc⟩

Result:
α : Type u_1
r : α → α → Prop
a c : α
h : TransGen r a c
⊢ ∃ b, r a b ∧ ReflTransGen r b c

Proof state:
α : Type u_1
r : α → α → Prop
a c : α
h : TransGen r a c
⊢ ∃ b, r a b ∧ ReflTransGen r b c

Tactic:
induction h with
| single hac => exact ⟨_, hac, by rfl⟩
| tail _ hbc IH =>
rcases IH with ⟨d, had, hdb⟩
exact ⟨_, had, hdb.tail hbc⟩

Result:
no goals

Proof state:
case tail.intro.intro
α : Type u_1
r : α → α → Prop
a c b✝ c✝ : α
a✝ : TransGen r a b✝
hbc : r b✝ c✝
d : α
had : r a d
hdb : ReflTransGen r d b✝
⊢ ∃ b, r a b ∧ ReflTransGen r b c✝

Tactic:
exact ⟨_, had, hdb.tail hbc⟩

Result:
no goals