harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Condensed/Discrete/Characterization.lean
lemma mem_locallyConstant_essImage_of_isColimit_mapCocone (X : CondensedSet.{u})
    (h : ∀ S : Profinite.{u}, IsColimit <|
      (profiniteToCompHaus.op ⋙ X.val).mapCocone S.asLimitCone.op) :
    CondensedSet.LocallyConstant.functor.essImage X

Proof state:
X : CondensedSet
h : (S : Profinite) → IsColimit ((profiniteToCompHaus.op ⋙ X.val).mapCocone S.asLimitCone.op)
e : CondensedSet ≌ Sheaf (coherentTopology Profinite) (Type (u + 1)) :=
  (Condensed.ProfiniteCompHaus.equivalence (Type (u + 1))).symm
⊢ LocallyConstant.functor.essImage X

Tactic:
let i : (e.functor.obj X).val ≅ (e.functor.obj (LocallyConstant.functor.obj _)).val :=
  Condensed.isoLocallyConstantOfIsColimit _ h

Result:
X : CondensedSet
h : (S : Profinite) → IsColimit ((profiniteToCompHaus.op ⋙ X.val).mapCocone S.asLimitCone.op)
e : CondensedSet ≌ Sheaf (coherentTopology Profinite) (Type (u + 1)) :=
  (Condensed.ProfiniteCompHaus.equivalence (Type (u + 1))).symm
i : (e.functor.obj X).val ≅
  (e.functor.obj
      (LocallyConstant.functor.obj
        ((e.functor.obj X).val.obj (toProfinite.op.obj (Opposite.op (of PUnit.{u + 1})))))).val :=
  Condensed.isoLocallyConstantOfIsColimit (e.functor.obj X).val h
⊢ LocallyConstant.functor.essImage X

Proof state:
X : CondensedSet
h : (S : Profinite) → IsColimit ((profiniteToCompHaus.op ⋙ X.val).mapCocone S.asLimitCone.op)
⊢ LocallyConstant.functor.essImage X

Tactic:
let e : CondensedSet.{u} ≌ Sheaf (coherentTopology Profinite) _ :=
  (Condensed.ProfiniteCompHaus.equivalence (Type (u + 1))).symm

Result:
X : CondensedSet
h : (S : Profinite) → IsColimit ((profiniteToCompHaus.op ⋙ X.val).mapCocone S.asLimitCone.op)
e : CondensedSet ≌ Sheaf (coherentTopology Profinite) (Type (u + 1)) :=
  (Condensed.ProfiniteCompHaus.equivalence (Type (u + 1))).symm
⊢ LocallyConstant.functor.essImage X

Proof state:
X : CondensedSet
h : (S : Profinite) → IsColimit ((profiniteToCompHaus.op ⋙ X.val).mapCocone S.asLimitCone.op)
e : CondensedSet ≌ Sheaf (coherentTopology Profinite) (Type (u + 1)) :=
  (Condensed.ProfiniteCompHaus.equivalence (Type (u + 1))).symm
i : (e.functor.obj X).val ≅
  (e.functor.obj
      (LocallyConstant.functor.obj
        ((e.functor.obj X).val.obj (toProfinite.op.obj (Opposite.op (of PUnit.{u + 1})))))).val :=
  Condensed.isoLocallyConstantOfIsColimit (e.functor.obj X).val h
⊢ LocallyConstant.functor.essImage X

Tactic:
exact ⟨_, ⟨e.functor.preimageIso ((sheafToPresheaf _ _).preimageIso i.symm)⟩⟩

Result:
no goals
-- Mathlib/Data/List/Lookmap.lean
theorem lookmap_cons_none {a : α} (l : List α) (h : f a = none) :
    (a :: l).lookmap f = a :: l.lookmap f

