harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem closedComplemented_top : ClosedComplemented (⊤ : Submodule R M) :=
  ⟨(id R M).codRestrict ⊤ fun _x => trivial, fun x => Subtype.ext_iff_val.2 <| by simp⟩

Proof state:
R : Type u_1
inst✝³ : Ring R
M : Type u_2
inst✝² : TopologicalSpace M
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : ↥⊤
⊢ ↑(((ContinuousLinearMap.id R M).codRestrict ⊤ ⋯) ↑x) = ↑x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/Basic.lean
theorem Units.neg_smul [Ring R] [AddCommGroup M] [Module R M] (u : Rˣ) (x : M) :
    -u • x = -(u • x)

Proof state:
R : Type u_2
M : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
u : Rˣ
x : M
⊢ -u • x = -(u • x)

Tactic:
rw [Units.smul_def, Units.val_neg, _root_.neg_smul, Units.smul_def]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem infsep_pair_le_toReal_inf (hxy : x ≠ y) :
    ({x, y} : Set α).infsep ≤ (edist x y ⊓ edist y x).toReal

Proof state:
α : Type u_1
inst✝ : EDist α
x y : α
hxy : x ≠ y
⊢ (edist x y ⊓ edist y x).toReal ≤ (edist x y ⊓ edist y x).toReal

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : EDist α
x y : α
hxy : x ≠ y
⊢ {x, y}.infsep ≤ (edist x y ⊓ edist y x).toReal

Tactic:
simp_rw [infsep, einfsep_pair_eq_inf hxy]

Result:
α : Type u_1
inst✝ : EDist α
x y : α
hxy : x ≠ y
⊢ (edist x y ⊓ edist y x).toReal ≤ (edist x y ⊓ edist y x).toReal
-- Mathlib/Topology/Algebra/SeparationQuotient/Section.lean
theorem outCLM_isUniformInducing : IsUniformInducing (outCLM K E)

Proof state:
K : Type u_1
E : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup E
inst✝³ : Module K E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousConstSMul K E
⊢ IsUniformInducing id

Tactic:
exact .id

Result:
no goals

Proof state:
K : Type u_1
E : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup E
inst✝³ : Module K E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousConstSMul K E
⊢ IsUniformInducing ⇑(outCLM K E)

Tactic:
rw [← isUniformInducing_mk.isUniformInducing_comp_iff, mk_comp_outCLM]

Result:
K : Type u_1
E : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup E
inst✝³ : Module K E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
inst✝ : ContinuousConstSMul K E
⊢ IsUniformInducing id
-- Mathlib/Algebra/Ring/NegOnePow.lean
lemma negOnePow_succ (n : ℤ) : (n + 1).negOnePow = - n.negOnePow

Proof state:
n : ℤ
⊢ (n + 1).negOnePow = -n.negOnePow

Tactic:
rw [negOnePow_add, negOnePow_one, mul_neg, mul_one]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
@[simp] lemma ncard_graphOn (s : Set α) (f : α → β) : (s.graphOn f).ncard = s.ncard

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ (graphOn f s).ncard = s.ncard

Tactic:
rw [← ncard_image_of_injOn fst_injOn_graph, image_fst_graphOn]

Result:
no goals
-- Mathlib/Order/Cover.lean
@[simp] lemma bot_covBy_coe : ⊥ ⋖ (a : WithBot α) ↔ IsMin a

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ ⊥ ⋖ ↑a ↔ IsMin a

Tactic:
simp only [covBy_iff_Ioo_eq, ← image_coe_Iio, bot_lt_coe, image_eq_empty,
  true_and, Iio_eq_empty_iff]

Result:
no goals
-- Mathlib/Dynamics/Ergodic/Action/Basic.lean
theorem aeconst_of_forall_smul_ae_eq (hm : NullMeasurableSet s μ) (h : ∀ g : G, g • s =ᵐ[μ] s) :
    EventuallyConst s (ae μ) :=
  aeconst_of_forall_preimage_smul_ae_eq G hm fun g ↦ by
    simpa only [preimage_smul] using h g⁻¹

