harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Assignment.lean
theorem has_remove_irrelevant (assignment : Assignment) (b : Bool) :
    hasAssignment b (removeAssignment (!b) assignment) → hasAssignment b assignment

Proof state:
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true

Tactic:
simp only [hb, removeAssignment, Bool.not_true, ite_false, hasAssignment, ite_true]

Result:
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ ((if false = true then removePosAssignment else removeNegAssignment) assignment).hasPosAssignment = true →
    assignment.hasPosAssignment = true

Proof state:
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ ((if false = true then removePosAssignment else removeNegAssignment) assignment).hasPosAssignment = true →
    assignment.hasPosAssignment = true

Tactic:
cases assignment <;> decide

Result:
no goals

Proof state:
assignment : Assignment
b : Bool
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true

Tactic:
by_cases hb : b

Result:
case pos
assignment : Assignment
b : Bool
hb : b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true

case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true

Proof state:
case neg
assignment : Assignment
b : Bool
hb : ¬b = true
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true

Tactic:
simp only [Bool.not_eq_true] at hb

Result:
case neg
assignment : Assignment
b : Bool
hb : b = false
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true

Proof state:
case neg
assignment : Assignment
b : Bool
hb : b = false
⊢ (if false = true then hasPosAssignment else hasNegAssignment)
        ((if (!false) = true then removePosAssignment else removeNegAssignment) assignment) =
      true →
    (if false = true then hasPosAssignment else hasNegAssignment) assignment = true

Tactic:
cases assignment <;> decide

Result:
no goals

Proof state:
case neg
assignment : Assignment
b : Bool
hb : b = false
⊢ hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true

Tactic:
simp only [hb, removeAssignment, Bool.not_true, ite_false, hasAssignment, ite_true]

Result:
case neg
assignment : Assignment
b : Bool
hb : b = false
⊢ (if false = true then hasPosAssignment else hasNegAssignment)
        ((if (!false) = true then removePosAssignment else removeNegAssignment) assignment) =
      true →
    (if false = true then hasPosAssignment else hasNegAssignment) assignment = true
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem ExprCnstr.denote_toPoly (ctx : Context) (c : ExprCnstr) : c.toPoly.denote ctx = c.denote ctx

Proof state:
case mk
ctx : Context
eq : Bool
lhs rhs : Expr
⊢ (bif eq then Poly.denote_eq ctx (lhs.toPoly, rhs.toPoly) else Poly.denote_le ctx (lhs.toPoly, rhs.toPoly)) ↔
    bif eq then Expr.denote ctx lhs = Expr.denote ctx rhs else Expr.denote ctx lhs ≤ Expr.denote ctx rhs

Tactic:
by_cases h : eq = true <;> simp [h]

Result:
case pos
ctx : Context
eq : Bool
lhs rhs : Expr
h : eq = true
⊢ Poly.denote_eq ctx (lhs.toPoly, rhs.toPoly) ↔ Expr.denote ctx lhs = Expr.denote ctx rhs

case neg
ctx : Context
eq : Bool
lhs rhs : Expr
h : ¬eq = true
⊢ Poly.denote_le ctx (lhs.toPoly, rhs.toPoly) ↔ Expr.denote ctx lhs ≤ Expr.denote ctx rhs

Proof state:
ctx : Context
c : ExprCnstr
⊢ PolyCnstr.denote ctx c.toPoly = denote ctx c

Tactic:
cases c

Result:
case mk
ctx : Context
eq✝ : Bool
lhs✝ rhs✝ : Expr
⊢ PolyCnstr.denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }.toPoly =
    denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }

Proof state:
case pos
ctx : Context
eq : Bool
lhs rhs : Expr
h : eq = true
⊢ Poly.denote_eq ctx (lhs.toPoly, rhs.toPoly) ↔ Expr.denote ctx lhs = Expr.denote ctx rhs

Tactic:
simp [Poly.denote_eq]

