harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
@[simp]
lemma negPart_algebraMap (r : ℝ) : (algebraMap ℝ A r)⁻ = algebraMap ℝ A r⁻

Proof state:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : T2Space A
r : ℝ
⊢ ((algebraMap ℝ A) r)⁻ = (algebraMap ℝ A) r⁻

Tactic:
rw [CFC.negPart_def, cfcₙ_eq_cfc]

Result:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : T2Space A
r : ℝ
⊢ cfc (fun x => x⁻) ((algebraMap ℝ A) r) = (algebraMap ℝ A) r⁻

Proof state:
A : Type u_1
inst✝⁵ : Ring A
inst✝⁴ : Algebra ℝ A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : ContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : T2Space A
r : ℝ
⊢ cfc (fun x => x⁻) ((algebraMap ℝ A) r) = (algebraMap ℝ A) r⁻

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean
theorem Filter.Tendsto.rpow_const {l : Filter α} {f : α → ℝ} {x p : ℝ} (hf : Tendsto f l (𝓝 x))
    (h : x ≠ 0 ∨ 0 ≤ p) : Tendsto (fun a => f a ^ p) l (𝓝 (x ^ p)) :=
  if h0 : 0 = p then h0 ▸ by simp [tendsto_const_nhds]
  else hf.rpow tendsto_const_nhds (h.imp id fun h' => h'.lt_of_ne h0)

Proof state:
α : Type u_1
l : Filter α
f : α → ℝ
x p : ℝ
hf : Tendsto f l (𝓝 x)
h : x ≠ 0 ∨ 0 ≤ p
h0 : 0 = p
⊢ Tendsto (fun a => f a ^ 0) l (𝓝 (x ^ 0))

Tactic:
simp [tendsto_const_nhds]

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem exists_pos_right_iff_sameRay (hx : x ≠ 0) (hy : y ≠ 0) :
    (∃ r : R, 0 < r ∧ x = r • y) ↔ SameRay R x y

Proof state:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R x y

Tactic:
rw [SameRay.sameRay_comm]

Result:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R y x

Proof state:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ x = r • y) ↔ SameRay R y x

Tactic:
simp_rw [eq_comm (a := x)]

Result:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ r • y = x) ↔ SameRay R y x

Proof state:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hy : y ≠ 0
⊢ (∃ r, 0 < r ∧ r • y = x) ↔ SameRay R y x

Tactic:
exact exists_pos_left_iff_sameRay hy hx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem add_max_add_left (a b c : Nat) : max (a + b) (a + c) = a + max b c

Proof state:
a b c : Nat
⊢ max (a + b) (a + c) = a + max b c

Tactic:
repeat rw [Nat.add_comm a]

Result:
a b c : Nat
⊢ max (b + a) (c + a) = max b c + a

Proof state:
a b c : Nat
⊢ max (b + a) (c + a) = max b c + a

Tactic:
exact Nat.add_max_add_right ..

Result:
no goals

Proof state:
a b c : Nat
⊢ max (b + a) (c + a) = a + max b c

Tactic:
rw [Nat.add_comm a]

Result:
a b c : Nat
⊢ max (b + a) (c + a) = max b c + a
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
theorem spanExt_app_left : (spanExt iX iY iZ wf wg).app WalkingSpan.left = iY

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Y
g : X ⟶ Z
f' : X' ⟶ Y'
g' : X' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iY.hom
wg : iX.hom ≫ g' = g ≫ iZ.hom
⊢ (spanExt iX iY iZ wf wg).app WalkingSpan.left = iY

Tactic:
dsimp [spanExt]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem Equiv.tprod_eq (e : γ ≃ β) (f : β → α) : ∏' c, f (e c) = ∏' b, f b :=
  e.injective.tprod_eq <| by simp

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
e : γ ≃ β
f : β → α
⊢ mulSupport f ⊆ Set.range ⇑e

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/FreeAlgebra/Cardinality.lean
theorem cardinalMk_eq_one [Subsingleton R] : #(FreeAlgebra R X) = 1

Proof state:
R : Type u
inst✝¹ : CommSemiring R
X : Type v
inst✝ : Subsingleton R
⊢ #(FreeAlgebra R X) = 1

Tactic:
rw [equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq, MonoidAlgebra, mk_eq_one]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem of_to_int (n : ZNum) : ((n : ℤ) : ZNum) = n

Proof state:
n : ZNum
⊢ ↑↑n = n

