harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk'_neg {M M' : Type*} [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M']
    (f : M →ₗ[R] M') [IsLocalizedModule S f] (m : M) (s : S) : mk' f (-m) s = -mk' f m s

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ mk' f (-m) s = -mk' f m s

Tactic:
delta mk'

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk (-m) s) = -(fromLocalizedModule S f) (LocalizedModule.mk m s)

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m : M
s : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk (-m) s) = -(fromLocalizedModule S f) (LocalizedModule.mk m s)

Tactic:
rw [LocalizedModule.mk_neg, map_neg]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem affineSpan_eq_bot : affineSpan k s = ⊥ ↔ s = ∅

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ affineSpan k s = ⊥ ↔ s = ∅

Tactic:
rw [← not_iff_not, ← Ne, ← Ne, ← nonempty_iff_ne_bot, affineSpan_nonempty,
  nonempty_iff_ne_empty]

Result:
no goals
-- Mathlib/RingTheory/LinearDisjoint.lean
theorem exists_field_of_isDomain_of_injective (A : Type v) [CommRing A] (B : Type w) [CommRing B]
    [Algebra R A] [Algebra R B] [Module.Flat R A] [Module.Flat R B] [IsDomain (A ⊗[R] B)]
    (ha : Function.Injective (algebraMap R A)) (hb : Function.Injective (algebraMap R B)) :
    ∃ (K : Type (max v w)) (_ : Field K) (_ : Algebra R K) (fa : A →ₐ[R] K) (fb : B →ₐ[R] K),
    Function.Injective fa ∧ Function.Injective fb ∧ fa.range.LinearDisjoint fb.range :=
  let K := FractionRing (A ⊗[R] B)
  let i := IsScalarTower.toAlgHom R (A ⊗[R] B) K
  have hi : Function.Injective i := IsFractionRing.injective (A ⊗[R] B) K
  ⟨K, inferInstance, inferInstance,
    i.comp Algebra.TensorProduct.includeLeft,
    i.comp Algebra.TensorProduct.includeRight,
    hi.comp (Algebra.TensorProduct.includeLeft_injective hb),
    hi.comp (Algebra.TensorProduct.includeRight_injective ha), by
      simpa only [AlgHom.range_comp] using (include_range R A B).map i hi⟩

Proof state:
R : Type u
inst✝⁷ : CommRing R
A : Type v
inst✝⁶ : CommRing A
B : Type w
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Module.Flat R A
inst✝¹ : Module.Flat R B
inst✝ : IsDomain (A ⊗[R] B)
ha : Function.Injective ⇑(algebraMap R A)
hb : Function.Injective ⇑(algebraMap R B)
K : Type (max w v) := FractionRing (A ⊗[R] B)
i : A ⊗[R] B →ₐ[R] K := IsScalarTower.toAlgHom R (A ⊗[R] B) K
hi : Function.Injective ⇑i
⊢ (i.comp Algebra.TensorProduct.includeLeft).range.LinearDisjoint (i.comp Algebra.TensorProduct.includeRight).range

Tactic:
simpa only [AlgHom.range_comp] using (include_range R A B).map i hi

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem isOpen_sUnion_countable [SecondCountableTopology α] (S : Set (Set α))
    (H : ∀ s ∈ S, IsOpen s) : ∃ T : Set (Set α), T.Countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S

Proof state:
α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
S : Set (Set α)
H : ∀ s ∈ S, IsOpen s
⊢ ∃ T, T.Countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S

Tactic:
simpa only [and_left_comm, sUnion_eq_biUnion] using isOpen_biUnion_countable S id H

Result:
no goals
-- Mathlib/Data/List/Sym.lean
theorem mem_sym2_iff {xs : List α} {z : Sym2 α} :
    z ∈ xs.sym2 ↔ ∀ y ∈ z, y ∈ xs

Proof state:
α : Type u_1
xs : List α
z : Sym2 α
a b : α
⊢ s(a, b) ∈ xs.sym2 ↔ ∀ y ∈ s(a, b), y ∈ xs

Tactic:
simp [mk_mem_sym2_iff]

Result:
no goals

Proof state:
α : Type u_1
xs : List α
z : Sym2 α
⊢ z ∈ xs.sym2 ↔ ∀ y ∈ z, y ∈ xs

Tactic:
refine z.ind (fun a b => ?_)

