harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_insertIfNew [LawfulBEq α] (h : m.WF) {k a : α} {fallback : β a} {v : β k} :
    (m.insertIfNew k v).getD a fallback =
      if h : k == a ∧ ¬k ∈ m then cast (congrArg β (eq_of_beq h.1)) v
      else m.getD a fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k a : α
fallback : β a
v : β k
⊢ (m.insertIfNew k v).getD a fallback =
    if h : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.getD a fallback

Tactic:
simp_to_raw using Raw₀.getD_insertIfNew

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k a : α
fallback : β a
v : β k
⊢ (m.insertIfNew k v).getD a fallback = if h : (k == a) = true ∧ ¬k ∈ m then cast ⋯ v else m.getD a fallback

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k a : α
fallback : β a
v : β k
⊢ (m.insertIfNew k v).getD a fallback =
    if h : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.getD a fallback
-- Mathlib/FieldTheory/PurelyInseparable/Tower.lean
/-- If `K / E / F` is a field extension tower, such that `E / F` is separable,
then $[E:F] [K:E]_s = [K:F]_s$.
It is a special case of `Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic`, and is an
intermediate result used to prove it. -/
lemma lift_rank_mul_lift_sepDegree_of_isSeparable [Algebra.IsSeparable F E] :
    Cardinal.lift.{w} (Module.rank F E) * Cardinal.lift.{v} (sepDegree E K) =
    Cardinal.lift.{v} (sepDegree F K)

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
⊢ Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (sepDegree E K) = Cardinal.lift.{v, w} (sepDegree F K)

Tactic:
rw [sepDegree, sepDegree, separableClosure.eq_restrictScalars_of_isSeparable F E K]

Result:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
⊢ Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (Module.rank E ↥(separableClosure E K)) =
    Cardinal.lift.{v, w} (Module.rank F ↥(restrictScalars F (separableClosure E K)))

Proof state:
F : Type u
E : Type v
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Algebra F E
K : Type w
inst✝⁴ : Field K
inst✝³ : Algebra F K
inst✝² : Algebra E K
inst✝¹ : IsScalarTower F E K
inst✝ : Algebra.IsSeparable F E
⊢ Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (Module.rank E ↥(separableClosure E K)) =
    Cardinal.lift.{v, w} (Module.rank F ↥(restrictScalars F (separableClosure E K)))

Tactic:
exact lift_rank_mul_lift_rank F E (separableClosure E K)

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem mem_wf : @WellFounded Class.{u} (· ∈ ·) :=
  ⟨by
    have H : ∀ x : ZFSet.{u}, @Acc Class.{u} (· ∈ ·) ↑x

Proof state:
case intro.intro
H : ∀ (x : ZFSet.{u}), Acc (fun x1 x2 => x1 ∈ x2) ↑x
A : Class.{u}
x : ZFSet.{u}
right✝ : A x
⊢ Acc (fun x1 x2 => x1 ∈ x2) ↑x

Tactic:
exact H x

Result:
no goals

Proof state:
H : ∀ (x : ZFSet.{u}), Acc (fun x1 x2 => x1 ∈ x2) ↑x
A : Class.{u}
⊢ ∀ y ∈ A, Acc (fun x1 x2 => x1 ∈ x2) y

Tactic:
rintro B ⟨x, rfl, _⟩

Result:
case intro.intro
H : ∀ (x : ZFSet.{u}), Acc (fun x1 x2 => x1 ∈ x2) ↑x
A : Class.{u}
x : ZFSet.{u}
right✝ : A x
⊢ Acc (fun x1 x2 => x1 ∈ x2) ↑x

Proof state:
H : ∀ (x : ZFSet.{u}), Acc (fun x1 x2 => x1 ∈ x2) ↑x
⊢ ∀ (a : Class.{u}), Acc (fun x1 x2 => x1 ∈ x2) a

Tactic:
refine fun A => ⟨A, ?_⟩