Tactic:
rw [← ofInt'_eq, of_to_int']

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueFree_compl : Gᶜ.CliqueFree n ↔ G.IndepSetFree n

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ Gᶜ.CliqueFree n ↔ G.IndepSetFree n

Tactic:
simp [IndepSetFree, CliqueFree]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem head!_eq_head? [Inhabited α] (l : List α) : head! l = (head? l).iget

Proof state:
α : Type u
inst✝ : Inhabited α
l : List α
⊢ l.head! = l.head?.iget

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Topology/Separation/Hausdorff.lean
theorem isIrreducible_iff_singleton [T2Space X] {S : Set X} : IsIrreducible S ↔ ∃ x, S = {x}

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
S : Set X
⊢ IsIrreducible S ↔ ∃ x, S = {x}

Tactic:
rw [IsIrreducible, isPreirreducible_iff_subsingleton,
  exists_eq_singleton_iff_nonempty_subsingleton]

Result:
no goals
-- Mathlib/Algebra/Lie/Basic.lean
theorem map_lie₂ (f : M →ₗ⁅R,L⁆ N →ₗ[R] P) (x : L) (m : M) (n : N) :
    ⁅x, f m n⁆ = f ⁅x, m⁆ n + f m ⁅x, n⁆

Proof state:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : AddCommGroup N
inst✝⁹ : AddCommGroup P
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieRingModule L N
inst✝³ : LieRingModule L P
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L N
inst✝ : LieModule R L P
f : M →ₗ⁅R,L⁆ N →ₗ[R] P
x : L
m : M
n : N
⊢ ⁅x, (f m) n⁆ = (f ⁅x, m⁆) n + (f m) ⁅x, n⁆

Tactic:
simp only [sub_add_cancel, map_lie, LieHom.lie_apply]

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean
theorem IsTranscendenceBasis.isEmpty_iff_isAlgebraic [Nontrivial R]
    (hx : IsTranscendenceBasis R x) :
    IsEmpty ι ↔ Algebra.IsAlgebraic R A

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
x✝ : IsEmpty ι
this : Algebra.IsAlgebraic (↥⊥) A
⊢ Algebra.IsAlgebraic R A

Tactic:
exact algebra_isAlgebraic_of_algebra_isAlgebraic_bot_left R A

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
⊢ IsEmpty ι ↔ Algebra.IsAlgebraic R A

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ hx.1.isEmpty_of_isAlgebraic⟩

Result:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
x✝ : IsEmpty ι
⊢ Algebra.IsAlgebraic R A

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
x✝ : IsEmpty ι
⊢ Algebra.IsAlgebraic R A

Tactic:
have := hx.isAlgebraic

Result:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
x✝ : IsEmpty ι
this : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
⊢ Algebra.IsAlgebraic R A

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
x✝ : IsEmpty ι
this : Algebra.IsAlgebraic (↥(adjoin R (range x))) A
⊢ Algebra.IsAlgebraic R A

Tactic:
rw [Set.range_eq_empty x, adjoin_empty] at this

Result:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
hx : IsTranscendenceBasis R x
x✝ : IsEmpty ι
this : Algebra.IsAlgebraic (↥⊥) A
⊢ Algebra.IsAlgebraic R A
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem intCast_val (n : ℤ) : (n : ℤ√d) = ⟨n, 0⟩

Proof state:
d n : ℤ
⊢ ↑n = { re := n, im := 0 }

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_ne {x y : BitVec n} : x.toInt ≠ y.toInt ↔ x ≠ y

Proof state:
n : Nat
x y : BitVec n
⊢ x.toInt ≠ y.toInt ↔ x ≠ y

Tactic:
rw [Ne, toInt_inj]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
/-- Variant of `of_isColimit` for an arbitrary cocone on a diagram `WalkingSpan ⥤ C`. -/
lemma of_isColimit_cocone {D : WalkingSpan ⥤ C} {c : Cocone D} (hc : IsColimit c) :
    IsPushout (D.map WalkingSpan.Hom.fst) (D.map WalkingSpan.Hom.snd)
      (c.ι.app .left) (c.ι.app .right) where
  w

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
D : WalkingSpan ⥤ C
c : Cocone D
hc : IsColimit c
⊢ D.map WalkingSpan.Hom.fst ≫ c.ι.app WalkingSpan.left = D.map WalkingSpan.Hom.snd ≫ c.ι.app WalkingSpan.right

