harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem log2_two_pow : (2 ^ n).log2 = n

Proof state:
n : Nat
⊢ (2 ^ n).log2 = n

Tactic:
apply Nat.eq_of_le_of_lt_succ <;> simp [le_log2, log2_lt, NeZero.ne, Nat.pow_lt_pow_iff_right]

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem reflTransGen_eq_self (refl : Reflexive r) (trans : Transitive r) : ReflTransGen r = r :=
  funext fun a ↦ funext fun b ↦ propext <|
    ⟨fun h ↦ by
      induction h with
      | refl => apply refl
      | tail _ h₂ IH => exact trans IH h₂, single⟩

Proof state:
case tail
α : Type u_1
r : α → α → Prop
refl : Reflexive r
trans : Transitive r
a b b✝ c✝ : α
a✝ : ReflTransGen r a b✝
h₂ : r b✝ c✝
IH : r a b✝
⊢ r a c✝

Tactic:
exact trans IH h₂

Result:
no goals

Proof state:
case refl
α : Type u_1
r : α → α → Prop
refl : Reflexive r
trans : Transitive r
a b : α
⊢ r a a

Tactic:
apply refl

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
refl : Reflexive r
trans : Transitive r
a b : α
h : ReflTransGen r a b
⊢ r a b

Tactic:
induction h with
| refl => apply refl
| tail _ h₂ IH => exact trans IH h₂

Result:
no goals
-- Mathlib/Data/List/Destutter.lean
theorem destutter_eq_self_iff : ∀ l : List α, l.destutter R = l ↔ l.Chain' R
  | [] => by simp
  | a :: l => l.destutter'_eq_self_iff R a

Proof state:
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
⊢ destutter R [] = [] ↔ Chain' R []

Tactic:
simp

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem blimsup_or_eq_sup : (blimsup u f fun x => p x ∨ q x) = blimsup u f p ⊔ blimsup u f q

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ (blimsup u f fun x => p x ∨ q x) = blimsup u f p ⊔ blimsup u f q

Tactic:
simp only [blimsup_eq_limsup, ← limsup_sup_filter, ← inf_sup_left, sup_principal, setOf_or]

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem sameRay_neg_smul_right_iff_of_ne {v : M} {r : R} (hv : v ≠ 0) (hr : r ≠ 0) :
    SameRay R (-v) (r • v) ↔ r < 0

Proof state:
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
v : M
r : R
hv : v ≠ 0
hr : r ≠ 0
⊢ SameRay R (-v) (r • v) ↔ r < 0

Tactic:
simp only [sameRay_neg_smul_right_iff, hv, or_false, hr.le_iff_lt]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Instances.lean
theorem coe_eq_zero [Nontrivial α] {x : Ico (0 : α) 1} : (x : α) = 0 ↔ x = 0

Proof state:
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Nontrivial α
x : ↑(Ico 0 1)
⊢ ↑x = 0 ↔ x = 0

Tactic:
symm

Result:
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Nontrivial α
x : ↑(Ico 0 1)
⊢ x = 0 ↔ ↑x = 0

Proof state:
α : Type u_1
inst✝¹ : OrderedSemiring α
inst✝ : Nontrivial α
x : ↑(Ico 0 1)
⊢ x = 0 ↔ ↑x = 0

Tactic:
exact Subtype.ext_iff

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degreeOf_pow_le (i : σ) (p : MvPolynomial σ R) (n : ℕ) :
    degreeOf i (p ^ n) ≤ n * degreeOf i p

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i : σ
p : MvPolynomial σ R
n : ℕ
⊢ degreeOf i (p ^ n) ≤ n * degreeOf i p

Tactic:
simpa using degreeOf_prod_le i (Finset.range n) (fun _ => p)

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem range_coe_eq_Ioo : range Real.toEReal = Ioo ⊥ ⊤

Proof state:
case h
x : EReal
⊢ x ∈ range Real.toEReal ↔ x ∈ Ioo ⊥ ⊤

Tactic:
induction x <;> simp

Result:
no goals

Proof state:
⊢ range Real.toEReal = Ioo ⊥ ⊤

Tactic:
ext x

