harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean
theorem mk_eq_fun_of_mem_aeSeqSet (hf : ∀ i, AEMeasurable (f i) μ) {x : α} (hx : x ∈ aeSeqSet hf p)
    (i : ι) : (hf i).mk (f i) x = f i x :=
  haveI h_ss : aeSeqSet hf p ⊆ { x | ∀ i, f i x = (hf i).mk (f i) x }

Proof state:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x✝ : α
hx : x✝ ∈ aeSeqSet hf p
i : ι
x : α
h : x ∈ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n => f n x}
⊢ x ∈ {x | ∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x}

Tactic:
exact h.1

Result:
no goals

Proof state:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ aeSeqSet hf p ⊆ {x | ∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x}

Tactic:
rw [aeSeqSet, ← compl_compl { x | ∀ i, f i x = (hf i).mk (f i) x }, Set.compl_subset_compl]

Result:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ {x | ∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x}ᶜ ⊆
    toMeasurable μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n => f n x}ᶜ

Proof state:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ {x | ∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x}ᶜ ⊆
    toMeasurable μ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n => f n x}ᶜ

Tactic:
refine Set.Subset.trans (Set.compl_subset_compl.mpr fun x h => ?_) (subset_toMeasurable _ _)

Result:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x✝ : α
hx : x✝ ∈ aeSeqSet hf p
i : ι
x : α
h : x ∈ {x | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun n => f n x}
⊢ x ∈ {x | ∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x}
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue_eq_getValueCast {β : Type v} [BEq α] [LawfulBEq α] {l : List ((_ : α) × β)} {a : α}
    {h} : getValue a l h = getValueCast a l h

Proof state:
case cons
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a k✝ : α
v✝ : β
tail✝ : List ((_ : α) × β)
a✝ : ∀ {h : containsKey a tail✝ = true}, getValue a tail✝ h = getValueCast a tail✝ h
h : containsKey a (⟨k✝, v✝⟩ :: tail✝) = true
⊢ getValue a (⟨k✝, v✝⟩ :: tail✝) h = getValueCast a (⟨k✝, v✝⟩ :: tail✝) h

Tactic:
simp_all [getValue_cons, getValueCast_cons]

Result:
no goals

Proof state:
case nil
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : containsKey a [] = true
⊢ getValue a [] h = getValueCast a [] h

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((_ : α) × β)
a : α
h : containsKey a l = true
⊢ getValue a l h = getValueCast a l h

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
h : containsKey a [] = true
⊢ getValue a [] h = getValueCast a [] h

case cons
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a k✝ : α
v✝ : β
tail✝ : List ((_ : α) × β)
a✝ : ∀ {h : containsKey a tail✝ = true}, getValue a tail✝ h = getValueCast a tail✝ h
h : containsKey a (⟨k✝, v✝⟩ :: tail✝) = true
⊢ getValue a (⟨k✝, v✝⟩ :: tail✝) h = getValueCast a (⟨k✝, v✝⟩ :: tail✝) h
-- Mathlib/Analysis/InnerProductSpace/Positive.lean
theorem isPositive_zero : IsPositive (0 : E →L[𝕜] E)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
⊢ IsPositive 0

Tactic:
refine ⟨.zero _, fun x => ?_⟩

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
x : E
⊢ 0 ≤ reApplyInnerSelf 0 x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
x : E
⊢ 0 ≤ re ⟪0 x, x⟫_𝕜

Tactic:
rw [zero_apply, inner_zero_left, ZeroHomClass.map_zero]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
x : E
⊢ 0 ≤ reApplyInnerSelf 0 x

Tactic:
change 0 ≤ re ⟪_, _⟫

Result:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
x : E
⊢ 0 ≤ re ⟪0 x, x⟫_𝕜
-- Mathlib/Data/Finset/Card.lean
/-- Reorder a finset.

The difference with `Finset.card_bij'` is that the bijection is specified as a surjective injection,
rather than by an inverse function.

