harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
theorem IsLocalMin.deriv_eq_zero (h : IsLocalMin f a) : deriv f a = 0

Proof state:
f : ℝ → ℝ
a : ℝ
h : IsLocalMin f a
⊢ deriv f a = 0

Tactic:
classical
exact if hf : DifferentiableAt ℝ f a then h.hasDerivAt_eq_zero hf.hasDerivAt
else deriv_zero_of_not_differentiableAt hf

Result:
no goals

Proof state:
f : ℝ → ℝ
a : ℝ
h : IsLocalMin f a
⊢ deriv f a = 0

Tactic:
exact if hf : DifferentiableAt ℝ f a then h.hasDerivAt_eq_zero hf.hasDerivAt
else deriv_zero_of_not_differentiableAt hf

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem iteratedDeriv_eq_equiv_comp : iteratedDeriv n f =
    (ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDeriv 𝕜 n f

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
⊢ iteratedDeriv n f = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDeriv 𝕜 n f

Tactic:
ext x

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ iteratedDeriv n f x = (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDeriv 𝕜 n f) x

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ iteratedDeriv n f x = (⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDeriv 𝕜 n f) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem mem_closedBall' : y ∈ closedBall x ε ↔ dist x y ≤ ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε : ℝ
⊢ y ∈ closedBall x ε ↔ dist x y ≤ ε

Tactic:
rw [dist_comm, mem_closedBall]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem pmap_attachWith (l : List α) {p : {x // q x} → Prop} (f : ∀ a, p a → β) (H₁ H₂) :
    pmap f (l.attachWith q H₁) H₂ =
      l.pmap (P := fun a => ∃ h : q a, p ⟨a, h⟩)
        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨H₁ _ h, H₂ ⟨a, H₁ _ h⟩ (by simpa)⟩)

Proof state:
α : Type ?u.42960
q : α → Prop
β : Type ?u.42990
l : List α
p : { x // q x } → Prop
f : (a : { x // q x }) → p a → β
H₁ : ∀ (x : α), x ∈ l → q x
H₂ : ∀ (a : { x // q x }), a ∈ l.attachWith q H₁ → p a
a : α
h : a ∈ l
⊢ ⟨a, ⋯⟩ ∈ l.attachWith q H₁

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
q : α → Prop
β : Type u_2
l : List α
p : { x // q x } → Prop
f : (a : { x // q x }) → p a → β
H₁ : ∀ (x : α), x ∈ l → q x
H₂ : ∀ (a : { x // q x }), a ∈ l.attachWith q H₁ → p a
⊢ pmap f (l.attachWith q H₁) H₂ = pmap (fun a h => f ⟨a, ⋯⟩ ⋯) l ⋯

Tactic:
apply ext_getElem <;> simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp, norm_cast]
lemma ofENat_add (m n : ℕ∞) : ofENat (m + n) = m + n

Proof state:
m n : ℕ∞
⊢ ↑(m + n) = ↑m + ↑n

Tactic:
apply toENat_injOn <;> simp

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem Metric.diam_closure {α : Type*} [PseudoMetricSpace α] (s : Set α) :
    Metric.diam (closure s) = diam s

Proof state:
α : Type u_4
inst✝ : PseudoMetricSpace α
s : Set α
⊢ diam (closure s) = diam s

Tactic:
simp only [Metric.diam, EMetric.diam_closure]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem mem_nhdsWithin_subtype {s : Set α} {a : { x // x ∈ s }} {t u : Set { x // x ∈ s }} :
    t ∈ 𝓝[u] a ↔ t ∈ comap ((↑) : s → α) (𝓝[(↑) '' u] a)

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
a : { x // x ∈ s }
t u : Set { x // x ∈ s }
⊢ t ∈ 𝓝[u] a ↔ t ∈ comap Subtype.val (𝓝[Subtype.val '' u] ↑a)

Tactic:
rw [nhdsWithin, nhds_subtype, principal_subtype, ← comap_inf, ← nhdsWithin]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem toOuterMeasure_apply_singleton (a : α) : p.toOuterMeasure {a} = p a

Proof state:
case refine_1
α : Type u_1
p : PMF α
a b : α
hb : b ≠ a
⊢ {a}.indicator (⇑p) b = 0

Tactic:
classical exact ite_eq_right_iff.2 fun hb' => False.elim <| hb hb'

Result:
no goals

Proof state:
case refine_2
α : Type u_1
p : PMF α
a : α
⊢ {a}.indicator (⇑p) a = p a

Tactic:
exact ite_eq_left_iff.2 fun ha' => False.elim <| ha' rfl

Result:
no goals

Proof state:
case refine_2
α : Type u_1
p : PMF α
a : α
⊢ {a}.indicator (⇑p) a = p a

Tactic:
classical exact ite_eq_left_iff.2 fun ha' => False.elim <| ha' rfl

Result:
no goals

Proof state:
case refine_1
α : Type u_1
p : PMF α
a b : α
hb : b ≠ a
⊢ {a}.indicator (⇑p) b = 0

Tactic:
exact ite_eq_right_iff.2 fun hb' => False.elim <| hb hb'

Result:
no goals

Proof state:
α : Type u_1
p : PMF α
a : α
⊢ p.toOuterMeasure {a} = p a

Tactic:
refine (p.toOuterMeasure_apply {a}).trans ((tsum_eq_single a fun b hb => ?_).trans ?_)

Result:
case refine_1
α : Type u_1
p : PMF α
a b : α
hb : b ≠ a
⊢ {a}.indicator (⇑p) b = 0

case refine_2
α : Type u_1
p : PMF α
a : α
⊢ {a}.indicator (⇑p) a = p a
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem rename_comp_bind₁ {υ : Type*} (f : σ → MvPolynomial τ R) (g : τ → υ) :
    (rename g).comp (bind₁ f) = bind₁ fun i => rename g <| f i

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → υ
⊢ (rename g).comp (bind₁ f) = bind₁ fun i => (rename g) (f i)

Tactic:
ext1 i

Result:
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → υ
i : σ
⊢ ((rename g).comp (bind₁ f)) (X i) = (bind₁ fun i => (rename g) (f i)) (X i)

Proof state:
case hf
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
υ : Type u_6
f : σ → MvPolynomial τ R
g : τ → υ
i : σ
⊢ ((rename g).comp (bind₁ f)) (X i) = (bind₁ fun i => (rename g) (f i)) (X i)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Nucleus.lean
theorem inf_apply (m n : Nucleus X) (x : X) : (m ⊓ n) x = m x ⊓ n x

Proof state:
X : Type u_1
inst✝ : CompleteLattice X
m n : Nucleus X
x : X
⊢ (m ⊓ n) x = m x ⊓ n x

Tactic:
rw [← sInf_pair, sInf_apply, iInf_pair]

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem Perm.subtypeCongr.left_apply {a : ε} (h : p a) : ep.subtypeCongr en a = ep ⟨a, h⟩

Proof state:
ε : Type u_9
p : ε → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
a : ε
h : p a
⊢ (ep.subtypeCongr en) a = ↑(ep ⟨a, h⟩)

Tactic:
simp [Perm.subtypeCongr.apply, h]

Result:
no goals
-- Mathlib/Topology/Exterior.lean
lemma exterior_minimal (h₁ : s ⊆ t) (h₂ : IsOpen t) : exterior s ⊆ t

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h₁ : s ⊆ t
h₂ : IsOpen t
⊢ exterior s ⊆ t

Tactic:
rw [exterior_def]

Result:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h₁ : s ⊆ t
h₂ : IsOpen t
⊢ ⋂₀ {t | IsOpen t ∧ s ⊆ t} ⊆ t

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
h₁ : s ⊆ t
h₂ : IsOpen t
⊢ ⋂₀ {t | IsOpen t ∧ s ⊆ t} ⊆ t

Tactic:
exact sInter_subset_of_mem ⟨h₂, h₁⟩

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem toReal_eq_toReal_iff (x y : ℝ≥0∞) :
    x.toReal = y.toReal ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0

Proof state:
x y : ℝ≥0∞
⊢ x.toReal = y.toReal ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0

Tactic:
simp only [ENNReal.toReal, NNReal.coe_inj, toNNReal_eq_toNNReal_iff]

Result:
no goals
-- Mathlib/Data/List/Permutation.lean
theorem permutations_append (is ts : List α) :
    permutations (is ++ ts) = (permutations is).map (· ++ ts) ++ permutationsAux ts is.reverse

Proof state:
α : Type u_1
is ts : List α
⊢ (is ++ ts).permutations = map (fun x => x ++ ts) is.permutations ++ ts.permutationsAux is.reverse

Tactic:
simp [permutations, permutationsAux_append]

Result:
no goals
-- Mathlib/Data/PFun.lean
theorem comp_id (f : α →. β) : f.comp (PFun.id α) = f :=
  ext fun _ _ => by simp

Proof state:
α : Type u_1
β : Type u_2
f : α →. β
x✝¹ : α
x✝ : β
⊢ x✝ ∈ f.comp (PFun.id α) x✝¹ ↔ x✝ ∈ f x✝¹

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.closure_diff_ssubset (hI : M.Indep I) (hX : (I ∩ X).Nonempty) :
    M.closure (I \ X) ⊂ M.closure I

Proof state:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.Indep I
hX : (I ∩ X).Nonempty
⊢ M.closure (I \ X) ⊂ M.closure I

Tactic:
refine hI.closure_ssubset_closure <| diff_subset.ssubset_of_ne fun h ↦ ?_

Result:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.Indep I
hX : (I ∩ X).Nonempty
h : I \ X = I
⊢ False

Proof state:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.Indep I
hX : (I ∩ X).Nonempty
h : I ∩ X = ∅
⊢ False

Tactic:
simp [h] at hX

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.Indep I
hX : (I ∩ X).Nonempty
h : I \ X = I
⊢ False

Tactic:
rw [sdiff_eq_left, disjoint_iff_inter_eq_empty] at h

Result:
α : Type u_2
M : Matroid α
X I : Set α
hI : M.Indep I
hX : (I ∩ X).Nonempty
h : I ∩ X = ∅
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem cond_eq_true_distrib : ∀(c t f : Bool),
    (cond c t f = true) = ite (c = true) (t = true) (f = true)

Proof state:
⊢ ∀ (c t f : Bool), ((bif c then t else f) = true) = if c = true then t = true else f = true

Tactic:
decide

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem factorThruImage_eq {Δ Δ'' : SimplexCategory} {φ : Δ ⟶ Δ''} {e : Δ ⟶ image φ} [Epi e]
    {i : image φ ⟶ Δ''} [Mono i] (fac : e ≫ i = φ) : factorThruImage φ = e

Proof state:
Δ Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ image φ
inst✝¹ : Epi e
i : image φ ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
⊢ factorThruImage φ = e

Tactic:
rw [← cancel_mono i, fac, ← image_ι_eq fac, image.fac]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem tendsto_nhds_left {f : Filter β} {u : β → α} {a : α} :
    Tendsto u f (𝓝 a) ↔ Tendsto (fun x => (u x, a)) f (𝓤 α)

Proof state:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto u f (𝓝 a) ↔ Tendsto (fun x => (u x, a)) f (𝓤 α)

Tactic:
rw [nhds_eq_comap_uniformity', tendsto_comap_iff]

Result:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto ((fun y => (y, a)) ∘ u) f (𝓤 α) ↔ Tendsto (fun x => (u x, a)) f (𝓤 α)

Proof state:
α : Type ua
β : Type ub
inst✝ : UniformSpace α
f : Filter β
u : β → α
a : α
⊢ Tendsto ((fun y => (y, a)) ∘ u) f (𝓤 α) ↔ Tendsto (fun x => (u x, a)) f (𝓤 α)

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem pullbackIsoUnopPushout_inv_fst {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g]
    [HasPushout f.op g.op] :
    (pullbackIsoUnopPushout f g).inv ≫ pullback.fst f g =
      (pushout.inl _ _ : _ ⟶ pushout f.op g.op).unop :=
  (IsLimit.conePointUniqueUpToIso_inv_comp _ _ _).trans (by simp [unop_id (X := { unop := X })])

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ (PushoutCocone.unop (colimit.cocone (span f.op g.op))).π.app WalkingCospan.left = (pushout.inl f.op g.op).unop

Tactic:
simp [unop_id (X := { unop := X })]

Result:
no goals
-- Mathlib/GroupTheory/Perm/List.lean
theorem formPerm_apply_getLast (x : α) (xs : List α) :
    formPerm (x :: xs) ((x :: xs).getLast (cons_ne_nil x xs)) = x

Proof state:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs : List α
⊢ (x :: xs).formPerm ((x :: xs).getLast ⋯) = x

Tactic:
induction' xs using List.reverseRecOn with xs y _ generalizing x <;> simp

Result:
no goals
-- Mathlib/NumberTheory/Pell.lean
theorem is_pell_solution_iff_mem_unitary {d : ℤ} {a : ℤ√d} :
    a.re ^ 2 - d * a.im ^ 2 = 1 ↔ a ∈ unitary (ℤ√d)

Proof state:
d : ℤ
a : ℤ√d
⊢ a.re ^ 2 - d * a.im ^ 2 = 1 ↔ a ∈ unitary (ℤ√d)

Tactic:
rw [← norm_eq_one_iff_mem_unitary, norm_def, sq, sq, ← mul_assoc]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_C : (C r).smeval x = r • x ^ 0

Proof state:
R : Type u_1
inst✝³ : Semiring R
r : R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
⊢ (C r).smeval x = r • x ^ 0

Tactic:
simp only [smeval_eq_sum, smul_pow, zero_smul, sum_C_index]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma spanning_iff_compl_coindep (hS : S ⊆ M.E

Proof state:
α : Type u_2
M : Matroid α
S : Set α
hS : autoParam (S ⊆ M.E) _auto✝
⊢ M.Spanning S ↔ M.Coindep (M.E \ S)

Tactic:
rw [coindep_iff_compl_spanning, diff_diff_cancel_left hS]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_add_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n + y) n = Int.bmod (x + y) n

Proof state:
y x : Int
n : Nat
⊢ (x % ↑n + y).bmod n = (x + y).bmod n

Tactic:
simp [Int.emod_def, Int.sub_eq_add_neg]

Result:
y x : Int
n : Nat
⊢ (x + -(↑n * (x / ↑n)) + y).bmod n = (x + y).bmod n

Proof state:
y x : Int
n : Nat
⊢ (x + -(↑n * (x / ↑n)) + y).bmod n = (x + y).bmod n

Tactic:
rw [←Int.mul_neg, Int.add_right_comm,  Int.bmod_add_mul_cancel]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem head?_eq_none_iff : l.head? = none ↔ l = []

Proof state:
α✝ : Type u_1
l : List α✝
⊢ l.head? = none ↔ l = []

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma eq_div_of_mul_eq_right (hc : c ≠ 0) (h : c * a = b) : a = b / c

Proof state:
a b c : ℕ
hc : c ≠ 0
h : c * a = b
⊢ a = b / c

Tactic:
rw [← h, Nat.mul_div_cancel_left _ (Nat.pos_iff_ne_zero.2 hc)]

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem continuousWithinAt_Icc_iff_Iic (h : a < b) :
    ContinuousWithinAt f (Icc a b) b ↔ ContinuousWithinAt f (Iic b) b

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
inst✝ : TopologicalSpace β
a b : α
f : α → β
h : a < b
⊢ ContinuousWithinAt f (Icc a b) b ↔ ContinuousWithinAt f (Iic b) b

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_Icc_eq_nhdsLE h]

Result:
no goals
-- Mathlib/RingTheory/PowerBasis.lean
theorem natDegree_minpoly [Nontrivial A] (pb : PowerBasis A S) :
    (minpoly A pb.gen).natDegree = pb.dim

Proof state:
S : Type u_2
inst✝³ : Ring S
A : Type u_4
inst✝² : CommRing A
inst✝¹ : Algebra A S
inst✝ : Nontrivial A
pb : PowerBasis A S
⊢ (minpoly A pb.gen).natDegree = pb.dim

Tactic:
rw [← minpolyGen_eq, natDegree_minpolyGen]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma pullbacks_monotone : Monotone (pullbacks (C := C))

Proof state:
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : MorphismProperty C
h : a✝ ≤ b✝
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
w✝⁴ w✝³ : C
w✝² : w✝⁴ ⟶ w✝³
w✝¹ : X✝ ⟶ w✝⁴
w✝ : Y✝ ⟶ w✝³
hp : a✝ w✝²
sq : IsPullback w✝¹ f✝ w✝² w✝
⊢ b✝.pullbacks f✝

Tactic:
exact ⟨_, _, _, _, _, h _ hp, sq⟩

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
⊢ Monotone pullbacks

Tactic:
rintro _ _ h _ _ _ ⟨_, _, _, _, _, hp, sq⟩

Result:
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : MorphismProperty C
h : a✝ ≤ b✝
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
w✝⁴ w✝³ : C
w✝² : w✝⁴ ⟶ w✝³
w✝¹ : X✝ ⟶ w✝⁴
w✝ : Y✝ ⟶ w✝³
hp : a✝ w✝²
sq : IsPullback w✝¹ f✝ w✝² w✝
⊢ b✝.pullbacks f✝
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem IsHilbertSum.linearIsometryEquiv_symm_apply_single
    [DecidableEq ι] (hV : IsHilbertSum 𝕜 G V) {i : ι} (x : G i) :
    hV.linearIsometryEquiv.symm (lp.single 2 i x) = V i x

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝⁶ : RCLike 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (G i)
inst✝² : (i : ι) → InnerProductSpace 𝕜 (G i)
inst✝¹ : CompleteSpace E
V : (i : ι) → G i →ₗᵢ[𝕜] E
inst✝ : DecidableEq ι
hV : IsHilbertSum 𝕜 G V
i : ι
x : G i
⊢ hV.linearIsometryEquiv.symm (lp.single 2 i x) = (V i) x

Tactic:
simp [IsHilbertSum.linearIsometryEquiv, OrthogonalFamily.linearIsometry_apply_single]

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/Banach.lean
theorem coe_ofBijective (f : E →SL[σ] F) (hinj : ker f = ⊥) (hsurj : LinearMap.range f = ⊤) :
    ↑(ofBijective f hinj hsurj) = f

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst✝⁵ : RingHomInvPair σ σ'
inst✝⁴ : RingHomIsometric σ
inst✝³ : RingHomIsometric σ'
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : RingHomInvPair σ' σ
f : E →SL[σ] F
hinj : LinearMap.ker f = ⊥
hsurj : LinearMap.range f = ⊤
⊢ ↑(ofBijective f hinj hsurj) = f

Tactic:
ext

Result:
case h
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst✝⁵ : RingHomInvPair σ σ'
inst✝⁴ : RingHomIsometric σ
inst✝³ : RingHomIsometric σ'
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : RingHomInvPair σ' σ
f : E →SL[σ] F
hinj : LinearMap.ker f = ⊥
hsurj : LinearMap.range f = ⊤
x✝ : E
⊢ ↑(ofBijective f hinj hsurj) x✝ = f x✝

Proof state:
case h
𝕜 : Type u_1
𝕜' : Type u_2
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NontriviallyNormedField 𝕜'
σ : 𝕜 →+* 𝕜'
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type u_4
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜' F
σ' : 𝕜' →+* 𝕜
inst✝⁵ : RingHomInvPair σ σ'
inst✝⁴ : RingHomIsometric σ
inst✝³ : RingHomIsometric σ'
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : RingHomInvPair σ' σ
f : E →SL[σ] F
hinj : LinearMap.ker f = ⊥
hsurj : LinearMap.range f = ⊤
x✝ : E
⊢ ↑(ofBijective f hinj hsurj) x✝ = f x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/PNat/Interval.lean
theorem card_Ioc : #(Ioc a b) = b - a

Proof state:
a b : ℕ+
⊢ #(Ioc a b) = ↑b - ↑a

Tactic:
rw [← Nat.card_Ioc, ← map_subtype_embedding_Ioc, card_map]

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/KLFun.lean
lemma not_differentiableAt_klFun_zero : ¬ DifferentiableAt ℝ klFun 0

Proof state:
⊢ ¬DifferentiableAt ℝ klFun 0

Tactic:
unfold klFun

Result:
⊢ ¬DifferentiableAt ℝ (fun x => x * log x + 1 - x) 0

Proof state:
⊢ ¬DifferentiableAt ℝ (fun x => x * log x + 1 - x) 0

Tactic:
simpa using not_DifferentiableAt_log_mul_zero

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_eq (x : ℝ) : sinh x = (exp x - exp (-x)) / 2 :=
  ofReal_injective <| by simp [Complex.sinh]

Proof state:
x : ℝ
⊢ ↑(sinh x) = ↑((rexp x - rexp (-x)) / 2)

Tactic:
simp [Complex.sinh]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat)
    (h : j < (a.set i v).size) :
    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v _ ▸ h)

Proof state:
α : Type u_1
a : Array α
i : Nat
h' : i < a.size
v : α
j : Nat
h : j < (a.set i v h').size
⊢ (a.set i v h')[j] = if i = j then v else a[j]

Tactic:
by_cases p : i = j <;> simp [p]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extChartAt_model_space_eq_id (x : E) : extChartAt 𝓘(𝕜, E) x = PartialEquiv.refl E

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
⊢ extChartAt 𝓘(𝕜, E) x = PartialEquiv.refl E

Tactic:
simp only [mfld_simps]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem iff_self_or : ∀ {a b : Bool}, (a = (a || b)) ↔ (b → a)

Proof state:
⊢ ∀ {a b : Bool}, a = (a || b) ↔ b = true → a = true

Tactic:
decide

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem inr_isoIsPushout_inv (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') :
    inr' ≫ (h.isoIsPushout _ _ h').inv = inr

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
P' : C
inl' : X ⟶ P'
inr' : Y ⟶ P'
h : IsPushout f g inl inr
h' : IsPushout f g inl' inr'
⊢ inr' ≫ (isoIsPushout X Y h h').inv = inr

Tactic:
simp only [Iso.comp_inv_eq, inr_isoIsPushout_hom]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Dual.lean
theorem polar_singleton {a : E} : polar 𝕜 {a} = { x | ‖x a‖ ≤ 1 }

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
a : E
⊢ polar 𝕜 {a} = {x | ‖x a‖ ≤ 1}

Tactic:
simp only [polar, LinearMap.polar_singleton, LinearMap.flip_apply, dualPairing_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean
theorem pullbackFst_eq_pullback_snd (F : WalkingParallelPair ⥤ C) :
    pullbackFst F = pullback.snd _ _

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ pullbackFst F =
    pullback.snd (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.left))
      (prod.lift (𝟙 (F.obj WalkingParallelPair.zero)) (F.map WalkingParallelPairHom.right))

Tactic:
convert (eq_whisker pullback.condition Limits.prod.fst :
    (_ : constructEqualizer F ⟶ F.obj WalkingParallelPair.zero) = _) <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mem_zipIdx_iff_getElem? {x : α × Nat} {l : Array α} :
    x ∈ l.zipIdx ↔ l[x.2]? = some x.1

Proof state:
α : Type u_1
x : α × Nat
l : Array α
⊢ x ∈ l.zipIdx ↔ l[x.snd]? = some x.fst

Tactic:
rw [mk_mem_zipIdx_iff_getElem?]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem LinearMap.rank_le_of_surjective (f : M →ₗ[R] M₁) (h : Surjective f) :
    Module.rank R M₁ ≤ Module.rank R M

Proof state:
R : Type u
M M₁ : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] M₁
h : Surjective ⇑f
⊢ Module.rank R ↥(range f) ≤ Module.rank R M

Tactic:
apply rank_range_le

Result:
no goals

Proof state:
R : Type u
M M₁ : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] M₁
h : Surjective ⇑f
⊢ Module.rank R M₁ ≤ Module.rank R M

Tactic:
rw [← rank_range_of_surjective f h]

Result:
R : Type u
M M₁ : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
f : M →ₗ[R] M₁
h : Surjective ⇑f
⊢ Module.rank R ↥(range f) ≤ Module.rank R M
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem ImageMap.mk.injEq' {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] {sq : f ⟶ g}
    (map : image f.hom ⟶ image g.hom)
    (map_ι : map ≫ image.ι g.hom = image.ι f.hom ≫ sq.right

Proof state:
C : Type u
inst✝² : Category.{v, u} C
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
map : image f.hom ⟶ image g.hom
map_ι : autoParam (map ≫ image.ι g.hom = image.ι f.hom ≫ sq.right) _auto✝
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ sq.right
⊢ map = map'

Tactic:
apply ImageMap.map_uniq_aux _ map_ι _ map_ι'

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
map : image f.hom ⟶ image g.hom
map_ι : autoParam (map ≫ image.ι g.hom = image.ι f.hom ≫ sq.right) _auto✝
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ sq.right
⊢ (map = map') = True

Tactic:
simp only [Functor.id_obj, eq_iff_iff, iff_true]

Result:
C : Type u
inst✝² : Category.{v, u} C
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
map : image f.hom ⟶ image g.hom
map_ι : autoParam (map ≫ image.ι g.hom = image.ι f.hom ≫ sq.right) _auto✝
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ sq.right
⊢ map = map'
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem dist_right_midpoint (p₁ p₂ : P) :
    dist p₂ (midpoint 𝕜 p₁ p₂) = ‖(2 : 𝕜)‖⁻¹ * dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : SeminormedAddCommGroup V
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor V P
𝕜 : Type u_5
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 V
inst✝ : Invertible 2
p₁ p₂ : P
⊢ dist p₂ (midpoint 𝕜 p₁ p₂) = ‖2‖⁻¹ * dist p₁ p₂

Tactic:
rw [dist_comm, dist_midpoint_right]

Result:
no goals