harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/HomologicalBicomplex.lean
@[reassoc (attr := simp)]
lemma d_f_comp_d_f (K : HomologicalComplex₂ C c₁ c₂)
    (i₁ i₁' i₁'' : I₁) (i₂ : I₂) :
    (K.d i₁ i₁').f i₂ ≫ (K.d i₁' i₁'').f i₂ = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
i₁ i₁' i₁'' : I₁
i₂ : I₂
⊢ (K.d i₁ i₁').f i₂ ≫ (K.d i₁' i₁'').f i₂ = 0

Tactic:
rw [← comp_f, d_comp_d, zero_f]

Result:
no goals
-- Mathlib/Geometry/Manifold/Diffeomorph.lean
lemma sumComm_inl : (Diffeomorph.sumComm I M n M') ∘ Sum.inl = Sum.inr

Proof state:
case h
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
n : WithTop ℕ∞
M' : Type u_13
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x✝ : M
⊢ (⇑(sumComm I M n M') ∘ Sum.inl) x✝ = Sum.inr x✝

Tactic:
exact Sum.swap_inl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
n : WithTop ℕ∞
M' : Type u_13
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
⊢ ⇑(sumComm I M n M') ∘ Sum.inl = Sum.inr

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_9
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
n : WithTop ℕ∞
M' : Type u_13
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
x✝ : M
⊢ (⇑(sumComm I M n M') ∘ Sum.inl) x✝ = Sum.inr x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem div_nonneg_iff_of_pos {a b : Int} (h : 0 < b) : a / b ≥ 0 ↔ a ≥ 0

Proof state:
a b : Int
h : 0 < b
⊢ a / b ≥ 0 ↔ a ≥ 0

Tactic:
rw [Int.div_def]

Result:
a b : Int
h : 0 < b
⊢ a.ediv b ≥ 0 ↔ a ≥ 0

Proof state:
a b : Int
h : 0 < b
⊢ a.ediv b ≥ 0 ↔ a ≥ 0

Tactic:
match b, h with
| Int.ofNat (b+1), _ =>
  rcases a with ⟨a⟩ <;> simp [Int.ediv]
  exact decide_eq_decide.mp rfl

Result:
no goals

Proof state:
a b✝ : Int
h : 0 < b✝
b : Nat
x✝ : 0 < ofNat (b + 1)
⊢ a.ediv (ofNat (b + 1)) ≥ 0 ↔ a ≥ 0

Tactic:
rcases a with ⟨a⟩ <;> simp [Int.ediv]

Result:
case ofNat
b✝ : Int
h : 0 < b✝
b : Nat
x✝ : 0 < ofNat (b + 1)
a : Nat
⊢ 0 ≤ ↑a / (↑b + 1) ↔ 0 ≤ ↑a

Proof state:
case ofNat
b✝ : Int
h : 0 < b✝
b : Nat
x✝ : 0 < ofNat (b + 1)
a : Nat
⊢ 0 ≤ ↑a / (↑b + 1) ↔ 0 ≤ ↑a

Tactic:
exact decide_eq_decide.mp rfl

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem div_le {a b c : Ordinal} (b0 : b ≠ 0) : a / b ≤ c ↔ a < b * succ c :=
  ⟨fun h => (lt_mul_succ_div a b0).trans_le (mul_le_mul_left' (succ_le_succ_iff.2 h) _), fun h => by
    rw [div_def a b0]; exact csInf_le' h⟩

Proof state:
a b c : Ordinal.{u_4}
b0 : b ≠ 0
h : a < b * succ c
⊢ sInf {o | a < b * succ o} ≤ c

Tactic:
exact csInf_le' h

Result:
no goals

Proof state:
a b c : Ordinal.{u_4}
b0 : b ≠ 0
h : a < b * succ c
⊢ a / b ≤ c

Tactic:
rw [div_def a b0]

Result:
a b c : Ordinal.{u_4}
b0 : b ≠ 0
h : a < b * succ c
⊢ sInf {o | a < b * succ o} ≤ c
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_nonneg_of_ae_restrict (hab : a ≤ b) (hf : 0 ≤ᵐ[μ.restrict (Icc a b)] f) :
    0 ≤ ∫ u in a..b, f u ∂μ

Proof state:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : 0 ≤ᶠ[ae (μ.restrict (Icc a b))] f
⊢ 0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ

Tactic:
let H := ae_restrict_of_ae_restrict_of_subset Ioc_subset_Icc_self hf

Result:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : 0 ≤ᶠ[ae (μ.restrict (Icc a b))] f
H : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioc a b), 0 x ≤ f x := ae_restrict_of_ae_restrict_of_subset Ioc_subset_Icc_self hf
⊢ 0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ

Proof state:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hab : a ≤ b
hf : 0 ≤ᶠ[ae (μ.restrict (Icc a b))] f
H : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioc a b), 0 x ≤ f x := ae_restrict_of_ae_restrict_of_subset Ioc_subset_Icc_self hf
⊢ 0 ≤ ∫ (u : ℝ) in a..b, f u ∂μ

Tactic:
simpa only [integral_of_le hab] using setIntegral_nonneg_of_ae_restrict H

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_countable [MeasurableSingletonClass α] (f : α → ℝ≥0∞) {s : Set α}
    (hs : s.Countable) : ∫⁻ a in s, f a ∂μ = ∑' a : s, f a * μ {(a : α)} :=
  calc
    ∫⁻ a in s, f a ∂μ = ∫⁻ a in ⋃ x ∈ s, {x}, f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
s : Set α
hs : s.Countable
⊢ ∑' (a : ↑s), ∫⁻ (x : α) in {↑a}, f x ∂μ = ∑' (a : ↑s), f ↑a * μ {↑a}

Tactic:
simp only [lintegral_singleton]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
f : α → ℝ≥0∞
s : Set α
hs : s.Countable
⊢ ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in ⋃ x ∈ s, {x}, f a ∂μ

Tactic:
rw [biUnion_of_singleton]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean
lemma shiftIso_hom_app (n a a' : ℤ) (ha' : n + a = a') (K : CochainComplex C ℤ) :
    (shiftIso C n a a' ha').hom.app K =
      ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').hom.app K)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
n a a' : ℤ
ha' : n + a = a'
K : CochainComplex C ℤ
⊢ (shiftIso C n a a' ha').hom.app K = ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').hom.app K)

Tactic:
dsimp [shiftIso]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
n a a' : ℤ
ha' : n + a = a'
K : CochainComplex C ℤ
⊢ 𝟙 (((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).obj K).homology a) ≫
      𝟙
          ((shortComplexFunctor C (up ℤ) a).obj
              ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).obj K)).homology ≫
        ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').hom.app K) ≫ 𝟙 (homology K a') =
    ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').hom.app K)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
n a a' : ℤ
ha' : n + a = a'
K : CochainComplex C ℤ
⊢ 𝟙 (((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).obj K).homology a) ≫
      𝟙
          ((shortComplexFunctor C (up ℤ) a).obj
              ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).obj K)).homology ≫
        ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').hom.app K) ≫ 𝟙 (homology K a') =
    ShortComplex.homologyMap ((shiftShortComplexFunctorIso C n a a' ha').hom.app K)

Tactic:
erw [id_comp, id_comp, comp_id]

Result:
no goals
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
@[to_additive (attr := simp)]
lemma divConst_inv_left (A B : Finset G) : δₘ[A⁻¹, B] = σₘ[A, B]

Proof state:
G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A B : Finset G
⊢ δₘ[A⁻¹, B] = σₘ[A, B]

Tactic:
rw [mulConst, divConst, card_inv, ← card_inv, inv_div, div_inv_eq_mul, mul_comm]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem sUnion_iUnion (s : ι → Set (Set α)) : ⋃₀ ⋃ i, s i = ⋃ i, ⋃₀ s i

Proof state:
α : Type u_1
ι : Sort u_5
s : ι → Set (Set α)
⊢ ⋃₀ ⋃ i, s i = ⋃ i, ⋃₀ s i

Tactic:
simp only [sUnion_eq_biUnion, biUnion_iUnion]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finrank.lean
theorem lt_rank_of_lt_finrank {n : ℕ} (h : n < finrank R M) : ↑n < Module.rank R M

Proof state:
case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : ℵ₀ ≤ Module.rank R M
⊢ finrank R M ≤ n

Tactic:
rw [finrank, Cardinal.toNat_apply_of_aleph0_le h]

Result:
case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : ℵ₀ ≤ Module.rank R M
⊢ 0 ≤ n

Proof state:
case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ ↑n < ℵ₀

Tactic:
exact nat_lt_aleph0 n

Result:
no goals

Proof state:
case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ Module.rank R M < ℵ₀

Tactic:
contrapose! h

Result:
case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : ℵ₀ ≤ Module.rank R M
⊢ finrank R M ≤ n

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ ↑n < Module.rank R M

Tactic:
rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_natCast]