Result:
case h
x : EReal
⊢ x ∈ range Real.toEReal ↔ x ∈ Ioo ⊥ ⊤
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem mk'_mem_edges_singleton {u v : V} (h : G.Adj u v) :
    s(u, v) ∈ (singleton h : G.Walk u v).edges

Proof state:
V : Type u
G : SimpleGraph V
u v : V
h : G.Adj u v
⊢ s(u, v) ∈ (↑(singleton h)).edges

Tactic:
simp [singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem shiftLeft_eq_zero {x : BitVec w} {n : Nat} (hn : w ≤ n) : x <<< n = 0#w

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : w ≤ n
⊢ x <<< n = 0#w

Tactic:
ext i hi

Result:
case pred
w : Nat
x : BitVec w
n : Nat
hn : w ≤ n
i : Nat
hi : i < w
⊢ (x <<< n).getLsbD i = (0#w).getLsbD i

Proof state:
case pred
w : Nat
x : BitVec w
n : Nat
hn : w ≤ n
i : Nat
hi : i < w
⊢ (x <<< n).getLsbD i = (0#w).getLsbD i

Tactic:
simp [hn, hi]

Result:
case pred
w : Nat
x : BitVec w
n : Nat
hn : w ≤ n
i : Nat
hi : i < w
⊢ n ≤ i → x.getLsbD (i - n) = false

Proof state:
case pred
w : Nat
x : BitVec w
n : Nat
hn : w ≤ n
i : Nat
hi : i < w
⊢ n ≤ i → x.getLsbD (i - n) = false

Tactic:
omega

Result:
no goals
-- Mathlib/NumberTheory/LSeries/RiemannZeta.lean
lemma riemannZeta_def_of_ne_zero {s : ℂ} (hs : s ≠ 0) :
    riemannZeta s = completedRiemannZeta s / Gammaℝ s

Proof state:
s : ℂ
hs : s ≠ 0
⊢ riemannZeta s = completedRiemannZeta s / s.Gammaℝ

Tactic:
rw [riemannZeta, hurwitzZetaEven, Function.update_of_ne hs, completedHurwitzZetaEven_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem Nat.lt_eq (a b : Nat) : (a < b) = (a + 1 ≤ b)

Proof state:
a b : Nat
⊢ (a < b) = (a + 1 ≤ b)

Tactic:
simp [Nat.lt, LT.lt]

Result:
no goals
-- Mathlib/Data/Fintype/Sets.lean
theorem mem_toFinset {s : Set α} [Fintype s] {a : α} : a ∈ s.toFinset ↔ a ∈ s

Proof state:
α : Type u_1
s : Set α
inst✝ : Fintype ↑s
a : α
⊢ a ∈ s.toFinset ↔ a ∈ s

Tactic:
simp [toFinset]

Result:
no goals
-- Mathlib/Data/Real/Cardinality.lean
theorem cantorFunctionAux_eq (h : f n = g n) :
    cantorFunctionAux c f n = cantorFunctionAux c g n

Proof state:
c : ℝ
f g : ℕ → Bool
n : ℕ
h : f n = g n
⊢ cantorFunctionAux c f n = cantorFunctionAux c g n

Tactic:
simp [cantorFunctionAux, h]

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem IsTopologicalBasis.mem_closure_iff {b : Set (Set α)} (hb : IsTopologicalBasis b) {s : Set α}
    {a : α} : a ∈ closure s ↔ ∀ o ∈ b, a ∈ o → (o ∩ s).Nonempty :=
  (mem_closure_iff_nhds_basis' hb.nhds_hasBasis).trans <| by simp only [and_imp]

Proof state:
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
a : α
⊢ (∀ (i : Set α), i ∈ b ∧ a ∈ i → (i ∩ s).Nonempty) ↔ ∀ o ∈ b, a ∈ o → (o ∩ s).Nonempty

Tactic:
simp only [and_imp]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Completion.lean
theorem uniformity_dist : 𝓤 (Completion α) = ⨅ ε > 0, 𝓟 { p | dist p.1 p.2 < ε }

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
⊢ 𝓤 (Completion α) = ⨅ ε, ⨅ (_ : ε > 0), 𝓟 {p | dist p.1 p.2 < ε}

Tactic:
simpa [iInf_subtype] using @Completion.uniformity_dist' α _

Result:
no goals
-- Mathlib/Order/BoundedOrder/Basic.lean
theorem coe_eq_top_iff [OrderTop α] [OrderTop (Subtype p)] (htop : p ⊤) {x : { x // p x }} :
    (x : α) = ⊤ ↔ x = ⊤

Proof state:
α : Type u
p : α → Prop
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : OrderTop (Subtype p)
htop : p ⊤
x : { x // p x }
⊢ ↑x = ⊤ ↔ x = ⊤

Tactic:
rw [← coe_top htop, Subtype.ext_iff]

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma CompleteOrthogonalIdempotents.equiv {J} [Fintype J] (i : J ≃ I) :
    CompleteOrthogonalIdempotents (e ∘ i) ↔ CompleteOrthogonalIdempotents e

Proof state:
R : Type u_1
inst✝² : Semiring R
I : Type u_3
e : I → R
inst✝¹ : Fintype I
J : Type u_4
inst✝ : Fintype J
i : J ≃ I
⊢ CompleteOrthogonalIdempotents (e ∘ ⇑i) ↔ CompleteOrthogonalIdempotents e

Tactic:
simp only [completeOrthogonalIdempotents_iff, OrthogonalIdempotents.equiv, Function.comp_apply,
  and_congr_right_iff, Fintype.sum_equiv i _ e (fun _ ↦ rfl)]

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rtake_concat_succ (x : α) : rtake (l ++ [x]) (n + 1) = rtake l n ++ [x]

Proof state:
α : Type u_1
l : List α
n : ℕ
x : α
⊢ (l ++ [x]).rtake (n + 1) = l.rtake n ++ [x]

Tactic:
simp [rtake_eq_reverse_take_reverse]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem map_mk_nhdsSet : map mk (𝓝ˢ s) = 𝓝ˢ (mk '' s)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ Filter.map mk (𝓝ˢ s) = 𝓝ˢ (mk '' s)

Tactic:
rw [← comap_mk_nhdsSet_image, map_comap_of_surjective surjective_mk]

Result:
no goals
-- Mathlib/RingTheory/PolynomialAlgebra.lean
theorem right_inv (x : A[X]) : (toFunAlgHom R A) (invFun R A x) = x

Proof state:
case refine_1
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ∀ (p q : A[X]),
    (toFunAlgHom R A) (invFun R A p) = p →
      (toFunAlgHom R A) (invFun R A q) = q → (toFunAlgHom R A) (invFun R A (p + q)) = p + q

Tactic:
intro p q hp hq

Result:
case refine_1
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x p q : A[X]
hp : (toFunAlgHom R A) (invFun R A p) = p
hq : (toFunAlgHom R A) (invFun R A q) = q
⊢ (toFunAlgHom R A) (invFun R A (p + q)) = p + q

Proof state:
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ (toFunAlgHom R A) (invFun R A ((monomial n) a)) = (monomial n) a

Tactic:
rw [invFun_monomial, Algebra.TensorProduct.tmul_pow,
    one_pow, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, toFunAlgHom_apply_tmul,
    X_pow_eq_monomial, sum_monomial_index] <;>
  simp

Result:
no goals

Proof state:
case refine_1
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x p q : A[X]
hp : (toFunAlgHom R A) (invFun R A p) = p
hq : (toFunAlgHom R A) (invFun R A q) = q
⊢ (toFunAlgHom R A) (invFun R A (p + q)) = p + q

Tactic:
simp only [invFun_add, map_add, hp, hq]

Result:
no goals

Proof state:
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ∀ (n : ℕ) (a : A), (toFunAlgHom R A) (invFun R A ((monomial n) a)) = (monomial n) a

Tactic:
intro n a

Result:
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ (toFunAlgHom R A) (invFun R A ((monomial n) a)) = (monomial n) a

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ (toFunAlgHom R A) (invFun R A x) = x

Tactic:
refine Polynomial.induction_on' x ?_ ?_

Result:
case refine_1
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ∀ (p q : A[X]),
    (toFunAlgHom R A) (invFun R A p) = p →
      (toFunAlgHom R A) (invFun R A q) = q → (toFunAlgHom R A) (invFun R A (p + q)) = p + q

case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ∀ (n : ℕ) (a : A), (toFunAlgHom R A) (invFun R A ((monomial n) a)) = (monomial n) a
-- Mathlib/Order/SuccPred/Limit.lean
theorem IsSuccPrelimit.lt_iff_exists_lt (h : IsSuccPrelimit b) : a < b ↔ ∃ c < b, a < c

Proof state:
α : Type u_1
a b : α
inst✝ : LinearOrder α
h : IsSuccPrelimit b
⊢ a < b ↔ ∃ c < b, a < c

Tactic:
rw [← not_iff_not]

Result:
α : Type u_1
a b : α
inst✝ : LinearOrder α
h : IsSuccPrelimit b
⊢ ¬a < b ↔ ¬∃ c < b, a < c

Proof state:
α : Type u_1
a b : α
inst✝ : LinearOrder α
h : IsSuccPrelimit b
⊢ ¬a < b ↔ ¬∃ c < b, a < c

Tactic:
simp [h.le_iff_forall_le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem all_eq_not_any_not {p : α → Bool} {xs : Vector α n} :
    xs.all p = !(xs.any (!p ·))

Proof state:
α : Type u_1
n : Nat
p : α → Bool
xs : Vector α n
⊢ xs.all p = !xs.any fun x => !p x

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ { toArray := xs, size_toArray := ⋯ }.all p = !{ toArray := xs, size_toArray := ⋯ }.any fun x => !p x

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : Array α
⊢ { toArray := xs, size_toArray := ⋯ }.all p = !{ toArray := xs, size_toArray := ⋯ }.any fun x => !p x

Tactic:
simp [Array.all_eq_not_any_not]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Pretopology.lean
lemma mem_sInf (T : Set (Pretopology C)) {X : C} (S : Presieve X) :
    S ∈ sInf T X ↔ ∀ t ∈ T, S ∈ t X

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
T : Set (Pretopology C)
X : C
S : Presieve X
⊢ S ∈ sInf (coverings '' T) X ↔ ∀ t ∈ T, S ∈ t.coverings X

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
T : Set (Pretopology C)
X : C
S : Presieve X
⊢ S ∈ (sInf T).coverings X ↔ ∀ t ∈ T, S ∈ t.coverings X

Tactic:
show S ∈ sInf (Pretopology.coverings '' T) X ↔ _

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
T : Set (Pretopology C)
X : C
S : Presieve X
⊢ S ∈ sInf (coverings '' T) X ↔ ∀ t ∈ T, S ∈ t.coverings X
-- Mathlib/Data/Nat/Log.lean
lemma log_le_self (b x : ℕ) : log b x ≤ x :=
  if hx : x = 0 then by simp [hx]
  else (log_lt_self b hx).le

Proof state:
b x : ℕ
hx : x = 0
⊢ log b x ≤ x

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigOWith_congr (e : PartialHomeomorph α β) {b : β} (hb : b ∈ e.target) {f : β → E}
    {g : β → F} {C : ℝ} : IsBigOWith C (𝓝 b) f g ↔ IsBigOWith C (𝓝 (e.symm b)) (f ∘ e) (g ∘ e) :=
  ⟨fun h =>
    h.comp_tendsto <| by
      have := e.continuousAt (e.map_target hb)
      rwa [ContinuousAt, e.rightInvOn hb] at this,
    fun h =>
    (h.comp_tendsto (e.continuousAt_symm hb)).congr' rfl
      ((e.eventually_right_inverse hb).mono fun _ hx => congr_arg f hx)
      ((e.eventually_right_inverse hb).mono fun _ hx => congr_arg g hx)⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : PartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
C : ℝ
h : IsBigOWith C (𝓝 b) f g
this : ContinuousAt (↑e) (↑e.symm b)
⊢ Tendsto (↑e) (𝓝 (↑e.symm b)) (𝓝 b)

Tactic:
rwa [ContinuousAt, e.rightInvOn hb] at this

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : PartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
C : ℝ
h : IsBigOWith C (𝓝 b) f g
⊢ Tendsto (↑e) (𝓝 (↑e.symm b)) (𝓝 b)

Tactic:
have := e.continuousAt (e.map_target hb)

Result:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
E : Type u_3
inst✝¹ : Norm E
F : Type u_4
inst✝ : Norm F
e : PartialHomeomorph α β
b : β
hb : b ∈ e.target
f : β → E
g : β → F
C : ℝ
h : IsBigOWith C (𝓝 b) f g
this : ContinuousAt (↑e) (↑e.symm b)
⊢ Tendsto (↑e) (𝓝 (↑e.symm b)) (𝓝 b)
-- Mathlib/Algebra/Group/Int/Units.lean
lemma isUnit_add_isUnit_eq_isUnit_add_isUnit {a b c d : ℤ} (ha : IsUnit a) (hb : IsUnit b)
    (hc : IsUnit c) (hd : IsUnit d) : a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c

Proof state:
a b c d : ℤ
ha : a = 1 ∨ a = -1
hb : b = 1 ∨ b = -1
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c

Tactic:
aesop

Result:
no goals

Proof state:
a b c d : ℤ
ha : IsUnit a
hb : IsUnit b
hc : IsUnit c
hd : IsUnit d
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c

Tactic:
rw [isUnit_iff] at ha hb hc hd

Result:
a b c d : ℤ
ha : a = 1 ∨ a = -1
hb : b = 1 ∨ b = -1
hc : c = 1 ∨ c = -1
hd : d = 1 ∨ d = -1
⊢ a + b = c + d ↔ a = c ∧ b = d ∨ a = d ∧ b = c
-- Mathlib/Topology/Hom/ContinuousEval.lean
theorem ContinuousEval.of_continuous_forget {F' : Type*} [FunLike F' X Y] [TopologicalSpace F']
    {f : F' → F} (hc : Continuous f) (hf : ∀ g, ⇑(f g) = g

Proof state:
F : Type u_1
X : Type u_2
Y : Type u_3
inst✝⁶ : FunLike F X Y
inst✝⁵ : TopologicalSpace F
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : ContinuousEval F X Y
F' : Type u_5
inst✝¹ : FunLike F' X Y
inst✝ : TopologicalSpace F'
f : F' → F
hc : Continuous f
hf : autoParam (∀ (g : F'), ⇑(f g) = ⇑g) _auto✝
⊢ Continuous fun fx => fx.1 fx.2

Tactic:
simpa only [← hf] using hc.fst'.eval continuous_snd

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem two_pow_pred_mul_two (h : 0 < w) :
    2 ^ (w - 1) * 2 = 2 ^ w

Proof state:
w : Nat
h : 0 < w
⊢ 2 ^ (w - 1) * 2 = 2 ^ w

Tactic:
simp [← Nat.pow_succ, Nat.sub_add_cancel h]

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem pathComponentIn_congr (h : x ∈ pathComponentIn y F) :
    pathComponentIn x F = pathComponentIn y F

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ∈ pathComponentIn y F
⊢ pathComponentIn x F = pathComponentIn y F

Tactic:
ext

Result:
case h
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ∈ pathComponentIn y F
x✝ : X
⊢ x✝ ∈ pathComponentIn x F ↔ x✝ ∈ pathComponentIn y F

Proof state:
case h
X : Type u_1
inst✝ : TopologicalSpace X
x y : X
F : Set X
h : x ∈ pathComponentIn y F
x✝ : X
⊢ x✝ ∈ pathComponentIn x F ↔ x✝ ∈ pathComponentIn y F

Tactic:
exact ⟨h.trans, h.symm.trans⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem prod_apply (i) :
    b.prod b' i = Sum.elim (LinearMap.inl R M M' ∘ b) (LinearMap.inr R M M' ∘ b') i

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι ⊕ ι'
⊢ (b.prod b') i = Sum.elim (⇑(LinearMap.inl R M M') ∘ ⇑b) (⇑(LinearMap.inr R M M') ∘ ⇑b') i

Tactic:
ext <;> cases i <;>
  simp only [prod_apply_inl_fst, Sum.elim_inl, LinearMap.inl_apply, prod_apply_inr_fst,
    Sum.elim_inr, LinearMap.inr_apply, prod_apply_inl_snd, prod_apply_inr_snd, Function.comp]

Result:
no goals
-- Mathlib/Data/List/ReduceOption.lean
theorem reduceOption_getElem?_iff {l : List (Option α)} {x : α} :
    (∃ i : ℕ, l[i]? = some (some x)) ↔ ∃ i : ℕ, l.reduceOption[i]? = some x

Proof state:
α : Type u_1
l : List (Option α)
x : α
⊢ (∃ i, l[i]? = some (some x)) ↔ ∃ i, l.reduceOption[i]? = some x

Tactic:
rw [← mem_iff_getElem?, ← mem_iff_getElem?, reduceOption_mem_iff]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem eventually_mem_of_tendsto_nhdsWithin {f : β → α} {a : α} {s : Set α} {l : Filter β}
    (h : Tendsto f l (𝓝[s] a)) : ∀ᶠ i in l, f i ∈ s

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : Tendsto f l (𝓝[s] a)
⊢ ∀ᶠ (i : β) in l, f i ∈ s

Tactic:
simp_rw [nhdsWithin_eq, tendsto_iInf, mem_setOf_eq, tendsto_principal, mem_inter_iff,
  eventually_and] at h

Result:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : ∀ (i : Set α), a ∈ i ∧ IsOpen i → (∀ᶠ (x : β) in l, f x ∈ i) ∧ ∀ᶠ (x : β) in l, f x ∈ s
⊢ ∀ᶠ (i : β) in l, f i ∈ s

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace α
f : β → α
a : α
s : Set α
l : Filter β
h : ∀ (i : Set α), a ∈ i ∧ IsOpen i → (∀ᶠ (x : β) in l, f x ∈ i) ∧ ∀ᶠ (x : β) in l, f x ∈ s
⊢ ∀ᶠ (i : β) in l, f i ∈ s

Tactic:
exact (h univ ⟨mem_univ a, isOpen_univ⟩).2

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem splits_prod_iff {ι : Type u} {s : ι → K[X]} {t : Finset ι} :
    (∀ j ∈ t, s j ≠ 0) → ((∏ x ∈ t, s x).Splits i ↔ ∀ j ∈ t, (s j).Splits i)

Proof state:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
ι : Type u
s : ι → K[X]
t : Finset ι
⊢ (∀ j ∈ t, s j ≠ 0) → (Splits i (∏ x ∈ t, s x) ↔ ∀ j ∈ t, Splits i (s j))

Tactic:
refine
  Finset.induction_on t (fun _ =>
      ⟨fun _ _ h => by simp only [Finset.not_mem_empty] at h, fun _ => splits_one i⟩)
    fun a t hat ih ht => ?_

Result:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : a ∉ t
ih : (∀ j ∈ t, s j ≠ 0) → (Splits i (∏ x ∈ t, s x) ↔ ∀ j ∈ t, Splits i (s j))
ht : ∀ j ∈ insert a t, s j ≠ 0
⊢ Splits i (∏ x ∈ insert a t, s x) ↔ ∀ j ∈ insert a t, Splits i (s j)

Proof state:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : a ∉ t
ih : (∀ j ∈ t, s j ≠ 0) → (Splits i (∏ x ∈ t, s x) ↔ ∀ j ∈ t, Splits i (s j))
ht : ∀ j ∈ insert a t, s j ≠ 0
⊢ Splits i (∏ x ∈ insert a t, s x) ↔ ∀ j ∈ insert a t, Splits i (s j)

Tactic:
rw [Finset.forall_mem_insert] at ht ⊢

Result:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : a ∉ t
ih : (∀ j ∈ t, s j ≠ 0) → (Splits i (∏ x ∈ t, s x) ↔ ∀ j ∈ t, Splits i (s j))
ht : s a ≠ 0 ∧ ∀ x ∈ t, s x ≠ 0
⊢ Splits i (∏ x ∈ insert a t, s x) ↔ Splits i (s a) ∧ ∀ x ∈ t, Splits i (s x)

Proof state:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
ι : Type u
s : ι → K[X]
t✝ : Finset ι
a : ι
t : Finset ι
hat : a ∉ t
ih : (∀ j ∈ t, s j ≠ 0) → (Splits i (∏ x ∈ t, s x) ↔ ∀ j ∈ t, Splits i (s j))
ht : s a ≠ 0 ∧ ∀ x ∈ t, s x ≠ 0
⊢ Splits i (∏ x ∈ insert a t, s x) ↔ Splits i (s a) ∧ ∀ x ∈ t, Splits i (s x)

Tactic:
rw [Finset.prod_insert hat, splits_mul_iff i ht.1 (Finset.prod_ne_zero_iff.2 ht.2), ih ht.2]

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
ι : Type u
s : ι → K[X]
t : Finset ι
x✝² : ∀ j ∈ ∅, s j ≠ 0
x✝¹ : Splits i (∏ x ∈ ∅, s x)
x✝ : ι
h : x✝ ∈ ∅
⊢ Splits i (s x✝)

Tactic:
simp only [Finset.not_mem_empty] at h

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
ι : Type u
s : ι → K[X]
t : Finset ι
⊢ (∀ j ∈ t, s j ≠ 0) → (Splits i (∏ x ∈ t, s x) ↔ ∀ j ∈ t, Splits i (s j))

Tactic:
classical
refine
  Finset.induction_on t (fun _ =>
      ⟨fun _ _ h => by simp only [Finset.not_mem_empty] at h, fun _ => splits_one i⟩)
    fun a t hat ih ht => ?_
rw [Finset.forall_mem_insert] at ht ⊢
rw [Finset.prod_insert hat, splits_mul_iff i ht.1 (Finset.prod_ne_zero_iff.2 ht.2), ih ht.2]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem monic_monomial_eq (m) :
    monomial m (1 : R) = (m.prod fun n e => X n ^ e : MvPolynomial σ R)

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m : σ →₀ ℕ
⊢ (monomial m) 1 = m.prod fun n e => X n ^ e

Tactic:
simp [monomial_eq]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
theorem coeff_scaleRoots (p : R[X]) (s : R) (i : ℕ) :
    (scaleRoots p s).coeff i = coeff p i * s ^ (p.natDegree - i)

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
i : ℕ
⊢ (p.scaleRoots s).coeff i = p.coeff i * s ^ (p.natDegree - i)

Tactic:
simp +contextual [scaleRoots, coeff_monomial]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean
theorem inr_pushoutZeroZeroIso_inv (X Y : C) [HasBinaryCoproduct X Y] :
    coprod.inr ≫ (pushoutZeroZeroIso X Y).inv = pushout.inr _ _

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ coprod.inr ≫ (pushoutZeroZeroIso X Y).inv = pushout.inr 0 0

Tactic:
simp [Iso.comp_inv_eq]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem coeff_expand_mul' {p : ℕ} (hp : 0 < p) (f : R[X]) (n : ℕ) :
    (expand R p f).coeff (p * n) = f.coeff n

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ ((expand R p) f).coeff (p * n) = f.coeff n

Tactic:
rw [mul_comm, coeff_expand_mul hp]

Result:
no goals
-- Mathlib/Analysis/Oscillation.lean
theorem oscillationWithin_nhd_eq_oscillation [TopologicalSpace E] (f : E → F) (D : Set E) (x : E)
    (hD : D ∈ 𝓝 x) : oscillationWithin f D x = oscillation f x

Proof state:
E : Type u
F : Type v
inst✝¹ : PseudoEMetricSpace F
inst✝ : TopologicalSpace E
f : E → F
D : Set E
x : E
hD : D ∈ 𝓝 x
⊢ oscillationWithin f D x = oscillation f x

Tactic:
rw [oscillation, oscillationWithin, nhdsWithin_eq_nhds.2 hD]

Result:
no goals
-- Mathlib/Data/Finset/Interval.lean
theorem card_Iio_finset : (Iio s).card = 2 ^ s.card - 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ #(Iio s) = 2 ^ #s - 1

Tactic:
rw [Iio_eq_ssubsets, ssubsets, card_erase_of_mem (mem_powerset_self _), card_powerset]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem List.norm_prod_le [NormOneClass α] : ∀ l : List α, ‖l.prod‖ ≤ (l.map norm).prod
  | [] => by simp
  | a::l => List.norm_prod_le' (List.cons_ne_nil a l)

Proof state:
α : Type u_2
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
⊢ ‖[].prod‖ ≤ (map norm []).prod

Tactic:
simp

Result:
no goals