The difference with `Finset.card_nbij` is that the bijection is allowed to use membership of the
domain, rather than being a non-dependent function. -/
lemma card_bij (i : ∀ a ∈ s, β) (hi : ∀ a ha, i a ha ∈ t)
    (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
    (i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) : #s = #t

Proof state:
case calc_2.e_s.h.mpr
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
b : β
h : b ∈ t
⊢ b ∈ image (fun a => i ↑a ⋯) s.attach

Tactic:
obtain ⟨a, ha, rfl⟩ := i_surj b h

Result:
case calc_2.e_s.h.mpr.intro.intro
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
a : α
ha : a ∈ s
h : i a ha ∈ t
⊢ i a ha ∈ image (fun a => i ↑a ⋯) s.attach

Proof state:
case calc_2
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ #(image (fun a => i ↑a ⋯) s.attach) = #t

Tactic:
congr 1

Result:
case calc_2.e_s
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
i : (a : α) → a ∈ s → β
hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t
i_inj : ∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂
i_surj : ∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b
⊢ image (fun a => i ↑a ⋯) s.attach = t
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem fp_bfamily_unbounded (H : ∀ i hi, IsNormal (f i hi)) :
    (⋂ (i) (hi), Function.fixedPoints (f i hi)).Unbounded (· < ·) := fun a =>
  ⟨nfpBFamily.{u, v} _ f a, by
    rw [Set.mem_iInter₂]
    exact fun i hi => nfpBFamily_fp (H i hi) _, (le_nfpBFamily f a).not_lt⟩

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ ∀ (i : Ordinal.{u}) (j : i < o), o.nfpBFamily f a ∈ fixedPoints (f i j)

Tactic:
exact fun i hi => nfpBFamily_fp (H i hi) _

Result:
no goals

Proof state:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ o.nfpBFamily f a ∈ ⋂ i, ⋂ (hi : i < o), fixedPoints (f i hi)

Tactic:
rw [Set.mem_iInter₂]

Result:
o : Ordinal.{u}
f : (b : Ordinal.{u}) → b < o → Ordinal.{max u v} → Ordinal.{max u v}
H : ∀ (i : Ordinal.{u}) (hi : i < o), IsNormal (f i hi)
a : Ordinal.{max u v}
⊢ ∀ (i : Ordinal.{u}) (j : i < o), o.nfpBFamily f a ∈ fixedPoints (f i j)
-- Mathlib/Order/Category/PartOrd.lean
lemma comp_apply {X Y Z : PartOrd} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
    (f ≫ g) x = g (f x)

Proof state:
X Y Z : PartOrd
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BoundedContinuousFunction.lean
lemma tendsto_integral_of_forall_limsup_integral_le_integral {ι : Type*} {L : Filter ι}
    {μ : Measure X} [IsProbabilityMeasure μ] {μs : ι → Measure X} [∀ i, IsProbabilityMeasure (μs i)]
    (h : ∀ f : X →ᵇ ℝ, 0 ≤ f → L.limsup (fun i ↦ ∫ x, f x ∂ (μs i)) ≤ ∫ x, f x ∂μ)
    (f : X →ᵇ ℝ) :
    Tendsto (fun i ↦ ∫ x, f x ∂ (μs i)) L (𝓝 (∫ x, f x ∂μ))

Proof state:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) L fun i => ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) L fun i => ∫ (x : X), f x ∂μs i
⊢ limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ

Tactic:
have key := h _ (f.add_norm_nonneg)

Result:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) L fun i => ∫ (x : X), f x ∂μs i
bdd_below : IsBoundedUnder (fun x1 x2 => x1 ≥ x2) L fun i => ∫ (x : X), f x ∂μs i
key : limsup (fun i => ∫ (x : X), (f + const X ‖f‖) x ∂μs i) L ≤ ∫ (x : X), (f + const X ‖f‖) x ∂μ
⊢ limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ

Proof state:
X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : MeasurableSpace X
inst✝² : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst✝¹ : IsProbabilityMeasure μ
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
h : ∀ (f : X →ᵇ ℝ), 0 ≤ f → limsup (fun i => ∫ (x : X), f x ∂μs i) L ≤ ∫ (x : X), f x ∂μ
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (Set.range fun i => ∫ (x : X), f x ∂μs i)
bdd_above : IsBoundedUnder (fun x1 x2 => x1 ≤ x2) L fun i => ∫ (x : X), f x ∂μs i
⊢ BddBelow (?m.39158 '' Set.univ)

Tactic:
simpa using obs.bddBelow

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem orthogonal_eq_inter : Kᗮ = ⨅ v : K, LinearMap.ker (innerSL 𝕜 (v : E))

Proof state:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
v : E
hv : v ∈ ⨅ v, LinearMap.ker ((innerSL 𝕜) ↑v)
w : E
hw : w ∈ K
⊢ inner w v = 0

Tactic:
simp only [mem_iInf] at hv

