harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
theorem PolishSpace.innerRegular_isCompact_isClosed_measurableSet [TopologicalSpace α]
    [PolishSpace α] [BorelSpace α] (P : Measure α) [IsFiniteMeasure P] :
    P.InnerRegularWRT (fun s ↦ IsCompact s ∧ IsClosed s) MeasurableSet

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
⊢ P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet

Tactic:
letI := upgradePolishSpace α

Result:
α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
this : UpgradedPolishSpace α := upgradePolishSpace α
⊢ P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : TopologicalSpace α
inst✝² : PolishSpace α
inst✝¹ : BorelSpace α
P : Measure α
inst✝ : IsFiniteMeasure P
this : UpgradedPolishSpace α := upgradePolishSpace α
⊢ P.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet

Tactic:
exact innerRegular_isCompact_isClosed_measurableSet_of_finite P

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem unitOfList_cons {hd : α} {tl : List α} :
    unitOfList (hd :: tl) = insertManyIfNewUnit ((∅ : Raw α (fun _ => Unit)).insertIfNew hd ()) tl

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
hd : α
tl : List α
⊢ unitOfList (hd :: tl) = insertManyIfNewUnit (∅.insertIfNew hd ()) tl

Tactic:
simp_to_raw

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
hd : α
tl : List α
⊢ (Raw₀.Const.insertManyIfNewUnit Raw₀.empty (hd :: tl)).val.val =
    (Raw₀.Const.insertManyIfNewUnit (Raw₀.insertIfNew ⟨Raw₀.empty.val, ⋯⟩ hd ()) tl).val.val

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
hd : α
tl : List α
⊢ (Raw₀.Const.insertManyIfNewUnit Raw₀.empty (hd :: tl)).val.val =
    (Raw₀.Const.insertManyIfNewUnit (Raw₀.insertIfNew ⟨Raw₀.empty.val, ⋯⟩ hd ()) tl).val.val

Tactic:
rw [Raw₀.Const.insertManyIfNewUnit_empty_list_cons]

Result:
no goals
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem coe_filter_univ (p : α → Prop) [DecidablePred p] :
    (univ.filter p : Set α) = { x | p x }