Proof state:
α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ (match none with
    | some b => b :: l
    | none => (#[].push a).toListAppend (lookmap f l)) =
    a :: lookmap.go f l #[]

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ lookmap f (a :: l) = a :: lookmap f l

Tactic:
simp only [lookmap, lookmap.go, Array.toListAppend_eq, Array.toList_toArray, nil_append]

Result:
α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ (match f a with
    | some b => b :: l
    | none => lookmap.go f l (#[].push a)) =
    a :: lookmap.go f l #[]

Proof state:
α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ (match f a with
    | some b => b :: l
    | none => lookmap.go f l (#[].push a)) =
    a :: lookmap.go f l #[]

Tactic:
rw [lookmap.go_append, h]

Result:
α : Type u_1
f : α → Option α
a : α
l : List α
h : f a = none
⊢ (match none with
    | some b => b :: l
    | none => (#[].push a).toListAppend (lookmap f l)) =
    a :: lookmap.go f l #[]
-- Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
theorem mem_sSup_of_directedOn {S : Set (NonUnitalSubsemiring R)} (Sne : S.Nonempty)
    (hS : DirectedOn (· ≤ ·) S) {x : R} : x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
S : Set (NonUnitalSubsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp only [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, Subtype.exists, exists_prop]

Result:
no goals

Proof state:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
S : Set (NonUnitalSubsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
haveI : Nonempty S := Sne.to_subtype

Result:
R : Type u
inst✝ : NonUnitalNonAssocSemiring R
S : Set (NonUnitalSubsemiring R)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : R
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_append (l₁ l₂) : countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂

Proof state:
α : Type u_1
p : α → Bool
l₁ l₂ : List α
⊢ countP p (l₁ ++ l₂) = countP p l₁ + countP p l₂

Tactic:
simp only [countP_eq_length_filter, filter_append, length_append]

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem span_gcd (x y : R) : span {gcd x y} = span {x, y}

Proof state:
R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
x y : R
⊢ Ideal.span {gcd x y} = Ideal.span {x, y}

Tactic:
rw [← IsBezout.span_gcd, IsBezout.span_gcd_eq_span_gcd]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem IsPrime.le_of_pow_le {I P : Ideal R} [hP : P.IsPrime] {n : ℕ} (h : I ^ n ≤ P) :
    I ≤ P

Proof state:
case pos
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ n ≤ P
hn : n = 0
⊢ I ≤ P

Tactic:
rw [hn, pow_zero, one_eq_top] at h

Result:
case pos
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : ⊤ ≤ P
hn : n = 0
⊢ I ≤ P

Proof state:
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ n ≤ P
⊢ I ≤ P

Tactic:
by_cases hn : n = 0

Result:
case pos
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ n ≤ P
hn : n = 0
⊢ I ≤ P

case neg
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ n ≤ P
hn : ¬n = 0
⊢ I ≤ P

Proof state:
case pos
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : ⊤ ≤ P
hn : n = 0
⊢ I ≤ P

Tactic:
exact fun ⦃_⦄ _ ↦ h Submodule.mem_top

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ n ≤ P
hn : ¬n = 0
⊢ I ≤ P

Tactic:
exact (pow_le_iff hn).mp h

Result:
no goals
-- Mathlib/NumberTheory/SiegelsLemma.lean
private lemma card_T_eq [DecidableEq β] : #T = (B + 1) ^ n

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq β
⊢ ∏ i : β, #(Icc (0 i) ↑B) = (B + 1) ^ n

Tactic:
simp only [Pi.zero_apply, card_Icc, sub_zero, toNat_ofNat_add_one, prod_const, card_univ,
  add_pos_iff, zero_lt_one, or_true]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq β
⊢ #T = (B + 1) ^ n

Tactic:
rw [Pi.card_Icc 0 B']

Result:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq β
⊢ ∏ i : β, #(Icc (0 i) ↑B) = (B + 1) ^ n
-- Mathlib/Algebra/MvPolynomial/PDeriv.lean
theorem pderiv_pow {i : σ} {f : MvPolynomial σ R} {n : ℕ} :
    pderiv i (f ^ n) = n * f ^ (n - 1) * pderiv i f

Proof state:
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
f : MvPolynomial σ R
n : ℕ
⊢ (pderiv i) (f ^ n) = ↑n * f ^ (n - 1) * (pderiv i) f

Tactic:
rw [(pderiv i).leibniz_pow f n, nsmul_eq_mul, smul_eq_mul, mul_assoc]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma coe_dual (hI : I ≠ 0) :
    (dual A K I : Submodule B L) = Iᵛ

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁸ : CommRing A
inst✝¹⁷ : Field K
inst✝¹⁶ : CommRing B
inst✝¹⁵ : Field L
inst✝¹⁴ : Algebra A K
inst✝¹³ : Algebra B L
inst✝¹² : Algebra A B
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : IsScalarTower A B L
inst✝⁷ : IsDomain A
inst✝⁶ : IsFractionRing A K
inst✝⁵ : FiniteDimensional K L
inst✝⁴ : Algebra.IsSeparable K L
inst✝³ : IsIntegralClosure B A L
inst✝² : IsFractionRing B L
inst✝¹ : IsIntegrallyClosed A
inst✝ : IsDedekindDomain B
I : FractionalIdeal B⁰ L
hI : I ≠ 0
⊢ ↑(dual A K I) = (↑I)ᵛ

Tactic:
rw [dual, dif_neg hI, coe_mk]

Result:
no goals
-- Mathlib/Topology/Algebra/UniformRing.lean
theorem extensionHom_coe [CompleteSpace β] [T0Space β] (a : α) :
    Completion.extensionHom f hf a = f a

Proof state:
α : Type u_1
inst✝⁹ : Ring α
inst✝⁸ : UniformSpace α
inst✝⁷ : IsTopologicalRing α
inst✝⁶ : UniformAddGroup α
β : Type u
inst✝⁵ : UniformSpace β
inst✝⁴ : Ring β
inst✝³ : UniformAddGroup β
inst✝² : IsTopologicalRing β
f : α →+* β
hf : Continuous ⇑f
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
a : α
⊢ (extensionHom f hf) ↑a = f a

Tactic:
simp only [Completion.extensionHom, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
  UniformSpace.Completion.extension_coe <| uniformContinuous_addMonoidHom_of_continuous hf]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem hasDerivWithinAt_of_bilinear
    (hu : HasDerivWithinAt u u' s x) (hv : HasDerivWithinAt v v' s x) :
    HasDerivWithinAt (fun x ↦ B (u x) (v x)) (B (u x) v' + B u' (v x)) s x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
x : 𝕜
s : Set 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
u' : E
v' : F
hu : HasDerivWithinAt u u' s x
hv : HasDerivWithinAt v v' s x
⊢ HasDerivWithinAt (fun x => (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) s x

Tactic:
simpa using (B.hasFDerivWithinAt_of_bilinear
  hu.hasFDerivWithinAt hv.hasFDerivWithinAt).hasDerivWithinAt

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem image_prod_mk_subset_prod_left (hb : b ∈ t) : (fun a => (a, b)) '' s ⊆ s ×ˢ t

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
hb : b ∈ t
a : α
ha : a ∈ s
⊢ (fun a => (a, b)) a ∈ s ×ˢ t

Tactic:
exact ⟨ha, hb⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
hb : b ∈ t
⊢ (fun a => (a, b)) '' s ⊆ s ×ˢ t

Tactic:
rintro _ ⟨a, ha, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
b : β
hb : b ∈ t
a : α
ha : a ∈ s
⊢ (fun a => (a, b)) a ∈ s ×ˢ t
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_add_cyc3 {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) :
    o.oangle x y + o.oangle y z + o.oangle z x = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ o.oangle x y + o.oangle y z + o.oangle z x = 0

Tactic:
simp [hx, hy, hz]

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem trans_of_set' {s : Set Y} (hs : IsOpen s) :
    e.trans (ofSet s hs) = e.restr (e.source ∩ e ⁻¹' s)

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Set Y
hs : IsOpen s
⊢ e.trans (ofSet s hs) = e.restr (e.source ∩ ↑e ⁻¹' s)

Tactic:
rw [trans_ofSet, restr_source_inter]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem getElem?_zero_flatten (L : Array (Array α)) :
    (flatten L)[0]? = L.findSome? fun l => l[0]?

Proof state:
case of
α : Type u_1
xss✝ : List (List α)
⊢ (List.map List.toArray xss✝).toArray.flatten[0]? = findSome? (fun l => l[0]?) (List.map List.toArray xss✝).toArray

Tactic:
simp [← List.head?_eq_getElem?, List.head?_flatten, List.findSome?_map, Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
L : Array (Array α)
⊢ L.flatten[0]? = findSome? (fun l => l[0]?) L

Tactic:
cases L using array₂_induction

Result:
case of
α : Type u_1
xss✝ : List (List α)
⊢ (List.map List.toArray xss✝).toArray.flatten[0]? = findSome? (fun l => l[0]?) (List.map List.toArray xss✝).toArray
-- Mathlib/Analysis/Normed/Order/Lattice.lean
theorem isClosed_le_of_isClosed_nonneg {G} [OrderedAddCommGroup G] [TopologicalSpace G]
    [ContinuousSub G] (h : IsClosed { x : G | 0 ≤ x }) :
    IsClosed { p : G × G | p.fst ≤ p.snd }

Proof state:
G : Type u_2
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
this : {p | p.1 ≤ p.2} = (fun p => p.2 - p.1) ⁻¹' {x | 0 ≤ x}
⊢ IsClosed {p | p.1 ≤ p.2}

Tactic:
rw [this]

Result:
G : Type u_2
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
this : {p | p.1 ≤ p.2} = (fun p => p.2 - p.1) ⁻¹' {x | 0 ≤ x}
⊢ IsClosed ((fun p => p.2 - p.1) ⁻¹' {x | 0 ≤ x})

Proof state:
G : Type u_2
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
⊢ IsClosed {p | p.1 ≤ p.2}

Tactic:
have : { p : G × G | p.fst ≤ p.snd } = (fun p : G × G => p.snd - p.fst) ⁻¹' { x : G | 0 ≤ x } :=
  by ext1 p; simp only [sub_nonneg, Set.preimage_setOf_eq]

Result:
G : Type u_2
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
this : {p | p.1 ≤ p.2} = (fun p => p.2 - p.1) ⁻¹' {x | 0 ≤ x}
⊢ IsClosed {p | p.1 ≤ p.2}

Proof state:
case h
G : Type u_2
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
p : G × G
⊢ p ∈ {p | p.1 ≤ p.2} ↔ p ∈ (fun p => p.2 - p.1) ⁻¹' {x | 0 ≤ x}

Tactic:
simp only [sub_nonneg, Set.preimage_setOf_eq]

Result:
no goals

Proof state:
G : Type u_2
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
this : {p | p.1 ≤ p.2} = (fun p => p.2 - p.1) ⁻¹' {x | 0 ≤ x}
⊢ IsClosed ((fun p => p.2 - p.1) ⁻¹' {x | 0 ≤ x})

Tactic:
exact IsClosed.preimage (continuous_snd.sub continuous_fst) h

Result:
no goals

Proof state:
G : Type u_2
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
⊢ {p | p.1 ≤ p.2} = (fun p => p.2 - p.1) ⁻¹' {x | 0 ≤ x}

Tactic:
ext1 p

Result:
case h
G : Type u_2
inst✝² : OrderedAddCommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousSub G
h : IsClosed {x | 0 ≤ x}
p : G × G
⊢ p ∈ {p | p.1 ≤ p.2} ↔ p ∈ (fun p => p.2 - p.1) ⁻¹' {x | 0 ≤ x}
-- Mathlib/Data/Seq/WSeq.lean
theorem destruct_cons (a : α) (s) : destruct (cons a s) = Computation.pure (some (a, s)) :=
  Computation.destruct_eq_pure <| by simp [destruct, cons, Computation.rmap]

Proof state:
α : Type u
a : α
s : WSeq α
⊢ (cons a s).destruct.destruct = Sum.inl (some (a, s))

Tactic:
simp [destruct, cons, Computation.rmap]

Result:
no goals
-- Mathlib/LinearAlgebra/FreeAlgebra.lean
theorem rank_eq [CommRing R] [Nontrivial R] :
    Module.rank R (FreeAlgebra R X) = Cardinal.lift.{u} (Cardinal.mk (List X))

Proof state:
R : Type u
X : Type v
inst✝¹ : CommRing R
inst✝ : Nontrivial R
⊢ Module.rank R (FreeAlgebra R X) = Cardinal.lift.{u, v} (Cardinal.mk (List X))

Tactic:
rw [← (Basis.mk_eq_rank'.{_,_,_,u} (basisFreeMonoid R X)).trans (Cardinal.lift_id _),
  Cardinal.lift_umax.{v, u}, FreeMonoid]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem card_support_eq_zero {f : Perm α} : #f.support = 0 ↔ f = 1

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ #f.support = 0 ↔ f = 1

Tactic:
rw [Finset.card_eq_zero, support_eq_empty_iff]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem dist_eq_abs_sub_dist_of_angle_eq_zero {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = 0) :
    dist p₁ p₃ = |dist p₁ p₂ - dist p₃ p₂|

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = 0
⊢ dist p₁ p₃ = |dist p₁ p₂ - dist p₃ p₂|

Tactic:
rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = 0
⊢ ‖p₁ -ᵥ ?p₃ - (p₃ -ᵥ ?p₃)‖ = |‖p₁ -ᵥ p₂‖ - ‖p₃ -ᵥ p₂‖|

case p₃
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = 0
⊢ P

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = 0
⊢ ‖p₁ -ᵥ ?p₃ - (p₃ -ᵥ ?p₃)‖ = |‖p₁ -ᵥ p₂‖ - ‖p₃ -ᵥ p₂‖|

case p₃
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = 0
⊢ P

Tactic:
exact norm_sub_eq_abs_sub_norm_of_angle_eq_zero h

Result:
no goals
-- Mathlib/Algebra/Field/Subfield/Basic.lean
theorem map_fieldRange : f.fieldRange.map g = (g.comp f).fieldRange

Proof state:
K : Type u
L : Type v
M : Type w
inst✝² : DivisionRing K
inst✝¹ : DivisionRing L
inst✝ : DivisionRing M
g : L →+* M
f : K →+* L
⊢ Subfield.map g f.fieldRange = (g.comp f).fieldRange

Tactic:
simpa only [fieldRange_eq_map] using (⊤ : Subfield K).map_map g f

Result:
no goals
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/InducedMaps.lean
theorem eq_path_of_eq_image :
    (πₘ (TopCat.ofHom f)).map ⟦p⟧ =
        hcast (start_path hfg) ≫ (πₘ (TopCat.ofHom g)).map ⟦q⟧ ≫ hcast (end_path hfg).symm

Proof state:
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ HEq ((π.map (TopCat.ofHom f)).map ⟦p⟧) ((π.map (TopCat.ofHom g)).map ⟦q⟧)

Tactic:
exact heq_path_of_eq_image hfg

Result:
no goals

Proof state:
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ (π.map (TopCat.ofHom f)).map ⟦p⟧ = hcast ⋯ ≫ (π.map (TopCat.ofHom g)).map ⟦q⟧ ≫ hcast ⋯

Tactic:
rw [conj_eqToHom_iff_heq
  ((πₘ (TopCat.ofHom f)).map ⟦p⟧) ((πₘ (TopCat.ofHom g)).map ⟦q⟧)
  (FundamentalGroupoid.ext <| start_path hfg)
  (FundamentalGroupoid.ext <| end_path hfg)]

Result:
X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ HEq ((π.map (TopCat.ofHom f)).map ⟦p⟧) ((π.map (TopCat.ofHom g)).map ⟦q⟧)
-- Mathlib/Algebra/Order/CompleteField.lean
theorem ringHom_monotone (hR : ∀ r : R, 0 ≤ r → ∃ s : R, s ^ 2 = r) (f : R →+* S) : Monotone f :=
  (monotone_iff_map_nonneg f).2 fun r h => by
    obtain ⟨s, rfl⟩ := hR r h; rw [map_pow]; apply sq_nonneg

Proof state:
R : Type u_5
S : Type u_6
inst✝¹ : OrderedRing R
inst✝ : LinearOrderedRing S
hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r
f : R →+* S
r : R
h : 0 ≤ r
⊢ 0 ≤ f r

Tactic:
obtain ⟨s, rfl⟩ := hR r h

Result:
case intro
R : Type u_5
S : Type u_6
inst✝¹ : OrderedRing R
inst✝ : LinearOrderedRing S
hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r
f : R →+* S
s : R
h : 0 ≤ s ^ 2
⊢ 0 ≤ f (s ^ 2)

Proof state:
case intro
R : Type u_5
S : Type u_6
inst✝¹ : OrderedRing R
inst✝ : LinearOrderedRing S
hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r
f : R →+* S
s : R
h : 0 ≤ s ^ 2
⊢ 0 ≤ f s ^ 2

Tactic:
apply sq_nonneg

Result:
no goals

Proof state:
case intro
R : Type u_5
S : Type u_6
inst✝¹ : OrderedRing R
inst✝ : LinearOrderedRing S
hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r
f : R →+* S
s : R
h : 0 ≤ s ^ 2
⊢ 0 ≤ f (s ^ 2)

Tactic:
rw [map_pow]

Result:
case intro
R : Type u_5
S : Type u_6
inst✝¹ : OrderedRing R
inst✝ : LinearOrderedRing S
hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r
f : R →+* S
s : R
h : 0 ≤ s ^ 2
⊢ 0 ≤ f s ^ 2
-- Mathlib/LinearAlgebra/Matrix/Spectrum.lean
theorem eigenvectorUnitary_mulVec (j : n) :
    eigenvectorUnitary hA *ᵥ Pi.single j 1 = ⇑(hA.eigenvectorBasis j)

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
j : n
⊢ ↑hA.eigenvectorUnitary *ᵥ Pi.single j 1 = (WithLp.equiv 2 ((i : n) → (fun x => 𝕜) i)) (hA.eigenvectorBasis j)

Tactic:
simp_rw [mulVec_single_one, eigenvectorUnitary_transpose_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
lemma rnDeriv_restrict (μ ν : Measure α) [HaveLebesgueDecomposition μ ν] [SigmaFinite ν]
    {s : Set α} (hs : MeasurableSet s) :
    (μ.restrict s).rnDeriv ν =ᵐ[ν] s.indicator (μ.rnDeriv ν)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
s : Set α
hs : MeasurableSet s
⊢ μ.restrict s = (μ.restrict s).singularPart ν + ν.withDensity (s.indicator (μ.rnDeriv ν))

Tactic:
rw [singularPart_restrict _ _ hs, withDensity_indicator hs, ← restrict_withDensity hs,
  ← Measure.restrict_add, ← μ.haveLebesgueDecomposition_add ν]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
s : Set α
hs : MeasurableSet s
⊢ (μ.restrict s).rnDeriv ν =ᶠ[ae ν] s.indicator (μ.rnDeriv ν)

Tactic:
refine (eq_rnDeriv (s := (μ.restrict s).singularPart ν)
  ((measurable_rnDeriv _ _).indicator hs) (mutuallySingular_singularPart _ _) ?_).symm

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite ν
s : Set α
hs : MeasurableSet s
⊢ μ.restrict s = (μ.restrict s).singularPart ν + ν.withDensity (s.indicator (μ.rnDeriv ν))
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean
lemma NormedSpace.exp_continuousMap_eq (f : C(α, 𝕜)) :
    exp 𝕜 f = (⟨exp 𝕜 ∘ f, exp_continuous.comp f.continuous⟩ : C(α, 𝕜))

Proof state:
case h
𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
a : α
h_sum : Summable fun n => (expSeries 𝕜 C(α, 𝕜) n) fun x => f
⊢ (∑' (n : ℕ), (expSeries 𝕜 C(α, 𝕜) n) fun x => f) a = { toFun := exp 𝕜 ∘ ⇑f, continuous_toFun := ⋯ } a

Tactic:
simp_rw [← ContinuousMap.tsum_apply h_sum a, NormedSpace.expSeries_apply_eq]

Result:
case h
𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
a : α
h_sum : Summable fun n => (expSeries 𝕜 C(α, 𝕜) n) fun x => f
⊢ ∑' (i : ℕ), ((↑i.factorial)⁻¹ • f ^ i) a = { toFun := exp 𝕜 ∘ ⇑f, continuous_toFun := ⋯ } a

Proof state:
case h
𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
a : α
⊢ (exp 𝕜 f) a = { toFun := exp 𝕜 ∘ ⇑f, continuous_toFun := ⋯ } a

Tactic:
simp only [Function.comp_apply, NormedSpace.exp, FormalMultilinearSeries.sum]

Result:
case h
𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
a : α
⊢ (∑' (n : ℕ), (expSeries 𝕜 C(α, 𝕜) n) fun x => f) a = { toFun := exp 𝕜 ∘ ⇑f, continuous_toFun := ⋯ } a

Proof state:
case h
𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
a : α
h_sum : Summable fun n => (expSeries 𝕜 C(α, 𝕜) n) fun x => f
⊢ ∑' (i : ℕ), ((↑i.factorial)⁻¹ • f ^ i) a = { toFun := exp 𝕜 ∘ ⇑f, continuous_toFun := ⋯ } a

Tactic:
simp [NormedSpace.exp_eq_tsum]

Result:
no goals

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
⊢ exp 𝕜 f = { toFun := exp 𝕜 ∘ ⇑f, continuous_toFun := ⋯ }

Tactic:
ext a

Result:
case h
𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
a : α
⊢ (exp 𝕜 f) a = { toFun := exp 𝕜 ∘ ⇑f, continuous_toFun := ⋯ } a

Proof state:
case h
𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
a : α
⊢ (∑' (n : ℕ), (expSeries 𝕜 C(α, 𝕜) n) fun x => f) a = { toFun := exp 𝕜 ∘ ⇑f, continuous_toFun := ⋯ } a

Tactic:
have h_sum := NormedSpace.expSeries_summable (𝕂 := 𝕜) f

Result:
case h
𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
a : α
h_sum : Summable fun n => (expSeries 𝕜 C(α, 𝕜) n) fun x => f
⊢ (∑' (n : ℕ), (expSeries 𝕜 C(α, 𝕜) n) fun x => f) a = { toFun := exp 𝕜 ∘ ⇑f, continuous_toFun := ⋯ } a