Result:
H : ∀ (x : ZFSet.{u}), Acc (fun x1 x2 => x1 ∈ x2) ↑x
A : Class.{u}
⊢ ∀ y ∈ A, Acc (fun x1 x2 => x1 ∈ x2) y

Proof state:
⊢ ∀ (x : ZFSet.{u}), Acc (fun x1 x2 => x1 ∈ x2) ↑x

Tactic:
refine fun a => ZFSet.inductionOn a fun x IH => ⟨_, ?_⟩

Result:
a x : ZFSet.{u}
IH : ∀ y ∈ x, Acc (fun x1 x2 => x1 ∈ x2) ↑y
⊢ ∀ y ∈ ↑x, Acc (fun x1 x2 => x1 ∈ x2) y

Proof state:
a x : ZFSet.{u}
IH : ∀ y ∈ x, Acc (fun x1 x2 => x1 ∈ x2) ↑y
⊢ ∀ y ∈ ↑x, Acc (fun x1 x2 => x1 ∈ x2) y

Tactic:
rintro A ⟨z, rfl, hz⟩

Result:
case intro.intro
a x : ZFSet.{u}
IH : ∀ y ∈ x, Acc (fun x1 x2 => x1 ∈ x2) ↑y
z : ZFSet.{u}
hz : ↑x z
⊢ Acc (fun x1 x2 => x1 ∈ x2) ↑z

Proof state:
case intro.intro
a x : ZFSet.{u}
IH : ∀ y ∈ x, Acc (fun x1 x2 => x1 ∈ x2) ↑y
z : ZFSet.{u}
hz : ↑x z
⊢ Acc (fun x1 x2 => x1 ∈ x2) ↑z

Tactic:
exact IH z hz

Result:
no goals
-- Mathlib/Data/Nat/Prime/Basic.lean
theorem coprime_or_dvd_of_prime {p} (pp : Prime p) (i : ℕ) : Coprime p i ∨ p ∣ i

Proof state:
p : ℕ
pp : Prime p
i : ℕ
⊢ p.Coprime i ∨ p ∣ i

Tactic:
rw [pp.dvd_iff_not_coprime]

Result:
p : ℕ
pp : Prime p
i : ℕ
⊢ p.Coprime i ∨ ¬p.Coprime i

Proof state:
p : ℕ
pp : Prime p
i : ℕ
⊢ p.Coprime i ∨ ¬p.Coprime i

Tactic:
apply em

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Units.lean
@[to_additive (attr := simp)]
lemma mem_iff_toUnits_mem_units (H : Subgroup G) (x : G) : toUnits x ∈ H.units ↔ x ∈ H

Proof state:
G : Type u_2
inst✝ : Group G
H : Subgroup G
x : G
⊢ toUnits x ∈ H.units ↔ x ∈ H

Tactic:
simp_rw [mem_units_iff_val_mem, val_toUnits_apply]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem range_inr : range (@Sum.inr α β) = {x | Sum.isRight x}

Proof state:
α : Type u_1
β : Type u_2
⊢ range Sum.inr = {x | x.isRight = true}

