harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem lowerCentralSeries_eq_bot_iff_lcs_eq_bot:
    lowerCentralSeries R L N k = ⊥ ↔ lcs k N = ⊥

Proof state:
case refine_2
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
h : lcs k N = ⊥
⊢ lowerCentralSeries R L (↥N) k = ⊥

Tactic:
rw [N.lowerCentralSeries_eq_lcs_comap, comap_incl_eq_bot]

Result:
case refine_2
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
h : lcs k N = ⊥
⊢ N ⊓ lcs k N = ⊥

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
⊢ lowerCentralSeries R L (↥N) k = ⊥ ↔ lcs k N = ⊥

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
h : lowerCentralSeries R L (↥N) k = ⊥
⊢ lcs k N = ⊥

case refine_2
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
h : lcs k N = ⊥
⊢ lowerCentralSeries R L (↥N) k = ⊥

Proof state:
case refine_2
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
h : lcs k N = ⊥
⊢ N ⊓ lcs k N = ⊥

Tactic:
simp [h]

Result:
no goals

Proof state:
case refine_1
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
h : lowerCentralSeries R L (↥N) k = ⊥
⊢ lowerCentralSeries R L (↥N) k ≤ N.incl.ker

Tactic:
simpa

Result:
no goals

Proof state:
case refine_1
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
h : lowerCentralSeries R L (↥N) k = ⊥
⊢ lcs k N = ⊥

Tactic:
rw [← N.lowerCentralSeries_map_eq_lcs, ← LieModuleHom.le_ker_iff_map]

Result:
case refine_1
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
k : ℕ
N : LieSubmodule R L M
inst✝ : LieModule R L M
h : lowerCentralSeries R L (↥N) k = ⊥
⊢ lowerCentralSeries R L (↥N) k ≤ N.incl.ker
-- Mathlib/Algebra/Homology/HomotopyCategory.lean
lemma isZero_quotient_obj_iff (C : HomologicalComplex V c) :
    IsZero ((quotient _ _).obj C) ↔ Nonempty (Homotopy (𝟙 C) 0)

Proof state:
case mp
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
h : 𝟙 ((quotient V c).obj C) = 0
⊢ Nonempty (Homotopy (𝟙 C) 0)

Tactic:
exact ⟨(homotopyOfEq _ _ (by simp [h]))⟩

Result:
no goals

Proof state:
case mpr
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
⊢ Nonempty (Homotopy (𝟙 C) 0) → 𝟙 ((quotient V c).obj C) = 0

Tactic:
rintro ⟨h⟩

Result:
case mpr.intro
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
h : Homotopy (𝟙 C) 0
⊢ 𝟙 ((quotient V c).obj C) = 0

Proof state:
case mp
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
⊢ 𝟙 ((quotient V c).obj C) = 0 → Nonempty (Homotopy (𝟙 C) 0)

Tactic:
intro h

Result:
case mp
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
h : 𝟙 ((quotient V c).obj C) = 0
⊢ Nonempty (Homotopy (𝟙 C) 0)

Proof state:
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
h : 𝟙 ((quotient V c).obj C) = 0
⊢ (quotient V c).map (𝟙 C) = (quotient V c).map 0

Tactic:
simp [h]

Result:
no goals

Proof state:
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
⊢ IsZero ((quotient V c).obj C) ↔ Nonempty (Homotopy (𝟙 C) 0)

Tactic:
rw [IsZero.iff_id_eq_zero]

Result:
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
⊢ 𝟙 ((quotient V c).obj C) = 0 ↔ Nonempty (Homotopy (𝟙 C) 0)

Proof state:
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
⊢ 𝟙 ((quotient V c).obj C) = 0 ↔ Nonempty (Homotopy (𝟙 C) 0)

Tactic:
constructor

Result:
case mp
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
⊢ 𝟙 ((quotient V c).obj C) = 0 → Nonempty (Homotopy (𝟙 C) 0)

case mpr
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
⊢ Nonempty (Homotopy (𝟙 C) 0) → 𝟙 ((quotient V c).obj C) = 0