Tactic:
simp_rw [Cocone.w]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem AffineEquiv.pointReflection_midpoint_left (x y : P) :
    pointReflection R (midpoint R x y) x = y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : Invertible 2
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ (pointReflection R (midpoint R x y)) x = y

Tactic:
rw [midpoint, pointReflection_apply, lineMap_apply, vadd_vsub, vadd_vadd, ← add_smul, ← two_mul,
  mul_invOf_self, one_smul, vsub_vadd]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
theorem prodComparison_inv_natural_whiskerLeft (g : B ⟶ B') [IsIso (prodComparison F A B')] :
    inv (prodComparison F A B) ≫ F.map (A ◁ g) =
      (F.obj A ◁ F.map g) ≫ inv (prodComparison F A B')

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ChosenFiniteProducts C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : ChosenFiniteProducts D
F : C ⥤ D
A B B' : C
inst✝¹ : IsIso (prodComparison F A B)
g : B ⟶ B'
inst✝ : IsIso (prodComparison F A B')
⊢ inv (prodComparison F A B) ≫ F.map (A ◁ g) = F.obj A ◁ F.map g ≫ inv (prodComparison F A B')

Tactic:
rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural_whiskerLeft]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma setLIntegral_condKernel_univ_left (hf : Measurable f) (a : α) {t : Set Ω}
    (ht : MeasurableSet t) :
    ∫⁻ b, ∫⁻ ω in t, f (b, ω) ∂(Kernel.condKernel κ (a, b)) ∂(Kernel.fst κ a)
      = ∫⁻ x in Set.univ ×ˢ t, f x ∂(κ a)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω) in Set.univ ×ˢ t, f x ∂κ a

Tactic:
rw [← setLIntegral_condKernel hf a MeasurableSet.univ ht]

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
    ∫⁻ (b : β) in Set.univ, ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
f : β × Ω → ℝ≥0∞
hf : Measurable f
a : α
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a =
    ∫⁻ (b : β) in Set.univ, ∫⁻ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a

Tactic:
simp_rw [Measure.restrict_univ]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem cthickening_thickening (hε : 0 ≤ ε) (hδ : 0 < δ) (s : Set E) :
    cthickening ε (thickening δ s) = cthickening (ε + δ) s :=
  (cthickening_thickening_subset hε _ _).antisymm fun x => by
    simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ.le, infEdist_thickening hδ]
    exact tsub_le_iff_right.2

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
s : Set E
x : E
⊢ infEdist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEdist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε

Tactic:
exact tsub_le_iff_right.2

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
s : Set E
x : E
⊢ x ∈ cthickening (ε + δ) s → x ∈ cthickening ε (thickening δ s)

Tactic:
simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ.le, infEdist_thickening hδ]

Result:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
s : Set E
x : E
⊢ infEdist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEdist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε
-- Mathlib/FieldTheory/Laurent.lean
theorem laurent_at_zero : laurent 0 f = f

Proof state:
R : Type u
inst✝¹ : CommRing R
f : RatFunc R
inst✝ : IsDomain R
⊢ (laurent 0) f = f

Tactic:
induction f using RatFunc.induction_on

Result:
case f
R : Type u
inst✝¹ : CommRing R
f : RatFunc R
inst✝ : IsDomain R
p✝ q✝ : R[X]
x✝ : q✝ ≠ 0
⊢ (laurent 0) ((algebraMap R[X] (RatFunc R)) p✝ / (algebraMap R[X] (RatFunc R)) q✝) =
    (algebraMap R[X] (RatFunc R)) p✝ / (algebraMap R[X] (RatFunc R)) q✝

Proof state:
case f
R : Type u
inst✝¹ : CommRing R
f : RatFunc R
inst✝ : IsDomain R
p✝ q✝ : R[X]
x✝ : q✝ ≠ 0
⊢ (laurent 0) ((algebraMap R[X] (RatFunc R)) p✝ / (algebraMap R[X] (RatFunc R)) q✝) =
    (algebraMap R[X] (RatFunc R)) p✝ / (algebraMap R[X] (RatFunc R)) q✝

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Hom/Basic.lean
theorem le_map_inv_iff (f : F) {a : α} {b : β} : a ≤ EquivLike.inv f b ↔ f a ≤ b

Proof state:
case h.e'_2.h.e'_4
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ b = f (EquivLike.inv f b)