Result:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
v w : E
hw : w ∈ K
hv : ∀ (i : ↥K), v ∈ LinearMap.ker ((innerSL 𝕜) ↑i)
⊢ inner w v = 0

Proof state:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
v w : E
hw : w ∈ K
hv : ∀ (i : ↥K), v ∈ LinearMap.ker ((innerSL 𝕜) ↑i)
⊢ inner w v = 0

Tactic:
exact hv ⟨w, hw⟩

Result:
no goals

Proof state:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ ⨅ v, LinearMap.ker ((innerSL 𝕜) ↑v) ≤ Kᗮ

Tactic:
intro v hv w hw

Result:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
v : E
hv : v ∈ ⨅ v, LinearMap.ker ((innerSL 𝕜) ↑v)
w : E
hw : w ∈ K
⊢ inner w v = 0

Proof state:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ ∀ (i : ↥K), Kᗮ ≤ LinearMap.ker ((innerSL 𝕜) ↑i)

Tactic:
rintro ⟨v, hv⟩ w hw

Result:
case a.mk
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
v : E
hv : v ∈ K
w : E
hw : w ∈ Kᗮ
⊢ w ∈ LinearMap.ker ((innerSL 𝕜) ↑⟨v, hv⟩)

Proof state:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ Kᗮ ≤ ⨅ v, LinearMap.ker ((innerSL 𝕜) ↑v)

Tactic:
rw [le_iInf_iff]

Result:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ ∀ (i : ↥K), Kᗮ ≤ LinearMap.ker ((innerSL 𝕜) ↑i)

Proof state:
case a.mk
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
v : E
hv : v ∈ K
w : E
hw : w ∈ Kᗮ
⊢ w ∈ LinearMap.ker ((innerSL 𝕜) ↑⟨v, hv⟩)

Tactic:
simpa using hw _ hv

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ Kᗮ = ⨅ v, LinearMap.ker ((innerSL 𝕜) ↑v)

Tactic:
apply le_antisymm

Result:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ Kᗮ ≤ ⨅ v, LinearMap.ker ((innerSL 𝕜) ↑v)

case a
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ ⨅ v, LinearMap.ker ((innerSL 𝕜) ↑v) ≤ Kᗮ
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem sum_reflectionCircumcenterWeightsWithCircumcenter {n : ℕ} {i₁ i₂ : Fin (n + 1)}
    (h : i₁ ≠ i₂) : ∑ i, reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ i = 1

Proof state:
n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ ∑ i : PointsWithCircumcenterIndex n, reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ i = 1

