harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem convergenceR_cond (h : Integrable I l f vol) (ε : ℝ) (c : ℝ≥0) :
    l.RCond (h.convergenceR ε c)

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
ε : ℝ
c : ℝ≥0
⊢ l.RCond ((if hε : 0 < ε then ⋯.choose else fun x x => ⟨1, convergenceR.proof_3⟩) c)

Tactic:
split_ifs with h₀

Result:
case pos
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
ε : ℝ
c : ℝ≥0
h₀ : 0 < ε
⊢ l.RCond (⋯.choose c)

case neg
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
ε : ℝ
c : ℝ≥0
h₀ : ¬0 < ε
⊢ l.RCond ((fun x x => ⟨1, convergenceR.proof_3⟩) c)

Proof state:
case pos
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
ε : ℝ
c : ℝ≥0
h₀ : 0 < ε
⊢ l.RCond (⋯.choose c)

case neg
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
ε : ℝ
c : ℝ≥0
h₀ : ¬0 < ε
⊢ l.RCond ((fun x x => ⟨1, convergenceR.proof_3⟩) c)

Tactic:
exacts [(hasIntegral_iff.1 h.hasIntegral ε h₀).choose_spec.1 _, fun _ x => rfl]

Result:
no goals

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
ε : ℝ
c : ℝ≥0
⊢ l.RCond (h.convergenceR ε c)

Tactic:
rw [convergenceR]