Result:
no goals

Proof state:
case mk
ctx : Context
eq✝ : Bool
lhs✝ rhs✝ : Expr
⊢ PolyCnstr.denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }.toPoly =
    denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }

Tactic:
rename_i eq lhs rhs

Result:
case mk
ctx : Context
eq : Bool
lhs rhs : Expr
⊢ PolyCnstr.denote ctx { eq := eq, lhs := lhs, rhs := rhs }.toPoly = denote ctx { eq := eq, lhs := lhs, rhs := rhs }

Proof state:
case neg
ctx : Context
eq : Bool
lhs rhs : Expr
h : ¬eq = true
⊢ Poly.denote_le ctx (lhs.toPoly, rhs.toPoly) ↔ Expr.denote ctx lhs ≤ Expr.denote ctx rhs

Tactic:
simp [Poly.denote_le]

Result:
no goals

Proof state:
case mk
ctx : Context
eq : Bool
lhs rhs : Expr
⊢ PolyCnstr.denote ctx { eq := eq, lhs := lhs, rhs := rhs }.toPoly = denote ctx { eq := eq, lhs := lhs, rhs := rhs }

Tactic:
simp [ExprCnstr.denote, PolyCnstr.denote, ExprCnstr.toPoly]

Result:
case mk
ctx : Context
eq : Bool
lhs rhs : Expr
⊢ (bif eq then Poly.denote_eq ctx (lhs.toPoly, rhs.toPoly) else Poly.denote_le ctx (lhs.toPoly, rhs.toPoly)) ↔
    bif eq then Expr.denote ctx lhs = Expr.denote ctx rhs else Expr.denote ctx lhs ≤ Expr.denote ctx rhs
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem mem_of_find?_eq_some : ∀ {l}, find? p l = some a → a ∈ l
  | b :: l, H => by
    by_cases h : p b <;> simp [find?, h] at H
    · exact H ▸ .head _
    · exact .tail _ (mem_of_find?_eq_some H)

Proof state:
α✝ : Type u_1
p : α✝ → Bool
a b : α✝
l : List α✝
H : find? p (b :: l) = some a
⊢ a ∈ b :: l

Tactic:
by_cases h : p b <;> simp [find?, h] at H

Result:
case pos
α✝ : Type u_1
p : α✝ → Bool
a b : α✝
l : List α✝
h : p b = true
H : b = a
⊢ a ∈ b :: l

case neg
α✝ : Type u_1
p : α✝ → Bool
a b : α✝
l : List α✝
h : ¬p b = true
H : find? p l = some a
⊢ a ∈ b :: l

Proof state:
case neg
α✝ : Type u_1
p : α✝ → Bool
a b : α✝
l : List α✝
h : ¬p b = true
H : find? p l = some a
⊢ a ∈ b :: l

Tactic:
exact .tail _ (mem_of_find?_eq_some H)

Result:
no goals

Proof state:
case pos
α✝ : Type u_1
p : α✝ → Bool
a b : α✝
l : List α✝
h : p b = true
H : b = a
⊢ a ∈ b :: l

Tactic:
exact H ▸ .head _

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Ideal.lean
theorem mem_jacobson_iff {x : R} {I : TwoSidedIdeal R} :
    x ∈ jacobson I ↔ ∀ y, ∃ z, z * y * x + z - 1 ∈ I

Proof state:
R : Type u
inst✝ : Ring R
x : R
I : TwoSidedIdeal R
⊢ x ∈ I.jacobson ↔ ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I

Tactic:
simp [jacobson, Ideal.mem_jacobson_iff]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
theorem fst_apply' (κ : Kernel α (β × γ)) (a : α) {s : Set β} (hs : MeasurableSet s) :
    fst κ a s = κ a {p | p.1 ∈ s}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ (κ.fst a) s = (κ a) {p | p.1 ∈ s}

