harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToSimpleFunc_smul {E} [NormedAddCommGroup E] [NormedField 𝕜] [NormedSpace 𝕜 E]
    [NormedSpace ℝ E] [NormedSpace 𝕜 F] (T : Set α → E →L[ℝ] F) (h_add : FinMeasAdditive μ T)
    (h_smul : ∀ c : 𝕜, ∀ s x, T s (c • x) = c • T s x) (c : 𝕜) {f : α →ₛ E} (hf : Integrable f μ) :
    setToSimpleFunc T (c • f) = c • setToSimpleFunc T f :=
  calc
    setToSimpleFunc T (c • f) = ∑ x ∈ f.range, T (f ⁻¹' {x}) (c • x)

Proof state:
α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 F
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ c • 0 = 0

Tactic:
rw [smul_zero]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 F
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α →ₛ E
hf : Integrable (⇑f) μ
b : E
x✝ : b ∈ f.range
⊢ (T (⇑f ⁻¹' {b})) (c • b) = c • (T (⇑f ⁻¹' {b})) b

Tactic:
rw [h_smul]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 F
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T (c • f) = ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (c • x)

Tactic:
rw [smul_eq_map c f, map_setToSimpleFunc T h_add hf]

Result:
α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 F
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ c • 0 = 0

Proof state:
α : Type u_1
F : Type u_3
𝕜 : Type u_6
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
E : Type u_7
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace 𝕜 F
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x
c : 𝕜
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range, c • (T (⇑f ⁻¹' {x})) x = c • setToSimpleFunc T f

Tactic:
simp only [setToSimpleFunc, smul_sum, smul_smul, mul_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem BinaryCofan.isPullback_initial_to_of_isVanKampen [HasInitial C] {c : BinaryCofan X Y}
    (h : IsVanKampenColimit c) : IsPullback (initial.to _) (initial.to _) c.inl c.inr

Proof state:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ mapPair (initial.to X) (𝟙 Y) ≫ c.ι =
    (BinaryCofan.mk (initial.to Y) (𝟙 Y)).ι ≫ (Functor.const (Discrete WalkingPair)).map c.inr

Tactic:
ext ⟨⟨⟩⟩ <;> dsimp

Result:
case refine_1.w.h.mk.left
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ initial.to X ≫ c.inl = initial.to Y ≫ c.inr

Proof state:
case refine_1.w.h.mk.left
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ initial.to X ≫ c.inl = initial.to Y ≫ c.inr

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsIso (𝟙 Y)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsPullback (initial.to ((pair X Y).obj { as := WalkingPair.left }))
    (initial.to ((pair X Y).obj { as := WalkingPair.right })) c.inl c.inr

Tactic:
refine ((h (BinaryCofan.mk (initial.to Y) (𝟙 Y)) (mapPair (initial.to X) (𝟙 Y)) c.inr ?_
    (mapPair_equifibered _)).mp ⟨?_⟩ ⟨WalkingPair.left⟩).flip

Result:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ mapPair (initial.to X) (𝟙 Y) ≫ c.ι =
    (BinaryCofan.mk (initial.to Y) (𝟙 Y)).ι ≫ (Functor.const (Discrete WalkingPair)).map c.inr

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsColimit (BinaryCofan.mk (initial.to Y) (𝟙 Y))

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsIso (BinaryCofan.mk (initial.to Y) (𝟙 Y)).inr

Tactic:
dsimp

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsIso (𝟙 Y)

Proof state:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasInitial C
c : BinaryCofan X Y
h : IsVanKampenColimit c
⊢ IsColimit (BinaryCofan.mk (initial.to Y) (𝟙 Y))

Tactic:
exact ((BinaryCofan.isColimit_iff_isIso_inr initialIsInitial _).mpr (by
  dsimp
  infer_instance)).some

Result:
no goals
-- Mathlib/RingTheory/PiTensorProduct.lean
protected lemma one_mul (x : ⨂[R] i, A i) : mul (tprod R 1) x = x

Proof state:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonAssocSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x : ⨂[R] (i : ι), A i
⊢ (mul ((tprod R) 1)) x = x

Tactic:
induction x using PiTensorProduct.induction_on with
| smul_tprod => simp
| add _ _ h1 h2 => simp [map_add, h1, h2]

Result:
no goals

Proof state:
case add
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonAssocSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x✝ y✝ : ⨂[R] (i : ι), A i
h1 : (mul ((tprod R) 1)) x✝ = x✝
h2 : (mul ((tprod R) 1)) y✝ = y✝
⊢ (mul ((tprod R) 1)) (x✝ + y✝) = x✝ + y✝

Tactic:
simp [map_add, h1, h2]

Result:
no goals

Proof state:
case smul_tprod
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonAssocSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
r✝ : R
f✝ : (i : ι) → A i
⊢ (mul ((tprod R) 1)) (r✝ • (tprod R) f✝) = r✝ • (tprod R) f✝

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Homotopy/HomotopyGroup.lean
theorem to_from (i : N) (p : Ω (Ω^ { j // j ≠ i } X x) const) : toLoop i (fromLoop i p) = p

Proof state:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p : Ω (↑(Ω^ { j // j ≠ i } X x)) const
⊢ toLoop i (fromLoop i p) = p

Tactic:
simp_rw [toLoop, fromLoop, ContinuousMap.comp_assoc,
  toContinuousMap_comp_symm, ContinuousMap.comp_id]

Result:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p : Ω (↑(Ω^ { j // j ≠ i } X x)) const
⊢ { toFun := fun t => ⟨({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp p.toContinuousMap).uncurry.curry t, ⋯⟩,
      continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } =
    p

Proof state:
case a.h.H
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p : Ω (↑(Ω^ { j // j ≠ i } X x)) const
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ ({ toFun := fun t => ⟨({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp p.toContinuousMap).uncurry.curry t, ⋯⟩,
          continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
        x✝)
      y✝ =
    (p x✝) y✝

Tactic:
rfl

Result:
no goals

Proof state:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p : Ω (↑(Ω^ { j // j ≠ i } X x)) const
⊢ { toFun := fun t => ⟨({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp p.toContinuousMap).uncurry.curry t, ⋯⟩,
      continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } =
    p

Tactic:
ext

Result:
case a.h.H
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p : Ω (↑(Ω^ { j // j ≠ i } X x)) const
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ ({ toFun := fun t => ⟨({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp p.toContinuousMap).uncurry.curry t, ⋯⟩,
          continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
        x✝)
      y✝ =
    (p x✝) y✝
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem exists_finset_of_mem_iSup {ι : Type*} {f : ι → IntermediateField F E} {x : E}
    (hx : x ∈ ⨆ i, f i) : ∃ s : Finset ι, x ∈ ⨆ i ∈ s, f i

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x : E
hx : x ∈ ⨆ i, f i
this : x ∈ ⨆ i, f i → ∃ s, x ∈ ⨆ i ∈ s, f i
⊢ ∃ s, x ∈ ⨆ i ∈ s, f i

Tactic:
exact this hx

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x : E
hx : x ∈ ⨆ i, f i
⊢ ∃ s, x ∈ ⨆ i ∈ s, f i

Tactic:
have := (adjoin_simple_isCompactElement x).exists_finset_of_le_iSup (IntermediateField F E) f

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x : E
hx : x ∈ ⨆ i, f i
this : F⟮x⟯ ≤ ⨆ i, f i → ∃ s, F⟮x⟯ ≤ ⨆ i ∈ s, f i
⊢ ∃ s, x ∈ ⨆ i ∈ s, f i

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x : E
hx : x ∈ ⨆ i, f i
this : F⟮x⟯ ≤ ⨆ i, f i → ∃ s, F⟮x⟯ ≤ ⨆ i ∈ s, f i
⊢ ∃ s, x ∈ ⨆ i ∈ s, f i

Tactic:
simp only [adjoin_simple_le_iff] at this

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
ι : Type u_3
f : ι → IntermediateField F E
x : E
hx : x ∈ ⨆ i, f i
this : x ∈ ⨆ i, f i → ∃ s, x ∈ ⨆ i ∈ s, f i
⊢ ∃ s, x ∈ ⨆ i ∈ s, f i
-- Mathlib/Topology/Sheaves/Sheafify.lean
theorem stalkToFiber_surjective (x : X) : Function.Surjective (F.stalkToFiber x)

Proof state:
case w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ ∀ (t : F.stalk x), ∃ U f, ∃ (_ : (Sheafify.isLocallyGerm F).pred f), f ⟨x, ⋯⟩ = t

Tactic:
intro t

Result:
case w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
t : F.stalk x
⊢ ∃ U f, ∃ (_ : (Sheafify.isLocallyGerm F).pred f), f ⟨x, ⋯⟩ = t

Proof state:
case h.w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : ToType (F.obj (op U))
⊢ (y : ↥{ obj := U, property := m }.obj) → F.stalk ↑y

Tactic:
exact fun y => F.germ _ _ y.2 s

Result:
no goals

Proof state:
X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ Function.Surjective (F.stalkToFiber x)

Tactic:
apply TopCat.stalkToFiber_surjective

Result:
case w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
⊢ ∀ (t : F.stalk x), ∃ U f, ∃ (_ : (Sheafify.isLocallyGerm F).pred f), f ⟨x, ⋯⟩ = t

Proof state:
case w.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : ToType (F.obj (op U))
⊢ ∃ U_1 f, ∃ (_ : (Sheafify.isLocallyGerm F).pred f), f ⟨x, ⋯⟩ = (ConcreteCategory.hom (F.germ U x m)) s

Tactic:
use ⟨U, m⟩

Result:
case h
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : ToType (F.obj (op U))
⊢ ∃ f, ∃ (_ : (Sheafify.isLocallyGerm F).pred f), f ⟨x, ⋯⟩ = (ConcreteCategory.hom (F.germ U x m)) s

Proof state:
case h.h
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : ToType (F.obj (op U))
⊢ ∃ (_ : (Sheafify.isLocallyGerm F).pred fun y => F.germ { obj := U, property := m }.obj ↑y ⋯ s),
    (fun y => F.germ { obj := U, property := m }.obj ↑y ⋯ s) ⟨x, ⋯⟩ = (ConcreteCategory.hom (F.germ U x m)) s

Tactic:
exact ⟨PrelocalPredicate.sheafifyOf ⟨s, fun _ => rfl⟩, rfl⟩

Result:
no goals

Proof state:
case w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
t : F.stalk x
⊢ ∃ U f, ∃ (_ : (Sheafify.isLocallyGerm F).pred f), f ⟨x, ⋯⟩ = t

Tactic:
obtain ⟨U, m, s, rfl⟩ := F.germ_exist _ t

Result:
case w.intro.intro.intro
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : ToType (F.obj (op U))
⊢ ∃ U_1 f, ∃ (_ : (Sheafify.isLocallyGerm F).pred f), f ⟨x, ⋯⟩ = (ConcreteCategory.hom (F.germ U x m)) s

Proof state:
case h
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : ToType (F.obj (op U))
⊢ ∃ f, ∃ (_ : (Sheafify.isLocallyGerm F).pred f), f ⟨x, ⋯⟩ = (ConcreteCategory.hom (F.germ U x m)) s

Tactic:
fconstructor

Result:
case h.w
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : ToType (F.obj (op U))
⊢ (y : ↥{ obj := U, property := m }.obj) → F.stalk ↑y

case h.h
X : TopCat
F : Presheaf (Type v) X
x : ↑X
U : Opens ↑X
m : x ∈ U
s : ToType (F.obj (op U))
⊢ ∃ (_ : (Sheafify.isLocallyGerm F).pred ?h.w), ?h.w ⟨x, ⋯⟩ = (ConcreteCategory.hom (F.germ U x m)) s
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem nullHomotopicMap_f_of_not_rel_left {k₁ k₀ : ι} (r₁₀ : c.Rel k₁ k₀)
    (hk₀ : ∀ l : ι, ¬c.Rel k₀ l) (hom : ∀ i j, C.X i ⟶ D.X j) :
    (nullHomotopicMap hom).f k₀ = hom k₀ k₁ ≫ D.d k₁ k₀

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (nullHomotopicMap hom).f k₀ = hom k₀ k₁ ≫ D.d k₁ k₀

Tactic:
dsimp only [nullHomotopicMap]

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (dNext k₀) hom + (prevD k₀) hom = hom k₀ k₁ ≫ D.d k₁ k₀

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (dNext k₀) hom + (prevD k₀) hom = hom k₀ k₁ ≫ D.d k₁ k₀

Tactic:
rw [prevD_eq hom r₁₀, dNext, AddMonoidHom.mk'_apply, C.shape, zero_comp, zero_add]

Result:
case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel k₀ (c.next k₀)

Proof state:
case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel k₀ (c.next k₀)

Tactic:
exact hk₀ _

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem rootMultiplicity_eq_multiplicity [DecidableEq R]
    (p : R[X]) (a : R) :
    rootMultiplicity a p =
      if p = 0 then 0 else multiplicity (X - C a) p

Proof state:
case isFalse
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h : ¬p = 0
⊢ Nat.find ⋯ = WithTop.untopD 1 (if h : FiniteMultiplicity (X - C a) p then ↑(Nat.find h) else ⊤)

Tactic:
simp only [finiteMultiplicity_X_sub_C a h, ↓reduceDIte]

Result:
case isFalse
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h : ¬p = 0
⊢ Nat.find ⋯ = WithTop.untopD 1 ↑(Nat.find ⋯)

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
⊢ (if h : p = 0 then 0 else Nat.find ⋯) =
    if p = 0 then 0 else WithTop.untopD 1 (if h : FiniteMultiplicity (X - C a) p then ↑(Nat.find h) else ⊤)

Tactic:
split

Result:
case isTrue
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h✝ : p = 0
⊢ 0 = 0

case isFalse
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h✝ : ¬p = 0
⊢ Nat.find ⋯ = WithTop.untopD 1 (if h : FiniteMultiplicity (X - C a) p then ↑(Nat.find h) else ⊤)

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
⊢ rootMultiplicity a p = if p = 0 then 0 else multiplicity (X - C a) p

Tactic:
simp only [rootMultiplicity, multiplicity, emultiplicity]

Result:
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
⊢ (if h : p = 0 then 0 else Nat.find ⋯) =
    if p = 0 then 0 else WithTop.untopD 1 (if h : FiniteMultiplicity (X - C a) p then ↑(Nat.find h) else ⊤)

Proof state:
case isFalse
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h : ¬p = 0
⊢ Nat.find ⋯ = WithTop.untopD 1 ↑(Nat.find ⋯)

Tactic:
rw [← ENat.some_eq_coe, WithTop.untopD_coe]

Result:
case isFalse
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h : ¬p = 0
⊢ Nat.find ⋯ = Nat.find ⋯

Proof state:
case isFalse
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h : ¬p = 0
⊢ Nat.find ⋯ = Nat.find ⋯

Tactic:
congr

Result:
no goals

Proof state:
case isFalse
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h✝ : ¬p = 0
⊢ Nat.find ⋯ = WithTop.untopD 1 (if h : FiniteMultiplicity (X - C a) p then ↑(Nat.find h) else ⊤)

Tactic:
rename_i h

Result:
case isFalse
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h : ¬p = 0
⊢ Nat.find ⋯ = WithTop.untopD 1 (if h : FiniteMultiplicity (X - C a) p then ↑(Nat.find h) else ⊤)

Proof state:
case isTrue
R : Type u
inst✝¹ : Ring R
inst✝ : DecidableEq R
p : R[X]
a : R
h✝ : p = 0
⊢ 0 = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Fin/Rev.lean
theorem rev_le_iff {i j : Fin n} : rev i ≤ j ↔ rev j ≤ i

Proof state:
n : ℕ
i j : Fin n
⊢ i.rev ≤ j ↔ j.rev ≤ i

Tactic:
rw [← rev_le_rev, rev_rev]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/ExtendToSucc.lean
lemma arrowMap_extendToSucc (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) :
    arrowMap (extendToSucc hj F τ) i₁ i₂ hi (hi₂.trans (Order.le_succ j)) =
      arrowMap F i₁ i₂ hi hi₂

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
J : Type u
inst✝¹ : LinearOrder J
inst✝ : SuccOrder J
j : J
hj : ¬IsMax j
F : ↑(Set.Iic j) ⥤ C
X : C
τ : F.obj ⟨j, ⋯⟩ ⟶ X
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ ≤ j
⊢ arrowMap (extendToSucc hj F τ) i₁ i₂ hi ⋯ = arrowMap F i₁ i₂ hi hi₂

Tactic:
simp [arrowMap, extendToSucc_map hj F τ i₁ i₂ hi hi₂,
  extendToSuccObjIso, extendToSucc.objIso]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem divp_eq_iff_mul_eq {x : α} {u : αˣ} {y : α} : x /ₚ u = y ↔ y * u = x :=
  u.mul_left_inj.symm.trans <| by rw [divp_mul_cancel]; exact ⟨Eq.symm, Eq.symm⟩

Proof state:
α : Type u
inst✝ : Monoid α
x : α
u : αˣ
y : α
⊢ x /ₚ u * ↑u = y * ↑u ↔ y * ↑u = x

Tactic:
rw [divp_mul_cancel]

Result:
α : Type u
inst✝ : Monoid α
x : α
u : αˣ
y : α
⊢ x = y * ↑u ↔ y * ↑u = x

Proof state:
α : Type u
inst✝ : Monoid α
x : α
u : αˣ
y : α
⊢ x = y * ↑u ↔ y * ↑u = x

Tactic:
exact ⟨Eq.symm, Eq.symm⟩

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/ArctanDeriv.lean
theorem hasStrictDerivAt_tan {x : ℝ} (h : cos x ≠ 0) : HasStrictDerivAt tan (1 / cos x ^ 2) x :=
  mod_cast (Complex.hasStrictDerivAt_tan (by exact mod_cast h)).real_of_complex

Proof state:
x : ℝ
h : cos x ≠ 0
⊢ Complex.cos ↑x ≠ 0

Tactic:
exact mod_cast h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Basic.lean
theorem dropLast_reverse (l : List α) : l.reverse.dropLast = l.tail.reverse

Proof state:
case h
α : Type u_1
l : List α
i : Nat
h₁ : i < l.reverse.dropLast.length
h₂ : i < l.tail.reverse.length
⊢ l[l.length - 1 - i] = l[l.length - 1 - 1 - i + 1]

Tactic:
congr

Result:
case h.e_i
α : Type u_1
l : List α
i : Nat
h₁ : i < l.reverse.dropLast.length
h₂ : i < l.tail.reverse.length
⊢ l.length - 1 - i = l.length - 1 - 1 - i + 1

Proof state:
case hl
α : Type u_1
l : List α
⊢ l.reverse.dropLast.length = l.tail.reverse.length

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
l : List α
i : Nat
h₁ : i < l.reverse.dropLast.length
h₂ : i < l.tail.reverse.length
⊢ l.reverse.dropLast[i] = l.tail.reverse[i]

Tactic:
simp only [getElem_dropLast, getElem_reverse, length_tail, getElem_tail]

Result:
case h
α : Type u_1
l : List α
i : Nat
h₁ : i < l.reverse.dropLast.length
h₂ : i < l.tail.reverse.length
⊢ l[l.length - 1 - i] = l[l.length - 1 - 1 - i + 1]

Proof state:
α : Type u_1
l : List α
⊢ l.reverse.dropLast = l.tail.reverse

Tactic:
apply ext_getElem

Result:
case hl
α : Type u_1
l : List α
⊢ l.reverse.dropLast.length = l.tail.reverse.length

case h
α : Type u_1
l : List α
⊢ ∀ (i : Nat) (h₁ : i < l.reverse.dropLast.length) (h₂ : i < l.tail.reverse.length),
    l.reverse.dropLast[i] = l.tail.reverse[i]

Proof state:
case h
α : Type u_1
l : List α
⊢ ∀ (i : Nat) (h₁ : i < l.reverse.dropLast.length) (h₂ : i < l.tail.reverse.length),
    l.reverse.dropLast[i] = l.tail.reverse[i]

Tactic:
intro i h₁ h₂

Result:
case h
α : Type u_1
l : List α
i : Nat
h₁ : i < l.reverse.dropLast.length
h₂ : i < l.tail.reverse.length
⊢ l.reverse.dropLast[i] = l.tail.reverse[i]

Proof state:
case h.e_i
α : Type u_1
l : List α
i : Nat
h₁ : i < l.reverse.dropLast.length
h₂ : i < l.tail.reverse.length
⊢ l.length - 1 - i = l.length - 1 - 1 - i + 1

Tactic:
simp only [length_dropLast, length_reverse, length_tail] at h₁ h₂

Result:
case h.e_i
α : Type u_1
l : List α
i : Nat
h₁ h₂ : i < l.length - 1
⊢ l.length - 1 - i = l.length - 1 - 1 - i + 1

Proof state:
case h.e_i
α : Type u_1
l : List α
i : Nat
h₁ h₂ : i < l.length - 1
⊢ l.length - 1 - i = l.length - 1 - 1 - i + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem hasSum_repr (b : HilbertBasis ι 𝕜 E) (x : E) :
    HasSum (fun i => b.repr x i • b i) x

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x : E
⊢ HasSum (fun i => ↑(b.repr x) i • b i) x

Tactic:
simpa using b.hasSum_repr_symm (b.repr x)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey?_insertManyIfNewUnit_empty_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
    {l : List α} {k : α} (h' : l.contains k = false) :
    getKey? (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l).1 k = none

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List α
k : α
h' : l.contains k = false
⊢ (insertManyIfNewUnit empty l).val.getKey? k = none

Tactic:
exact getKey?_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false _ Raw.WF.empty₀
  contains_empty h'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem negSucc_max_zero (n : Nat) : (max (Int.negSucc n) 0) = 0

Proof state:
n : Nat
⊢ max -[n+1] 0 = 0

Tactic:
rw [Int.max_eq_right (negSucc_le_zero _)]

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
theorem mulRothNumber_spec :
    ∃ t ⊆ s, #t = mulRothNumber s ∧ ThreeGPFree (t : Set α) :=
  Nat.findGreatest_spec (P := fun m ↦ ∃ t ⊆ s, #t = m ∧ ThreeGPFree (t : Set α))
    (Nat.zero_le _) ⟨∅, empty_subset _, card_empty, by norm_cast; exact threeGPFree_empty⟩

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ ThreeGPFree ∅

Tactic:
exact threeGPFree_empty

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ ThreeGPFree ↑∅

Tactic:
norm_cast

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ ThreeGPFree ∅