Result:
case hc
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ ↑n < ℵ₀

case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : n < finrank R M
⊢ Module.rank R M < ℵ₀

Proof state:
case hd
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
h : ℵ₀ ≤ Module.rank R M
⊢ 0 ≤ n

Tactic:
exact n.zero_le

Result:
no goals
-- Mathlib/Data/Set/Countable.lean
theorem Countable.image2 {s : Set α} {t : Set β} (hs : s.Countable) (ht : t.Countable)
    (f : α → β → γ) : (image2 f s t).Countable

Proof state:
α : Type u
β : Type v
γ : Type w
s : Set α
t : Set β
hs : s.Countable
ht : t.Countable
f : α → β → γ
⊢ (Set.image2 f s t).Countable

Tactic:
rw [← image_prod]

Result:
α : Type u
β : Type v
γ : Type w
s : Set α
t : Set β
hs : s.Countable
ht : t.Countable
f : α → β → γ
⊢ ((fun x => f x.1 x.2) '' s ×ˢ t).Countable

Proof state:
α : Type u
β : Type v
γ : Type w
s : Set α
t : Set β
hs : s.Countable
ht : t.Countable
f : α → β → γ
⊢ ((fun x => f x.1 x.2) '' s ×ˢ t).Countable

Tactic:
exact (hs.prod ht).image _

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean
lemma NNReal.closedBall_zero_eq_Icc' (c : ℝ≥0) :
    Metric.closedBall (0 : ℝ≥0) c.toReal = Set.Icc 0 c