Tactic:
rw [fst_apply, Measure.map_apply measurable_fst hs]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ (κ a) (Prod.fst ⁻¹' s) = (κ a) {p | p.1 ∈ s}

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set β
hs : MeasurableSet s
⊢ (κ a) (Prod.fst ⁻¹' s) = (κ a) {p | p.1 ∈ s}

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/FunctorCategory.lean
/-- If `Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*)` preserves limits of shape `J`, so will `F`. -/
lemma preservesLimit_of_lan_preservesLimit {C D : Type u} [SmallCategory C]
    [SmallCategory D] (F : C ⥤ D) (J : Type u) [SmallCategory J]
    [PreservesLimitsOfShape J (F.op.lan : _ ⥤ Dᵒᵖ ⥤ Type u)] : PreservesLimitsOfShape J F

Proof state:
C D : Type u
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
F : C ⥤ D
J : Type u
inst✝¹ : SmallCategory J
inst✝ : PreservesLimitsOfShape J F.op.lan
⊢ PreservesLimitsOfShape J F

Tactic:
apply @preservesLimitsOfShape_of_reflects_of_preserves _ _ _ _ _ _ _ _ F yoneda ?_

Result:
C D : Type u
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
F : C ⥤ D
J : Type u
inst✝¹ : SmallCategory J
inst✝ : PreservesLimitsOfShape J F.op.lan
⊢ PreservesLimitsOfShape J (F ⋙ yoneda)

Proof state:
C D : Type u
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
F : C ⥤ D
J : Type u
inst✝¹ : SmallCategory J
inst✝ : PreservesLimitsOfShape J F.op.lan
⊢ PreservesLimitsOfShape J (F ⋙ yoneda)

Tactic:
exact preservesLimitsOfShape_of_natIso (Presheaf.compYonedaIsoYonedaCompLan F).symm

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToL1_indicatorConstLp (hT : DominatedFinMeasAdditive μ T C) {s : Set α}
    (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : E) :
    setToL1 hT (indicatorConstLp 1 hs hμs x) = T s x

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E
⊢ (setToL1 hT) (indicatorConstLp 1 hs hμs x) = (T s) x

Tactic:
rw [← Lp.simpleFunc.coe_indicatorConst hs hμs x]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E
⊢ (setToL1 hT) ↑(indicatorConst 1 hs hμs x) = (T s) x

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : E
⊢ (setToL1 hT) ↑(indicatorConst 1 hs hμs x) = (T s) x

Tactic:
exact setToL1_simpleFunc_indicatorConst hT hs hμs.lt_top x

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem IsInitial.principal_mul {o : Ordinal} (h : IsInitial o) (ho : ω ≤ o) :
    Principal (· * ·) o

Proof state:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ Principal (fun x1 x2 => x1 * x2) o.card.ord

Tactic:
apply principal_mul_ord

Result:
case hc
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ ℵ₀ ≤ o.card

Proof state:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ Principal (fun x1 x2 => x1 * x2) o

Tactic:
rw [← h.ord_card]

Result:
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ Principal (fun x1 x2 => x1 * x2) o.card.ord

Proof state:
case hc
o : Ordinal.{u_1}
h : o.IsInitial
ho : ω ≤ o
⊢ ℵ₀ ≤ o.card

Tactic:
rwa [aleph0_le_card]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_ne_zero_and_ne_pi_iff_linearIndependent {x y : V} :
    o.oangle x y ≠ 0 ∧ o.oangle x y ≠ π ↔ LinearIndependent ℝ ![x, y]

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle x y ≠ 0 ∧ o.oangle x y ≠ ↑π ↔ LinearIndependent ℝ ![x, y]

Tactic:
rw [← not_or, ← not_iff_not, Classical.not_not,
  oangle_eq_zero_or_eq_pi_iff_not_linearIndependent]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/DotProduct.lean
theorem dotProduct_eq (v w : n → R) (h : ∀ u, dotProduct v u = dotProduct w u) : v = w

Proof state:
case h
n : Type u_2
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Fintype n
v w : n → R
h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u
x : n
⊢ v x = w x

Tactic:
classical rw [← dotProduct_single_one v x, ← dotProduct_single_one w x, h]

Result:
no goals

Proof state:
n : Type u_2
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Fintype n
v w : n → R
h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u
⊢ v = w

Tactic:
funext x

Result:
case h
n : Type u_2
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Fintype n
v w : n → R
h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u
x : n
⊢ v x = w x

Proof state:
case h
n : Type u_2
R : Type u_4
inst✝¹ : Semiring R
inst✝ : Fintype n
v w : n → R
h : ∀ (u : n → R), v ⬝ᵥ u = w ⬝ᵥ u
x : n
⊢ v x = w x

Tactic:
rw [← dotProduct_single_one v x, ← dotProduct_single_one w x, h]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_split_single (f : β → α) (i₀ : β) : ⨆ i, f i = f i₀ ⊔ ⨆ (i) (_ : i ≠ i₀), f i

Proof state:
case h.e'_3.h.e'_3
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
i₀ : β
⊢ f i₀ = ⨆ i, ⨆ (_ : i = i₀), f i

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
i₀ : β
⊢ ⨆ i, f i = f i₀ ⊔ ⨆ i, ⨆ (_ : i ≠ i₀), f i

Tactic:
convert iSup_split f (fun i => i = i₀)

Result:
case h.e'_3.h.e'_3
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
i₀ : β
⊢ f i₀ = ⨆ i, ⨆ (_ : i = i₀), f i
-- Mathlib/Order/Filter/AtTopBot/Disjoint.lean
theorem disjoint_atBot_atTop [PartialOrder α] [Nontrivial α] :
    Disjoint (atBot : Filter α) atTop

Proof state:
case pos
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint (Iic x) (Ici y)

Tactic:
exact Iic_disjoint_Ici.2 (hle.lt_of_ne hne).not_le

Result:
no goals

Proof state:
case neg
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint atBot atTop

Tactic:
refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot y) (Ici_mem_atTop x)

Result:
case neg
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint (Iic y) (Ici x)

Proof state:
case intro.intro
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
⊢ Disjoint atBot atTop

Tactic:
by_cases hle : x ≤ y

Result:
case pos
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint atBot atTop

case neg
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint atBot atTop

Proof state:
case neg
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint (Iic y) (Ici x)

Tactic:
exact Iic_disjoint_Ici.2 hle

Result:
no goals

Proof state:
case pos
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint atBot atTop

Tactic:
refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot x) (Ici_mem_atTop y)