Proof state:
α : Type u_1
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ ↑(filter p univ) = {x | p x}

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean
lemma congr_zero (p : FormalMultilinearSeries 𝕜 E F) {k l : ℕ} (h : k = l) (h' : p k = 0) :
    p l = 0

Proof state:
𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
k l : ℕ
h : k = l
h' : p k = 0
⊢ p l = 0

Tactic:
subst h

Result:
𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
k : ℕ
h' : p k = 0
⊢ p k = 0

Proof state:
𝕜 : Type u
E : Type v
F : Type w
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module 𝕜 E
inst✝⁷ : TopologicalSpace E
inst✝⁶ : ContinuousAdd E
inst✝⁵ : ContinuousConstSMul 𝕜 E
inst✝⁴ : AddCommMonoid F
inst✝³ : Module 𝕜 F
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousAdd F
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
k : ℕ
h' : p k = 0
⊢ p k = 0

Tactic:
exact h'

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem support_eq_empty {p} : p.support = ∅ ↔ (p : SkewMonoidAlgebra k G) = 0

Proof state:
case ofFinsupp
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
toFinsupp✝ : G →₀ k
⊢ { toFinsupp := toFinsupp✝ }.support = ∅ ↔ { toFinsupp := toFinsupp✝ } = 0

Tactic:
simp only [support, Finsupp.support_eq_empty, ofFinsupp_eq_zero]

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
p : SkewMonoidAlgebra k G
⊢ p.support = ∅ ↔ p = 0

Tactic:
rcases p with ⟨⟩

Result:
case ofFinsupp
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
toFinsupp✝ : G →₀ k
⊢ { toFinsupp := toFinsupp✝ }.support = ∅ ↔ { toFinsupp := toFinsupp✝ } = 0
-- Mathlib/Order/Filter/Lift.lean
theorem lift'_inf (f g : Filter α) {s : Set α → Set β} (hs : ∀ t₁ t₂, s (t₁ ∩ t₂) = s t₁ ∩ s t₂) :
    (f ⊓ g).lift' s = f.lift' s ⊓ g.lift' s

Proof state:
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ ⨅ i, (bif i then f else g).lift' s = ⨅ b, bif b then f.lift' s else g.lift' s

Tactic:
refine iInf_congr ?_

Result:
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ ∀ (i : Bool), (bif i then f else g).lift' s = bif i then f.lift' s else g.lift' s

Proof state:
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ (f ⊓ g).lift' s = f.lift' s ⊓ g.lift' s

Tactic:
rw [inf_eq_iInf, inf_eq_iInf, lift'_iInf hs]

Result:
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ ⨅ i, (bif i then f else g).lift' s = ⨅ b, bif b then f.lift' s else g.lift' s

Proof state:
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ ∀ (i : Bool), (bif i then f else g).lift' s = bif i then f.lift' s else g.lift' s

Tactic:
rintro (_|_) <;> rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem comp_fderiv' {f : G → E} :
    fderiv 𝕜 (iso ∘ f) = fun x ↦ (iso : E →L[𝕜] F).comp (fderiv 𝕜 f x)

Proof state:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
x : G
⊢ fderiv 𝕜 (⇑iso ∘ f) x =
    (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp (fderiv 𝕜 f x)

Tactic:
exact LinearIsometryEquiv.comp_fderiv iso

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
⊢ fderiv 𝕜 (⇑iso ∘ f) = fun x =>
    (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp (fderiv 𝕜 f x)

Tactic:
ext x : 1

Result:
case h
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃ₗᵢ[𝕜] F
f : G → E
x : G
⊢ fderiv 𝕜 (⇑iso ∘ f) x =
    (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp (fderiv 𝕜 f x)
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
@[simp]
lemma toMvPolynomial_zero : (0 : M₁ →ₗ[R] M₂).toMvPolynomial b₁ b₂ = 0

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Finite ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
⊢ (fun i => ((toMatrix b₁ b₂) 0).toMvPolynomial i) = 0

Tactic:
simp only [map_zero, Matrix.toMvPolynomial_zero]

Result:
no goals

Proof state:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Finite ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
⊢ toMvPolynomial b₁ b₂ 0 = 0

Tactic:
unfold toMvPolynomial

Result:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Finite ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
⊢ (fun i => ((toMatrix b₁ b₂) 0).toMvPolynomial i) = 0
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem mem_iff_lt_colLen {μ : YoungDiagram} {i j : ℕ} : (i, j) ∈ μ ↔ i < μ.colLen j

Proof state:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ i < μ.colLen j

Tactic:
rw [← rowLen_transpose, ← mem_iff_lt_rowLen]

Result:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ (j, i) ∈ μ.transpose

Proof state:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ (j, i) ∈ μ.transpose

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem cliqueFree_of_chromaticNumber_lt {n : ℕ} (hc : G.chromaticNumber < n) :
    G.CliqueFree n

Proof state:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
hne : G.chromaticNumber ≠ ⊤
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.CliqueFree n

Tactic:
refine this.cliqueFree ?_

Result:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
hne : G.chromaticNumber ≠ ⊤
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.chromaticNumber.toNat < n

Proof state:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
hc : ↑G.chromaticNumber.toNat < ↑n
hne : ↑G.chromaticNumber.toNat = G.chromaticNumber
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.chromaticNumber.toNat < n

Tactic:
simpa using hc

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
⊢ G.CliqueFree n

Tactic:
have hne : G.chromaticNumber ≠ ⊤ := hc.ne_top

Result:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
hne : G.chromaticNumber ≠ ⊤
⊢ G.CliqueFree n

Proof state:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
hne : ↑G.chromaticNumber.toNat = G.chromaticNumber
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.chromaticNumber.toNat < n

Tactic:
rw [← hne] at hc

Result:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
hc : ↑G.chromaticNumber.toNat < ↑n
hne : ↑G.chromaticNumber.toNat = G.chromaticNumber
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.chromaticNumber.toNat < n

Proof state:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
hne : G.chromaticNumber ≠ ⊤
⊢ G.CliqueFree n

Tactic:
obtain ⟨m, hc'⟩ := chromaticNumber_ne_top_iff_exists.mp hne

Result:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
hne : G.chromaticNumber ≠ ⊤
m : ℕ
hc' : G.Colorable m
⊢ G.CliqueFree n

Proof state:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
hne : G.chromaticNumber ≠ ⊤
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.chromaticNumber.toNat < n

Tactic:
rw [← ENat.coe_toNat_eq_self] at hne

Result:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
hne : ↑G.chromaticNumber.toNat = G.chromaticNumber
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.chromaticNumber.toNat < n

Proof state:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
hne : G.chromaticNumber ≠ ⊤
m : ℕ
hc' : G.Colorable m
⊢ G.CliqueFree n

Tactic:
have := colorable_chromaticNumber hc'

Result:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.chromaticNumber < ↑n
hne : G.chromaticNumber ≠ ⊤
m : ℕ
hc' : G.Colorable m
this : G.Colorable G.chromaticNumber.toNat
⊢ G.CliqueFree n
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem coe_nsmulRec : ∀ n, ⇑(nsmulRec n f) = n • ⇑f
  | 0 => by rw [nsmulRec, zero_smul, coe_zero]
  | n + 1 => by rw [nsmulRec, succ_nsmul, coe_add, coe_nsmulRec n]

Proof state:
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : AddMonoid β
inst✝¹ : BoundedAdd β
inst✝ : ContinuousAdd β
f : α →ᵇ β
n : ℕ
⊢ ⇑(nsmulRec (n + 1) f) = (n + 1) • ⇑f

Tactic:
rw [nsmulRec, succ_nsmul, coe_add, coe_nsmulRec n]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : AddMonoid β
inst✝¹ : BoundedAdd β
inst✝ : ContinuousAdd β
f : α →ᵇ β
⊢ ⇑(nsmulRec 0 f) = 0 • ⇑f

Tactic:
rw [nsmulRec, zero_smul, coe_zero]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem moebius_apply_one : μ 1 = 1

Proof state:
⊢ μ 1 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Filter.lean
theorem nhds_mono {l₁ l₂ : Filter α} : 𝓝 l₁ ≤ 𝓝 l₂ ↔ l₁ ≤ l₂

Proof state:
α : Type u_2
l₁ l₂ : Filter α
⊢ 𝓝 l₁ ≤ 𝓝 l₂ ↔ l₁ ≤ l₂

Tactic:
refine ⟨fun h => ?_, fun h => monotone_nhds h⟩

Result:
α : Type u_2
l₁ l₂ : Filter α
h : 𝓝 l₁ ≤ 𝓝 l₂
⊢ l₁ ≤ l₂

Proof state:
α : Type u_2
l₁ l₂ : Filter α
h : 𝓝 l₁ ≤ 𝓝 l₂
⊢ l₁ ≤ l₂

Tactic:
rw [← Iic_subset_Iic, ← sInter_nhds, ← sInter_nhds]

Result:
α : Type u_2
l₁ l₂ : Filter α
h : 𝓝 l₁ ≤ 𝓝 l₂
⊢ ⋂₀ {s | s ∈ 𝓝 l₁} ⊆ ⋂₀ {s | s ∈ 𝓝 l₂}

Proof state:
α : Type u_2
l₁ l₂ : Filter α
h : 𝓝 l₁ ≤ 𝓝 l₂
⊢ ⋂₀ {s | s ∈ 𝓝 l₁} ⊆ ⋂₀ {s | s ∈ 𝓝 l₂}

Tactic:
exact sInter_subset_sInter h

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma eLpNorm_sub_comm (f g : α → E) (p : ℝ≥0∞) (μ : Measure α) :
    eLpNorm (f - g) p μ = eLpNorm (g - f) p μ

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f g : α → E
p : ℝ≥0∞
μ : Measure α
⊢ eLpNorm (f - g) p μ = eLpNorm (g - f) p μ

Tactic:
simp [← eLpNorm_neg (f := f - g)]

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem mem_erase {a a' : α} {s : Finmap β} : a' ∈ erase a s ↔ a' ≠ a ∧ a' ∈ s :=
  induction_on s fun s => by simp

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
s✝ : Finmap β
s : AList β
⊢ a' ∈ erase a ⟦s⟧ ↔ a' ≠ a ∧ a' ∈ ⟦s⟧

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
theorem trunc_add (n) (φ ψ : R⟦X⟧) : trunc n (φ + ψ) = trunc n φ + trunc n ψ :=
  Polynomial.ext fun m => by
    simp only [coeff_trunc, AddMonoidHom.map_add, Polynomial.coeff_add]
    split_ifs with H
    · rfl
    · rw [zero_add]

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
H : ¬m < n
⊢ 0 = 0 + 0

Tactic:
rw [zero_add]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
⊢ (trunc n (φ + ψ)).coeff m = (trunc n φ + trunc n ψ).coeff m

Tactic:
simp only [coeff_trunc, AddMonoidHom.map_add, Polynomial.coeff_add]

Result:
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
⊢ (if m < n then (coeff R m) (φ + ψ) else 0) = (if m < n then (coeff R m) φ else 0) + if m < n then (coeff R m) ψ else 0

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
⊢ (if m < n then (coeff R m) (φ + ψ) else 0) = (if m < n then (coeff R m) φ else 0) + if m < n then (coeff R m) ψ else 0

Tactic:
split_ifs with H

Result:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
H : m < n
⊢ (coeff R m) (φ + ψ) = (coeff R m) φ + (coeff R m) ψ

case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
H : ¬m < n
⊢ 0 = 0 + 0

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
H : m < n
⊢ (coeff R m) (φ + ψ) = (coeff R m) φ + (coeff R m) ψ

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_const (c : ℝ≥0∞) : ∫⁻ _, c ∂μ = c * μ univ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
⊢ ∫⁻ (x : α), c ∂μ = c * μ univ

Tactic:
rw [← SimpleFunc.const_lintegral, ← SimpleFunc.lintegral_eq_lintegral, SimpleFunc.coe_const]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
⊢ ∫⁻ (x : α), c ∂μ = ∫⁻ (a : α), Function.const α c a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
⊢ ∫⁻ (x : α), c ∂μ = ∫⁻ (a : α), Function.const α c a ∂μ

Tactic:
rfl

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem exists_of_lt_mex {ι} {f : ι → Ordinal} {a} (ha : a < mex f) : ∃ i, f i = a

Proof state:
ι : Type u_4
f : ι → Ordinal.{max u_5 u_4}
a : Ordinal.{max u_4 u_5}
ha : a < mex f
ha' : ∀ (i : ι), f i ≠ a
⊢ False

Tactic:
exact ha.not_le (mex_le_of_ne ha')

Result:
no goals

Proof state:
ι : Type u_4
f : ι → Ordinal.{max u_5 u_4}
a : Ordinal.{max u_4 u_5}
ha : a < mex f
⊢ ∃ i, f i = a

Tactic:
by_contra! ha'

Result:
ι : Type u_4
f : ι → Ordinal.{max u_5 u_4}
a : Ordinal.{max u_4 u_5}
ha : a < mex f
ha' : ∀ (i : ι), f i ≠ a
⊢ False
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblY_of_Y_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q z ≠ 0)
    (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 = Q y * P z ^ 3)
    (hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3) : W'.dblY P = W'.dblU P ^ 3

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ W'.dblY P = W'.dblU P ^ 3

Tactic:
rw [dblY, negY_eq, negDblY_of_Y_eq hQz hx hy hy', dblZ_of_Y_eq hQz hx hy hy']

Result:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ -(-W'.dblU P) ^ 3 - W'.a₁ * W'.dblX P * 0 - W'.a₃ * 0 ^ 3 = W'.dblU P ^ 3

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Jacobian R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy : P y * Q z ^ 3 = Q y * P z ^ 3
hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3
⊢ -(-W'.dblU P) ^ 3 - W'.a₁ * W'.dblX P * 0 - W'.a₃ * 0 ^ 3 = W'.dblU P ^ 3

Tactic:
ring1

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive]
lemma prod_mulIndicator_eq_prod_inter [DecidableEq ι] (s t : Finset ι) (f : ι → β) :
    ∏ i ∈ s, (t : Set ι).mulIndicator f i = ∏ i ∈ s ∩ t, f i

Proof state:
ι : Type u_1
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → β
⊢ ∏ i ∈ filter (fun i => i ∈ ↑t) s, f i = ∏ i ∈ filter (fun i => i ∈ t) s, f i

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → β
⊢ ∏ i ∈ s, (↑t).mulIndicator f i = ∏ i ∈ s ∩ t, f i

Tactic:
rw [← filter_mem_eq_inter, prod_mulIndicator_eq_prod_filter]

Result:
ι : Type u_1
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → β
⊢ ∏ i ∈ filter (fun i => i ∈ ↑t) s, f i = ∏ i ∈ filter (fun i => i ∈ t) s, f i
-- Mathlib/Data/Matroid/Circuit.lean
lemma dual_rankPos_iff_exists_isCircuit : M✶.RankPos ↔ ∃ C, M.IsCircuit C

Proof state:
α : Type u_1
M : Matroid α
⊢ M✶.RankPos ↔ ∃ C, M.IsCircuit C

Tactic:
rw [rankPos_iff, dual_isBase_iff, diff_empty, not_iff_comm, not_exists,
  ← ground_indep_iff_isBase, indep_iff_forall_subset_not_isCircuit]

Result:
α : Type u_1
M : Matroid α
⊢ (∀ (x : Set α), ¬M.IsCircuit x) ↔ ∀ C ⊆ M.E, ¬M.IsCircuit C

Proof state:
α : Type u_1
M : Matroid α
⊢ (∀ (x : Set α), ¬M.IsCircuit x) ↔ ∀ C ⊆ M.E, ¬M.IsCircuit C

Tactic:
exact ⟨fun h C _ ↦ h C, fun h C hC ↦ h C hC.subset_ground hC⟩

Result:
no goals
-- Mathlib/Algebra/Homology/SingleHomology.lean
lemma CochainComplex.exactAt_succ_single_obj (A : C) (n : ℕ) :
    ExactAt ((single₀ C).obj A) (n + 1) :=
  exactAt_single_obj _ _ _ _ (by simp)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
A : C
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Configuration.lean
theorem lineCount_eq [Finite P] [Finite L] (p : P) : lineCount L p = order P L + 1

Proof state:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
⊢ lineCount L p = order P L + 1

Tactic:
classical
  obtain ⟨q, -, -, l, -, -, -, -, h, -⟩ := Classical.choose_spec (@exists_config P L _ _)
  cases nonempty_fintype { l : L // q ∈ l }
  rw [order, lineCount_eq_lineCount L p q, lineCount_eq_lineCount L (Classical.choose _) q,
    lineCount, Nat.card_eq_fintype_card, Nat.sub_add_cancel]
  exact Fintype.card_pos_iff.mpr ⟨⟨l, h⟩⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
l : L
h : q ∈ l
⊢ lineCount L p = order P L + 1

Tactic:
cases nonempty_fintype { l : L // q ∈ l }

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
l : L
h : q ∈ l
val✝ : Fintype { l // q ∈ l }
⊢ lineCount L p = order P L + 1

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
l : L
h : q ∈ l
val✝ : Fintype { l // q ∈ l }
⊢ 1 ≤ Fintype.card { l // q ∈ l }

Tactic:
exact Fintype.card_pos_iff.mpr ⟨⟨l, h⟩⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
l : L
h : q ∈ l
val✝ : Fintype { l // q ∈ l }
⊢ lineCount L p = order P L + 1

Tactic:
rw [order, lineCount_eq_lineCount L p q, lineCount_eq_lineCount L (Classical.choose _) q,
  lineCount, Nat.card_eq_fintype_card, Nat.sub_add_cancel]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
l : L
h : q ∈ l
val✝ : Fintype { l // q ∈ l }
⊢ 1 ≤ Fintype.card { l // q ∈ l }

Proof state:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p : P
⊢ lineCount L p = order P L + 1

Tactic:
obtain ⟨q, -, -, l, -, -, -, -, h, -⟩ := Classical.choose_spec (@exists_config P L _ _)

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
p q : P
l : L
h : q ∈ l
⊢ lineCount L p = order P L + 1
-- Mathlib/Order/Minimal.lean
theorem minimal_true : Minimal (fun _ ↦ True) x ↔ IsMin x

Proof state:
α : Type u_1
x : α
inst✝ : LE α
⊢ Minimal (fun x => True) x ↔ IsMin x

Tactic:
simp [IsMin, Minimal]

Result:
no goals