Proof state:
case h
c x : ℝ≥0
⊢ x ∈ closedBall 0 ↑c ↔ x ∈ Icc 0 c

Tactic:
simp

Result:
no goals

Proof state:
c : ℝ≥0
⊢ closedBall 0 ↑c = Icc 0 c

Tactic:
ext x

Result:
case h
c x : ℝ≥0
⊢ x ∈ closedBall 0 ↑c ↔ x ∈ Icc 0 c
-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma mk₃_surjective (X : ComposableArrows C 3) :
    ∃ (X₀ X₁ X₂ X₃ : C) (f₀ : X₀ ⟶ X₁) (f₁ : X₁ ⟶ X₂) (f₂ : X₂ ⟶ X₃), X = mk₃ f₀ f₁ f₂ :=
  ⟨_, _, _, _, X.map' 0 1, X.map' 1 2, X.map' 2 3,
    ext₃ rfl rfl rfl rfl (by simp) (by simp) (by simp)⟩

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ComposableArrows C 3
⊢ X.map' 2 3 ⋯ ⋯ = eqToHom ⋯ ≫ (mk₃ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯)).map' 2 3 ⋯ ⋯ ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ComposableArrows C 3
⊢ X.map' 0 1 ⋯ ⋯ = eqToHom ⋯ ≫ (mk₃ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯)).map' 0 1 ⋯ ⋯ ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X : ComposableArrows C 3
⊢ X.map' 1 2 ⋯ ⋯ = eqToHom ⋯ ≫ (mk₃ (X.map' 0 1 ⋯ ⋯) (X.map' 1 2 ⋯ ⋯) (X.map' 2 3 ⋯ ⋯)).map' 1 2 ⋯ ⋯ ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem indep_or_dep (hX : X ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.Indep X ∨ ¬M.Indep X

Tactic:
apply em

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.Indep X ∨ M.Dep X

Tactic:
rw [Dep, and_iff_left hX]

Result:
α : Type u_1
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.Indep X ∨ ¬M.Indep X
-- Mathlib/LinearAlgebra/Matrix/HermitianFunctionalCalculus.lean
lemma cfc_eq (f : ℝ → ℝ) : cfc f A = hA.cfc f

Proof state:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : cfcHom hA' = hA.cfcAux
⊢ hA.cfcAux { toFun := (spectrum ℝ A).restrict f, continuous_toFun := ⋯ } = hA.cfc f

Tactic:
simp only [cfcAux_apply, ContinuousMap.coe_mk, Function.comp_def, Set.restrict_apply,
  IsHermitian.cfc]

Result:
no goals

Proof state:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : cfcHom hA' = hA.cfcAux
⊢ Continuous ((spectrum ℝ A).restrict f)

Tactic:
fun_prop

Result:
no goals

Proof state:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : cfcHom hA' = hA.cfcAux
⊢ cfc f A = hA.cfc f