Tactic:
simp_rw [sum_pointsWithCircumcenter, reflectionCircumcenterWeightsWithCircumcenter, sum_ite,
  sum_const, filter_or, filter_eq']

Result:
n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ #((if i₁ ∈ univ then {i₁} else ∅) ∪ if i₂ ∈ univ then {i₂} else ∅) • 1 +
        #(filter (fun x => ¬(x = i₁ ∨ x = i₂)) univ) • 0 +
      -1 =
    1

Proof state:
n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ (#(if i₁ ∈ univ then {i₁} else ∅) + #(if i₂ ∈ univ then {i₂} else ∅)) • 1 +
        #(filter (fun x => ¬(x = i₁ ∨ x = i₂)) univ) • 0 +
      -1 =
    1

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ Disjoint (if i₁ ∈ univ then {i₁} else ∅) (if i₂ ∈ univ then {i₂} else ∅)

Tactic:
simpa only [if_true, mem_univ, disjoint_singleton] using h

Result:
no goals

Proof state:
n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ #((if i₁ ∈ univ then {i₁} else ∅) ∪ if i₂ ∈ univ then {i₂} else ∅) • 1 +
        #(filter (fun x => ¬(x = i₁ ∨ x = i₂)) univ) • 0 +
      -1 =
    1

Tactic:
rw [card_union_of_disjoint]

Result:
n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ (#(if i₁ ∈ univ then {i₁} else ∅) + #(if i₂ ∈ univ then {i₂} else ∅)) • 1 +
        #(filter (fun x => ¬(x = i₁ ∨ x = i₂)) univ) • 0 +
      -1 =
    1

n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ Disjoint (if i₁ ∈ univ then {i₁} else ∅) (if i₂ ∈ univ then {i₂} else ∅)

Proof state:
n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ (#(if i₁ ∈ univ then {i₁} else ∅) + #(if i₂ ∈ univ then {i₂} else ∅)) • 1 +
        #(filter (fun x => ¬(x = i₁ ∨ x = i₂)) univ) • 0 +
      -1 =
    1

Tactic:
set_option simprocs false in simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem map_toArray_inj [Monad m] [LawfulMonad m] [Nonempty α]
    {v₁ : m (Vector α n)} {v₂ : m (Vector α n)} (w : toArray <$> v₁ = toArray <$> v₂) :
    v₁ = v₂

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
n : Nat
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : Nonempty α
v₁ v₂ : m (Vector α n)
w : toArray <$> v₁ = toArray <$> v₂
⊢ ∀ (x y : Vector α n), x.toArray = y.toArray → x = y

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
n : Nat
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : Nonempty α
v₁ v₂ : m (Vector α n)
w : toArray <$> v₁ = toArray <$> v₂
⊢ v₁ = v₂

Tactic:
apply map_inj_of_inj ?_ w

Result:
m : Type u_1 → Type u_2
α : Type u_1
n : Nat
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : Nonempty α
v₁ v₂ : m (Vector α n)
w : toArray <$> v₁ = toArray <$> v₂
⊢ ∀ (x y : Vector α n), x.toArray = y.toArray → x = y
-- Mathlib/Data/Nat/Init.lean
@[simp] protected lemma div_eq_zero_iff : a / b = 0 ↔ b = 0 ∨ a < b where
  mp h

Proof state:
a b : ℕ
⊢ b = 0 ∨ a < b → a / b = 0

Tactic:
obtain rfl | hb := Decidable.em (b = 0)

Result:
case inl
a : ℕ
⊢ 0 = 0 ∨ a < 0 → a / 0 = 0

case inr
a b : ℕ
hb : ¬b = 0
⊢ b = 0 ∨ a < b → a / b = 0

Proof state:
case inr
a b : ℕ
hb : ¬b = 0
⊢ b = 0 ∨ a < b → a / b = 0

Tactic:
simp only [hb, false_or]

Result:
case inr
a b : ℕ
hb : ¬b = 0
⊢ a < b → a / b = 0

Proof state:
case inl
a : ℕ
⊢ 0 = 0 ∨ a < 0 → a / 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
a b : ℕ
hb : ¬b = 0
⊢ a < b → a / b = 0

Tactic:
rw [← Nat.mul_right_inj hb, ← Nat.add_left_cancel_iff, mod_add_div]

Result:
case inr
a b : ℕ
hb : ¬b = 0
⊢ a < b → a = a % b + b * 0

Proof state:
a b : ℕ
h : a / b = 0
⊢ b = 0 ∨ a < b

Tactic:
rw [← mod_add_div a b, h, Nat.mul_zero, Nat.add_zero, Decidable.or_iff_not_imp_left]

Result:
a b : ℕ
h : a / b = 0
⊢ ¬b = 0 → a % b < b

Proof state:
a b : ℕ
h : a / b = 0
⊢ ¬b = 0 → a % b < b

Tactic:
exact mod_lt _ ∘ Nat.pos_iff_ne_zero.2

Result:
no goals

Proof state:
case inr
a b : ℕ
hb : ¬b = 0
⊢ a < b → a = a % b + b * 0

Tactic:
simp +contextual [mod_eq_of_lt]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_union_eq (h : Disjoint s t) (hs : s.Finite

Proof state:
α : Type u_1
s t : Set α
h : Disjoint s t
hs : autoParam s.Finite _auto✝
ht : autoParam t.Finite _auto✝
⊢ ↑(s ∪ t).ncard = ↑s.ncard + ↑t.ncard

Tactic:
rw [hs.cast_ncard_eq, ht.cast_ncard_eq, (hs.union ht).cast_ncard_eq, encard_union_eq h]

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
h : Disjoint s t
hs : autoParam s.Finite _auto✝
ht : autoParam t.Finite _auto✝
⊢ (s ∪ t).ncard = s.ncard + t.ncard

Tactic:
to_encard_tac

Result:
α : Type u_1
s t : Set α
h : Disjoint s t
hs : autoParam s.Finite _auto✝
ht : autoParam t.Finite _auto✝
⊢ ↑(s ∪ t).ncard = ↑s.ncard + ↑t.ncard
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem hsum_mul {β : Type*} (s : SummableFamily Γ R α) (t : SummableFamily Γ R β) :
    (mul s t).hsum = s.hsum * t.hsum

Proof state:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
β : Type u_7
s : SummableFamily Γ R α
t : SummableFamily Γ R β
⊢ (s.smul t).hsum = s.hsum • t.hsum

Tactic:
exact smul_hsum s t

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
β : Type u_7
s : SummableFamily Γ R α
t : SummableFamily Γ R β
⊢ (s.mul t).hsum = s.hsum * t.hsum

Tactic:
rw [← smul_eq_mul, mul_eq_smul]

Result:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
β : Type u_7
s : SummableFamily Γ R α
t : SummableFamily Γ R β
⊢ (s.smul t).hsum = s.hsum • t.hsum
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_alter_eq_self_of_mem [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
    (h : m.WF) (h₁ : k ∈ m) (h₂ : (f (m.get? k)).isSome)  :
    (m.alter k f).size = m.size

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ k ∈ m → (f (m.get? k)).isSome = true → (m.alter k f).size = m.size

Tactic:
simp only [mem_iff_contains]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ m.contains k = true → (f (m.get? k)).isSome = true → (m.alter k f).size = m.size

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ m.contains k = true → (f (m.get? k)).isSome = true → (m.alter k f).size = m.size

Tactic:
simp_to_raw using Raw₀.size_alter_eq_self_of_mem

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
h₁ : k ∈ m
h₂ : (f (m.get? k)).isSome = true
⊢ (m.alter k f).size = m.size

Tactic:
revert h₁ h₂

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
h : m.WF
⊢ k ∈ m → (f (m.get? k)).isSome = true → (m.alter k f).size = m.size
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem LinearIsometry.norm_compContinuousMultilinearMap (g : G →ₗᵢ[𝕜] G')
    (f : ContinuousMultilinearMap 𝕜 E G) :
    ‖g.toContinuousLinearMap.compContinuousMultilinearMap f‖ = ‖f‖

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
G' : Type wG'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
g : G →ₗᵢ[𝕜] G'
f : ContinuousMultilinearMap 𝕜 E G
⊢ ‖g.toContinuousLinearMap.compContinuousMultilinearMap f‖ = ‖f‖

Tactic:
simp only [ContinuousLinearMap.compContinuousMultilinearMap_coe,
  LinearIsometry.coe_toContinuousLinearMap, LinearIsometry.norm_map,
  ContinuousMultilinearMap.norm_def, Function.comp_apply]

Result:
no goals
-- Mathlib/RingTheory/Artinian/Module.lean
theorem isArtinian_of_fg_of_artinian {R M} [Ring R] [AddCommGroup M] [Module R M]
    (N : Submodule R M) [IsArtinianRing R] (hN : N.FG) : IsArtinian R N

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : Module.Finite R ↥N
⊢ IsArtinian R ↥N

Tactic:
infer_instance

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : N.FG
⊢ IsArtinian R ↥N

Tactic:
rw [← Module.Finite.iff_fg] at hN

Result:
R : Type u_1
M : Type u_2
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsArtinianRing R
hN : Module.Finite R ↥N
⊢ IsArtinian R ↥N
-- Mathlib/Analysis/Calculus/Deriv/Shift.lean
/-- Translation in the domain does not change the derivative. -/
lemma deriv_comp_const_add : deriv (fun x ↦ f (a + x)) x = deriv f (a + x)

Proof state:
case pos
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a x : 𝕜
hf : DifferentiableAt 𝕜 f (a + x)
⊢ deriv (fun x => f (a + x)) x = deriv f (a + x)

Tactic:
exact HasDerivAt.deriv hf.hasDerivAt.comp_const_add

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a x : 𝕜
⊢ deriv (fun x => f (a + x)) x = deriv f (a + x)

Tactic:
by_cases hf : DifferentiableAt 𝕜 f (a + x)

Result:
case pos
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a x : 𝕜
hf : DifferentiableAt 𝕜 f (a + x)
⊢ deriv (fun x => f (a + x)) x = deriv f (a + x)

case neg
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a x : 𝕜
hf : ¬DifferentiableAt 𝕜 f (a + x)
⊢ deriv (fun x => f (a + x)) x = deriv f (a + x)

Proof state:
case neg
𝕜 : Type u_1
F : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
a x : 𝕜
hf : ¬DifferentiableAt 𝕜 f (a + x)
⊢ deriv (fun x => f (a + x)) x = deriv f (a + x)

Tactic:
rw [deriv_zero_of_not_differentiableAt (differentiableAt_comp_const_add.not.2 hf),
  deriv_zero_of_not_differentiableAt hf]

Result:
no goals