harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
theorem trivializationAt_model_space_apply (p : TangentBundle I H) (x : H) :
    trivializationAt E (TangentSpace I) x p = (p.1, p.2)

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
x : H
this : fderivWithin 𝕜 (↑I ∘ ↑I.symm) (range ↑I) (↑I p.proj) = fderivWithin 𝕜 _root_.id (range ↑I) (↑I p.proj)
⊢ (fderivWithin 𝕜 (↑I ∘ ↑I.symm) (range ↑I) (↑I p.proj)) p.snd = p.snd

Tactic:
simp [this, fderivWithin_id (ModelWithCorners.uniqueDiffWithinAt_image I)]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
x : H
y : E
hy : y ∈ range ↑I
⊢ (↑I ∘ ↑I.symm) y = _root_.id y

Tactic:
simp [hy]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
x : H
⊢ (fderivWithin 𝕜 (↑I ∘ ↑I.symm) (range ↑I) (↑I p.proj)) p.snd = p.snd

Tactic:
have : fderivWithin 𝕜 (↑I ∘ ↑I.symm) (range I) (I p.proj) =
    fderivWithin 𝕜 id (range I) (I p.proj) :=
  fderivWithin_congr' (fun y hy ↦ by simp [hy]) (mem_range_self p.proj)

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
x : H
this : fderivWithin 𝕜 (↑I ∘ ↑I.symm) (range ↑I) (↑I p.proj) = fderivWithin 𝕜 _root_.id (range ↑I) (↑I p.proj)
⊢ (fderivWithin 𝕜 (↑I ∘ ↑I.symm) (range ↑I) (↑I p.proj)) p.snd = p.snd

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
x : H
⊢ ↑(trivializationAt E (TangentSpace I) x) p = (p.proj, p.snd)

Tactic:
simp [TangentBundle.trivializationAt_apply]

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
x : H
⊢ (fderivWithin 𝕜 (↑I ∘ ↑I.symm) (range ↑I) (↑I p.proj)) p.snd = p.snd
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem add_thirds (a : α) : a / 3 + a / 3 + a / 3 = a

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a : α
⊢ a / 3 + a / 3 + a / 3 = a

Tactic:
rw [div_add_div_same, div_add_div_same, ← two_mul, ← add_one_mul 2 a, two_add_one_eq_three,
  mul_div_cancel_left₀ a three_ne_zero]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Equiv.lean
/-- If `p` is a closed complemented submodule,
then there exists a submodule `q` and a continuous linear equivalence `M ≃L[R] (p × q)` such that
`e (x : p) = (x, 0)`, `e (y : q) = (0, y)`, and `e.symm x = x.1 + x.2`.

In fact, the properties of `e` imply the properties of `e.symm` and vice versa,
but we provide both for convenience. -/
lemma ClosedComplemented.exists_submodule_equiv_prod [IsTopologicalAddGroup M]
    {p : Submodule R M} (hp : p.ClosedComplemented) :
    ∃ (q : Submodule R M) (e : M ≃L[R] (p × q)),
      (∀ x : p, e x = (x, 0)) ∧ (∀ y : q, e y = (0, y)) ∧ (∀ x, e.symm x = x.1 + x.2) :=
  let ⟨f, hf⟩ := hp
  ⟨LinearMap.ker f, .equivOfRightInverse _ p.subtypeL hf,
    fun _ ↦ by ext <;> simp [hf], fun _ ↦ by ext <;> simp [hf], fun _ ↦ rfl⟩