Tactic:
ext (_|_) <;> simp

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem equicontinuousAt_iff_pair {F : ι → X → α} {x₀ : X} :
    EquicontinuousAt F x₀ ↔
      ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ i, (F i x, F i y) ∈ U

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
simp_rw [← equicontinuousWithinAt_univ, equicontinuousWithinAt_iff_pair (mem_univ x₀),
  nhdsWithin_univ]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_eval_C (r : R) (a : A) (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
r : R
a : A
ha : autoParam (p a) _auto✝
⊢ cfc (fun a => Polynomial.eval a (Polynomial.C r)) a = (algebraMap R A) r

Tactic:
simp [cfc_const r a]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem norm_iteratedFDeriv_zero : ‖iteratedFDeriv 𝕜 0 f x‖ = ‖f x‖

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ ‖iteratedFDeriv 𝕜 0 f x‖ = ‖f x‖

Tactic:
rw [iteratedFDeriv_zero_eq_comp, comp_apply, LinearIsometryEquiv.norm_map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_replicate_of_pos (h : p a) : (replicate n a).filter p = replicate n a

Proof state:
α✝ : Type u_1
p : α✝ → Bool
n : Nat
a : α✝
h : p a = true
⊢ filter p (replicate n a) = replicate n a

Tactic:
simp [filter_replicate, h]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem deleteVerts_adj {u v : V} :
    (G'.deleteVerts s).Adj u v ↔ u ∈ G'.verts ∧ ¬u ∈ s ∧ v ∈ G'.verts ∧ ¬v ∈ s ∧ G'.Adj u v

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set V
u v : V
⊢ (G'.deleteVerts s).Adj u v ↔ u ∈ G'.verts ∧ u ∉ s ∧ v ∈ G'.verts ∧ v ∉ s ∧ G'.Adj u v

Tactic:
simp [and_assoc]

Result:
no goals
-- Mathlib/Computability/EpsilonNFA.lean
theorem εClosure_empty : M.εClosure ∅ = ∅ :=
  eq_empty_of_forall_not_mem fun s hs ↦ by induction hs <;> assumption

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
s : σ
hs : s ∈ M.εClosure ∅
⊢ False

Tactic:
induction hs <;> assumption

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem comp_right_hasFDerivAt_iff' {f : F → G} {x : E} {f' : E →L[𝕜] G} :
    HasFDerivAt (f ∘ iso) f' x ↔ HasFDerivAt f (f'.comp (iso.symm : F →L[𝕜] E)) (iso x)

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 ≃L[𝕜] F
f : F → G
x : E
f' : E →L[𝕜] G
⊢ HasFDerivAt (f ∘ ⇑iso) f' x ↔ HasFDerivAt f (f'.comp ↑iso.symm) (iso x)

Tactic:
simp only [← hasFDerivWithinAt_univ, ← iso.comp_right_hasFDerivWithinAt_iff', preimage_univ]

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_sub [AddGroup α] [StarAddMonoid α] (M N : Matrix m n α) :
    (M - N)ᴴ = Mᴴ - Nᴴ :=
  Matrix.ext <| by simp

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : AddGroup α
inst✝ : StarAddMonoid α
M N : Matrix m n α
⊢ ∀ (i : n) (j : m), (M - N)ᴴ i j = (Mᴴ - Nᴴ) i j

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem equalizer_eq_top {φ ψ : F} : equalizer φ ψ = ⊤ ↔ φ = ψ

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
F : Type u_4
inst✝¹ : FunLike F A B
inst✝ : AlgHomClass F R A B
φ ψ : F
⊢ equalizer φ ψ = ⊤ ↔ φ = ψ

Tactic:
simp [SetLike.ext_iff, DFunLike.ext_iff]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
lemma map_eq_mapOfHomotopy : map φ₁ φ₂ a b comm = mapOfHomotopy (Homotopy.ofEq comm)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K₁ L₁ K₂ L₂ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
⊢ map φ₁ φ₂ a b comm = mapOfHomotopy (Homotopy.ofEq comm)

Tactic:
simp [map, mapOfHomotopy]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_append (f : α → β) (l₁ : Vector α n) (l₂ : Vector α m) :
    map f (l₁ ++ l₂) = map f l₁ ++ map f l₂

Proof state:
case mk
α : Type u_1
β : Type u_2
m : Nat
f : α → β
l₂ : Vector α m
l₁ : Array α
⊢ map f ({ toArray := l₁, size_toArray := ⋯ } ++ l₂) = map f { toArray := l₁, size_toArray := ⋯ } ++ map f l₂

Tactic:
rcases l₂ with ⟨l₂, rfl⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
f : α → β
l₁ l₂ : Array α
⊢ map f ({ toArray := l₁, size_toArray := ⋯ } ++ { toArray := l₂, size_toArray := ⋯ }) =
    map f { toArray := l₁, size_toArray := ⋯ } ++ map f { toArray := l₂, size_toArray := ⋯ }

Proof state:
α : Type u_1
β : Type u_2
n m : Nat
f : α → β
l₁ : Vector α n
l₂ : Vector α m
⊢ map f (l₁ ++ l₂) = map f l₁ ++ map f l₂

Tactic:
rcases l₁ with ⟨l₁, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
m : Nat
f : α → β
l₂ : Vector α m
l₁ : Array α
⊢ map f ({ toArray := l₁, size_toArray := ⋯ } ++ l₂) = map f { toArray := l₁, size_toArray := ⋯ } ++ map f l₂

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
f : α → β
l₁ l₂ : Array α
⊢ map f ({ toArray := l₁, size_toArray := ⋯ } ++ { toArray := l₂, size_toArray := ⋯ }) =
    map f { toArray := l₁, size_toArray := ⋯ } ++ map f { toArray := l₂, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrixAlgEquiv_id : LinearMap.toMatrixAlgEquiv v₁ id = 1

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
⊢ (toMatrixAlgEquiv v₁) id = 1

Tactic:
simp_rw [LinearMap.toMatrixAlgEquiv, AlgEquiv.ofLinearEquiv_apply, LinearMap.toMatrix_id]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
/-- `succAbove` is injective at the pivot -/
lemma succAbove_left_injective : Injective (@succAbove n) := fun _ _ h => by
  simpa [range_succAbove] using congr_arg (fun f : Fin n → Fin (n + 1) => (Set.range f)ᶜ) h

Proof state:
n : ℕ
x✝¹ x✝ : Fin (n + 1)
h : x✝¹.succAbove = x✝.succAbove
⊢ x✝¹ = x✝

Tactic:
simpa [range_succAbove] using congr_arg (fun f : Fin n → Fin (n + 1) => (Set.range f)ᶜ) h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem contains_cons [BEq α] {a : α} {b : α} {l : List α} :
    (a :: l).contains b = (b == a || l.contains b)

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
l : List α
⊢ (a :: l).contains b = (b == a || l.contains b)

Tactic:
simp only [contains, elem_cons]

Result:
α : Type u_1
inst✝ : BEq α
a b : α
l : List α
⊢ (match b == a with
    | true => true
    | false => elem b l) =
    (b == a || elem b l)

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
l : List α
⊢ (match b == a with
    | true => true
    | false => elem b l) =
    (b == a || elem b l)

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/EpiMono.lean
theorem reflects_mono_of_reflectsLimit {X Y : C} (f : X ⟶ Y) [ReflectsLimit (cospan f f) F]
    [Mono (F.map f)] : Mono f

Proof state:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsLimit (cospan f f) F
inst✝ : Mono (F.map f)
⊢ Mono f

Tactic:
have := PullbackCone.isLimitMkIdId (F.map f)

Result:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsLimit (cospan f f) F
inst✝ : Mono (F.map f)
this : IsLimit (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) ⋯)
⊢ Mono f

Proof state:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsLimit (cospan f f) F
inst✝ : Mono (F.map f)
this : IsLimit (PullbackCone.mk (𝟙 (F.obj X)) (𝟙 (F.obj X)) ⋯)
⊢ Mono f

Tactic:
simp_rw [← F.map_id] at this

Result:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsLimit (cospan f f) F
inst✝ : Mono (F.map f)
this : IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) ⋯)
⊢ Mono f