Result:
case pos
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : x ≤ y
⊢ Disjoint (Iic x) (Ici y)

Proof state:
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
⊢ Disjoint atBot atTop

Tactic:
rcases exists_pair_ne α with ⟨x, y, hne⟩

Result:
case intro.intro
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
⊢ Disjoint atBot atTop
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem mk_d_2_0 : (mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 2 = d₁

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 2 = d₁

Tactic:
change ite (2 = 1 + 1) (d₁ ≫ 𝟙 X₂) 0 = d₁

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
⊢ (if 2 = 1 + 1 then d₁ ≫ 𝟙 X₂ else 0) = d₁

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
⊢ (if 2 = 1 + 1 then d₁ ≫ 𝟙 X₂ else 0) = d₁

Tactic:
rw [if_pos rfl, Category.comp_id]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev.lean
theorem U_complex_cosh (n : ℤ) : (U ℂ n).eval (cosh θ) * sinh θ = sinh ((n + 1) * θ) := calc
  (U ℂ n).eval (cosh θ) * sinh θ
  _ = (U ℂ n).eval (cos (θ * I)) * sin (θ * I) * (-I)

Proof state:
θ : ℂ
n : ℤ
⊢ sin ((↑n + 1) * (θ * I)) * -I = sin ((↑n + 1) * θ * I) * -I

Tactic:
rw [mul_assoc]

Result:
no goals

Proof state:
θ : ℂ
n : ℤ
⊢ sin ((↑n + 1) * θ * I) * -I = sinh ((↑n + 1) * θ)

Tactic:
rw [sin_mul_I ((n + 1) * θ), mul_assoc, mul_neg, I_mul_I, neg_neg, mul_one]

Result:
no goals

Proof state:
θ : ℂ
n : ℤ
⊢ eval (cosh θ) (U ℂ n) * sinh θ = eval (cos (θ * I)) (U ℂ n) * sin (θ * I) * -I

Tactic:
simp [cos_mul_I, sin_mul_I, mul_assoc]

Result:
no goals

Proof state:
θ : ℂ
n : ℤ
⊢ eval (cos (θ * I)) (U ℂ n) * sin (θ * I) * -I = sin ((↑n + 1) * (θ * I)) * -I

Tactic:
rw [U_complex_cos]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem HasFPowerSeriesWithinOnBall.hasSum_derivSeries_of_hasFDerivWithinAt
    (h : HasFPowerSeriesWithinOnBall f p s x r)
    {f' : E →L[𝕜] F}
    {y : E} (hy : (‖y‖₊ : ℝ≥0∞) < r) (h'y : x + y ∈ insert x s)
    (hf' : HasFDerivWithinAt f f' (insert x s) (x + y))
    (hu : UniqueDiffOn 𝕜 (insert x s)) :
    HasSum (fun n ↦ p.derivSeries n (fun _ ↦ y)) f'

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : ↑‖y‖₊ < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
b : (E →L[𝕜] F) →ₗᵢ[𝕜] E →L[𝕜] F' := UniformSpace.Completion.toComplₗᵢ.postcomp
this : HasFPowerSeriesWithinOnBall (⇑a ∘ f) (a.compFormalMultilinearSeries p) s x r
Z :
  HasSum (fun n => ((a.compFormalMultilinearSeries p).derivSeries n) fun x => y)
    (fderivWithin 𝕜 (⇑a ∘ f) (insert x s) (x + y))
⊢ HasFDerivWithinAt (⇑a ∘ f) (a.comp f') (insert x s) (x + y)

Tactic:
exact a.hasFDerivAt.comp_hasFDerivWithinAt (x + y) hf'

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : ↑‖y‖₊ < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
⊢ HasSum (fun n => (p.derivSeries n) fun x => y) f'

Tactic:
let F' := UniformSpace.Completion F

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinOnBall f p s x r
f' : E →L[𝕜] F
y : E
hy : ↑‖y‖₊ < r
h'y : x + y ∈ insert x s
hf' : HasFDerivWithinAt f f' (insert x s) (x + y)
hu : UniqueDiffOn 𝕜 (insert x s)
F' : Type v := UniformSpace.Completion F
⊢ HasSum (fun n => (p.derivSeries n) fun x => y) f'
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem HasFDerivWithinAt.of_local_left_inverse {g : F → E} {f' : E ≃L[𝕜] F} {a : F} {t : Set F}
    (hg : Tendsto g (𝓝[t] a) (𝓝[s] (g a))) (hf : HasFDerivWithinAt f (f' : E →L[𝕜] F) s (g a))
    (ha : a ∈ t) (hfg : ∀ᶠ y in 𝓝[t] a, f (g y) = y) :
    HasFDerivWithinAt g (f'.symm : F →L[𝕜] E) t a

Proof state:
case refine_1
𝕜 : 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
f : E → F
s : Set E
g : F → E
f' : E ≃L[𝕜] F
a : F
t : Set F
hg : Tendsto g (𝓝[t] a) (𝓝[s] g a)
hf : HasFDerivWithinAt f (↑f') s (g a)
ha : a ∈ t
hfg : ∀ᶠ (y : F) in 𝓝[t] a, f (g y) = y
p : F
hp : f (g p) = p
⊢ (fun x => ↑f' (g x - g a) - (f (g x) - f (g a))) p = f' (g p - g a) - (p - a)

Tactic:
simp [hp, hfg.self_of_nhdsWithin ha]

Result:
no goals

Proof state:
case refine_1
𝕜 : 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
f : E → F
s : Set E
g : F → E
f' : E ≃L[𝕜] F
a : F
t : Set F
hg : Tendsto g (𝓝[t] a) (𝓝[s] g a)
hf : HasFDerivWithinAt f (↑f') s (g a)
ha : a ∈ t
hfg : ∀ᶠ (y : F) in 𝓝[t] a, f (g y) = y
⊢ ∀ (x : F), f (g x) = x → (fun x => ↑f' (g x - g a) - (f (g x) - f (g a))) x = f' (g x - g a) - (x - a)

Tactic:
intro p hp

Result:
case refine_1
𝕜 : 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
f : E → F
s : Set E
g : F → E
f' : E ≃L[𝕜] F
a : F
t : Set F
hg : Tendsto g (𝓝[t] a) (𝓝[s] g a)
hf : HasFDerivWithinAt f (↑f') s (g a)
ha : a ∈ t
hfg : ∀ᶠ (y : F) in 𝓝[t] a, f (g y) = y
p : F
hp : f (g p) = p
⊢ (fun x => ↑f' (g x - g a) - (f (g x) - f (g a))) p = f' (g p - g a) - (p - a)
-- Mathlib/Order/SuccPred/Limit.lean
theorem not_isPredPrelimit_iff : ¬ IsPredPrelimit a ↔ ∃ b, ¬ IsMin b ∧ pred b = a

Proof state:
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
⊢ ¬IsSuccPrelimit (toDual a) ↔ ∃ b, ¬IsMin b ∧ pred b = a

Tactic:
exact not_isSuccPrelimit_iff

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
⊢ ¬IsPredPrelimit a ↔ ∃ b, ¬IsMin b ∧ pred b = a

Tactic:
rw [← isSuccPrelimit_toDual_iff]

Result:
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
⊢ ¬IsSuccPrelimit (toDual a) ↔ ∃ b, ¬IsMin b ∧ pred b = a
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem eq_of_forall_toMeasure_apply_eq (μ ν : ProbabilityMeasure Ω)
    (h : ∀ s : Set Ω, MeasurableSet s → (μ : Measure Ω) s = (ν : Measure Ω) s) : μ = ν

Proof state:
case a.h
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s
s : Set Ω
s_mble : MeasurableSet s
⊢ ↑μ s = ↑ν s

Tactic:
exact h s s_mble

Result:
no goals

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s
⊢ μ = ν

Tactic:
apply toMeasure_injective

Result:
case a
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s
⊢ ↑μ = ↑ν

Proof state:
case a
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s
⊢ ↑μ = ↑ν

Tactic:
ext1 s s_mble

Result:
case a.h
Ω : Type u_1
inst✝ : MeasurableSpace Ω
μ ν : ProbabilityMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s
s : Set Ω
s_mble : MeasurableSet s
⊢ ↑μ s = ↑ν s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head_mem_head? : ∀ {l : List α} (h : l ≠ []), head l h ∈ head? l
  | [], h => by contradiction
  | _ :: _, _ => rfl

Proof state:
α : Type u_1
h : [] ≠ []
⊢ [].head h ∈ [].head?

Tactic:
contradiction

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem singularPart_sub (s t : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ]
    [t.HaveLebesgueDecomposition μ] :
    (s - t).singularPart μ = s.singularPart μ - t.singularPart μ

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝¹ : s.HaveLebesgueDecomposition μ
inst✝ : t.HaveLebesgueDecomposition μ
⊢ (s - t).singularPart μ = s.singularPart μ - t.singularPart μ

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, singularPart_add, singularPart_neg]

Result:
no goals