Proof state:
case mpr.intro
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
h : Homotopy (𝟙 C) 0
⊢ 𝟙 ((quotient V c).obj C) = 0

Tactic:
simpa using (eq_of_homotopy _ _ h)

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Pullback.lean
lemma commShiftPullback_iso_eq (a : A) (b : B) (h : b = φ a) :
    (PullbackShift.functor φ F).commShiftIso a (C := PullbackShift C φ) (D := PullbackShift D φ) =
      isoWhiskerRight (pullbackShiftIso C φ a b h) F ≪≫ (F.commShiftIso b) ≪≫
        isoWhiskerLeft F (pullbackShiftIso D φ a b h).symm

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_6, u_1} C
A : Type u_2
B : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
φ : A →+ B
inst✝³ : HasShift C B
D : Type u_4
inst✝² : Category.{u_5, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
a : A
b : B
h : b = φ a
⊢ (PullbackShift.functor φ F).commShiftIso a =
    isoWhiskerRight (pullbackShiftIso C φ a b h) F ≪≫
      F.commShiftIso b ≪≫ isoWhiskerLeft F (pullbackShiftIso D φ a b h).symm

Tactic:
obtain rfl : b = φ a := h

Result:
C : Type u_1
inst✝⁶ : Category.{u_6, u_1} C
A : Type u_2
B : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
φ : A →+ B
inst✝³ : HasShift C B
D : Type u_4
inst✝² : Category.{u_5, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
a : A
⊢ (PullbackShift.functor φ F).commShiftIso a =
    isoWhiskerRight (pullbackShiftIso C φ a (φ a) ⋯) F ≪≫
      F.commShiftIso (φ a) ≪≫ isoWhiskerLeft F (pullbackShiftIso D φ a (φ a) ⋯).symm

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_6, u_1} C
A : Type u_2
B : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : AddMonoid B
φ : A →+ B
inst✝³ : HasShift C B
D : Type u_4
inst✝² : Category.{u_5, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
a : A
⊢ (PullbackShift.functor φ F).commShiftIso a =
    isoWhiskerRight (pullbackShiftIso C φ a (φ a) ⋯) F ≪≫
      F.commShiftIso (φ a) ≪≫ isoWhiskerLeft F (pullbackShiftIso D φ a (φ a) ⋯).symm

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem condExpL1_smul (c : 𝕜) (f : α → F') : condExpL1 hm μ (c • f) = c • condExpL1 hm μ f

Proof state:
α : Type u_1
F' : Type u_3
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
c : 𝕜
f : α → F'
⊢ ∀ (c : 𝕜) (s : Set α) (x : F'), (condExpInd F' hm μ s) (c • x) = c • (condExpInd F' hm μ s) x

Tactic:
exact fun c _ x => condExpInd_smul' c x

Result:
no goals

Proof state:
α : Type u_1
F' : Type u_3
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
c : 𝕜
f : α → F'
⊢ condExpL1 hm μ (c • f) = c • condExpL1 hm μ f

Tactic:
refine setToFun_smul _ ?_ c f

Result:
α : Type u_1
F' : Type u_3
𝕜 : Type u_6
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup F'
inst✝³ : NormedSpace 𝕜 F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
c : 𝕜
f : α → F'
⊢ ∀ (c : 𝕜) (s : Set α) (x : F'), (condExpInd F' hm μ s) (c • x) = c • (condExpInd F' hm μ s) x
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_mono' {m : MeasurableSpace α} ⦃μ ν : Measure α⦄ (hμν : μ ≤ ν) ⦃f g : α → ℝ≥0∞⦄
    (hfg : f ≤ g) : ∫⁻ a, f a ∂μ ≤ ∫⁻ a, g a ∂ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
f g : α → ℝ≥0∞
hfg : f ≤ g
⊢ ∫⁻ (a : α), f a ∂μ ≤ ∫⁻ (a : α), g a ∂ν

Tactic:
rw [lintegral, lintegral]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
f g : α → ℝ≥0∞
hfg : f ≤ g
⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun a => f a), g.lintegral μ ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => g a), g_1.lintegral ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hμν : μ ≤ ν
f g : α → ℝ≥0∞
hfg : f ≤ g
⊢ ⨆ g, ⨆ (_ : ⇑g ≤ fun a => f a), g.lintegral μ ≤ ⨆ g_1, ⨆ (_ : ⇑g_1 ≤ fun a => g a), g_1.lintegral ν

Tactic:
exact iSup_mono fun φ => iSup_mono' fun hφ => ⟨le_trans hφ hfg, lintegral_mono (le_refl φ) hμν⟩

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WeakSpace.lean
theorem LinearEquiv.image_closure_of_convex' {s : Set E} (hs : Convex ℝ s) (e : E ≃ₗ[𝕜] F)
    (e_dual : (F →L[𝕜] 𝕜) ≃ (E →L[𝕜] 𝕜))
    (he : ∀ f : F →L[𝕜] 𝕜, (e_dual f : E →ₗ[𝕜] 𝕜) = e.dualMap f) :
    e '' (closure s) = closure (e '' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : (F →L[𝕜] 𝕜) ≃ (E →L[𝕜] 𝕜)
f : E →L[𝕜] 𝕜
he : ∀ (f : F →L[𝕜] 𝕜), ⇑(e_dual f) = ⇑(e.dualMap ↑f)
g : E →L[𝕜] 𝕜
⊢ ⇑g = ⇑(e_dual.symm g) ∘ ⇑e

Tactic:
have := he _ ▸ congr(⇑$(e_dual.apply_symm_apply g)).symm

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : (F →L[𝕜] 𝕜) ≃ (E →L[𝕜] 𝕜)
f : E →L[𝕜] 𝕜
he : ∀ (f : F →L[𝕜] 𝕜), ⇑(e_dual f) = ⇑(e.dualMap ↑f)
g : E →L[𝕜] 𝕜
this : ⇑g = ⇑(e.dualMap ↑(e_dual.symm g))
⊢ ⇑g = ⇑(e_dual.symm g) ∘ ⇑e

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁶ : RCLike 𝕜
inst✝¹⁵ : AddCommGroup E
inst✝¹⁴ : Module 𝕜 E
inst✝¹³ : AddCommGroup F
inst✝¹² : Module 𝕜 F
inst✝¹¹ : Module ℝ E
inst✝¹⁰ : IsScalarTower ℝ 𝕜 E
inst✝⁹ : Module ℝ F
inst✝⁸ : IsScalarTower ℝ 𝕜 F
inst✝⁷ : TopologicalSpace E
inst✝⁶ : IsTopologicalAddGroup E
inst✝⁵ : ContinuousSMul 𝕜 E
inst✝⁴ : LocallyConvexSpace ℝ E
inst✝³ : TopologicalSpace F
inst✝² : IsTopologicalAddGroup F
inst✝¹ : ContinuousSMul 𝕜 F
inst✝ : LocallyConvexSpace ℝ F
s : Set E
hs : Convex ℝ s
e : E ≃ₗ[𝕜] F
e_dual : (F →L[𝕜] 𝕜) ≃ (E →L[𝕜] 𝕜)
f : E →L[𝕜] 𝕜
he : ∀ (f : F →L[𝕜] 𝕜), ⇑(e_dual f) = ⇑(e.dualMap ↑f)
g : E →L[𝕜] 𝕜
this : ⇑g = ⇑(e.dualMap ↑(e_dual.symm g))
⊢ ⇑g = ⇑(e_dual.symm g) ∘ ⇑e

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_eq_getD [LawfulBEq α] (h : m.WF) {a : α} {fallback : β} :
    getD m a fallback = m.getD a fallback

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
h : m.WF
a : α
fallback : β
⊢ getD m a fallback = m.getD a fallback

Tactic:
simp_to_raw using Raw₀.Const.getD_eq_getD

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem row_mulVec [Fintype n] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : n → α) :
    Matrix.row ι (M *ᵥ v) = (M * Matrix.col ι v)ᵀ

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
i✝ : ι
j✝ : m
⊢ row ι (M *ᵥ v) i✝ j✝ = (M * col ι v)ᵀ i✝ j✝

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
⊢ row ι (M *ᵥ v) = (M * col ι v)ᵀ

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
i✝ : ι
j✝ : m
⊢ row ι (M *ᵥ v) i✝ j✝ = (M * col ι v)ᵀ i✝ j✝
-- Mathlib/Data/Seq/Computation.lean
theorem empty_orElse (c) : (empty α <|> c) = c

Proof state:
α : Type u
c s' s : Computation α
h : (empty α <|> s) = s'
⊢ BisimO (fun c₁ c₂ => (empty α <|> c₂) = c₁) s'.destruct s.destruct

Tactic:
rw [← h]

Result:
α : Type u
c s' s : Computation α
h : (empty α <|> s) = s'
⊢ BisimO (fun c₁ c₂ => (empty α <|> c₂) = c₁) (empty α <|> s).destruct s.destruct

Proof state:
α : Type u
c s' s : Computation α
h : (empty α <|> s) = s'
⊢ BisimO (fun c₁ c₂ => (empty α <|> c₂) = c₁) (empty α <|> s).destruct s.destruct

Tactic:
apply recOn s <;> intro s <;> rw [think_empty] <;> simp

Result:
case h2
α : Type u
c s' s✝ : Computation α
h : (empty α <|> s✝) = s'
s : Computation α
⊢ ((empty α).think <|> s) = (empty α <|> s)

Proof state:
α : Type u
c : Computation α
⊢ (empty α <|> c) = c

Tactic:
apply eq_of_bisim (fun c₁ c₂ => (empty α <|> c₂) = c₁) _ rfl

Result:
α : Type u
c : Computation α
⊢ IsBisimulation fun c₁ c₂ => (empty α <|> c₂) = c₁

Proof state:
α : Type u
c : Computation α
⊢ IsBisimulation fun c₁ c₂ => (empty α <|> c₂) = c₁

Tactic:
intro s' s h

Result:
α : Type u
c s' s : Computation α
h : (empty α <|> s) = s'
⊢ BisimO (fun c₁ c₂ => (empty α <|> c₂) = c₁) s'.destruct s.destruct

Proof state:
case h2
α : Type u
c s' s✝ : Computation α
h : (empty α <|> s✝) = s'
s : Computation α
⊢ ((empty α).think <|> s) = (empty α <|> s)

Tactic:
rw [← think_empty]

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/EulerMascheroni.lean
lemma eulerMascheroniSeq_lt_eulerMascheroniSeq' (m n : ℕ) :
    eulerMascheroniSeq m < eulerMascheroniSeq' n

Proof state:
m n : ℕ
this : ∀ (r : ℕ), eulerMascheroniSeq r < eulerMascheroniSeq' r
⊢ eulerMascheroniSeq m < eulerMascheroniSeq' n

Tactic:
apply (strictMono_eulerMascheroniSeq.monotone (le_max_left m n)).trans_lt

Result:
m n : ℕ
this : ∀ (r : ℕ), eulerMascheroniSeq r < eulerMascheroniSeq' r
⊢ eulerMascheroniSeq (m ⊔ n) < eulerMascheroniSeq' n

Proof state:
case inr
m n r : ℕ
hr : 0 < r
⊢ ↑(harmonic r) - log (↑r + 1) < ↑(harmonic r) - log ↑r

Tactic:
gcongr

Result:
case inr.h.h
m n r : ℕ
hr : 0 < r
⊢ ↑r < ↑r + 1

Proof state:
m n r : ℕ
⊢ eulerMascheroniSeq r < eulerMascheroniSeq' r

Tactic:
rcases eq_zero_or_pos r with rfl | hr

Result:
case inl
m n : ℕ
⊢ eulerMascheroniSeq 0 < eulerMascheroniSeq' 0

case inr
m n r : ℕ
hr : 0 < r
⊢ eulerMascheroniSeq r < eulerMascheroniSeq' r

Proof state:
case inr
m n r : ℕ
hr : 0 < r
⊢ eulerMascheroniSeq r < eulerMascheroniSeq' r

Tactic:
simp only [eulerMascheroniSeq, eulerMascheroniSeq', hr.ne', if_false]

Result:
case inr
m n r : ℕ
hr : 0 < r
⊢ ↑(harmonic r) - log (↑r + 1) < ↑(harmonic r) - log ↑r

Proof state:
case inl
m n : ℕ
⊢ eulerMascheroniSeq 0 < eulerMascheroniSeq' 0

Tactic:
simp [eulerMascheroniSeq, eulerMascheroniSeq']

Result:
no goals

Proof state:
m n : ℕ
this : ∀ (r : ℕ), eulerMascheroniSeq r < eulerMascheroniSeq' r
⊢ eulerMascheroniSeq (m ⊔ n) < eulerMascheroniSeq' n

Tactic:
exact (this _).trans_le (strictAnti_eulerMascheroniSeq'.antitone (le_max_right m n))

Result:
no goals

Proof state:
case inr.h.h
m n r : ℕ
hr : 0 < r
⊢ ↑r < ↑r + 1

Tactic:
linarith

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/End.lean
theorem η_app_obj (n : M) (X : C) [F.Monoidal] :
    (η F).app ((F.obj n).obj X) = (μ F n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (η F).app ((F.obj n).obj X) = (μ F n (𝟙_ M)).app X ≫ (δ F n (𝟙_ M) ≫ F.obj n ◁ η F ≫ (ρ_ (F.obj n)).hom).app X

Tactic:
dsimp

Result:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (η F).app ((F.obj n).obj X) =
    (μ F n (𝟙_ M)).app X ≫ (δ F n (𝟙_ M)).app X ≫ (η F).app ((F.obj n).obj X) ≫ 𝟙 ((F.obj n).obj X)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (η F).app ((F.obj n).obj X) = (μ F n (𝟙_ M)).app X ≫ (F.map (ρ_ n).hom).app X

Tactic:
rw [map_rightUnitor]

Result:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (η F).app ((F.obj n).obj X) = (μ F n (𝟙_ M)).app X ≫ (δ F n (𝟙_ M) ≫ F.obj n ◁ η F ≫ (ρ_ (F.obj n)).hom).app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (η F).app ((F.obj n).obj X) =
    (μ F n (𝟙_ M)).app X ≫ (δ F n (𝟙_ M)).app X ≫ (η F).app ((F.obj n).obj X) ≫ 𝟙 ((F.obj n).obj X)

Tactic:
simp only [Category.comp_id, μ_δ_app_assoc]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem coe_smul (r : F) : ((r • f : RatFunc F) : F⸨X⸩) = r • (f : F⸨X⸩)

Proof state:
F : Type u
inst✝ : Field F
f : RatFunc F
r : F
⊢ ↑(r • f) = r • ↑f

Tactic:
rw [RatFunc.smul_eq_C_mul, ← C_mul_eq_smul, coe_mul, coe_C]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_zipWithAll (f : Option α → Option β → γ) (as : Array α) (bs : Array β) :
    (zipWithAll f as bs).toList = List.zipWithAll f as.toList bs.toList

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : Option α → Option β → γ
toList✝¹ : List α
toList✝ : List β
⊢ (zipWithAll f { toList := toList✝¹ } { toList := toList✝ }).toList =
    List.zipWithAll f { toList := toList✝¹ }.toList { toList := toList✝ }.toList

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Option α → Option β → γ
as : Array α
bs : Array β
⊢ (zipWithAll f as bs).toList = List.zipWithAll f as.toList bs.toList

Tactic:
cases as

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : Option α → Option β → γ
bs : Array β
toList✝ : List α
⊢ (zipWithAll f { toList := toList✝ } bs).toList = List.zipWithAll f { toList := toList✝ }.toList bs.toList

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : Option α → Option β → γ
bs : Array β
toList✝ : List α
⊢ (zipWithAll f { toList := toList✝ } bs).toList = List.zipWithAll f { toList := toList✝ }.toList bs.toList

Tactic:
cases bs

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : Option α → Option β → γ
toList✝¹ : List α
toList✝ : List β
⊢ (zipWithAll f { toList := toList✝¹ } { toList := toList✝ }).toList =
    List.zipWithAll f { toList := toList✝¹ }.toList { toList := toList✝ }.toList
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_eq_lintegral_pos_part_sub_lintegral_neg_part {f : α → ℝ} (hf : Integrable f μ) :
    ∫ a, f a ∂μ =
      ENNReal.toReal (∫⁻ a, .ofReal (f a) ∂μ) - ENNReal.toReal (∫⁻ a, .ofReal (-f a) ∂μ)

Proof state:
case h.e_a.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart f₁) a✝ = -(↑↑f₁ a✝ ⊓ 0)
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(-f a✝).toNNReal = ↑‖-(f a✝ ⊓ 0)‖₊

Tactic:
simp only [Real.coe_toNNReal', coe_nnnorm, nnnorm_neg]

Result:
case h.e_a.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
eq₁ : (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal = ‖Lp.posPart f₁‖
a✝ : α
h₁ : ↑↑(Lp.negPart f₁) a✝ = -(↑↑f₁ a✝ ⊓ 0)
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ -f a✝ ⊔ 0 = ‖f a✝ ⊓ 0‖

Proof state:
case h.e_a.a
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
f₁ : ↥(Lp ℝ 1 μ) := Integrable.toL1 f hf
a✝ : α
h₁ : ↑↑(Lp.posPart f₁) a✝ = ↑↑f₁ a✝ ⊔ 0
h₂ : ↑↑(Integrable.toL1 f hf) a✝ = f a✝
⊢ ↑(f a✝).toNNReal = ↑⟨f a✝ ⊔ 0, ⋯⟩

Tactic:
rw [Real.coe_toNNReal', NNReal.coe_mk]

Result:
no goals
-- Mathlib/GroupTheory/Exponent.lean
theorem _root_.Submonoid.pow_exponent_eq_one {S : Submonoid G} {g : G} (g_in_s : g ∈ S) :
    g ^ (Monoid.exponent S) = 1

Proof state:
G : Type u
inst✝ : Monoid G
S : Submonoid G
g : G
g_in_s : g ∈ S
this : ⟨g, g_in_s⟩ ^ exponent ↥S = 1
⊢ g ^ exponent ↥S = 1

Tactic:
rwa [SubmonoidClass.mk_pow, ← OneMemClass.coe_eq_one] at this

Result:
no goals

Proof state:
G : Type u
inst✝ : Monoid G
S : Submonoid G
g : G
g_in_s : g ∈ S
⊢ g ^ exponent ↥S = 1

Tactic:
have := Monoid.pow_exponent_eq_one (⟨g, g_in_s⟩ : S)

Result:
G : Type u
inst✝ : Monoid G
S : Submonoid G
g : G
g_in_s : g ∈ S
this : ⟨g, g_in_s⟩ ^ exponent ↥S = 1
⊢ g ^ exponent ↥S = 1
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma mapEquiv_indep_iff {I : Set β} : (M.mapEquiv f).Indep I ↔ M.Indep (f.symm '' I)

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) ↔ M.Indep (⇑f.symm '' I)

Tactic:
exact ⟨by rintro ⟨I, hI, rfl⟩; simpa, fun h ↦ ⟨_, h, by simp⟩⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) → M.Indep (⇑f.symm '' I)

Tactic:
rintro ⟨I, hI, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set α
hI : M.Indep I
⊢ M.Indep (⇑f.symm '' (⇑f '' I))

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set β
⊢ (M.mapEquiv f).Indep I ↔ M.Indep (⇑f.symm '' I)

Tactic:
rw [mapEquiv_eq_map, map_indep_iff]

Result:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set β
⊢ (∃ I₀, M.Indep I₀ ∧ I = ⇑f '' I₀) ↔ M.Indep (⇑f.symm '' I)

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set β
h : M.Indep (⇑f.symm '' I)
⊢ I = ⇑f '' (⇑f.symm '' I)

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set α
hI : M.Indep I
⊢ M.Indep (⇑f.symm '' (⇑f '' I))

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_one : ⌊(1 : α)⌋₊ = 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
⊢ ⌊1⌋₊ = 1

Tactic:
rw [← Nat.cast_one, floor_natCast]

Result:
no goals