Result:
α : Type u_1
xs : List α
z : Sym2 α
a b : α
⊢ s(a, b) ∈ xs.sym2 ↔ ∀ y ∈ s(a, b), y ∈ xs
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Products.lean
/-- If `pi_comparison G f` is an isomorphism, then `G` preserves the limit of `f`. -/
lemma PreservesProduct.of_iso_comparison [i : IsIso (piComparison G f)] :
    PreservesLimit (Discrete.functor f) G

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun j => G.obj (f j)
i : IsIso (piComparison G f)
⊢ PreservesLimit (Discrete.functor f) G

Tactic:
apply preservesLimit_of_preserves_limit_cone (productIsProduct f)

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun j => G.obj (f j)
i : IsIso (piComparison G f)
⊢ IsLimit (G.mapCone (Fan.mk (∏ᶜ f) (Pi.π f)))

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun j => G.obj (f j)
i : IsIso (piComparison G f)
⊢ IsLimit (Fan.mk (G.obj (∏ᶜ f)) fun j => G.map (Pi.π f j))

Tactic:
exact @IsLimit.ofPointIso _ _ _ _ _ _ _
  (limit.isLimit (Discrete.functor fun j : J => G.obj (f j))) i

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun j => G.obj (f j)
i : IsIso (piComparison G f)
⊢ IsLimit (G.mapCone (Fan.mk (∏ᶜ f) (Pi.π f)))

Tactic:
apply (isLimitMapConeFanMkEquiv _ _ _).symm _

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun j => G.obj (f j)
i : IsIso (piComparison G f)
⊢ IsLimit (Fan.mk (G.obj (∏ᶜ f)) fun j => G.map (Pi.π f j))
-- Mathlib/Data/Finset/Union.lean
theorem biUnion_image [DecidableEq γ] {s : Finset α} {t : α → Finset β} {f : β → γ} :
    (s.biUnion t).image f = s.biUnion fun a => (t a).image f :=
  haveI := Classical.decEq α
  Finset.induction_on s rfl fun a s _ ih => by simp only [biUnion_insert, image_union, ih]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
s✝ : Finset α
t : α → Finset β
f : β → γ
this : DecidableEq α
a : α
s : Finset α
x✝ : a ∉ s
ih : image f (s.biUnion t) = s.biUnion fun a => image f (t a)
⊢ image f ((insert a s).biUnion t) = (insert a s).biUnion fun a => image f (t a)

Tactic:
simp only [biUnion_insert, image_union, ih]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/Basic.lean
@[simp] lemma image_add_left_Icc (a b c : α) : (Icc a b).image (c + ·) = Icc (c + a) (c + b)

Proof state:
α : Type u_2
inst✝³ : OrderedCancelAddCommMonoid α
inst✝² : ExistsAddOfLE α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b c : α
⊢ image (fun x => c + x) (Icc a b) = Icc (c + a) (c + b)

Tactic:
rw [← map_add_left_Icc, map_eq_image, addLeftEmbedding, Embedding.coeFn_mk]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mul_mod_right (m n : Nat) : (m * n) % m = 0

Proof state:
m n : Nat
⊢ m * n % m = 0

Tactic:
rw [← Nat.zero_add (m * n), add_mul_mod_self_left, zero_mod]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem image_circleMap_Ioc (c : ℂ) (R : ℝ) : circleMap c R '' Ioc 0 (2 * π) = sphere c |R|

Proof state:
c : ℂ
R : ℝ
⊢ circleMap c R '' Ioc 0 (2 * π) = sphere c |R|

Tactic:
rw [← range_circleMap, ← (periodic_circleMap c R).image_Ioc Real.two_pi_pos 0, zero_add]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem isNormal_iff_lt_succ_and_blsub_eq {f : Ordinal.{u} → Ordinal.{max u v}} :
    IsNormal f ↔ (∀ a, f a < f (succ a)) ∧
      ∀ o, IsLimit o → (blsub.{_, v} o fun x _ => f x) = f o

Proof state:
f : Ordinal.{u} → Ordinal.{max u v}
⊢ (∀ (a : Ordinal.{u}), f a < f (succ a)) →
    ((∀ (o : Ordinal.{u}), o.IsLimit → (o.bsup fun x x_1 => f x) = f o) ↔
      ∀ (o : Ordinal.{u}), o.IsLimit → (o.blsub fun x x_1 => f x) = f o)