Tactic:
rw [cfc_apply f A hA' (by rw [continuousOn_iff_continuous_restrict]; fun_prop), this]

Result:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : cfcHom hA' = hA.cfcAux
⊢ hA.cfcAux { toFun := (spectrum ℝ A).restrict f, continuous_toFun := ⋯ } = hA.cfc f

Proof state:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : cfcHom hA' = hA.cfcAux
⊢ ContinuousOn f (spectrum ℝ A)

Tactic:
rw [continuousOn_iff_continuous_restrict]

Result:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : cfcHom hA' = hA.cfcAux
⊢ Continuous ((spectrum ℝ A).restrict f)

Proof state:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
⊢ cfc f A = hA.cfc f

Tactic:
have hA' : IsSelfAdjoint A := hA

Result:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
⊢ cfc f A = hA.cfc f

Proof state:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
⊢ cfc f A = hA.cfc f

Tactic:
have := cfcHom_eq_of_continuous_of_map_id hA' hA.cfcAux hA.isClosedEmbedding_cfcAux.continuous
  hA.cfcAux_id

Result:
n : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : ℝ → ℝ
hA' : IsSelfAdjoint A
this : cfcHom hA' = hA.cfcAux
⊢ cfc f A = hA.cfc f
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_mul_X_pow' (p : R⟦X⟧) (n d : ℕ) :
    coeff R d (p * X ^ n) = ite (n ≤ d) (coeff R (d - n) p) 0

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : n ≤ d
⊢ (coeff R d) (p * X ^ n) = (coeff R (d - n)) p

Tactic:
rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right]

Result:
no goals

Proof state:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ ¬x.2 = n

Tactic:
exact ((le_of_add_le_right (mem_antidiagonal.mp hx).le).trans_lt <| not_le.mp h).ne

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ (coeff R x.1) p * (coeff R x.2) (X ^ n) = 0

Tactic:
rw [coeff_X_pow, if_neg, mul_zero]

Result:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ ¬x.2 = n

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
⊢ (coeff R d) (p * X ^ n) = if n ≤ d then (coeff R (d - n)) p else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : n ≤ d
⊢ (coeff R d) (p * X ^ n) = (coeff R (d - n)) p

case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
⊢ (coeff R d) (p * X ^ n) = 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
⊢ (coeff R d) (p * X ^ n) = 0

Tactic:
refine (coeff_mul _ _ _).trans (Finset.sum_eq_zero fun x hx => ?_)

Result:
case neg
R : Type u_1
inst✝ : Semiring R
p : R⟦X⟧
n d : ℕ
h : ¬n ≤ d
x : ℕ × ℕ
hx : x ∈ antidiagonal d
⊢ (coeff R x.1) p * (coeff R x.2) (X ^ n) = 0
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_eq_foldl : ∀ {l : List M}, l.prod = foldl (· * ·) 1 l
  | [] => rfl
  | cons a l => by
    rw [prod_cons, prod_eq_foldl, ← foldl_assoc (α := M) (op := (· * ·))]
    simp

Proof state:
M : Type u_4
inst✝ : Monoid M
a : M
l : List M
⊢ foldl (fun x1 x2 => x1 * x2) (a * 1) l = foldl (fun x1 x2 => x1 * x2) 1 (a :: l)

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem rowLen_anti (μ : YoungDiagram) (i1 i2 : ℕ) (hi : i1 ≤ i2) : μ.rowLen i2 ≤ μ.rowLen i1

Proof state:
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : μ.rowLen i1 < μ.rowLen i2
⊢ False

Tactic:
rw [← lt_self_iff_false (μ.rowLen i1)]

Result:
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : μ.rowLen i1 < μ.rowLen i2
⊢ μ.rowLen i1 < μ.rowLen i1

Proof state:
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : (i2, μ.rowLen i1) ∈ μ
⊢ μ.rowLen i1 ≤ μ.rowLen i1

Tactic:
rfl

Result:
no goals

Proof state:
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : (i2, μ.rowLen i1) ∈ μ
⊢ (i1, μ.rowLen i1) ∈ μ

Tactic:
exact μ.up_left_mem hi (by rfl) h_lt

Result:
no goals

Proof state:
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : μ.rowLen i1 < μ.rowLen i2
⊢ μ.rowLen i1 < μ.rowLen i1

Tactic:
rw [← mem_iff_lt_rowLen] at h_lt ⊢

Result:
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : (i2, μ.rowLen i1) ∈ μ
⊢ (i1, μ.rowLen i1) ∈ μ

Proof state:
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
⊢ μ.rowLen i2 ≤ μ.rowLen i1