Proof state:
R : Type u_3
inst✝⁴ : Ring R
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥p
⊢ (ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝ = (x✝, 0)

Tactic:
ext <;> simp [hf]

Result:
no goals

Proof state:
R : Type u_3
inst✝⁴ : Ring R
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x✝ : ↥(LinearMap.ker f)
⊢ (ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf) ↑x✝ = (0, x✝)

Tactic:
ext <;> simp [hf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_insertIfNew [LawfulBEq α] (h : m.1.WF) {k a : α} {fallback : β a} {v : β k} :
    (m.insertIfNew k v).getD a fallback =
      if h : k == a ∧ m.contains k = false then cast (congrArg β (eq_of_beq h.1)) v
      else m.getD a fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k a : α
fallback : β a
v : β k
⊢ (m.insertIfNew k v).getD a fallback =
    if h : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.getD a fallback

Tactic:
simp_to_model [insertIfNew] using List.getValueCastD_insertEntryIfNew

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_mul_le (p q : R[X]) : degree (p * q) ≤ degree p + degree q

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ (p * q).degree ≤ p.degree + q.degree

Tactic:
simpa only [degree, ← support_toFinsupp, toFinsupp_mul]
  using AddMonoidAlgebra.sup_support_mul_le (WithBot.coe_add _ _).le _ _

Result:
no goals
-- Mathlib/Data/DFinsupp/Order.lean
theorem coe_tsub (f g : Π₀ i, α i) : ⇑(f - g) = f - g

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → AddCommMonoid (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝¹ : (i : ι) → Sub (α i)
inst✝ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
⊢ ⇑(f - g) = ⇑f - ⇑g

Tactic:
ext i

Result:
case h
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → AddCommMonoid (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝¹ : (i : ι) → Sub (α i)
inst✝ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
⊢ (f - g) i = (⇑f - ⇑g) i

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : (i : ι) → AddCommMonoid (α i)
inst✝³ : (i : ι) → PartialOrder (α i)
inst✝² : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝¹ : (i : ι) → Sub (α i)
inst✝ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
⊢ (f - g) i = (⇑f - ⇑g) i

Tactic:
exact tsub_apply f g i

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
theorem LpAddConst_zero : LpAddConst 0 = 1

Proof state:
case hnc

⊢ 0 ∉ Set.Ioo 0 1

Tactic:
intro h

Result:
case hnc
h : 0 ∈ Set.Ioo 0 1
⊢ False

Proof state:
case hnc
h : 0 ∈ Set.Ioo 0 1
⊢ False

Tactic:
exact lt_irrefl _ h.1

Result:
no goals

Proof state:
⊢ LpAddConst 0 = 1

Tactic:
rw [LpAddConst, if_neg]

Result:
case hnc

⊢ 0 ∉ Set.Ioo 0 1
-- Mathlib/Topology/Connected/Basic.lean
theorem isPreconnected_univ_pi [∀ i, TopologicalSpace (π i)] {s : ∀ i, Set (π i)}
    (hs : ∀ i, IsPreconnected (s i)) : IsPreconnected (pi univ s)

Proof state:
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (π i)
s : (i : ι) → Set (π i)
hs : ∀ (i : ι), IsPreconnected (s i)
u v : Set ((i : ι) → π i)
uo : IsOpen u
vo : IsOpen v
hsuv : univ.pi s ⊆ u ∪ v
f : (i : ι) → π i
hfs : f ∈ univ.pi s
hfu : f ∈ u
g : (i : ι) → π i
hgs : g ∈ univ.pi s
hgv : g ∈ v
i : ι
I : Finset ι
a✝ : i ∉ I
ihI : I.piecewise f g ∈ u → (univ.pi s ∩ (u ∩ v)).Nonempty
hI : update (I.piecewise f g) i (f i) ∈ u
this : I.piecewise f g ∈ univ.pi s
h : I.piecewise f g ∈ v
S : Set ((a : ι) → π a) := update (I.piecewise f g) i '' s i
z : π i
hz : z ∈ s i
⊢ ∀ (j : ι), j ≠ i → I.piecewise f g j ∈ s j

Tactic:
exact fun j _ => this j trivial

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_apply₀ (ht : NullMeasurableSet t (μ.restrict s)) : μ.restrict s t = μ (t ∩ s)

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t (μ.restrict s)
⊢ (μ.restrict s) t = μ (t ∩ s)

Tactic:
rw [← restrictₗ_apply, restrictₗ, liftLinear_apply₀ _ ht, OuterMeasure.restrict_apply,
  coe_toOuterMeasure]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem pairwise_gt_iota (n : Nat) : Pairwise (· > ·) (iota n)

Proof state:
n : Nat
⊢ Pairwise (fun x1 x2 => x1 > x2) (iota n)

Tactic:
simpa only [iota_eq_reverse_range', pairwise_reverse] using pairwise_lt_range' 1 n

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem comap_neBot_iff {f : Filter β} {m : α → β} : NeBot (comap m f) ↔ ∀ t ∈ f, ∃ a, m a ∈ t

Proof state:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ (comap m f).NeBot ↔ ∀ t ∈ f, ∃ a, m a ∈ t

Tactic:
simp only [← forall_mem_nonempty_iff_neBot, mem_comap, forall_exists_index, and_imp]

Result:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ (∀ (s : Set α), ∀ x ∈ f, m ⁻¹' x ⊆ s → s.Nonempty) ↔ ∀ t ∈ f, ∃ a, m a ∈ t

Proof state:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ (∀ (s : Set α), ∀ x ∈ f, m ⁻¹' x ⊆ s → s.Nonempty) ↔ ∀ t ∈ f, ∃ a, m a ∈ t

Tactic:
exact ⟨fun h t t_in => h (m ⁻¹' t) t t_in Subset.rfl, fun h s t ht hst => (h t ht).imp hst⟩

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem mem_iff_infEdist_zero_of_closed (h : IsClosed s) : x ∈ s ↔ infEdist x s = 0

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
h : IsClosed s
⊢ x ∈ s ↔ infEdist x s = 0

Tactic:
rw [← mem_closure_iff_infEdist_zero, h.closure_eq]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem norm_mul (n m : ℤ√d) : norm (n * m) = norm n * norm m

Proof state:
d : ℤ
n m : ℤ√d
⊢ (n * m).norm = n.norm * m.norm

Tactic:
simp only [norm, mul_im, mul_re]

Result:
d : ℤ
n m : ℤ√d
⊢ (n.re * m.re + d * n.im * m.im) * (n.re * m.re + d * n.im * m.im) -
      d * (n.re * m.im + n.im * m.re) * (n.re * m.im + n.im * m.re) =
    (n.re * n.re - d * n.im * n.im) * (m.re * m.re - d * m.im * m.im)

Proof state:
d : ℤ
n m : ℤ√d
⊢ (n.re * m.re + d * n.im * m.im) * (n.re * m.re + d * n.im * m.im) -
      d * (n.re * m.im + n.im * m.re) * (n.re * m.im + n.im * m.re) =
    (n.re * n.re - d * n.im * n.im) * (m.re * m.re - d * m.im * m.im)

Tactic:
ring

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Ioo_cons_left (h : a < b) : a ::ₘ Ioo a b = Ico a b

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ a ::ₘ Ioo a b = Ico a b

Tactic:
classical
  rw [Ioo, ← Finset.insert_val_of_not_mem left_not_mem_Ioo, Finset.Ioo_insert_left h]
  rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ (Finset.Ico a b).val = Ico a b

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ a ::ₘ Ioo a b = Ico a b

Tactic:
rw [Ioo, ← Finset.insert_val_of_not_mem left_not_mem_Ioo, Finset.Ioo_insert_left h]

Result:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ (Finset.Ico a b).val = Ico a b
-- Mathlib/Topology/Semicontinuous.lean
theorem lowerSemicontinuousAt_ciSup {f : ι → α → δ'}
    (bdd : ∀ᶠ y in 𝓝 x, BddAbove (range fun i => f i y)) (h : ∀ i, LowerSemicontinuousAt (f i) x) :
    LowerSemicontinuousAt (fun x' => ⨆ i, f i x') x

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
ι : Sort u_3
δ' : Type u_5
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝 x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousAt (f i) x
⊢ LowerSemicontinuousAt (fun x' => ⨆ i, f i x') x

Tactic:
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
ι : Sort u_3
δ' : Type u_5
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝 x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') univ x

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
ι : Sort u_3
δ' : Type u_5
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝 x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') univ x

Tactic:
rw [← nhdsWithin_univ] at bdd

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
ι : Sort u_3
δ' : Type u_5
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[univ] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') univ x

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
x : α
ι : Sort u_3
δ' : Type u_5
inst✝ : ConditionallyCompleteLinearOrder δ'
f : ι → α → δ'
bdd : ∀ᶠ (y : α) in 𝓝[univ] x, BddAbove (range fun i => f i y)
h : ∀ (i : ι), LowerSemicontinuousWithinAt (f i) univ x
⊢ LowerSemicontinuousWithinAt (fun x' => ⨆ i, f i x') univ x

Tactic:
exact lowerSemicontinuousWithinAt_ciSup bdd h

Result:
no goals
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem inl_aut (g : G) (n : N) : (inl (φ g n) : N ⋊[φ] G) = inr g * inl n * inr g⁻¹

Proof state:
N : Type u_1
G : Type u_2
inst✝¹ : Group N
inst✝ : Group G
φ : G →* MulAut N
g : G
n : N
⊢ inl ((φ g) n) = inr g * inl n * inr g⁻¹

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Data/Int/Bitwise.lean
theorem bodd_add_div2 : ∀ n, cond (bodd n) 1 0 + 2 * div2 n = n
  | (n : ℕ) => by
    rw [show (cond (bodd n) 1 0 : ℤ) = (cond (bodd n) 1 0 : ℕ) by cases bodd n <;> rfl]
    exact congr_arg ofNat n.bodd_add_div2
  | -[n+1] => by
    refine Eq.trans ?_ (congr_arg negSucc n.bodd_add_div2)
    dsimp [bodd]; cases Nat.bodd n <;> dsimp [cond, not, div2, Int.mul]
    · change -[2 * Nat.div2 n+1] = _
      rw [zero_add]
    · rw [zero_add, add_comm]
      rfl

Proof state:
case true
n : ℕ
⊢ 0 + 2 * -[n.div2+1] = -[1 + 2 * n.div2+1]

Tactic:
rw [zero_add, add_comm]

Result:
case true
n : ℕ
⊢ 2 * -[n.div2+1] = -[2 * n.div2 + 1+1]

Proof state:
n : ℕ
⊢ (bif (↑n).bodd then 1 else 0) + 2 * (↑n).div2 = ↑n

Tactic:
rw [show (cond (bodd n) 1 0 : ℤ) = (cond (bodd n) 1 0 : ℕ) by cases bodd n <;> rfl]

Result:
n : ℕ
⊢ ↑(bif (↑n).bodd then 1 else 0) + 2 * (↑n).div2 = ↑n

Proof state:
n : ℕ
⊢ (bif -[n+1].bodd then 1 else 0) + 2 * -[n+1].div2 = -[n+1]

Tactic:
refine Eq.trans ?_ (congr_arg negSucc n.bodd_add_div2)

Result:
n : ℕ
⊢ (bif -[n+1].bodd then 1 else 0) + 2 * -[n+1].div2 = -[n.bodd.toNat + 2 * n.div2+1]

Proof state:
case false
n : ℕ
⊢ -[2 * n.div2+1] = -[0 + 2 * n.div2+1]

Tactic:
rw [zero_add]

Result:
no goals

Proof state:
n : ℕ
⊢ (bif (↑n).bodd then 1 else 0) = ↑(bif (↑n).bodd then 1 else 0)

Tactic:
cases bodd n <;> rfl

Result:
no goals

Proof state:
case true
n : ℕ
⊢ 2 * -[n.div2+1] = -[2 * n.div2 + 1+1]

Tactic:
rfl

Result:
no goals

Proof state:
case false
n : ℕ
⊢ 1 + 2 * -[n.div2+1] = -[0 + 2 * n.div2+1]

Tactic:
change -[2 * Nat.div2 n+1] = _

Result:
case false
n : ℕ
⊢ -[2 * n.div2+1] = -[0 + 2 * n.div2+1]

Proof state:
n : ℕ
⊢ (bif -[n+1].bodd then 1 else 0) + 2 * -[n+1].div2 = -[n.bodd.toNat + 2 * n.div2+1]

Tactic:
dsimp [bodd]

Result:
n : ℕ
⊢ (bif !n.bodd then 1 else 0) + 2 * -[n+1].div2 = -[n.bodd.toNat + 2 * n.div2+1]

Proof state:
n : ℕ
⊢ (bif !n.bodd then 1 else 0) + 2 * -[n+1].div2 = -[n.bodd.toNat + 2 * n.div2+1]

Tactic:
cases Nat.bodd n <;> dsimp [cond, not, div2, Int.mul]

Result:
case false
n : ℕ
⊢ 1 + 2 * -[n.div2+1] = -[0 + 2 * n.div2+1]

case true
n : ℕ
⊢ 0 + 2 * -[n.div2+1] = -[1 + 2 * n.div2+1]

Proof state:
n : ℕ
⊢ ↑(bif (↑n).bodd then 1 else 0) + 2 * (↑n).div2 = ↑n

Tactic:
exact congr_arg ofNat n.bodd_add_div2

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
protected lemma norm_pos {x : E} (hx : x ≠ 0) : 0 < ‖x‖

Proof state:
A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℂ E
inst✝² : SMul Aᵐᵒᵖ E
inst✝¹ : Norm E
inst✝ : CStarModule A E
x : E
hx : x ≠ 0
H : x = 0
⊢ False

Tactic:
exact hx H

Result:
no goals

Proof state:
A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℂ E
inst✝² : SMul Aᵐᵒᵖ E
inst✝¹ : Norm E
inst✝ : CStarModule A E
x : E
hx : x ≠ 0
H : inner x x = 0
⊢ False

Tactic:
rw [inner_self] at H

Result:
A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℂ E
inst✝² : SMul Aᵐᵒᵖ E
inst✝¹ : Norm E
inst✝ : CStarModule A E
x : E
hx : x ≠ 0
H : x = 0
⊢ False

Proof state:
A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℂ E
inst✝² : SMul Aᵐᵒᵖ E
inst✝¹ : Norm E
inst✝ : CStarModule A E
x : E
hx : x ≠ 0
⊢ inner x x ≠ 0

Tactic:
intro H

Result:
A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℂ E
inst✝² : SMul Aᵐᵒᵖ E
inst✝¹ : Norm E
inst✝ : CStarModule A E
x : E
hx : x ≠ 0
H : inner x x = 0
⊢ False

Proof state:
A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℂ E
inst✝² : SMul Aᵐᵒᵖ E
inst✝¹ : Norm E
inst✝ : CStarModule A E
x : E
hx : x ≠ 0
⊢ 0 < ‖x‖

Tactic:
simp only [norm_eq_sqrt_norm_inner_self, Real.sqrt_pos, norm_pos_iff]

Result:
A : Type u_1
E : Type u_2
inst✝⁶ : NonUnitalCStarAlgebra A
inst✝⁵ : PartialOrder A
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℂ E
inst✝² : SMul Aᵐᵒᵖ E
inst✝¹ : Norm E
inst✝ : CStarModule A E
x : E
hx : x ≠ 0
⊢ inner x x ≠ 0
-- Mathlib/Data/Real/Hyperreal.lean
theorem neg_lt_of_tendsto_zero_of_pos {f : ℕ → ℝ} (hf : Tendsto f atTop (𝓝 0)) :
    ∀ {r : ℝ}, 0 < r → (-r : ℝ*) < ofSeq f := fun hr =>
  have hg := hf.neg
  neg_lt_of_neg_lt (by rw [neg_zero] at hg; exact lt_of_tendsto_zero_of_pos hg hr)

Proof state:
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r✝ : ℝ
hr : 0 < r✝
hg : Tendsto (fun x => -f x) atTop (𝓝 (-0))
⊢ -ofSeq f < ↑r✝

Tactic:
rw [neg_zero] at hg

Result:
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r✝ : ℝ
hr : 0 < r✝
hg : Tendsto (fun x => -f x) atTop (𝓝 0)
⊢ -ofSeq f < ↑r✝

Proof state:
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r✝ : ℝ
hr : 0 < r✝
hg : Tendsto (fun x => -f x) atTop (𝓝 0)
⊢ -ofSeq f < ↑r✝

Tactic:
exact lt_of_tendsto_zero_of_pos hg hr

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem eq_prod_roots_of_splits {p : K[X]} {i : K →+* L} (hsplit : Splits i p) :
    p.map i = C (i p.leadingCoeff) * ((p.map i).roots.map fun a => X - C a).prod

Proof state:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ map i p = C (i p.leadingCoeff) * (Multiset.map (fun a => X - C a) (map i p).roots).prod

Tactic:
rw [← leadingCoeff_map]

Result:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ map i p = C (map i p).leadingCoeff * (Multiset.map (fun a => X - C a) (map i p).roots).prod

Proof state:
case hroots
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ (map i p).roots.card = (map i p).natDegree

Tactic:
rw [natDegree_map]

Result:
case hroots
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ (map i p).roots.card = p.natDegree

Proof state:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ C (map i p).leadingCoeff * (Multiset.map (fun a => X - C a) (map i p).roots).prod = map i p

Tactic:
apply C_leadingCoeff_mul_prod_multiset_X_sub_C

Result:
case hroots
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ (map i p).roots.card = (map i p).natDegree

Proof state:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ map i p = C (map i p).leadingCoeff * (Multiset.map (fun a => X - C a) (map i p).roots).prod

Tactic:
symm

Result:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ C (map i p).leadingCoeff * (Multiset.map (fun a => X - C a) (map i p).roots).prod = map i p

Proof state:
case hroots
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
p : K[X]
i : K →+* L
hsplit : Splits i p
⊢ (map i p).roots.card = p.natDegree

Tactic:
exact (natDegree_eq_card_roots hsplit).symm

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem dichotomy (p : ℝ≥0∞) [Fact (1 ≤ p)] : p = ∞ ∨ 1 ≤ p.toReal :=
  haveI : p = ⊤ ∨ 0 < p.toReal ∧ 1 ≤ p.toReal

Proof state:
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
⊢ p = ⊤ ∨ 0 < p.toReal ∧ 1 ≤ p.toReal

Tactic:
simpa using ENNReal.trichotomy₂ (Fact.out : 1 ≤ p)

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
@[simp] lemma div_dvd_iff_dvd_mul (h : b ∣ a) (hb : b ≠ 0) : a / b ∣ c ↔ a ∣ b * c :=
  exists_congr <| fun d => by
  have := Nat.dvd_trans (Nat.dvd_mul_left _ d) (Nat.mul_dvd_mul_left d h)
  rw [eq_comm, Nat.mul_comm, ← Nat.mul_div_assoc d h,
    Nat.div_eq_iff_eq_mul_right (Nat.pos_of_ne_zero hb) this, Nat.mul_comm, eq_comm]

Proof state:
a b c : ℕ
h : b ∣ a
hb : b ≠ 0
d : ℕ
⊢ c = a / b * d ↔ b * c = a * d

Tactic:
have := Nat.dvd_trans (Nat.dvd_mul_left _ d) (Nat.mul_dvd_mul_left d h)

Result:
a b c : ℕ
h : b ∣ a
hb : b ≠ 0
d : ℕ
this : b ∣ d * a
⊢ c = a / b * d ↔ b * c = a * d

Proof state:
a b c : ℕ
h : b ∣ a
hb : b ≠ 0
d : ℕ
this : b ∣ d * a
⊢ c = a / b * d ↔ b * c = a * d

Tactic:
rw [eq_comm, Nat.mul_comm, ← Nat.mul_div_assoc d h,
  Nat.div_eq_iff_eq_mul_right (Nat.pos_of_ne_zero hb) this, Nat.mul_comm, eq_comm]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean
theorem Γ₀_obj_termwise_mapMono_comp_PInfty (X : SimplicialObject C) {Δ Δ' : SimplexCategory}
    (i : Δ ⟶ Δ') [Mono i] :
    Γ₀.Obj.Termwise.mapMono (AlternatingFaceMapComplex.obj X) i ≫ PInfty.f Δ.len =
      PInfty.f Δ'.len ≫ X.map i.op

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
h' : ⦋n'⦌ = ⦋n⦌
⊢ False

Tactic:
exact h (congr_arg SimplexCategory.len h'.symm)

Result:
no goals

Proof state:
case pos.h₀
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ PInfty.f (n + 1) ≫ ((-1) ^ ↑b • X.δ b) = 0

Tactic:
rw [Preadditive.comp_zsmul, SimplicialObject.δ,
  PInfty_comp_map_mono_eq_zero X (SimplexCategory.δ b) h
    (by
      rw [Isδ₀.iff]
      exact hb),
  zsmul_zero]

Result:
no goals

Proof state:
case neg.h₂
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
h' : Isδ₀ i
⊢ False

Tactic:
exact hi h'

Result:
no goals

Proof state:
case pos.h₁
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ 0 ∉ Finset.univ → PInfty.f (n + 1) ≫ ((-1) ^ ↑0 • X.δ 0) = 0

Tactic:
simp only [Finset.mem_univ, not_true, IsEmpty.forall_iff]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f Δ.len = PInfty.f Δ'.len ≫ X.map i.op

Tactic:
induction' Δ using SimplexCategory.rec with n

Result:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n : ℕ
i : ⦋n⦌ ⟶ Δ'
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f ⦋n⦌.len = PInfty.f Δ'.len ≫ X.map i.op

Proof state:
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : Isδ₀ i
h' : n' = n + 1
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f n = PInfty.f n' ≫ X.map i.op

Tactic:
subst h'

Result:
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f n = PInfty.f (n + 1) ≫ X.map i.op