Proof state:
G : Type u_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : ErgodicSMul G α μ
s : Set α
hm : NullMeasurableSet s μ
h : ∀ (g : G), g • s =ᶠ[ae μ] s
g : G
⊢ (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s

Tactic:
simpa only [preimage_smul] using h g⁻¹

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem injective_sum_to : Function.Injective (sum_to C ho)

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x✝¹ : ↑(GoodProducts (π C fun x => ord I x < o))
x✝ : ↑(MaxProducts C ho)
a : Products I
ha : a ∈ GoodProducts (π C fun x => ord I x < o)
b : Products I
hb : a ∈ MaxProducts C ho
hab : a = b
ha' : ord I (term I ho) < o
⊢ False

Tactic:
simp only [ord_term_aux, lt_self_iff_false] at ha'

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ Function.Injective (sum_to C ho)

Tactic:
refine Function.Injective.sumElim Subtype.val_injective Subtype.val_injective
  (fun ⟨a,ha⟩ ⟨b,hb⟩  ↦ (fun (hab : a = b) ↦ ?_))

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x✝¹ : ↑(GoodProducts (π C fun x => ord I x < o))
x✝ : ↑(MaxProducts C ho)
a : Products I
ha : a ∈ GoodProducts (π C fun x => ord I x < o)
b : Products I
hb : b ∈ MaxProducts C ho
hab : a = b
⊢ False

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x✝¹ : ↑(GoodProducts (π C fun x => ord I x < o))
x✝ : ↑(MaxProducts C ho)
a : Products I
ha : a ∈ GoodProducts (π C fun x => ord I x < o)
b : Products I
hb : b ∈ MaxProducts C ho
hab : a = b
⊢ False

Tactic:
rw [← hab] at hb

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x✝¹ : ↑(GoodProducts (π C fun x => ord I x < o))
x✝ : ↑(MaxProducts C ho)
a : Products I
ha : a ∈ GoodProducts (π C fun x => ord I x < o)
b : Products I
hb : a ∈ MaxProducts C ho
hab : a = b
⊢ False

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x✝¹ : ↑(GoodProducts (π C fun x => ord I x < o))
x✝ : ↑(MaxProducts C ho)
a : Products I
ha : a ∈ GoodProducts (π C fun x => ord I x < o)
b : Products I
hb : a ∈ MaxProducts C ho
hab : a = b
⊢ False

Tactic:
have ha' := Products.prop_of_isGood  C _ ha (term I ho) hb.2

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
x✝¹ : ↑(GoodProducts (π C fun x => ord I x < o))
x✝ : ↑(MaxProducts C ho)
a : Products I
ha : a ∈ GoodProducts (π C fun x => ord I x < o)
b : Products I
hb : a ∈ MaxProducts C ho
hab : a = b
ha' : ord I (term I ho) < o
⊢ False
-- Mathlib/Data/Bool/Basic.lean
theorem coe_true : ↑true = True

Proof state:
⊢ (true = true) = True

Tactic:
simp

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
theorem le_def {p q : ℚ≥0} : p ≤ q ↔ p.num * q.den ≤ q.num * p.den

Proof state:
p q : ℚ≥0
⊢ (↑p).num * ↑(↑q).den ≤ (↑q).num * ↑(↑p).den ↔ p.num * q.den ≤ q.num * p.den

Tactic:
norm_cast

Result:
no goals

Proof state:
p q : ℚ≥0
⊢ p ≤ q ↔ p.num * q.den ≤ q.num * p.den

Tactic:
rw [← NNRat.coe_le_coe, Rat.le_def]

Result:
p q : ℚ≥0
⊢ (↑p).num * ↑(↑q).den ≤ (↑q).num * ↑(↑p).den ↔ p.num * q.den ≤ q.num * p.den
-- Mathlib/MeasureTheory/Function/Jacobian.lean
lemma _root_.MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul
    (f : ℝ ≃ᵐ ℝ) {s : Set ℝ} (hs : MeasurableSet s)
    {g : ℝ → ℝ} (hg : ∀ᵐ x, x ∈ f '' s → 0 ≤ g x) (hg_int : IntegrableOn g (f '' s))
    {f' : ℝ → ℝ} (hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) :
    (volume.withDensity (fun x ↦ ENNReal.ofReal (g x))).map f.symm s
      = ENNReal.ofReal (∫ x in s, |f' x| * g (f x))

Proof state:
f : ℝ ≃ᵐ ℝ
s : Set ℝ
hs : MeasurableSet s
g : ℝ → ℝ
hg : ∀ᵐ (x : ℝ), x ∈ ⇑f '' s → 0 ≤ g x
hg_int : IntegrableOn g (⇑f '' s) volume
f' : ℝ → ℝ
hf' : ∀ x ∈ s, HasDerivWithinAt (⇑f) (f' x) s x
⊢ ENNReal.ofReal (∫ (x : ℝ) in s, |(ContinuousLinearMap.smulRight 1 (f' x)).det| * g (f x)) =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))

Tactic:
simp only [det_one_smulRight]

Result:
no goals

Proof state:
f : ℝ ≃ᵐ ℝ
s : Set ℝ
hs : MeasurableSet s
g : ℝ → ℝ
hg : ∀ᵐ (x : ℝ), x ∈ ⇑f '' s → 0 ≤ g x
hg_int : IntegrableOn g (⇑f '' s) volume
f' : ℝ → ℝ
hf' : ∀ x ∈ s, HasDerivWithinAt (⇑f) (f' x) s x
⊢ (Measure.map (⇑f.symm) (volume.withDensity fun x => ENNReal.ofReal (g x))) s =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))

Tactic:
rw [MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul volume hs
    f hg hg_int hf']

Result:
f : ℝ ≃ᵐ ℝ
s : Set ℝ
hs : MeasurableSet s
g : ℝ → ℝ
hg : ∀ᵐ (x : ℝ), x ∈ ⇑f '' s → 0 ≤ g x
hg_int : IntegrableOn g (⇑f '' s) volume
f' : ℝ → ℝ
hf' : ∀ x ∈ s, HasDerivWithinAt (⇑f) (f' x) s x
⊢ ENNReal.ofReal (∫ (x : ℝ) in s, |(ContinuousLinearMap.smulRight 1 (f' x)).det| * g (f x)) =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))
-- Mathlib/Analysis/Calculus/BumpFunction/Basic.lean
theorem pos_of_mem_ball (hx : x ∈ ball c f.rOut) : 0 < f x :=
  f.nonneg.lt_of_ne' <| by rwa [← support_eq, mem_support] at hx

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
hx : x ∈ ball c f.rOut
⊢ ↑f x ≠ 0

Tactic:
rwa [← support_eq, mem_support] at hx

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem liftRel_destruct {R : α → β → Prop} {s : WSeq α} {t : WSeq β} :
    LiftRel R s t → Computation.LiftRel (LiftRelO R (LiftRel R)) (destruct s) (destruct t)
  | ⟨R, h1, h2⟩ => by
    refine Computation.LiftRel.imp ?_ _ _ (h2 h1)
    apply LiftRelO.imp_right
    exact fun s' t' h' => ⟨R, h', @h2⟩

Proof state:
α : Type u
β : Type v
R✝ : α → β → Prop
s : WSeq α
t : WSeq β
R : WSeq α → WSeq β → Prop
h1 : R s t
h2 : ∀ {s : WSeq α} {t : WSeq β}, R s t → Computation.LiftRel (LiftRelO R✝ R) s.destruct t.destruct
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R✝ R a b → LiftRelO R✝ (LiftRel R✝) a b

Tactic:
apply LiftRelO.imp_right

Result:
case H
α : Type u
β : Type v
R✝ : α → β → Prop
s : WSeq α
t : WSeq β
R : WSeq α → WSeq β → Prop
h1 : R s t
h2 : ∀ {s : WSeq α} {t : WSeq β}, R s t → Computation.LiftRel (LiftRelO R✝ R) s.destruct t.destruct
⊢ ∀ (s : WSeq α) (t : WSeq β), R s t → LiftRel R✝ s t

Proof state:
case H
α : Type u
β : Type v
R✝ : α → β → Prop
s : WSeq α
t : WSeq β
R : WSeq α → WSeq β → Prop
h1 : R s t
h2 : ∀ {s : WSeq α} {t : WSeq β}, R s t → Computation.LiftRel (LiftRelO R✝ R) s.destruct t.destruct
⊢ ∀ (s : WSeq α) (t : WSeq β), R s t → LiftRel R✝ s t

Tactic:
exact fun s' t' h' => ⟨R, h', @h2⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
R✝ : α → β → Prop
s : WSeq α
t : WSeq β
R : WSeq α → WSeq β → Prop
h1 : R s t
h2 : ∀ {s : WSeq α} {t : WSeq β}, R s t → Computation.LiftRel (LiftRelO R✝ R) s.destruct t.destruct
⊢ Computation.LiftRel (LiftRelO R✝ (LiftRel R✝)) s.destruct t.destruct

Tactic:
refine Computation.LiftRel.imp ?_ _ _ (h2 h1)

Result:
α : Type u
β : Type v
R✝ : α → β → Prop
s : WSeq α
t : WSeq β
R : WSeq α → WSeq β → Prop
h1 : R s t
h2 : ∀ {s : WSeq α} {t : WSeq β}, R s t → Computation.LiftRel (LiftRelO R✝ R) s.destruct t.destruct
⊢ ∀ {a : Option (α × WSeq α)} {b : Option (β × WSeq β)}, LiftRelO R✝ R a b → LiftRelO R✝ (LiftRel R✝) a b
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem toCNF.go_sat (aig : AIG Nat) (start : Nat) (h1 : start < aig.decls.size) (assign1 : Nat → Bool)
    (state : toCNF.State aig) :
    (go aig start h1 state).val.Sat (cnfSatAssignment aig assign1)

Proof state:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
state : State aig
this : CNF.Sat (cnfSatAssignment aig assign1) (go aig start h1 state).val.cnf
⊢ CNF.Sat (cnfSatAssignment aig assign1) (go aig start h1 state).val.cnf

Tactic:
simp [this]

Result:
no goals

Proof state:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
state : State aig
⊢ State.Sat (cnfSatAssignment aig assign1) (go aig start h1 state).val

Tactic:
have := (go aig start h1 state).val.inv assign1

Result:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
state : State aig
this : CNF.Sat (cnfSatAssignment aig assign1) (go aig start h1 state).val.cnf
⊢ State.Sat (cnfSatAssignment aig assign1) (go aig start h1 state).val

Proof state:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
state : State aig
this : CNF.Sat (cnfSatAssignment aig assign1) (go aig start h1 state).val.cnf
⊢ State.Sat (cnfSatAssignment aig assign1) (go aig start h1 state).val

Tactic:
rw [State.sat_iff]

Result:
aig : AIG Nat
start : Nat
h1 : start < aig.decls.size
assign1 : Nat → Bool
state : State aig
this : CNF.Sat (cnfSatAssignment aig assign1) (go aig start h1 state).val.cnf
⊢ CNF.Sat (cnfSatAssignment aig assign1) (go aig start h1 state).val.cnf
-- Mathlib/RingTheory/Artinian/Module.lean
theorem isArtinian_of_range_eq_ker [IsArtinian R M] [IsArtinian R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P)
    (h : LinearMap.range f = LinearMap.ker g) : IsArtinian R N :=
  wellFounded_lt_exact_sequence (LinearMap.range f) (Submodule.map (f.ker.liftQ f le_rfl))
    (Submodule.comap (f.ker.liftQ f le_rfl))
    (Submodule.comap g.rangeRestrict) (Submodule.map g.rangeRestrict)
    (Submodule.gciMapComap <| LinearMap.ker_eq_bot.mp <| Submodule.ker_liftQ_eq_bot _ _ _ le_rfl)
    (Submodule.giMapComap g.surjective_rangeRestrict)
    (by simp [Submodule.map_comap_eq, inf_comm, Submodule.range_liftQ])
    (by simp [Submodule.comap_map_eq, h])

Proof state:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
inst✝¹ : IsArtinian R M
inst✝ : IsArtinian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : LinearMap.range f = LinearMap.ker g
⊢ ∀ (a : Submodule R N),
    Submodule.map ((LinearMap.ker f).liftQ f ⋯) (Submodule.comap ((LinearMap.ker f).liftQ f ⋯) a) =
      a ⊓ LinearMap.range f

Tactic:
simp [Submodule.map_comap_eq, inf_comm, Submodule.range_liftQ]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup P
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R M
inst✝³ : Module R P
inst✝² : Module R N
inst✝¹ : IsArtinian R M
inst✝ : IsArtinian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : LinearMap.range f = LinearMap.ker g
⊢ ∀ (a : Submodule R N), Submodule.comap g.rangeRestrict (Submodule.map g.rangeRestrict a) = a ⊔ LinearMap.range f

Tactic:
simp [Submodule.comap_map_eq, h]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙHom_nonneg_iff [NonnegSpectrumClass R A] {a : A} (ha : p a) {f : C(σₙ R a, R)₀} :
    0 ≤ cfcₙHom ha f ↔ 0 ≤ f

Proof state:
case mp
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : OrderedCommSemiring R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : ∀ (α : Type ?u.875310) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
⊢ 0 ≤ (cfcₙHom ha) f → 0 ≤ f

Tactic:
exact fun hf x ↦
  (cfcₙHom_map_quasispectrum ha (R := R) _ ▸ quasispectrum_nonneg_of_nonneg (cfcₙHom ha f) hf)
  _ ⟨x, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : OrderedCommSemiring R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : ∀ (α : Type ?u.875310) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
⊢ 0 ≤ (cfcₙHom ha) f ↔ 0 ≤ f

Tactic:
constructor

Result:
case mp
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : OrderedCommSemiring R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : ∀ (α : Type ?u.875310) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
⊢ 0 ≤ (cfcₙHom ha) f → 0 ≤ f

case mpr
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : OrderedCommSemiring R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalSemiring R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : ∀ (α : Type ?u.875310) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
a : A
ha : p a
f : C(↑(σₙ R a), R)₀
⊢ 0 ≤ f → 0 ≤ (cfcₙHom ha) f
-- Mathlib/Analysis/Calculus/Gradient/Basic.lean
theorem HasGradientAtFilter.hasDerivAtFilter (h : HasGradientAtFilter g g' u L') :
    HasDerivAtFilter g (starRingEnd 𝕜 g') u L'

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasGradientAtFilter g g' u L'
⊢ ContinuousLinearMap.smulRight 1 ((starRingEnd 𝕜) g') = (toDual 𝕜 𝕜) g'

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasGradientAtFilter g g' u L'
⊢ (ContinuousLinearMap.smulRight 1 ((starRingEnd 𝕜) g')) 1 = ((toDual 𝕜 𝕜) g') 1

Proof state:
case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasGradientAtFilter g g' u L'
⊢ (ContinuousLinearMap.smulRight 1 ((starRingEnd 𝕜) g')) 1 = ((toDual 𝕜 𝕜) g') 1

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasGradientAtFilter g g' u L'
⊢ HasDerivAtFilter g ((starRingEnd 𝕜) g') u L'

Tactic:
have : ContinuousLinearMap.smulRight (1 : 𝕜 →L[𝕜] 𝕜) (starRingEnd 𝕜 g') = (toDual 𝕜 𝕜) g' := by
  ext; simp

Result:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasGradientAtFilter g g' u L'
this : ContinuousLinearMap.smulRight 1 ((starRingEnd 𝕜) g') = (toDual 𝕜 𝕜) g'
⊢ HasDerivAtFilter g ((starRingEnd 𝕜) g') u L'

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
g : 𝕜 → 𝕜
g' u : 𝕜
L' : Filter 𝕜
h : HasGradientAtFilter g g' u L'
this : ContinuousLinearMap.smulRight 1 ((starRingEnd 𝕜) g') = (toDual 𝕜 𝕜) g'
⊢ HasDerivAtFilter g ((starRingEnd 𝕜) g') u L'

Tactic:
rwa [HasDerivAtFilter, this]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mdifferentiableOn_univ : MDifferentiableOn I I' f univ ↔ MDifferentiable I I' f

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
⊢ MDifferentiableOn I I' f univ ↔ MDifferentiable I I' f

Tactic:
simp only [MDifferentiableOn, mdifferentiableWithinAt_univ, mfld_simps]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
⊢ (∀ (x : M), MDifferentiableAt I I' f x) ↔ MDifferentiable I I' f

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
⊢ (∀ (x : M), MDifferentiableAt I I' f x) ↔ MDifferentiable I I' f

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Trunc.lean
theorem coeff_trunc (m : σ →₀ ℕ) (φ : MvPowerSeries σ R) :
    (trunc R n φ).coeff m = if m < n then coeff R m φ else 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
φ : MvPowerSeries σ R
⊢ MvPolynomial.coeff m ((trunc R n) φ) = if m < n then (coeff R m) φ else 0

Tactic:
classical simp [trunc, coeff_truncFun]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n m : σ →₀ ℕ
φ : MvPowerSeries σ R
⊢ MvPolynomial.coeff m ((trunc R n) φ) = if m < n then (coeff R m) φ else 0

Tactic:
simp [trunc, coeff_truncFun]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem e_isoExt_hom : F.e ≫ (isoExt hF hF').hom = F'.e

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ F.e ≫ (hF.isoExt hF').hom = F'.e

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
@[simp] protected lemma inv_zero : (0 : Finset α)⁻¹ = 0

Proof state:
case h
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a✝ : α
⊢ a✝ ∈ 0⁻¹ ↔ a✝ ∈ 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
⊢ 0⁻¹ = 0

Tactic:
ext

Result:
case h
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a✝ : α
⊢ a✝ ∈ 0⁻¹ ↔ a✝ ∈ 0
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem AnalyticOnNhd.fderiv_of_isOpen (h : AnalyticOnNhd 𝕜 f s) (hs : IsOpen s) :
    AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s

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
f : E → F
s : Set E
h : AnalyticOnNhd 𝕜 f s
hs : IsOpen s
⊢ AnalyticOnNhd 𝕜 (fderiv 𝕜 f) s

Tactic:
rw [← hs.analyticOn_iff_analyticOnNhd] at h ⊢

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hs : IsOpen s
⊢ AnalyticOn 𝕜 (fderiv 𝕜 f) s

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
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hs : IsOpen s
⊢ AnalyticOn 𝕜 (fderiv 𝕜 f) s

Tactic:
exact (h.fderivWithin hs.uniqueDiffOn).congr (fun x hx ↦ (fderivWithin_of_isOpen hs hx).symm)

Result:
no goals
-- Mathlib/Algebra/Group/Subsemigroup/Membership.lean
theorem coe_sSup_of_directed_on {S : Set (Subsemigroup M)} (hS : DirectedOn (· ≤ ·) S) :
    (↑(sSup S) : Set M) = ⋃ s ∈ S, ↑s :=
  Set.ext fun x => by simp [mem_sSup_of_directed_on hS]

Proof state:
M : Type u_2
inst✝ : Mul M
S : Set (Subsemigroup M)
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ ↑(sSup S) ↔ x ∈ ⋃ s ∈ S, ↑s

Tactic:
simp [mem_sSup_of_directed_on hS]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem head_dropWhile_not (p : α → Bool) (l : List α) (w) :
    p ((l.dropWhile p).head w) = false

Proof state:
α : Type u_1
p : α → Bool
l : List α
w : dropWhile p l ≠ []
⊢ p ((dropWhile p l).head w) = false

Tactic:
simpa [head?_eq_head, w] using head?_dropWhile_not p l

Result:
no goals