harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem orthonormalBasis_one_dim (b : OrthonormalBasis ι ℝ ℝ) :
    (⇑b = fun _ => (1 : ℝ)) ∨ ⇑b = fun _ => (-1 : ℝ)

Proof state:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : b default = 1 ∨ b default = -1
a✝ : b default = -1
⊢ const ι (b default) = fun x => -1

Tactic:
ext

Result:
case refine_2.h
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : b default = 1 ∨ b default = -1
a✝ : b default = -1
x✝ : ι
⊢ const ι (b default) x✝ = -1

Proof state:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : b default = 1 ∨ b default = -1
⊢ (const ι (b default) = fun x => 1) ∨ const ι (b default) = fun x => -1

Tactic:
refine this.imp ?_ ?_ <;> (intro; ext; simp [*])

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : ‖b default‖ = 1
⊢ b default = 1 ∨ b default = -1

Tactic:
rwa [Real.norm_eq_abs, abs_eq (zero_le_one' ℝ)] at this

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
⊢ (⇑b = fun x => 1) ∨ ⇑b = fun x => -1

Tactic:
have : Unique ι := b.toBasis.unique

Result:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this : Unique ι
⊢ (⇑b = fun x => 1) ∨ ⇑b = fun x => -1

Proof state:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this : Unique ι
⊢ (⇑b = fun x => 1) ∨ ⇑b = fun x => -1

Tactic:
have : b default = 1 ∨ b default = -1 := by
  have : ‖b default‖ = 1 := b.orthonormal.1 _
  rwa [Real.norm_eq_abs, abs_eq (zero_le_one' ℝ)] at this

Result:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : b default = 1 ∨ b default = -1
⊢ (⇑b = fun x => 1) ∨ ⇑b = fun x => -1

Proof state:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : b default = 1 ∨ b default = -1
⊢ b default = -1 → const ι (b default) = fun x => -1

Tactic:
intro

Result:
case refine_2
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : b default = 1 ∨ b default = -1
a✝ : b default = -1
⊢ const ι (b default) = fun x => -1

Proof state:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this : Unique ι
⊢ b default = 1 ∨ b default = -1

Tactic:
have : ‖b default‖ = 1 := b.orthonormal.1 _

Result:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : ‖b default‖ = 1
⊢ b default = 1 ∨ b default = -1

Proof state:
case refine_2.h
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : b default = 1 ∨ b default = -1
a✝ : b default = -1
x✝ : ι
⊢ const ι (b default) x✝ = -1

Tactic:
simp [*]

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : b default = 1 ∨ b default = -1
⊢ (⇑b = fun x => 1) ∨ ⇑b = fun x => -1

Tactic:
rw [eq_const_of_unique b]

Result:
ι : Type u_1
inst✝ : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this✝ : Unique ι
this : b default = 1 ∨ b default = -1
⊢ (const ι (b default) = fun x => 1) ∨ const ι (b default) = fun x => -1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_append {a : α} {s t : Array α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t

Proof state:
α : Type u_1
a : α
s t : Array α
⊢ a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t

Tactic:
simp only [mem_def, toList_append, List.mem_append]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0)
    (him : z.im = 0) : Tendsto log (𝓝[{ z : ℂ | z.im < 0 }] z) (𝓝 <| Real.log ‖z‖ - π * I)

Proof state:
case convert_1.intro
z : ℝ
hre : (↑z).re < 0
⊢ ‖↑z‖ ≠ 0

Tactic:
simpa using hre.ne

Result:
no goals

Proof state:
case h.e'_5
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 (↑(Real.log ‖z‖) - ↑π * I) = 𝓝 ((ofReal ∘ fun x => Real.log ‖x‖) z + ↑(-π) * I)

Tactic:
simp [sub_eq_add_neg]

Result:
no goals

Proof state:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto log (𝓝[{z | z.im < 0}] z) (𝓝 (↑(Real.log ‖z‖) - ↑π * I))

Tactic:
convert
  (continuous_ofReal.continuousAt.comp_continuousWithinAt
          (continuous_norm.continuousWithinAt.log _)).tendsto.add
    (((continuous_ofReal.tendsto _).comp <|
          tendsto_arg_nhdsWithin_im_neg_of_re_neg_of_im_zero hre him).mul
      tendsto_const_nhds) using 1

Result:
case h.e'_5
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ 𝓝 (↑(Real.log ‖z‖) - ↑π * I) = 𝓝 ((ofReal ∘ fun x => Real.log ‖x‖) z + ↑(-π) * I)

case convert_1
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0

Proof state:
case convert_1
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ ‖z‖ ≠ 0

Tactic:
lift z to ℝ using him

Result:
case convert_1.intro
z : ℝ
hre : (↑z).re < 0
⊢ ‖↑z‖ ≠ 0
-- Mathlib/Algebra/Star/Conjneg.lean
@[simp] lemma conjneg_eq_zero : conjneg f = 0 ↔ f = 0

Proof state:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommSemiring R
inst✝ : StarRing R
f : G → R
⊢ conjneg f = 0 ↔ f = 0

Tactic:
rw [← conjneg_inj, conjneg_conjneg, conjneg_zero]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/LevelOne.lean
lemma ModularForm.levelOne_neg_weight_rank_zero (hk : k < 0) :
    Module.rank ℂ (ModularForm Γ(1) k) = 0

Proof state:
k : ℤ
hk : k < 0
⊢ Module.rank ℂ (ModularForm Γ(1) k) = 0

Tactic:
refine rank_eq_zero_iff.mpr fun f ↦ ⟨_, one_ne_zero, ?_⟩

Result:
k : ℤ
hk : k < 0
f : ModularForm Γ(1) k
⊢ 1 • f = 0

Proof state:
k : ℤ
hk : k < 0
f : ModularForm Γ(1) k
⊢ 1 • f = 0

Tactic:
simpa only [one_smul, ← DFunLike.coe_injective.eq_iff] using levelOne_neg_weight_eq_zero hk f

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem reverse_pmap {P : α → Prop} (f : (a : α) → P a → β) (xs : List α)
    (H : ∀ (a : α), a ∈ xs → P a) :
    (xs.pmap f H).reverse = xs.reverse.pmap f (fun a h => H a (by simpa using h))

Proof state:
α : Type ?u.78020
β : Type ?u.78055
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
a : α
h : a ∈ xs.reverse
⊢ a ∈ xs

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : (a : α) → P a → β
xs : List α
H : ∀ (a : α), a ∈ xs → P a
⊢ (pmap f xs H).reverse = pmap f xs.reverse ⋯

Tactic:
rw [pmap_reverse]

Result:
no goals
-- Mathlib/Data/Fintype/Units.lean
theorem Nat.card_units [GroupWithZero α] :
    Nat.card αˣ = Nat.card α - 1

Proof state:
case inr
α : Type u_1
inst✝ : GroupWithZero α
h✝ : Infinite { a // a ≠ 0 }
⊢ Nat.card ({ a // a = 0 } ⊕ { a // ¬a = 0 }) - 1 = Nat.card { a // a ≠ 0 }

Tactic:
rw [Nat.card_eq_zero_of_infinite, Nat.card_eq_zero_of_infinite, zero_tsub]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : GroupWithZero α
⊢ Nat.card ({ a // a = 0 } ⊕ { a // ¬a = 0 }) - 1 = Nat.card { a // a ≠ 0 }

Tactic:
rcases finite_or_infinite {a : α // a ≠ 0}

Result:
case inl
α : Type u_1
inst✝ : GroupWithZero α
h✝ : Finite { a // a ≠ 0 }
⊢ Nat.card ({ a // a = 0 } ⊕ { a // ¬a = 0 }) - 1 = Nat.card { a // a ≠ 0 }

case inr
α : Type u_1
inst✝ : GroupWithZero α
h✝ : Infinite { a // a ≠ 0 }
⊢ Nat.card ({ a // a = 0 } ⊕ { a // ¬a = 0 }) - 1 = Nat.card { a // a ≠ 0 }

Proof state:
case inl
α : Type u_1
inst✝ : GroupWithZero α
h✝ : Finite { a // a ≠ 0 }
⊢ Nat.card ({ a // a = 0 } ⊕ { a // ¬a = 0 }) - 1 = Nat.card { a // a ≠ 0 }

Tactic:
rw [Nat.card_sum, Nat.card_unique, add_tsub_cancel_left]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem ENNReal.tendsto_pow_atTop_nhds_zero_iff {r : ℝ≥0∞} :
    Tendsto (fun n : ℕ => r ^ n) atTop (𝓝 0) ↔ r < 1

Proof state:
case intro
r : ℝ≥0
h : Tendsto (fun n => ↑r ^ n) atTop (𝓝 0)
⊢ ↑r < 1

Tactic:
rw [← coe_zero] at h

Result:
case intro
r : ℝ≥0
h : Tendsto (fun n => ↑r ^ n) atTop (𝓝 ↑0)
⊢ ↑r < 1

Proof state:
case intro
r : ℝ≥0
h : Tendsto (HPow.hPow r) atTop (𝓝 0)
⊢ r < 1

Tactic:
exact NNReal.tendsto_pow_atTop_nhds_zero_iff.mp h

Result:
no goals

Proof state:
r : ℝ≥0∞
h : Tendsto (fun n => r ^ n) atTop (𝓝 0)
⊢ r ≠ ⊤

Tactic:
refine fun hr ↦ top_ne_zero (tendsto_nhds_unique (EventuallyEq.tendsto ?_) (hr ▸ h))

Result:
r : ℝ≥0∞
h : Tendsto (fun n => r ^ n) atTop (𝓝 0)
hr : r = ⊤
⊢ (fun n => ⊤ ^ n) =ᶠ[atTop] fun x => ⊤

Proof state:
case intro
r : ℝ≥0
h : Tendsto (fun n => ↑r ^ n) atTop (𝓝 ↑0)
⊢ ↑r < 1

Tactic:
norm_cast at h ⊢

Result:
case intro
r : ℝ≥0
h : Tendsto (HPow.hPow r) atTop (𝓝 0)
⊢ r < 1

Proof state:
r : ℝ≥0∞
h : Tendsto (fun n => r ^ n) atTop (𝓝 0)
hr : r = ⊤
⊢ (fun n => ⊤ ^ n) =ᶠ[atTop] fun x => ⊤

Tactic:
exact eventually_atTop.mpr ⟨1, fun _ hn ↦ pow_eq_top_iff.mpr ⟨rfl, Nat.pos_iff_ne_zero.mp hn⟩⟩

Result:
no goals

Proof state:
r : ℝ≥0∞
h : Tendsto (fun n => r ^ n) atTop (𝓝 0)
⊢ r < 1

Tactic:
lift r to NNReal

Result:
r : ℝ≥0∞
h : Tendsto (fun n => r ^ n) atTop (𝓝 0)
⊢ r ≠ ⊤

case intro
r : ℝ≥0
h : Tendsto (fun n => ↑r ^ n) atTop (𝓝 0)
⊢ ↑r < 1

Proof state:
r : ℝ≥0∞
⊢ Tendsto (fun n => r ^ n) atTop (𝓝 0) ↔ r < 1

Tactic:
refine ⟨fun h ↦ ?_, tendsto_pow_atTop_nhds_zero_of_lt_one⟩

Result:
r : ℝ≥0∞
h : Tendsto (fun n => r ^ n) atTop (𝓝 0)
⊢ r < 1
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
theorem denote_mkFullAdderCarry (assign : α → Bool) (aig : AIG α) (input : FullAdderInput aig) :
    ⟦mkFullAdderCarry aig input, assign⟧
      =
      ((⟦aig, input.lhs, assign⟧ ^^ ⟦aig, input.rhs, assign⟧) && ⟦aig, input.cin, assign⟧ ||
       ⟦aig, input.lhs, assign⟧ && ⟦aig, input.rhs, assign⟧)

Proof state:
case e_y.e_y
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ ⟦assign,
      {
        aig :=
          ((aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).aig.mkAndCached
              { lhs := (aig.mkXorCached { lhs := input.lhs, rhs := input.rhs }).ref,
                rhs := { gate := input.cin.gate, hgate := ⋯ } }).aig,
        ref := { gate := input.rhs.gate, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := input.rhs }⟧

Tactic:
rw [
  LawfulOperator.denote_mem_prefix
    (f := mkAndCached)
    (h := by
      apply LawfulOperator.lt_size_of_lt_aig_size (f := mkXorCached)
      apply Ref.hgate),
  LawfulOperator.denote_mem_prefix (f := mkXorCached) (h := input.rhs.hgate)]

Result:
no goals

Proof state:
case h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : FullAdderInput aig
⊢ input.lhs.gate < aig.decls.size

Tactic:
apply Ref.hgate

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem norm_iteratedFDerivWithin_one (f : E → F) (h : UniqueDiffWithinAt 𝕜 s x) :
    ‖iteratedFDerivWithin 𝕜 1 f s x‖ = ‖fderivWithin 𝕜 f s x‖

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
x : E
f : E → F
h : UniqueDiffWithinAt 𝕜 s x
⊢ ‖(↑{ toLinearEquiv := (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearEquiv, continuous_toFun := ⋯,
              continuous_invFun := ⋯ }).comp
        (fderivWithin 𝕜 f s x)‖ =
    ‖fderivWithin 𝕜 f s x‖

Tactic:
apply (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearIsometry.norm_toContinuousLinearMap_comp

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
x : E
f : E → F
h : UniqueDiffWithinAt 𝕜 s x
⊢ ‖iteratedFDerivWithin 𝕜 1 f s x‖ = ‖fderivWithin 𝕜 f s x‖

Tactic:
simp only [← norm_fderivWithin_iteratedFDerivWithin,
  iteratedFDerivWithin_zero_eq_comp, LinearIsometryEquiv.comp_fderivWithin _ h]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
x : E
f : E → F
h : UniqueDiffWithinAt 𝕜 s x
⊢ ‖(↑{ toLinearEquiv := (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearEquiv, continuous_toFun := ⋯,
              continuous_invFun := ⋯ }).comp
        (fderivWithin 𝕜 f s x)‖ =
    ‖fderivWithin 𝕜 f s x‖
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_bound_div_one_sub_of_interval {x : ℝ} (h1 : 0 ≤ x) (h2 : x < 1) :
    Real.exp x ≤ 1 / (1 - x)

Proof state:
case inr
x : ℝ
h1✝ : 0 ≤ x
h2 : x < 1
h1 : 0 < x
⊢ rexp x ≤ 1 / (1 - x)

Tactic:
exact (exp_bound_div_one_sub_of_interval' h1 h2).le

Result:
no goals

Proof state:
x : ℝ
h1 : 0 ≤ x
h2 : x < 1
⊢ rexp x ≤ 1 / (1 - x)

Tactic:
rcases eq_or_lt_of_le h1 with (rfl | h1)

Result:
case inl
h1 : 0 ≤ 0
h2 : 0 < 1
⊢ rexp 0 ≤ 1 / (1 - 0)

case inr
x : ℝ
h1✝ : 0 ≤ x
h2 : x < 1
h1 : 0 < x
⊢ rexp x ≤ 1 / (1 - x)

Proof state:
case inl
h1 : 0 ≤ 0
h2 : 0 < 1
⊢ rexp 0 ≤ 1 / (1 - 0)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem forall_mem_filterMap {f : α → Option β} {l : Array α} {P : β → Prop} :
    (∀ (i) (_ : i ∈ filterMap f l), P i) ↔ ∀ (j) (_ : j ∈ l) (b), f j = some b → P b

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
P : β → Prop
a : α
⊢ (∀ (a_1 : β), a ∈ l → f a = some a_1 → P a_1) ↔ a ∈ l → ∀ (b : β), f a = some b → P b

Tactic:
rw [forall_comm]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
P : β → Prop
⊢ (∀ (b : α) (a : β), b ∈ l → f b = some a → P a) ↔ ∀ (j : α), j ∈ l → ∀ (b : β), f j = some b → P b

Tactic:
apply forall_congr'

Result:
case h
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
P : β → Prop
⊢ ∀ (a : α), (∀ (a_1 : β), a ∈ l → f a = some a_1 → P a_1) ↔ a ∈ l → ∀ (b : β), f a = some b → P b

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
P : β → Prop
⊢ (∀ (i : β), i ∈ filterMap f l → P i) ↔ ∀ (j : α), j ∈ l → ∀ (b : β), f j = some b → P b

Tactic:
simp only [mem_filterMap, forall_exists_index, and_imp]

Result:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
P : β → Prop
⊢ (∀ (i : β) (x : α), x ∈ l → f x = some i → P i) ↔ ∀ (j : α), j ∈ l → ∀ (b : β), f j = some b → P b

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
P : β → Prop
⊢ ∀ (a : α), (∀ (a_1 : β), a ∈ l → f a = some a_1 → P a_1) ↔ a ∈ l → ∀ (b : β), f a = some b → P b

Tactic:
intro a

Result:
case h
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
P : β → Prop
a : α
⊢ (∀ (a_1 : β), a ∈ l → f a = some a_1 → P a_1) ↔ a ∈ l → ∀ (b : β), f a = some b → P b

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
P : β → Prop
⊢ (∀ (i : β) (x : α), x ∈ l → f x = some i → P i) ↔ ∀ (j : α), j ∈ l → ∀ (b : β), f j = some b → P b

Tactic:
rw [forall_comm]

Result:
α : Type u_1
β : Type u_2
f : α → Option β
l : Array α
P : β → Prop
⊢ (∀ (b : α) (a : β), b ∈ l → f b = some a → P a) ↔ ∀ (j : α), j ∈ l → ∀ (b : β), f j = some b → P b
-- Mathlib/Topology/CWComplex/Classical/Basic.lean
lemma RelCWComplex.closed (C : Set X) {D : Set X} [RelCWComplex C D] [T2Space X] (A : Set X)
    (asubc : A ⊆ C) :
    IsClosed A ↔ (∀ n (j : cell C n), IsClosed (A ∩ closedCell n j)) ∧ IsClosed (A ∩ D)

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
asubc : A ⊆ C
⊢ IsClosed A ↔ (∀ (n : ℕ) (j : cell C n), IsClosed (A ∩ closedCell n j)) ∧ IsClosed (A ∩ D)

Tactic:
refine ⟨?_, closed' A asubc⟩

Result:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
asubc : A ⊆ C
⊢ IsClosed A → (∀ (n : ℕ) (j : cell C n), IsClosed (A ∩ closedCell n j)) ∧ IsClosed (A ∩ D)

Proof state:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
asubc : A ⊆ C
⊢ IsClosed A → (∀ (n : ℕ) (j : cell C n), IsClosed (A ∩ closedCell n j)) ∧ IsClosed (A ∩ D)

Tactic:
exact fun closedA ↦ ⟨fun _ _ ↦ closedA.inter isClosed_closedCell, closedA.inter (isClosedBase C)⟩

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_lt_neg_iff {x y : PGame} : -y < -x ↔ x < y

Proof state:
x y : PGame
⊢ -y < -x ↔ x < y

Tactic:
rw [lt_iff_le_and_lf, lt_iff_le_and_lf, neg_le_neg_iff, neg_lf_neg_iff]

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean
lemma hom_comp_singleFunctor_map_shift [HasDerivedCategory.{w'} C]
    {X Y Z : C} {n : ℕ} (x : Ext X Y n) (f : Y ⟶ Z) :
    x.hom ≫ ((DerivedCategory.singleFunctor C 0).map f)⟦(n : ℤ)⟧' =
      (x.comp (mk₀ f) (add_zero n)).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
inst✝ : HasDerivedCategory C
X Y Z : C
n : ℕ
x : Ext X Y n
f : Y ⟶ Z
⊢ x.hom ≫ (shiftFunctor (DerivedCategory C) ↑n).map ((singleFunctor C 0).map f) = (x.comp (mk₀ f) ⋯).hom

Tactic:
simp only [comp_hom, mk₀_hom, ShiftedHom.comp_mk₀]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
lemma map_le_of_subsingleton (f : V ↪ W) [Subsingleton V] : G.map f ≤ G'

Proof state:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V ↪ W
inst✝ : Subsingleton V
⊢ G ≤ SimpleGraph.comap (⇑f) G'

Tactic:
apply le_comap_of_subsingleton

Result:
no goals

Proof state:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V ↪ W
inst✝ : Subsingleton V
⊢ SimpleGraph.map f G ≤ G'

Tactic:
rw [map_le_iff_le_comap]

Result:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : V ↪ W
inst✝ : Subsingleton V
⊢ G ≤ SimpleGraph.comap (⇑f) G'
-- Mathlib/Data/List/Count.lean
lemma countP_erase (p : α → Bool) (l : List α) (a : α) :
    countP p (l.erase a) = countP p l - if a ∈ l ∧ p a then 1 else 0

Proof state:
α : Type u_1
inst✝ : DecidableEq α
p : α → Bool
l : List α
a : α
⊢ countP p (l.erase a) = countP p l - if a ∈ l ∧ p a = true then 1 else 0

Tactic:
rw [countP_eq_length_filter, countP_eq_length_filter, ← erase_filter, length_erase]

Result:
α : Type u_1
inst✝ : DecidableEq α
p : α → Bool
l : List α
a : α
⊢ (if a ∈ filter p l then (filter p l).length - 1 else (filter p l).length) =
    (filter p l).length - if a ∈ l ∧ p a = true then 1 else 0

Proof state:
α : Type u_1
inst✝ : DecidableEq α
p : α → Bool
l : List α
a : α
⊢ (if a ∈ filter p l then (filter p l).length - 1 else (filter p l).length) =
    (filter p l).length - if a ∈ l ∧ p a = true then 1 else 0

Tactic:
aesop

Result:
no goals
-- Mathlib/Probability/Martingale/BorelCantelli.lean
theorem Submartingale.stoppedValue_leastGE [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ) (r : ℝ) :
    Submartingale (fun i => stoppedValue f (leastGE f r i)) ℱ μ

Proof state:
case intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
r : ℝ
σ π : Ω → ℕ
hσ : IsStoppingTime ℱ σ
hπ : IsStoppingTime ℱ π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ n
⊢ ∫ (x : Ω), stoppedValue (stoppedProcess f (leastGE f r n)) σ x ∂μ ≤
    ∫ (x : Ω), stoppedValue (fun i => stoppedValue f (leastGE f r i)) π x ∂μ

Tactic:
simp_rw [stoppedValue_stoppedValue_leastGE f π r hπ_le_n]

Result:
case intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
r : ℝ
σ π : Ω → ℕ
hσ : IsStoppingTime ℱ σ
hπ : IsStoppingTime ℱ π
hσ_le_π : σ ≤ π
n : ℕ
hπ_le_n : ∀ (x : Ω), π x ≤ n
⊢ ∫ (x : Ω), stoppedValue (stoppedProcess f (leastGE f r n)) σ x ∂μ ≤
    ∫ (x : Ω), stoppedValue (stoppedProcess f (leastGE f r n)) π x ∂μ
-- Mathlib/Algebra/Polynomial/Eval/Degree.lean
theorem eval_eq_sum_range' {p : R[X]} {n : ℕ} (hn : p.natDegree < n) (x : R) :
    p.eval x = ∑ i ∈ Finset.range n, p.coeff i * x ^ i

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
x : R
⊢ eval x p = ∑ i ∈ range n, p.coeff i * x ^ i

Tactic:
rw [eval_eq_sum, p.sum_over_range' _ _ hn]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
x : R
⊢ ∀ (n : ℕ), 0 * x ^ n = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
x : R
⊢ ∀ (n : ℕ), 0 * x ^ n = 0

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Equivalence.lean
theorem unit_inverse_comp (e : C ≌ D) (Y : D) :
    e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫
      (e.inverse.map (e.counitInv.app (e.functor.obj (e.inverse.obj Y))) ≫
          e.unitIso.hom.app
              (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y))))) ≫
            e.unitIso.inv.app
                (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y))))) ≫
              e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
        e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)

Tactic:
slice_lhs 2 3 => erw [e.unit.naturality]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
Y : D
⊢ e.unit.app (e.inverse.obj Y) ≫
      (((e.unit.app (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj Y))) ≫
              (e.functor ⋙ e.inverse).map
                (e.inverse.toPrefunctor.2 (e.counitInv.app (e.functor.obj (e.inverse.obj Y))))) ≫
            e.unitIso.inv.app
              (e.inverse.toPrefunctor.1 (e.functor.obj (e.inverse.obj (e.functor.obj (e.inverse.obj Y)))))) ≫
          e.inverse.map (e.functor.map (e.unitInv.app (e.inverse.obj Y)))) ≫
        e.inverse.map (e.counit.app Y) =
    𝟙 (e.inverse.obj Y)
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem nthRoots_one_eq_biUnion_primitiveRoots [DecidableEq R] {n : ℕ} :
    nthRootsFinset n R = (Nat.divisors n).biUnion fun i ↦ primitiveRoots i R

Proof state:
case pos
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
hn : n = 0
⊢ nthRootsFinset n R = n.divisors.biUnion fun i => primitiveRoots i R

Tactic:
simp only [hn, nthRootsFinset_zero, Nat.divisors_zero, biUnion_empty]

Result:
no goals

Proof state:
case neg
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
hn : ¬n = 0
⊢ nthRootsFinset n R = n.divisors.biUnion fun i => primitiveRoots i R

Tactic:
have : NeZero n := ⟨hn⟩

Result:
case neg
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
hn : ¬n = 0
this : NeZero n
⊢ nthRootsFinset n R = n.divisors.biUnion fun i => primitiveRoots i R

Proof state:
case neg
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
hn : ¬n = 0
this : NeZero n
⊢ nthRootsFinset n R = n.divisors.biUnion fun i => primitiveRoots i R

Tactic:
exact nthRoots_one_eq_biUnion_primitiveRoots'

Result:
no goals

Proof state:
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
⊢ nthRootsFinset n R = n.divisors.biUnion fun i => primitiveRoots i R

Tactic:
by_cases hn : n = 0

Result:
case pos
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
hn : n = 0
⊢ nthRootsFinset n R = n.divisors.biUnion fun i => primitiveRoots i R

case neg
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : DecidableEq R
n : ℕ
hn : ¬n = 0
⊢ nthRootsFinset n R = n.divisors.biUnion fun i => primitiveRoots i R