Tactic:
intro h

Result:
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
⊢ (∀ (o : Ordinal.{u}), o.IsLimit → (o.bsup fun x x_1 => f x) = f o) ↔
    ∀ (o : Ordinal.{u}), o.IsLimit → (o.blsub fun x x_1 => f x) = f o

Proof state:
f : Ordinal.{u} → Ordinal.{max u v}
h : ∀ (a : Ordinal.{u}), f a < f (succ a)
⊢ (∀ (o : Ordinal.{u}), o.IsLimit → (o.bsup fun x x_1 => f x) = f o) ↔
    ∀ (o : Ordinal.{u}), o.IsLimit → (o.blsub fun x x_1 => f x) = f o

Tactic:
constructor <;> intro H o ho <;> have := H o ho <;>
  rwa [← bsup_eq_blsub_of_lt_succ_limit ho fun a _ => h a] at *

Result:
no goals

Proof state:
f : Ordinal.{u} → Ordinal.{max u v}
⊢ IsNormal f ↔
    (∀ (a : Ordinal.{u}), f a < f (succ a)) ∧ ∀ (o : Ordinal.{u}), o.IsLimit → (o.blsub fun x x_1 => f x) = f o

Tactic:
rw [isNormal_iff_lt_succ_and_bsup_eq.{u, v}, and_congr_right_iff]

Result:
f : Ordinal.{u} → Ordinal.{max u v}
⊢ (∀ (a : Ordinal.{u}), f a < f (succ a)) →
    ((∀ (o : Ordinal.{u}), o.IsLimit → (o.bsup fun x x_1 => f x) = f o) ↔
      ∀ (o : Ordinal.{u}), o.IsLimit → (o.blsub fun x x_1 => f x) = f o)
-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem IsVanKampenColimit.whiskerEquivalence_iff {K : Type*} [Category K] (e : J ≌ K)
    {F : K ⥤ C} {c : Cocone F} :
    IsVanKampenColimit (c.whisker e.functor) ↔ IsVanKampenColimit c :=
  ⟨fun hc ↦ ((hc.whiskerEquivalence e.symm).precompose_isIso (e.invFunIdAssoc F).inv).of_iso
      (Cocones.ext (Iso.refl _) (by simp)), IsVanKampenColimit.whiskerEquivalence e⟩

Proof state:
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
K : Type u_3
inst✝ : Category.{u_4, u_3} K
e : J ≌ K
F : K ⥤ C
c : Cocone F
hc : IsVanKampenColimit (Cocone.whisker e.functor c)
⊢ ∀ (j : K),
    ((Cocones.precompose (e.invFunIdAssoc F).inv).obj
                (Cocone.whisker e.symm.functor (Cocone.whisker e.functor c))).ι.app
          j ≫
        (Iso.refl
            ((Cocones.precompose (e.invFunIdAssoc F).inv).obj
                (Cocone.whisker e.symm.functor (Cocone.whisker e.functor c))).pt).hom =
      c.ι.app j

Tactic:
simp

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sup_eq_sdiff_sup_sdiff_sup_inf : x ⊔ y = x \ y ⊔ y \ x ⊔ x ⊓ y :=
  Eq.symm <|
    calc
      x \ y ⊔ y \ x ⊔ x ⊓ y = (x \ y ⊔ y \ x ⊔ x) ⊓ (x \ y ⊔ y \ x ⊔ y)

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x \ y ⊔ y \ x ⊔ x) ⊓ (x \ y ⊔ y \ x ⊔ y) = (x \ y ⊔ x ⊔ y \ x) ⊓ (x \ y ⊔ (y \ x ⊔ y))

Tactic:
ac_rfl

Result:
no goals

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊔ y \ x) ⊓ (x \ y ⊔ y) = x ⊔ y

Tactic:
rw [sup_sdiff_self_right, sup_sdiff_self_left, inf_idem]

Result:
no goals

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x \ y ⊔ x ⊔ y \ x) ⊓ (x \ y ⊔ (y \ x ⊔ y)) = (x ⊔ y \ x) ⊓ (x \ y ⊔ y)

Tactic:
rw [sup_sdiff_right, sup_sdiff_right]

Result:
no goals