Result:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
h : Integrable I l f vol
ε : ℝ
c : ℝ≥0
⊢ l.RCond ((if hε : 0 < ε then ⋯.choose else fun x x => ⟨1, convergenceR.proof_3⟩) c)
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
lemma sqrt_nnrpow_two (a : A) (ha : 0 ≤ a

Proof state:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ a ^ 1 = a

Tactic:
rw [nnrpow_one _]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ sqrt (a ^ 2) = a

Tactic:
simp only [sqrt_nnrpow, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, div_self]

Result:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
inst✝¹ : IsTopologicalRing A
inst✝ : T2Space A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ a ^ 1 = a
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem eq_of_comp_left_eq {f g : X ⟶ Y} (w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h) :
    f = g

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f g : X ⟶ Y
w : ∀ {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h
⊢ f = g

Tactic:
convert w (𝟙 Y) <;> simp

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_binop_subset (op : M → N → P) (op1 : op 1 1 = 1) (f : α → M) (g : α → N) :
    (mulSupport fun x => op (f x) (g x)) ⊆ mulSupport f ∪ mulSupport g := fun x hx =>
  not_or_of_imp fun hf hg => hx <| by simp only [hf, hg, op1]

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
P : Type u_8
inst✝² : One M
inst✝¹ : One N
inst✝ : One P
op : M → N → P
op1 : op 1 1 = 1
f : α → M
g : α → N
x : α
hx : x ∈ mulSupport fun x => op (f x) (g x)
hf : f x = 1
hg : g x = 1
⊢ (fun x => op (f x) (g x)) x = 1

Tactic:
simp only [hf, hg, op1]

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
lemma ωScottContinuous.iSup {f : ι → α → β} (hf : ∀ i, ωScottContinuous (f i)) :
    ωScottContinuous (⨆ i, f i)

Proof state:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), ωScottContinuous (f i)
c : Chain α
a : β
⊢ (⨆ i, f i) (ωSup c) ≤ a ↔ ωSup (c.map { toFun := ⨆ i, f i, monotone' := ⋯ }) ≤ a

Tactic:
simp +contextual [ωSup_le_iff, (hf _).map_ωSup, @forall_swap ι]

Result:
no goals

Proof state:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), ωScottContinuous (f i)
⊢ ωScottContinuous (⨆ i, f i)

Tactic:
refine ωScottContinuous.of_monotone_map_ωSup
  ⟨Monotone.iSup fun i ↦ (hf i).monotone, fun c ↦ eq_of_forall_ge_iff fun a ↦ ?_⟩

Result:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), ωScottContinuous (f i)
c : Chain α
a : β
⊢ (⨆ i, f i) (ωSup c) ≤ a ↔ ωSup (c.map { toFun := ⨆ i, f i, monotone' := ⋯ }) ≤ a
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem [EquivBEq α] [LawfulHashable α]
    (h : m.WF) {l : List α} {k k' : α} (k_beq : k == k') :
    ¬ k ∈ m → l.Pairwise (fun a b => (a == b) = false) → k ∈ l →
      getKey? (insertManyIfNewUnit m l) k' = some k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k k' : α
k_beq : (k == k') = true
⊢ m.contains k = false →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).getKey? k' = some k

Tactic:
simp_to_raw using Raw₀.Const.getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_mem

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k k' : α
k_beq : (k == k') = true
⊢ ¬k ∈ m → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).getKey? k' = some k

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List α
k k' : α
k_beq : (k == k') = true
⊢ m.contains k = false →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (insertManyIfNewUnit m l).getKey? k' = some k
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCastD_eraseKey_self [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k : α}
    {fallback : β k} (hl : DistinctKeys l) :
    getValueCastD k (eraseKey k l) fallback = fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k : α
fallback : β k
hl : DistinctKeys l
⊢ getValueCastD k (eraseKey k l) fallback = fallback

Tactic:
simp [getValueCastD_eq_getValueCast?, getValueCast?_eraseKey_self hl]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem Basis.equivFun_self [Finite ι] [DecidableEq ι] (b : Basis ι R M) (i j : ι) :
    b.equivFun (b i) j = if i = j then 1 else 0

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
b : Basis ι R M
i j : ι
⊢ b.equivFun (b i) j = if i = j then 1 else 0

Tactic:
rw [b.equivFun_apply, b.repr_self_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Adjunction.lean
lemma η_app (X₂ : C₂) :
    (η adj L₁ L₂ W₂ G' F').app (L₂.obj X₂) =
      G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
        (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂) ≫
        L₂.map (adj.counit.app X₂)

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁶ : Category.{u_8, u_1} C₁
inst✝⁵ : Category.{u_7, u_2} C₂
inst✝⁴ : Category.{u_6, u_3} D₁
inst✝³ : Category.{u_5, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
⊢ (η adj L₁ L₂ W₂ G' F').app (L₂.obj X₂) =
    G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
      (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)

Tactic:
letI : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') :=
  Lifting.mk (CatCommSq.hComp F G L₂ L₁ L₂ F' G').iso'.symm

Result:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁶ : Category.{u_8, u_1} C₁
inst✝⁵ : Category.{u_7, u_2} C₂
inst✝⁴ : Category.{u_6, u_3} D₁
inst✝³ : Category.{u_5, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
this : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') := { iso' := CatCommSq.iso'.symm }
⊢ (η adj L₁ L₂ W₂ G' F').app (L₂.obj X₂) =
    G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
      (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)

Proof state:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁶ : Category.{u_8, u_1} C₁
inst✝⁵ : Category.{u_7, u_2} C₂
inst✝⁴ : Category.{u_6, u_3} D₁
inst✝³ : Category.{u_5, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
this : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') := { iso' := CatCommSq.iso'.symm }
⊢ (η adj L₁ L₂ W₂ G' F').app (L₂.obj X₂) =
    G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
      (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)

Tactic:
simp only [η, liftNatTrans_app, Lifting.iso, Iso.symm, CatCommSq.hComp_iso'_inv_app,
  whiskerRight_app, Lifting.id_iso', Functor.rightUnitor_inv_app, comp_id, assoc]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_nonneg' (a : E) : 0 ≤ ‖a‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ 0 ≤ dist a 1

Tactic:
exact dist_nonneg

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ 0 ≤ ‖a‖

Tactic:
rw [← dist_one_right]

Result:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
⊢ 0 ≤ dist a 1
-- Mathlib/Data/Matrix/Rank.lean
theorem rank_diagonal [Fintype m] [DecidableEq m] [DecidableEq R] (w : m → R) :
    (diagonal w).rank = Fintype.card {i // (w i) ≠ 0}

Proof state:
m : Type u_2
R : Type u_5
inst✝³ : Field R
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq R
w : m → R
⊢ (diagonal w).rank = Fintype.card { i // w i ≠ 0 }

Tactic:
rw [Matrix.rank, ← Matrix.toLin'_apply', Module.finrank, ← LinearMap.rank,
  LinearMap.rank_diagonal, Cardinal.toNat_natCast]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem mem_ball_self (h : 0 < ε) : x ∈ ball x ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 < ε
⊢ x ∈ ball x ε

Tactic:
rwa [mem_ball, dist_self]

Result:
no goals
-- Mathlib/Order/Filter/Tendsto.lean
theorem not_tendsto_iff_exists_frequently_nmem {f : α → β} {l₁ : Filter α} {l₂ : Filter β} :
    ¬Tendsto f l₁ l₂ ↔ ∃ s ∈ l₂, ∃ᶠ x in l₁, f x ∉ s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l₁ : Filter α
l₂ : Filter β
⊢ ¬Tendsto f l₁ l₂ ↔ ∃ s ∈ l₂, ∃ᶠ (x : α) in l₁, f x ∉ s

Tactic:
simp only [tendsto_iff_forall_eventually_mem, not_forall, exists_prop, not_eventually]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem cond_true_same  : ∀(c b : Bool), cond c c b = (c || b)

Proof state:
⊢ ∀ (c b : Bool), (bif c then c else b) = (c || b)

Tactic:
decide

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem lf_of_le_of_lf {x y z : PGame} (h₁ : x ≤ y) (h₂ : y ⧏ z) : x ⧏ z

Proof state:
x y z : PGame
h₁ : x ≤ y
h₂ : y ⧏ z
⊢ x ⧏ z

Tactic:
rw [← PGame.not_le] at h₂ ⊢

Result:
x y z : PGame
h₁ : x ≤ y
h₂ : ¬z ≤ y
⊢ ¬z ≤ x

Proof state:
x y z : PGame
h₁ : x ≤ y
h₂ : ¬z ≤ y
⊢ ¬z ≤ x

Tactic:
exact fun h₃ => h₂ (h₃.trans h₁)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma tilted_apply' (μ : Measure α) (f : α → ℝ) {s : Set α} (hs : MeasurableSet s) :
    μ.tilted f s = ∫⁻ a in s, ENNReal.ofReal (exp (f a) / ∫ x, exp (f x) ∂μ) ∂μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
s : Set α
hs : MeasurableSet s
⊢ (μ.tilted f) s = ∫⁻ (a : α) in s, ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) ∂μ

Tactic:
rw [Measure.tilted, withDensity_apply _ hs]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem toSignedMeasure_zero : (0 : Measure α).toSignedMeasure = 0

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
i : Set α
a✝ : MeasurableSet i
⊢ ↑(toSignedMeasure 0) i = ↑0 i

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
⊢ toSignedMeasure 0 = 0

Tactic:
ext i

Result:
case h
α : Type u_1
m : MeasurableSpace α
i : Set α
a✝ : MeasurableSet i
⊢ ↑(toSignedMeasure 0) i = ↑0 i
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_eq_one_iff_of_norm_one {x y : E} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) :
    ⟪x, y⟫ = 1 ↔ x = y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ⟪x, y⟫_𝕜 = 1 ↔ x = y

Tactic:
convert inner_eq_norm_mul_iff (𝕜 := 𝕜) (E := E) using 2 <;> simp [hx, hy]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Verschiebung.lean
theorem ghostComponent_zero_verschiebungFun [hp : Fact p.Prime] (x : 𝕎 R) :
    ghostComponent 0 (verschiebungFun x) = 0

Proof state:
p : ℕ
R : Type u_1
inst✝ : CommRing R
hp : Fact (Nat.Prime p)
x : 𝕎 R
⊢ (ghostComponent 0) x.verschiebungFun = 0

Tactic:
rw [ghostComponent_apply, aeval_wittPolynomial, Finset.range_one, Finset.sum_singleton,
  verschiebungFun_coeff_zero, pow_zero, pow_zero, pow_one, one_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem leftAdjointMate_id {X : C} [HasLeftDual X] : (ᘁ(𝟙 X)) = 𝟙 (ᘁX)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X : C
inst✝ : HasLeftDual X
⊢ (ᘁ𝟙 X) = 𝟙 ᘁX

Tactic:
simp [leftAdjointMate]

Result:
no goals
-- Mathlib/Tactic/Abel.lean
lemma subst_into_smul_upcast {α} [AddCommGroup α]
    (l r tl zl tr t) (prl₁ : l = tl) (prl₂ : ↑tl = zl) (prr : r = tr)
    (prt : @smulg α _ zl tr = t) : smul l r = t

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
l : ℕ
r : α
tl : ℕ
zl : ℤ
tr t : α
prl₁ : l = tl
prl₂ : ↑tl = zl
prr : r = tr
prt : smulg zl tr = t
⊢ smul l r = t

Tactic:
simp [← prt, prl₁, ← prl₂, prr, smul, smulg, natCast_zsmul]

Result:
no goals
-- Mathlib/Data/NNReal/Basic.lean
theorem mul_iSup (f : ι → ℝ≥0) (a : ℝ≥0) : (a * ⨆ i, f i) = ⨆ i, a * f i

Proof state:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ ↑a * ⨆ i, ↑(f i) = ⨆ i, ↑(a * f i)

Tactic:
exact Real.mul_iSup_of_nonneg (NNReal.coe_nonneg _) _

Result:
no goals

Proof state:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Tactic:
rw [← coe_inj, NNReal.coe_mul, NNReal.coe_iSup, NNReal.coe_iSup]

Result:
ι : Sort u_2
f : ι → ℝ≥0
a : ℝ≥0
⊢ ↑a * ⨆ i, ↑(f i) = ⨆ i, ↑(a * f i)
-- Mathlib/Logic/Function/ULift.lean
theorem ULift.down_inj {α : Sort _} {a b : ULift α} : a.down = b.down ↔ a = b :=
  ⟨fun h ↦ ULift.down_injective h, fun h ↦ by rw [h]⟩

Proof state:
α : Type u_1
a b : ULift α
h : a = b
⊢ a.down = b.down

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
/-- For `k ≠ 0` and a constant `r` the function `r / n ^ k` tends to zero. -/
lemma tendsto_const_div_pow (r : ℝ) (k : ℕ) (hk : k ≠ 0) :
    Tendsto (fun n : ℕ => r / n ^ k) atTop (𝓝 0)

Proof state:
r : ℝ
k : ℕ
hk : k ≠ 0
⊢ Tendsto (fun n => r / ↑n ^ k) atTop (𝓝 0)

Tactic:
simpa using Filter.Tendsto.const_div_atTop (tendsto_natCast_atTop_atTop (R := ℝ).comp
  (tendsto_pow_atTop hk) ) r

Result:
no goals
-- Mathlib/Algebra/Pointwise/Stabilizer.lean
@[to_additive]
lemma mem_stabilizer_set_iff_subset_smul_set {s : Set α} (hs : s.Finite) :
    a ∈ stabilizer G s ↔ s ⊆ a • s

Proof state:
case intro
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Finset α
⊢ a ∈ stabilizer G ↑s ↔ ↑s ⊆ a • ↑s

Tactic:
rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_subset_smul_finset, ← Finset.coe_smul_finset,
  Finset.coe_subset]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Set α
hs : s.Finite
⊢ a ∈ stabilizer G s ↔ s ⊆ a • s

Tactic:
lift s to Finset α using hs

Result:
case intro
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Finset α
⊢ a ∈ stabilizer G ↑s ↔ ↑s ⊆ a • ↑s

Proof state:
case intro
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
a : G
s : Finset α
⊢ a ∈ stabilizer G ↑s ↔ ↑s ⊆ a • ↑s

Tactic:
classical
rw [stabilizer_coe_finset, mem_stabilizer_finset_iff_subset_smul_finset, ← Finset.coe_smul_finset,
  Finset.coe_subset]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldl_congr {as bs : Vector α n} (h₀ : as = bs) {f g : β → α → β} (h₁ : f = g)
     {a b : β} (h₂ : a = b) :
    as.foldl f a = bs.foldl g b

Proof state:
α : Type u_1
n : Nat
β : Type u_2
as bs : Vector α n
h₀ : as = bs
f g : β → α → β
h₁ : f = g
a b : β
h₂ : a = b
⊢ foldl f a as = foldl g b bs

Tactic:
congr

Result:
no goals
-- Mathlib/Tactic/NormNum/Basic.lean
theorem isRat_neg {α} [Ring α] : ∀ {f : α → α} {a : α} {n n' : ℤ} {d : ℕ},
    f = Neg.neg → IsRat a n d → Int.neg n = n' → IsRat (-a) n' d
  | _, _, _, _, _, rfl, ⟨h, rfl⟩, rfl => ⟨h, by rw [← neg_mul, ← Int.cast_neg]; rfl⟩

Proof state:
α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
h : Invertible ↑denom✝
⊢ -(↑num✝ * ⅟↑denom✝) = ↑num✝.neg * ⅟↑denom✝

Tactic:
rw [← neg_mul, ← Int.cast_neg]

Result:
α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
h : Invertible ↑denom✝
⊢ ↑(-num✝) * ⅟↑denom✝ = ↑num✝.neg * ⅟↑denom✝

Proof state:
α : Type u_1
inst✝ : Ring α
num✝ : ℤ
denom✝ : ℕ
h : Invertible ↑denom✝
⊢ ↑(-num✝) * ⅟↑denom✝ = ↑num✝.neg * ⅟↑denom✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc (attr := simp)]
lemma pOpcycles_comp_opcyclesIso_hom : S.pOpcycles ≫ h.opcyclesIso.hom = h.p

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
inst✝ : S.HasRightHomology
⊢ S.pOpcycles ≫ h.opcyclesIso.hom = h.p

Tactic:
simp only [← h.p_comp_opcyclesIso_inv, assoc, Iso.inv_hom_id, comp_id]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
@[simp] lemma one_lt_cast : 1 < (p : K) ↔ 1 < p

Proof state:
K : Type u_5
inst✝ : LinearOrderedSemifield K
p : ℚ≥0
⊢ 1 < ↑p ↔ 1 < p

Tactic:
norm_cast

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem sum_measure_le_measure_univ {s : Finset ι} {t : ι → Set α}
    (h : ∀ i ∈ s, NullMeasurableSet (t i) μ) (H : Set.Pairwise s (AEDisjoint μ on t)) :
    (∑ i ∈ s, μ (t i)) ≤ μ (univ : Set α)

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : (↑s).Pairwise (AEDisjoint μ on t)
⊢ ∑ i ∈ s, μ (t i) ≤ μ univ

Tactic:
rw [← measure_biUnion_finset₀ H h]

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : (↑s).Pairwise (AEDisjoint μ on t)
⊢ μ (⋃ b ∈ s, t b) ≤ μ univ

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, NullMeasurableSet (t i) μ
H : (↑s).Pairwise (AEDisjoint μ on t)
⊢ μ (⋃ b ∈ s, t b) ≤ μ univ

Tactic:
exact measure_mono (subset_univ _)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
lemma norm_integral_le_norm [IsProbabilityMeasure μ] (f : X →ᵇ E) :
    ‖∫ x, f x ∂μ‖ ≤ ‖f‖

Proof state:
X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsProbabilityMeasure μ
f : X →ᵇ E
⊢ ‖∫ (x : X), f x ∂μ‖ ≤ ‖f‖

Tactic:
convert f.norm_integral_le_mul_norm μ

Result:
case h.e'_4
X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsProbabilityMeasure μ
f : X →ᵇ E
⊢ ‖f‖ = (μ Set.univ).toReal * ‖f‖

Proof state:
case h.e'_4
X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsProbabilityMeasure μ
f : X →ᵇ E
⊢ ‖f‖ = (μ Set.univ).toReal * ‖f‖

Tactic:
simp only [measure_univ, ENNReal.one_toReal, one_mul]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem modEq_iff_toIcoMod_eq_left : a ≡ b [PMOD p] ↔ toIcoMod hp a b = a :=
  modEq_iff_eq_add_zsmul.trans
    ⟨by
      rintro ⟨n, rfl⟩
      rw [toIcoMod_add_zsmul, toIcoMod_apply_left], fun h => ⟨toIcoDiv hp a b, eq_add_of_sub_eq h⟩⟩

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ (∃ z, b = a + z • p) → toIcoMod hp a b = a

Tactic:
rintro ⟨n, rfl⟩

Result:
case intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
n : ℤ
⊢ toIcoMod hp a (a + n • p) = a

Proof state:
case intro
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
n : ℤ
⊢ toIcoMod hp a (a + n • p) = a

Tactic:
rw [toIcoMod_add_zsmul, toIcoMod_apply_left]

Result:
no goals
-- Mathlib/Logic/IsEmpty.lean
theorem isEmpty_prod {α β : Type*} : IsEmpty (α × β) ↔ IsEmpty α ∨ IsEmpty β

Proof state:
α : Type u_4
β : Type u_5
⊢ IsEmpty (α × β) ↔ IsEmpty α ∨ IsEmpty β

Tactic:
simp only [← not_nonempty_iff, nonempty_prod, not_and_or]

Result:
no goals