Tactic:
exact (EquivLike.right_inv _ _).symm

Result:
no goals

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ a ≤ EquivLike.inv f b ↔ f a ≤ b

Tactic:
convert (map_le_map_iff f (a := a) (b := EquivLike.inv f b)).symm

Result:
case h.e'_2.h.e'_4
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ b = f (EquivLike.inv f b)
-- Mathlib/Data/ENat/Lattice.lean
lemma add_biSup' {p : ι → Prop} (h : ∃ i, p i) (f : ι → ℕ∞) :
    a + ⨆ i, ⨆ _ : p i, f i = ⨆ i, ⨆ _ : p i, a + f i

Proof state:
ι : Sort u_2
a : ℕ∞
p : ι → Prop
h : ∃ i, p i
f : ι → ℕ∞
this : Nonempty { i // p i }
⊢ a + ⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), a + f i

Tactic:
simp only [iSup_subtype', add_iSup]

Result:
no goals

Proof state:
ι : Sort u_2
a : ℕ∞
p : ι → Prop
h : ∃ i, p i
f : ι → ℕ∞
⊢ a + ⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), a + f i

Tactic:
haveI : Nonempty {i // p i} := nonempty_subtype.2 h

Result:
ι : Sort u_2
a : ℕ∞
p : ι → Prop
h : ∃ i, p i
f : ι → ℕ∞
this : Nonempty { i // p i }
⊢ a + ⨆ i, ⨆ (_ : p i), f i = ⨆ i, ⨆ (_ : p i), a + f i
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem image_ι_comp_eq_zero {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [HasImage f]
    [Epi (factorThruImage f)] (h : f ≫ g = 0) : image.ι f ≫ g = 0 :=
  zero_of_epi_comp (factorThruImage f) <| by simp [h]

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasImage f
inst✝ : Epi (factorThruImage f)
h : f ≫ g = 0
⊢ factorThruImage f ≫ image.ι f ≫ g = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem _root_.ProbabilityMeasure.toFiniteMeasure_normalize_eq_self {m0 : MeasurableSpace Ω}
    (μ : ProbabilityMeasure Ω) : μ.toFiniteMeasure.normalize = μ

Proof state:
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s : Set Ω
_s_mble : MeasurableSet s
⊢ μ.toFiniteMeasure.normalize s = μ s

Tactic:
rw [μ.toFiniteMeasure.normalize_eq_of_nonzero μ.toFiniteMeasure_nonzero s]

Result:
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s : Set Ω
_s_mble : MeasurableSet s
⊢ μ.toFiniteMeasure.mass⁻¹ * μ.toFiniteMeasure s = μ s

Proof state:
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ μ.toFiniteMeasure.normalize = μ

Tactic:
apply ProbabilityMeasure.eq_of_forall_apply_eq

Result:
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ ∀ (s : Set Ω), MeasurableSet s → μ.toFiniteMeasure.normalize s = μ s

Proof state:
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
⊢ ∀ (s : Set Ω), MeasurableSet s → μ.toFiniteMeasure.normalize s = μ s

Tactic:
intro s _s_mble

Result:
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s : Set Ω
_s_mble : MeasurableSet s
⊢ μ.toFiniteMeasure.normalize s = μ s

Proof state:
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : ProbabilityMeasure Ω
s : Set Ω
_s_mble : MeasurableSet s
⊢ μ.toFiniteMeasure.mass⁻¹ * μ.toFiniteMeasure s = μ s

Tactic:
simp only [ProbabilityMeasure.mass_toFiniteMeasure, inv_one, one_mul, μ.coeFn_toFiniteMeasure]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma IsUnramified.stabilizer_eq_bot (h : IsUnramified k w) : Stab w = ⊥

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
⊢ ∀ (a : K ≃ₐ[k] K), ComplexEmbedding.IsConj w.embedding a → a = 1

Tactic:
exact fun σ hσ ↦ hσ.isUnramified_mk_iff.mp ((mk_embedding w).symm ▸ h)

Result:
no goals

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
⊢ Stab w = ⊥

Tactic:
rw [eq_bot_iff, ← mk_embedding w, SetLike.le_def]

Result:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
⊢ ∀ ⦃x : K ≃ₐ[k] K⦄, x ∈ Stab (mk w.embedding) → x ∈ ⊥

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
⊢ ∀ ⦃x : K ≃ₐ[k] K⦄, x ∈ Stab (mk w.embedding) → x ∈ ⊥

Tactic:
simp only [mem_stabilizer_mk_iff, Subgroup.mem_bot, forall_eq_or_imp, true_and]

Result:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
⊢ ∀ (a : K ≃ₐ[k] K), ComplexEmbedding.IsConj w.embedding a → a = 1
-- Mathlib/Order/UpperLower/Basic.lean
theorem disjoint_coe : Disjoint (s : Set α) t ↔ Disjoint s t

Proof state:
α : Type u_1
inst✝ : LE α
s t : LowerSet α
⊢ Disjoint ↑s ↑t ↔ Disjoint s t

Tactic:
simp [disjoint_iff, SetLike.ext'_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/CurryingThree.lean
@[simp]
lemma currying₃_unitIso_hom_app_app_app_app (F : C₁ ⥤ C₂ ⥤ C₃ ⥤ E)
    (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) :
    (((currying₃.unitIso.hom.app F).app X₁).app X₂).app X₃ = 𝟙 _

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_4
E : Type u_9
inst✝³ : Category.{u_10, u_1} C₁
inst✝² : Category.{u_13, u_2} C₂
inst✝¹ : Category.{u_12, u_4} C₃
inst✝ : Category.{u_11, u_9} E
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
X₁ : C₁
X₂ : C₂
X₃ : C₃
⊢ (((currying₃.unitIso.hom.app F).app X₁).app X₂).app X₃ = 𝟙 (((((𝟭 (C₁ ⥤ C₂ ⥤ C₃ ⥤ E)).obj F).obj X₁).obj X₂).obj X₃)

Tactic:
simp [currying₃, Equivalence.unit]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem lift_relrank_comap_comap_eq_lift_relrank_of_le (f : L →ₐ[F] E) (h : B ≤ f.fieldRange) :
    Cardinal.lift.{v} (relrank (A.comap f) (B.comap f)) = Cardinal.lift.{w} (relrank A B)

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
L : Type w
inst✝¹ : Field L
inst✝ : Algebra F L
A B : IntermediateField F E
f : L →ₐ[F] E
h : B ≤ f.fieldRange
⊢ Cardinal.lift.{v, w} ((comap f A).relrank (comap f B)) = Cardinal.lift.{w, v} (A.relrank B)

Tactic:
simpa only [inf_of_le_left h] using lift_relrank_comap_comap_eq_lift_relrank_inf A B f

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem lt_inv_iff_lt_inv : a < b⁻¹ ↔ b < a⁻¹

Proof state:
a b : ℝ≥0∞
⊢ a < b⁻¹ ↔ b < a⁻¹

Tactic:
simpa only [inv_inv] using @ENNReal.inv_lt_inv a⁻¹ b

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem iSup_eq_bsup {o} {f : ∀ a < o, Ordinal} : ⨆ a : Iio o, f a.1 a.2 = bsup o f

Proof state:
o : Ordinal.{u_4}
f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_5 u_4}
⊢ ⨆ a, f ↑a ⋯ = o.bsup f

Tactic:
simp_rw [Iio, bsup, sup, iSup, range_familyOfBFamily, brange, range, Subtype.exists, mem_setOf]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Rank.lean
theorem rank_empty : rank ∅ = 0

Proof state:
⊢ ∅.rank = 0

Tactic:
simp [empty_def, rank]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem neg_mul (M : Matrix m n α) (N : Matrix n o α) : (-M) * N = -(M * N)

Proof state:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n o α
i✝ : m
j✝ : o
⊢ (-M * N) i✝ j✝ = (-(M * N)) i✝ j✝

Tactic:
apply neg_dotProduct

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n o α
⊢ -M * N = -(M * N)

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n o α
i✝ : m
j✝ : o
⊢ (-M * N) i✝ j✝ = (-(M * N)) i✝ j✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_mk (a : Array α) (h : a.size = n) (f : α → β) :
    (Vector.mk a h).map f = Vector.mk (a.map f) (by simp [h]) := rfl

Proof state:
α : Type ?u.10588
n : Nat
β : Type ?u.10612
a : Array α
h : a.size = n
f : α → β
⊢ (Array.map f a).size = n

Tactic:
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem tailD_eq_tail? (l l' : List α) : tailD l l' = (tail? l).getD l'

Proof state:
α : Type u_1
l l' : List α
⊢ l.tailD l' = l.tail?.getD l'

Tactic:
cases l <;> rfl

Result:
no goals