Proof state:
α : Type u
x y : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y ⊔ y \ x ⊔ x ⊓ y = (x \ y ⊔ y \ x ⊔ x) ⊓ (x \ y ⊔ y \ x ⊔ y)

Tactic:
rw [sup_inf_left]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem oneCoboundaries_eq_bot_of_isTrivial (A : Rep k G) [A.IsTrivial] :
    oneCoboundaries A = ⊥

Proof state:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ LinearMap.range 0 = ⊥

Tactic:
exact LinearMap.range_eq_bot.2 rfl

Result:
no goals

Proof state:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ oneCoboundaries A = ⊥

Tactic:
simp_rw [oneCoboundaries, dZero_eq_zero]

Result:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ LinearMap.range 0 = ⊥
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem of_has_biproduct₂ [HasBinaryBiproduct X Y] :
    BicartesianSq (0 : 0 ⟶ X) (0 : 0 ⟶ Y) biprod.inl biprod.inr

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y : C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproduct X Y
⊢ BicartesianSq 0 0 biprod.inl biprod.inr

Tactic:
convert of_is_biproduct₂ (BinaryBiproduct.isBilimit X Y)

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Kernel.lean
lemma ker_eq_bot : ker f = ⊥ ↔ Function.Injective f

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ ker f = ⊥ ↔ Function.Injective ⇑f

Tactic:
fconstructor

Result:
case mp
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ ker f = ⊥ → Function.Injective ⇑f

case mpr
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ Function.Injective ⇑f → ker f = ⊥

Proof state:
case mp
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
h : ker f = ⊥
x y : R
hxy : f x = f y
⊢ x = y

Tactic:
simpa [h, rel_iff, mem_bot, sub_eq_zero] using show (ker f).ringCon x y from hxy

Result:
no goals

Proof state:
case mpr
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ Function.Injective ⇑f → ker f = ⊥

Tactic:
exact fun h ↦ eq_bot_iff.2 fun x hx => h hx

Result:
no goals

Proof state:
case mp
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ ker f = ⊥ → Function.Injective ⇑f

Tactic:
intro h x y hxy

Result:
case mp
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
h : ker f = ⊥
x y : R
hxy : f x = f y
⊢ x = y
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem mem_alterKey_of_key_not_beq [EquivBEq α] {β : Type v} {a : α} {f : Option β → Option β}
    {l : List ((_ : α) × β)} (p : (_ : α) × β) (hne : (p.1 == a) = false) :
    p ∈ alterKey a f l ↔ p ∈ l

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
β : Type v
a : α
f : Option β → Option β
l : List ((_ : α) × β)
p : (_ : α) × β
hne : (p.fst == a) = false
⊢ (p ∈
      match f (getValue? a l) with
      | none => eraseKey a l
      | some v => insertEntry a v l) ↔
    p ∈ l

Tactic:
split <;> simp only
  [mem_eraseKey_of_key_beq_eq_false p hne, mem_insertEntry_of_key_beq_eq_false p hne]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
β : Type v
a : α
f : Option β → Option β
l : List ((_ : α) × β)
p : (_ : α) × β
hne : (p.fst == a) = false
⊢ p ∈ alterKey a f l ↔ p ∈ l

Tactic:
rw [alterKey]

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
β : Type v
a : α
f : Option β → Option β
l : List ((_ : α) × β)
p : (_ : α) × β
hne : (p.fst == a) = false
⊢ (p ∈
      match f (getValue? a l) with
      | none => eraseKey a l
      | some v => insertEntry a v l) ↔
    p ∈ l
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem cast_eq_id {α : Type u} : cast (rfl : α = α) = id