Proof state:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
X Y : C
f : X ⟶ Y
inst✝¹ : ReflectsLimit (cospan f f) F
inst✝ : Mono (F.map f)
this : IsLimit (PullbackCone.mk (F.map (𝟙 X)) (F.map (𝟙 X)) ⋯)
⊢ Mono f

Tactic:
apply PullbackCone.mono_of_isLimitMkIdId _ (isLimitOfIsLimitPullbackConeMap F _ this)

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem limsup_eq_iInf_iSup_of_nat {u : ℕ → α} : limsup u atTop = ⨅ n : ℕ, ⨆ i ≥ n, u i :=
  (atTop_basis.map u).limsSup_eq_iInf_sSup.trans <| by simp only [sSup_image, iInf_const]; rfl

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ ⨅ i, ⨆ a ∈ Ici i, u a = ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), u i

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ ⨅ i, ⨅ (_ : True), sSup (u '' Ici i) = ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), u i

Tactic:
simp only [sSup_image, iInf_const]

Result:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ ⨅ i, ⨆ a ∈ Ici i, u a = ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), u i
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem lintegral_add (f g : α →ₘ[μ] ℝ≥0∞) : lintegral (f + g) = lintegral f + lintegral g :=
  induction_on₂ f g fun f hf g _ => by simp [lintegral_add_left' hf.aemeasurable]

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f✝ g✝ : α →ₘ[μ] ℝ≥0∞
f : α → ℝ≥0∞
hf : AEStronglyMeasurable f μ
g : α → ℝ≥0∞
x✝ : AEStronglyMeasurable g μ
⊢ (mk f hf + mk g x✝).lintegral = (mk f hf).lintegral + (mk g x✝).lintegral

Tactic:
simp [lintegral_add_left' hf.aemeasurable]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem condExpIndL1_of_measurableSet_of_measure_ne_top (hs : MeasurableSet s) (hμs : μ s ≠ ∞)
    (x : G) : condExpIndL1 hm μ s x = condExpIndL1Fin hm hs hμs x

Proof state:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
⊢ condExpIndL1 hm μ s x = condExpIndL1Fin hm hs hμs x

Tactic:
simp only [condExpIndL1, And.intro hs hμs, dif_pos, Ne, not_false_iff, and_self_iff]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma toENat_lt_top {a : Cardinal} : toENat a < ⊤ ↔ a < ℵ₀

Proof state:
a : Cardinal.{u_1}
⊢ toENat a < ⊤ ↔ a < ℵ₀

Tactic:
simp [lt_top_iff_ne_top]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem add_neg_mul_emod_self_left {a b c : Int} : (a + -(b * c)) % b = a % b

Proof state:
a b c : Int
⊢ (a + -(b * c)) % b = a % b

Tactic:
rw [Int.neg_mul_eq_mul_neg, add_mul_emod_self_left]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Subsheaf.lean
theorem Subpresheaf.le_sheafify : G ≤ G.sheafify J

Proof state:
case h.e'_5
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
V : C
i : V ⟶ unop U
⊢ (G.sieveOfSection s).arrows i

Tactic:
exact G.map i.op hs

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
⊢ G.sieveOfSection s ∈ J (unop U)

Tactic:
convert J.top_mem U.unop

Result:
case h.e'_5
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
⊢ G.sieveOfSection s = ⊤

Proof state:
case h.e'_5
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
⊢ G.sieveOfSection s = ⊤

Tactic:
rw [eq_top_iff]

Result:
case h.e'_5
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
⊢ ⊤ ≤ G.sieveOfSection s

Proof state:
case h.e'_5
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
⊢ ⊤ ≤ G.sieveOfSection s

Tactic:
rintro V i -

Result:
case h.e'_5
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
V : C
i : V ⟶ unop U
⊢ (G.sieveOfSection s).arrows i

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
⊢ G ≤ sheafify J G

Tactic:
intro U s hs

Result:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
⊢ s ∈ (sheafify J G).obj U

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
⊢ s ∈ (sheafify J G).obj U

Tactic:
change _ ∈ J _

Result:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
U : Cᵒᵖ
s : F.obj U
hs : s ∈ G.obj U
⊢ G.sieveOfSection s ∈ J (unop U)
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem dFrom_comp_xNextIsoSelf {i : ι} (h : ¬c.Rel i (c.next i)) :
    C.dFrom i ≫ (C.xNextIsoSelf h).hom = 0

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i : ι
h : ¬c.Rel i (c.next i)
⊢ C.dFrom i ≫ (C.xNextIsoSelf h).hom = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem integrable_finset_sum {ι} (s : Finset ι) {f : ι → α → β}
    (hf : ∀ i ∈ s, Integrable (f i) μ) : Integrable (fun a => ∑ i ∈ s, f i a) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
ι : Type u_6
s : Finset ι
f : ι → α → β
hf : ∀ i ∈ s, Integrable (f i) μ
⊢ Integrable (fun a => ∑ i ∈ s, f i a) μ

Tactic:
simpa only [← Finset.sum_apply] using integrable_finset_sum' s hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem mem_bind_iff {o : Option α} {f : α → Option β} :
    b ∈ o.bind f ↔ ∃ a, a ∈ o ∧ b ∈ f a

Proof state:
α : Type u_1
β : Type u_2
b : β
o : Option α
f : α → Option β
⊢ b ∈ o.bind f ↔ ∃ a, a ∈ o ∧ b ∈ f a

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma Hom.le_ker_comp (f : X ⟶ Y) (g : Y.Hom Z) : g.ker ≤ (f ≫ g).ker

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y.Hom Z
⊢ g.ker ≤ ker (f ≫ g)

Tactic:
refine ofIdeals_mono fun U ↦ ?_

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y.Hom Z
U : ↑Z.affineOpens
⊢ RingHom.ker (CommRingCat.Hom.hom (g.app ↑U)) ≤ RingHom.ker (CommRingCat.Hom.hom (app (f ≫ g) ↑U))

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y.Hom Z
U : ↑Z.affineOpens
⊢ RingHom.ker (CommRingCat.Hom.hom (g.app ↑U)) ≤
    Ideal.comap (CommRingCat.Hom.hom (g.app ↑U)) (RingHom.ker (CommRingCat.Hom.hom (app f (g ⁻¹ᵁ ↑U))))

Tactic:
exact Ideal.ker_le_comap _

Result:
no goals

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y.Hom Z
U : ↑Z.affineOpens
⊢ RingHom.ker (CommRingCat.Hom.hom (g.app ↑U)) ≤ RingHom.ker (CommRingCat.Hom.hom (app (f ≫ g) ↑U))

Tactic:
rw [Scheme.comp_app f g U, CommRingCat.hom_comp, ← RingHom.comap_ker]

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y.Hom Z
U : ↑Z.affineOpens
⊢ RingHom.ker (CommRingCat.Hom.hom (g.app ↑U)) ≤
    Ideal.comap (CommRingCat.Hom.hom (g.app ↑U)) (RingHom.ker (CommRingCat.Hom.hom (app f (g ⁻¹ᵁ ↑U))))
-- Mathlib/Data/Nat/MaxPowDiv.lean
theorem zero {p : ℕ} : maxPowDiv p 0 = 0

Proof state:
p : ℕ
⊢ p.maxPowDiv 0 = 0

Tactic:
dsimp [maxPowDiv]

Result:
p : ℕ
⊢ go 0 p 0 = 0

Proof state:
p : ℕ
⊢ go 0 p 0 = 0

Tactic:
rw [maxPowDiv.go]

Result:
p : ℕ
⊢ (if 1 < p ∧ 0 < 0 ∧ 0 % p = 0 then go (0 + 1) p (0 / p) else 0) = 0

Proof state:
p : ℕ
⊢ (if 1 < p ∧ 0 < 0 ∧ 0 % p = 0 then go (0 + 1) p (0 / p) else 0) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_eq_get!_get? [LawfulBEq α] (h : m.WF) {a : α} [Inhabited (β a)] :
    m.get! a = (m.get? a).get!

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
a : α
inst✝ : Inhabited (β a)
⊢ m.get! a = (m.get? a).get!

Tactic:
simp_to_raw using Raw₀.get!_eq_get!_get?

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma negAddY_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2) : W.negAddY P Q / addZ P Q ^ 3 =
      W.toAffine.negAddY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
        (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ W.negAddY P Q / addZ P Q ^ 3 =
    (toAffine W).negAddY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
      ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3))

Tactic:
rw [negAddY_eq hPz hQz, addX_eq' hP hQ, toAffine_slope_of_ne hPz hQz hx,
  toAffine_negAddY_of_ne hPz hQz <| addZ_ne_zero_of_X_ne hx]

Result:
no goals