Tactic:
by_contra! h_lt

Result:
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : μ.rowLen i1 < μ.rowLen i2
⊢ False
-- Mathlib/Data/Finite/Card.lean
theorem card_eq_zero_iff [Finite α] : Nat.card α = 0 ↔ IsEmpty α

Proof state:
α : Type u_1
inst✝ : Finite α
⊢ Nat.card α = 0 ↔ IsEmpty α

Tactic:
haveI := Fintype.ofFinite α

Result:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α = 0 ↔ IsEmpty α

Proof state:
α : Type u_1
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α = 0 ↔ IsEmpty α

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_eq_zero_iff]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem mk (h : ∀ ⦃s : Set α⦄, MeasurableSet s → w s = 0 → v s = 0) : v ≪ᵥ w

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0
⊢ v ≪ᵥ w

Tactic:
intro s hs

Result:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0
s : Set α
hs : ↑w s = 0
⊢ ↑v s = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0
s : Set α
hs : ↑w s = 0
⊢ ↑v s = 0

Tactic:
by_cases hmeas : MeasurableSet s

Result:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0
s : Set α
hs : ↑w s = 0
hmeas : MeasurableSet s
⊢ ↑v s = 0

case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0
s : Set α
hs : ↑w s = 0
hmeas : ¬MeasurableSet s
⊢ ↑v s = 0

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0
s : Set α
hs : ↑w s = 0
hmeas : MeasurableSet s
⊢ ↑v s = 0

Tactic:
exact h hmeas hs

Result:
no goals

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
M : Type u_4
N : Type u_5
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
v : VectorMeasure α M
w : VectorMeasure α N
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0
s : Set α
hs : ↑w s = 0
hmeas : ¬MeasurableSet s
⊢ ↑v s = 0

Tactic:
exact not_measurable v hmeas

Result:
no goals
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem closure_Ioc {a b : α} (hab : a ≠ b) : closure (Ioc a b) = Icc a b

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure (Ioo a b)

Tactic:
rw [closure_Ioo hab]

Result:
no goals

Proof state:
case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure (Ioc a b)

Tactic:
apply Subset.trans _ (closure_mono Ioo_subset_Ioc_self)

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure (Ioo a b)

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure (Ioc a b) = Icc a b

Tactic:
apply Subset.antisymm

Result:
case h₁
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure (Ioc a b) ⊆ Icc a b

case h₂
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ Icc a b ⊆ closure (Ioc a b)

Proof state:
case h₁
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a b : α
hab : a ≠ b
⊢ closure (Ioc a b) ⊆ Icc a b

Tactic:
exact closure_minimal Ioc_subset_Icc_self isClosed_Icc

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
lemma tendsto_zpow_atTop_atTop {n : ℤ} (hn : 0 < n) : Tendsto (fun x : α ↦ x ^ n) atTop atTop

Proof state:
case intro
α : Type u_1
inst✝ : LinearOrderedSemifield α
n : ℕ
hn : 0 < ↑n
⊢ Tendsto (fun x => x ^ ↑n) atTop atTop

Tactic:
simp [(Int.ofNat_pos.mp hn).ne']

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
n : ℤ
hn : 0 < n
⊢ Tendsto (fun x => x ^ n) atTop atTop

Tactic:
lift n to ℕ using hn.le

Result:
case intro
α : Type u_1
inst✝ : LinearOrderedSemifield α
n : ℕ
hn : 0 < ↑n
⊢ Tendsto (fun x => x ^ ↑n) atTop atTop
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
/-- A variant of `inv_mul_eq_iff_eq_mul₀` that moves the nonzero hypothesis to another variable. -/
lemma eq_mul_of_inv_mul_eq₀ (hc : c ≠ 0) (h : b⁻¹ * a = c) : a = b * c

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a c : G₀
hc : c ≠ 0
h : 0⁻¹ * a = c
⊢ False

Tactic:
simp [hc.symm] at h

Result:
no goals

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hc : c ≠ 0
h : b⁻¹ * a = c
⊢ a = b * c

Tactic:
rwa [← inv_mul_eq_iff_eq_mul₀]

Result:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hc : c ≠ 0
h : b⁻¹ * a = c
⊢ b ≠ 0

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b c : G₀
hc : c ≠ 0
h : b⁻¹ * a = c
⊢ b ≠ 0

Tactic:
rintro rfl

Result:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a c : G₀
hc : c ≠ 0
h : 0⁻¹ * a = c
⊢ False