Proof state:
α : Type u
⊢ cast ⋯ = id

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_dite_eq' (i : ι) (f : ∀ j, j = i → M) :
    𝔼 j, (if h : j = i then f j h else 0) = f i rfl /ℚ card ι

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : Fintype ι
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → j = i → M
⊢ (𝔼 j : ι, if h : j = i then f j h else 0) = (↑(card ι))⁻¹ • f i ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_of_isEmpty [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
    m.isEmpty = true → m.getD a fallback = fallback

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
a : α
fallback : β a
⊢ m.isEmpty = true → m.getD a fallback = fallback

Tactic:
simp_to_raw using Raw₀.getD_of_isEmpty ⟨m, _⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem bind_eq_none {o : Option α} {f : α → Option β} :
    o.bind f = none ↔ ∀ a, o = some a → f a = none

Proof state:
α : Type u_1
β : Type u_2
o : Option α
f : α → Option β
⊢ o.bind f = none ↔ ∀ (a : α), o = some a → f a = none

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Data/Nat/Hyperoperation.lean
theorem hyperoperation_three : hyperoperation 3 = (· ^ ·)

Proof state:
case h.h
m k : ℕ
⊢ hyperoperation 3 m k = m ^ k

Tactic:
induction' k with bn bih

Result:
case h.h.zero
m : ℕ
⊢ hyperoperation 3 m 0 = m ^ 0

case h.h.succ
m bn : ℕ
bih : hyperoperation 3 m bn = m ^ bn
⊢ hyperoperation 3 m (bn + 1) = m ^ (bn + 1)

Proof state:
case h.h.succ
m bn : ℕ
bih : hyperoperation 3 m bn = m ^ bn
⊢ (fun x1 x2 => x1 * x2) m (m ^ bn) = m ^ (bn + 1)

Tactic:
exact (pow_succ' m bn).symm

Result:
no goals

Proof state:
case h.h.succ
m bn : ℕ
bih : hyperoperation 3 m bn = m ^ bn
⊢ hyperoperation 3 m (bn + 1) = m ^ (bn + 1)

Tactic:
rw [hyperoperation_recursion, hyperoperation_two, bih]

Result:
case h.h.succ
m bn : ℕ
bih : hyperoperation 3 m bn = m ^ bn
⊢ (fun x1 x2 => x1 * x2) m (m ^ bn) = m ^ (bn + 1)

Proof state:
case h.h.zero
m : ℕ
⊢ 1 = m ^ 0

Tactic:
exact (pow_zero m).symm

Result:
no goals

Proof state:
case h.h.zero
m : ℕ
⊢ hyperoperation 3 m 0 = m ^ 0

Tactic:
rw [hyperoperation_ge_three_eq_one]

Result:
case h.h.zero
m : ℕ
⊢ 1 = m ^ 0

Proof state:
⊢ hyperoperation 3 = fun x1 x2 => x1 ^ x2

Tactic:
ext m k

Result:
case h.h
m k : ℕ
⊢ hyperoperation 3 m k = m ^ k
-- Mathlib/Topology/Order/LeftRight.lean
theorem continuousWithinAt_Ioi_iff_Ici {a : α} {f : α → β} :
    ContinuousWithinAt f (Ioi a) a ↔ ContinuousWithinAt f (Ici a) a

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousWithinAt f (Ioi a) a ↔ ContinuousWithinAt f (Ici a) a

Tactic:
simp only [← Ici_diff_left, continuousWithinAt_diff_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue_cons_of_false [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β}
    {h₁ : containsKey a (⟨k, v⟩ :: l)} (h₂ : (k == a) = false) : getValue a (⟨k, v⟩ :: l) h₁ =
      getValue a l (containsKey_of_containsKey_cons (k := k) (v := v) h₁ h₂)

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
k a : α
v : β
h₁ : containsKey a (⟨k, v⟩ :: l) = true
h₂ : (k == a) = false
⊢ getValue a (⟨k, v⟩ :: l) h₁ = getValue a l ⋯

Tactic:
simp [getValue, getValue?_cons_of_false h₂]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoUniformlyOnFilter.tendsto_at (h : TendstoUniformlyOnFilter F f p p')
    (hx : 𝓟 {x} ≤ p') : Tendsto (fun n => F n x) p <| 𝓝 (f x)

Proof state:
case h
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
p' : Filter α
h : TendstoUniformlyOnFilter F f p p'
hx : 𝓟 {x} ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ (a : ι), (∀ᶠ (y : α) in p', (f y, F a y) ∈ u) → a ∈ (fun x_1 => (f x, F x_1 x)) ⁻¹' u

Tactic:
intro i h

Result:
case h
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
p' : Filter α
h✝ : TendstoUniformlyOnFilter F f p p'
hx : 𝓟 {x} ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
i : ι
h : ∀ᶠ (y : α) in p', (f y, F i y) ∈ u
⊢ i ∈ (fun x_1 => (f x, F x_1 x)) ⁻¹' u

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
p' : Filter α
h : TendstoUniformlyOnFilter F f p p'
hx : 𝓟 {x} ≤ p'
⊢ Tendsto (fun n => F n x) p (𝓝 (f x))

Tactic:
refine Uniform.tendsto_nhds_right.mpr fun u hu => mem_map.mpr ?_

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
p' : Filter α
h : TendstoUniformlyOnFilter F f p p'
hx : 𝓟 {x} ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ (fun x_1 => (f x, F x_1 x)) ⁻¹' u ∈ p

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
p' : Filter α
h : TendstoUniformlyOnFilter F f p p'
hx : 𝓟 {x} ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ (fun x_1 => (f x, F x_1 x)) ⁻¹' u ∈ p

Tactic:
filter_upwards [(h u hu).curry]

Result:
case h
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
p' : Filter α
h : TendstoUniformlyOnFilter F f p p'
hx : 𝓟 {x} ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
⊢ ∀ (a : ι), (∀ᶠ (y : α) in p', (f y, F a y) ∈ u) → a ∈ (fun x_1 => (f x, F x_1 x)) ⁻¹' u

Proof state:
case h
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
p' : Filter α
h✝ : TendstoUniformlyOnFilter F f p p'
hx : 𝓟 {x} ≤ p'
u : Set (β × β)
hu : u ∈ 𝓤 β
i : ι
h : ∀ᶠ (y : α) in p', (f y, F i y) ∈ u
⊢ i ∈ (fun x_1 => (f x, F x_1 x)) ⁻¹' u

Tactic:
simpa using h.filter_mono hx

Result:
no goals
-- Mathlib/AlgebraicGeometry/Stalk.lean
lemma Spec_stalkClosedPointIso :
    Spec.map (stalkClosedPointIso R).inv = (Spec R).fromSpecStalk (closedPoint R)

Proof state:
R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ Spec.map (stalkClosedPointIso R).inv = (Spec R).fromSpecStalk (closedPoint ↑R)

Tactic:
rw [stalkClosedPointIso_inv, Scheme.Spec_fromSpecStalk']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_append_right' (l₁ : List α) {l₂ : List α} {i : Nat} (hi : i < l₂.length) :
    l₂[i] = (l₁ ++ l₂)[i + l₁.length]'(by simpa [Nat.add_comm] using Nat.add_lt_add_left hi _)

Proof state:
α : Type u_1
l₁ l₂ : List α
i : Nat
hi : i < l₂.length
⊢ l₂[i] = (l₁ ++ l₂)[i + l₁.length]

Tactic:
rw [getElem_append_right] <;> simp [*, le_add_left]

Result:
no goals

Proof state:
α : Type ?u.184551
l₁ l₂ : List α
i : Nat
hi : i < l₂.length
⊢ i + l₁.length < (l₁ ++ l₂).length

Tactic:
simpa [Nat.add_comm] using Nat.add_lt_add_left hi _

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
lemma iteratedDeriv_neg (n : ℕ) (f : 𝕜 → F) (a : 𝕜) :
    iteratedDeriv n (fun x ↦ -(f x)) a = -(iteratedDeriv n f a)

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

Tactic:
simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_neg f

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem id : Primrec (@id α) :=
  (@Primcodable.prim α).of_eq <| by simp

Proof state:
α : Type u_1
inst✝ : Primcodable α
⊢ ∀ (n : ℕ), encode (decode n) = encode (Option.map id (decode n))

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem tail_drop' {i : ℕ} {s : Stream' α} : tail (drop i s) = s.drop (i + 1)

Proof state:
case a
α : Type u
i : ℕ
s : Stream' α
n✝ : ℕ
⊢ (drop i s).tail.get n✝ = (drop (i + 1) s).get n✝

Tactic:
simp [Nat.add_comm, Nat.add_assoc, Nat.add_left_comm]

Result:
no goals

Proof state:
α : Type u
i : ℕ
s : Stream' α
⊢ (drop i s).tail = drop (i + 1) s

Tactic:
ext

Result:
case a
α : Type u
i : ℕ
s : Stream' α
n✝ : ℕ
⊢ (drop i s).tail.get n✝ = (drop (i + 1) s).get n✝
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffDist_closure₂ : hausdorffDist s (closure t) = hausdorffDist s t

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
⊢ hausdorffDist s (closure t) = hausdorffDist s t

Tactic:
simp [hausdorffDist]

Result:
no goals