harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem ofReal_setAverage {f : α → ℝ} (hf : IntegrableOn f s μ) (hf₀ : 0 ≤ᵐ[μ.restrict s] f) :
    ENNReal.ofReal (⨍ x in s, f x ∂μ) = (∫⁻ x in s, ENNReal.ofReal (f x) ∂μ) / μ s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hf : IntegrableOn f s μ
hf₀ : 0 ≤ᶠ[ae (μ.restrict s)] f
⊢ ENNReal.ofReal (⨍ (x : α) in s, f x ∂μ) = (∫⁻ (x : α) in s, ENNReal.ofReal (f x) ∂μ) / μ s

Tactic:
simpa using ofReal_average hf hf₀

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Chain.lean
lemma genWeightSpace_neg_add_chainBot :
    genWeightSpace M (-α + chainBot α β : L → R) = ⊥

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ genWeightSpace M (-α + ⇑(chainBot α β)) = ⊥

Tactic:
rw [← chainTop_neg, genWeightSpace_add_chainTop _ _ (by simpa using hα)]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
hα : α ≠ 0
⊢ -α ≠ 0

Tactic:
simpa using hα

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Yoneda.lean
theorem full_comp_preadditiveCoyonedaObj [F.Full] {G : C} [Projective G] (hG : IsSeparator G)
    (hG₂ : ∀ X, ∃ (p : G ⟶ F.obj X), Epi p) : (F ⋙ preadditiveCoyonedaObj G).Full where
  map_surjective {X Y} f

Proof state:
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
F : D ⥤ C
inst✝¹ : F.Full
G : C
inst✝ : Projective G
hG : IsSeparator G
hG₂ : ∀ (X : D), ∃ p, Epi p
X Y : D
p : G ⟶ F.obj X
h✝ : Epi p
f : F.obj X ⟶ F.obj Y
⊢ ∃ a, (F ⋙ preadditiveCoyonedaObj G).map a = (preadditiveCoyonedaObj G).map f

Tactic:
obtain ⟨f, rfl⟩ := F.map_surjective f

Result:
case intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
F : D ⥤ C
inst✝¹ : F.Full
G : C
inst✝ : Projective G
hG : IsSeparator G
hG₂ : ∀ (X : D), ∃ p, Epi p
X Y : D
p : G ⟶ F.obj X
h✝ : Epi p
f : X ⟶ Y
⊢ ∃ a, (F ⋙ preadditiveCoyonedaObj G).map a = (preadditiveCoyonedaObj G).map (F.map f)

Proof state:
case intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
F : D ⥤ C
inst✝¹ : F.Full
G : C
inst✝ : Projective G
hG : IsSeparator G
hG₂ : ∀ (X : D), ∃ p, Epi p
X Y : D
p : G ⟶ F.obj X
h✝ : Epi p
f : X ⟶ Y
⊢ ∃ a, (F ⋙ preadditiveCoyonedaObj G).map a = (preadditiveCoyonedaObj G).map (F.map f)

Tactic:
exact ⟨f, rfl⟩

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
F : D ⥤ C
inst✝¹ : F.Full
G : C
inst✝ : Projective G
hG : IsSeparator G
hG₂ : ∀ (X : D), ∃ p, Epi p
X Y : D
f : (F ⋙ preadditiveCoyonedaObj G).obj X ⟶ (F ⋙ preadditiveCoyonedaObj G).obj Y
⊢ ∃ a, (F ⋙ preadditiveCoyonedaObj G).map a = f

Tactic:
obtain ⟨p, _⟩ := hG₂ X

Result:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
F : D ⥤ C
inst✝¹ : F.Full
G : C
inst✝ : Projective G
hG : IsSeparator G
hG₂ : ∀ (X : D), ∃ p, Epi p
X Y : D
f : (F ⋙ preadditiveCoyonedaObj G).obj X ⟶ (F ⋙ preadditiveCoyonedaObj G).obj Y
p : G ⟶ F.obj X
h✝ : Epi p
⊢ ∃ a, (F ⋙ preadditiveCoyonedaObj G).map a = f

Proof state:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
F : D ⥤ C
inst✝¹ : F.Full
G : C
inst✝ : Projective G
hG : IsSeparator G
hG₂ : ∀ (X : D), ∃ p, Epi p
X Y : D
f : (F ⋙ preadditiveCoyonedaObj G).obj X ⟶ (F ⋙ preadditiveCoyonedaObj G).obj Y
p : G ⟶ F.obj X
h✝ : Epi p
⊢ ∃ a, (F ⋙ preadditiveCoyonedaObj G).map a = f

Tactic:
obtain ⟨f, rfl⟩ := preadditiveCoyonedaObj_map_surjective hG p f

Result:
case intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
D : Type u'
inst✝² : Category.{v', u'} D
F : D ⥤ C
inst✝¹ : F.Full
G : C
inst✝ : Projective G
hG : IsSeparator G
hG₂ : ∀ (X : D), ∃ p, Epi p
X Y : D
p : G ⟶ F.obj X
h✝ : Epi p
f : F.obj X ⟶ F.obj Y
⊢ ∃ a, (F ⋙ preadditiveCoyonedaObj G).map a = (preadditiveCoyonedaObj G).map f
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getD_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β}
    {f : Option β → Option β} :
    Const.getD (Const.alter m k f) k fallback = (f (Const.get? m k)).getD fallback

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
fallback : β
f : Option β → Option β
⊢ getD (alter m k f) k fallback = (f (get? m k)).getD fallback

Tactic:
simp [getD_alter]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftedHom.lean
@[simp]
lemma mk₀_id_comp (m₀ : M) (hm₀ : m₀ = 0) {a : M} (f : ShiftedHom X Y a) :
    (mk₀ m₀ hm₀ (𝟙 X)).comp f (by rw [hm₀, add_zero]) = f

Proof state:
C : Type u_1
inst✝⁶ : Category.{?u.19853, u_1} C
D : Type u_2
inst✝⁵ : Category.{?u.19860, u_2} D
E : Type u_3
inst✝⁴ : Category.{?u.19867, u_3} E
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
inst✝ : HasShift E M
X Y Z T : C
m₀ : M
hm₀ : m₀ = 0
a : M
f : ShiftedHom X Y a
⊢ a + m₀ = a

Tactic:
rw [hm₀, add_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y : C
m₀ : M
hm₀ : m₀ = 0
a : M
f : ShiftedHom X Y a
⊢ (mk₀ m₀ hm₀ (𝟙 X)).comp f ⋯ = f

Tactic:
simp [mk₀_comp]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean
theorem eval₂_one_cyclotomic_prime {R S : Type*} [CommRing R] [Semiring S] (f : R →+* S) {p : ℕ}
    [Fact p.Prime] : eval₂ f 1 (cyclotomic p R) = p

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : Semiring S
f : R →+* S
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ eval₂ f 1 (cyclotomic p R) = ↑p

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_mul_C (p : R[X]) (n : ℕ) (a : R) : coeff (p * C a) n = coeff p n * a

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
p : R[ℕ]
⊢ ({ toFinsupp := p } * C a).coeff n = { toFinsupp := p }.coeff n * a

Tactic:
simp_rw [← monomial_zero_left, ← ofFinsupp_single, ← ofFinsupp_mul, coeff]

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
p : R[ℕ]
⊢ (p * Finsupp.single 0 a) n = p n * a

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
p : R[ℕ]
⊢ (p * Finsupp.single 0 a) n = p n * a

Tactic:
exact AddMonoidAlgebra.mul_single_zero_apply p a n

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (p * C a).coeff n = p.coeff n * a

Tactic:
rcases p with ⟨p⟩

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
n : ℕ
a : R
p : R[ℕ]
⊢ ({ toFinsupp := p } * C a).coeff n = { toFinsupp := p }.coeff n * a
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasStrictDerivAt.scomp (hg : HasStrictDerivAt g₁ g₁' (h x)) (hh : HasStrictDerivAt h h' x) :
    HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
hg : HasStrictDerivAt g₁ g₁' (h x)
hh : HasStrictDerivAt h h' x
⊢ HasStrictDerivAt (g₁ ∘ h) (h' • g₁') x

Tactic:
simpa using ((hg.restrictScalars 𝕜).comp x hh).hasStrictDerivAt

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem map_inr_inv_coprodComparison [IsIso (coprodComparison F A B)] :
    F.map coprod.inr ≫ inv (coprodComparison F A B) = coprod.inr

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u₂
inst✝³ : Category.{w, u₂} D
F : C ⥤ D
A B : C
inst✝² : HasBinaryCoproduct A B
inst✝¹ : HasBinaryCoproduct (F.obj A) (F.obj B)
inst✝ : IsIso (coprodComparison F A B)
⊢ F.map coprod.inr ≫ inv (coprodComparison F A B) = coprod.inr

Tactic:
simp [IsIso.inv_comp_eq]

Result:
no goals
-- Mathlib/Data/Complex/Norm.lean
theorem dist_self_conj (z : ℂ) : dist z (conj z) = 2 * |z.im|

Proof state:
z : ℂ
⊢ dist z ((starRingEnd ℂ) z) = 2 * |z.im|

Tactic:
rw [dist_comm, dist_conj_self]

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem col_mulVec [Fintype n] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : n → α) :
    Matrix.col ι (M *ᵥ v) = M * Matrix.col ι v

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
i✝ : m
j✝ : ι
⊢ col ι (M *ᵥ v) i✝ j✝ = (M * col ι v) i✝ j✝

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
⊢ col ι (M *ᵥ v) = M * col ι v

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : n → α
i✝ : m
j✝ : ι
⊢ col ι (M *ᵥ v) i✝ j✝ = (M * col ι v) i✝ j✝
-- Mathlib/Algebra/Tropical/BigOperators.lean
theorem trop_iInf [ConditionallyCompleteLinearOrder R] [Fintype S] (f : S → WithTop R) :
    trop (⨅ i : S, f i) = ∑ i : S, trop (f i)

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : ConditionallyCompleteLinearOrder R
inst✝ : Fintype S
f : S → WithTop R
⊢ trop (⨅ i, f i) = ∑ i : S, trop (f i)

Tactic:
rw [iInf, ← Set.image_univ, ← coe_univ, trop_sInf_image]

Result:
no goals
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem comap_comp (f : R →+* S) (g : S →+* P) (U : Opens (PrimeSpectrum.Top R))
    (V : Opens (PrimeSpectrum.Top S)) (W : Opens (PrimeSpectrum.Top P))
    (hUV : ∀ p ∈ V, PrimeSpectrum.comap f p ∈ U) (hVW : ∀ p ∈ W, PrimeSpectrum.comap g p ∈ V) :
    (comap (g.comp f) U W fun p hpW => hUV (PrimeSpectrum.comap g p) (hVW p hpW)) =
      (comap g V W hVW).comp (comap f U V hUV) :=
  RingHom.ext fun s =>
    Subtype.eq <|
      funext fun p => by
        rw [comap_apply]
        rw [Localization.localRingHom_comp _ (PrimeSpectrum.comap g p.1).asIdeal] <;>
        -- refl works here, because `PrimeSpectrum.comap (g.comp f) p` is defeq to
        -- `PrimeSpectrum.comap f (PrimeSpectrum.comap g p)`
        rfl

Proof state:
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
g : S →+* P
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
W : Opens ↑(PrimeSpectrum.Top P)
hUV : ∀ p ∈ V, (PrimeSpectrum.comap f) p ∈ U
hVW : ∀ p ∈ W, (PrimeSpectrum.comap g) p ∈ V
s : ↑((structureSheaf R).val.obj (op U))
p : ↥(unop (op W))
⊢ (Localization.localRingHom ((PrimeSpectrum.comap (g.comp f)) ↑p).asIdeal (↑p).asIdeal (g.comp f) ⋯)
      (↑s ⟨(PrimeSpectrum.comap (g.comp f)) ↑p, ⋯⟩) =
    ↑(((comap g V W hVW).comp (comap f U V hUV)) s) p

Tactic:
rw [Localization.localRingHom_comp _ (PrimeSpectrum.comap g p.1).asIdeal] <;>
rfl

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
g : S →+* P
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
W : Opens ↑(PrimeSpectrum.Top P)
hUV : ∀ p ∈ V, (PrimeSpectrum.comap f) p ∈ U
hVW : ∀ p ∈ W, (PrimeSpectrum.comap g) p ∈ V
s : ↑((structureSheaf R).val.obj (op U))
p : ↥(unop (op W))
⊢ ↑((comap (g.comp f) U W ⋯) s) p = ↑(((comap g V W hVW).comp (comap f U V hUV)) s) p

Tactic:
rw [comap_apply]

Result:
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
g : S →+* P
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
W : Opens ↑(PrimeSpectrum.Top P)
hUV : ∀ p ∈ V, (PrimeSpectrum.comap f) p ∈ U
hVW : ∀ p ∈ W, (PrimeSpectrum.comap g) p ∈ V
s : ↑((structureSheaf R).val.obj (op U))
p : ↥(unop (op W))
⊢ (Localization.localRingHom ((PrimeSpectrum.comap (g.comp f)) ↑p).asIdeal (↑p).asIdeal (g.comp f) ⋯)
      (↑s ⟨(PrimeSpectrum.comap (g.comp f)) ↑p, ⋯⟩) =
    ↑(((comap g V W hVW).comp (comap f U V hUV)) s) p
-- Mathlib/ModelTheory/Graph.lean
theorem Theory.simpleGraph_model_iff [Language.graph.Structure V] :
    V ⊨ Theory.simpleGraph ↔
      (Irreflexive fun x y : V => RelMap adj ![x, y]) ∧
        Symmetric fun x y : V => RelMap adj ![x, y]

Proof state:
V : Type u
inst✝ : Language.graph.Structure V
⊢ V ⊨ Theory.simpleGraph ↔ (Irreflexive fun x y => RelMap adj ![x, y]) ∧ Symmetric fun x y => RelMap adj ![x, y]

Tactic:
simp [Theory.simpleGraph]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
lemma LinearMap.toMatrix_pow (f : M₁ →ₗ[R] M₁) (k : ℕ) :
    (toMatrix v₁ v₁ f) ^ k = toMatrix v₁ v₁ (f ^ k)

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₁
f : M₁ →ₗ[R] M₁
k : ℕ
⊢ (toMatrix v₁ v₁) f ^ k = (toMatrix v₁ v₁) (f ^ k)

Tactic:
induction k with
| zero => simp
| succ k ih => rw [pow_succ, pow_succ, ih, ← toMatrix_mul]

Result:
no goals

Proof state:
case zero
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₁
f : M₁ →ₗ[R] M₁
⊢ (toMatrix v₁ v₁) f ^ 0 = (toMatrix v₁ v₁) (f ^ 0)

Tactic:
simp

Result:
no goals

Proof state:
case succ
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₁
f : M₁ →ₗ[R] M₁
k : ℕ
ih : (toMatrix v₁ v₁) f ^ k = (toMatrix v₁ v₁) (f ^ k)
⊢ (toMatrix v₁ v₁) f ^ (k + 1) = (toMatrix v₁ v₁) (f ^ (k + 1))

Tactic:
rw [pow_succ, pow_succ, ih, ← toMatrix_mul]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma exists_isCircuit [RankPos M✶] : ∃ C, M.IsCircuit C :=
  dual_rankPos_iff_exists_isCircuit.1 (by assumption)

Proof state:
α : Type u_1
M : Matroid α
inst✝ : M✶.RankPos
⊢ M✶.RankPos

Tactic:
assumption

Result:
no goals
-- Mathlib/Data/Nat/Dist.lean
theorem dist_eq_sub_of_le {n m : ℕ} (h : n ≤ m) : dist n m = m - n

Proof state:
n m : ℕ
h : n ≤ m
⊢ n.dist m = m - n

Tactic:
rw [dist, tsub_eq_zero_iff_le.mpr h, zero_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
    {l : List ((a : α) × β a)}
    {k k' fallback : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Sigma.fst) :
    (m.insertMany l).getKeyD k' fallback = k

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
l : List ((a : α) × β a)
k k' fallback : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Sigma.fst l
⊢ (m.insertMany l).getKeyD k' fallback = k

Tactic:
simp_to_raw using Raw₀.getKeyD_insertMany_list_of_mem

Result:
no goals
-- Mathlib/Data/Subtype.lean
theorem _root_.exists_subtype_mk_eq_iff {a : Subtype p} {b : α} :
    (∃ h : p b, Subtype.mk b h = a) ↔ b = a

Proof state:
α : Sort u_1
p : α → Prop
a : Subtype p
b : α
⊢ (∃ h, ⟨b, h⟩ = a) ↔ b = ↑a

Tactic:
simp only [@eq_comm _ b, exists_eq_subtype_mk_iff, @eq_comm _ _ a]

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem leftInverse_iff {g : α → α} :
    g.LeftInverse f ↔ g = f :=
  ⟨fun hg ↦ funext fun x ↦ by rw [← h x, hg, h], fun he ↦ he ▸ h.leftInverse⟩

Proof state:
α : Sort u
f : α → α
h : Involutive f
g : α → α
hg : LeftInverse g f
x : α
⊢ g x = f x

Tactic:
rw [← h x, hg, h]

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem mem_iff_eq_smul_generator (S : Submodule R M) [S.IsPrincipal] {x : M} :
    x ∈ S ↔ ∃ s : R, x = s • generator S

Proof state:
R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
x : M
⊢ x ∈ S ↔ ∃ s, x = s • generator S

Tactic:
simp_rw [@eq_comm _ x, ← mem_span_singleton, span_singleton_generator]

Result:
no goals
-- Mathlib/Order/SuccPred/LinearLocallyFinite.lean
lemma toZ_nonneg (hi : i0 ≤ i) : 0 ≤ toZ i0 i

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ 0 ≤ toZ i0 i

Tactic:
rw [toZ_of_ge hi]

Result:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ 0 ≤ ↑(Nat.find ⋯)

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i0 ≤ i
⊢ 0 ≤ ↑(Nat.find ⋯)

Tactic:
exact Int.natCast_nonneg _

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem inv_logb (a b : ℝ) : (logb a b)⁻¹ = logb b a

Proof state:
a b : ℝ
⊢ (logb a b)⁻¹ = logb b a

Tactic:
simp_rw [logb, inv_div]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem erase_union_of_mem (ha : a ∈ t) (s : Finset α) : s.erase a ∪ t = s ∪ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
t : Finset α
a : α
ha : a ∈ t
s : Finset α
⊢ s.erase a ∪ t = s ∪ t

Tactic:
rw [← insert_erase (mem_union_right s ha), erase_union_distrib, ← union_insert, insert_erase ha]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem X_inv (s : σ) : (X s : MvPowerSeries σ k)⁻¹ = 0

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
s : σ
⊢ (X s)⁻¹ = 0

Tactic:
rw [inv_eq_zero, constantCoeff_X]

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Ideal.lean
theorem isPrimary_of_isMaximal_radical [CommRing R] {I : Ideal R} (hi : IsMaximal (radical I)) :
    I.IsPrimary :=
  have : radical I = jacobson I :=
    le_antisymm (le_sInf fun _ ⟨him, hm⟩ => hm.isPrime.radical_le_iff.2 him)
      (sInf_le ⟨le_radical, hi⟩)
  isPrimary_iff.mpr
  ⟨ne_top_of_lt <| lt_of_le_of_lt le_radical (lt_top_iff_ne_top.2 hi.1.1), fun {x y} hxy =>
    ((isLocal_of_isMaximal_radical hi).mem_jacobson_or_exists_inv y).symm.imp
      (fun ⟨z, hz⟩ => by
        rw [← mul_one x, ← sub_sub_cancel (z * y) 1, mul_sub, mul_left_comm]
        exact I.sub_mem (I.mul_mem_left _ hxy) (I.mul_mem_left _ hz))
      (this ▸ id)⟩

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
hi : I.radical.IsMaximal
this : I.radical = I.jacobson
x y : R
hxy : x * y ∈ I
x✝ : ∃ y_1, y_1 * y - 1 ∈ I
z : R
hz : z * y - 1 ∈ I
⊢ z * (x * y) - x * (z * y - 1) ∈ I

Tactic:
exact I.sub_mem (I.mul_mem_left _ hxy) (I.mul_mem_left _ hz)

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
hi : I.radical.IsMaximal
this : I.radical = I.jacobson
x y : R
hxy : x * y ∈ I
x✝ : ∃ y_1, y_1 * y - 1 ∈ I
z : R
hz : z * y - 1 ∈ I
⊢ x ∈ I

Tactic:
rw [← mul_one x, ← sub_sub_cancel (z * y) 1, mul_sub, mul_left_comm]

Result:
R : Type u
inst✝ : CommRing R
I : Ideal R
hi : I.radical.IsMaximal
this : I.radical = I.jacobson
x y : R
hxy : x * y ∈ I
x✝ : ∃ y_1, y_1 * y - 1 ∈ I
z : R
hz : z * y - 1 ∈ I
⊢ z * (x * y) - x * (z * y - 1) ∈ I
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_sub {x : ℝ} (hx : 0 < x) (y z : ℝ) : x ^ (y - z) = x ^ y / x ^ z

Proof state:
x : ℝ
hx : 0 < x
y z : ℝ
⊢ x ^ (y - z) = x ^ y / x ^ z

Tactic:
simp only [sub_eq_add_neg, rpow_add hx, rpow_neg (le_of_lt hx), div_eq_mul_inv]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Integers.lean
theorem eq_algebraMap_or_inv_eq_algebraMap (hv : Integers v O) (x : F) :
    ∃ a : O, x = algebraMap O F a ∨ x⁻¹ = algebraMap O F a

Proof state:
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : F
⊢ ∃ a, x = (algebraMap O F) a ∨ x⁻¹ = (algebraMap O F) a

Tactic:
rcases val_le_one_or_val_inv_le_one v x with h | h <;>
obtain ⟨a, ha⟩ := exists_of_le_one hv h

Result:
case inl.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : F
h : v x ≤ 1
a : O
ha : (algebraMap O F) a = x
⊢ ∃ a, x = (algebraMap O F) a ∨ x⁻¹ = (algebraMap O F) a

case inr.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : F
h : v x⁻¹ ≤ 1
a : O
ha : (algebraMap O F) a = x⁻¹
⊢ ∃ a, x = (algebraMap O F) a ∨ x⁻¹ = (algebraMap O F) a

Proof state:
case inl.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : F
h : v x ≤ 1
a : O
ha : (algebraMap O F) a = x
⊢ ∃ a, x = (algebraMap O F) a ∨ x⁻¹ = (algebraMap O F) a

case inr.intro
F : Type u
Γ₀ : Type v
inst✝³ : Field F
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation F Γ₀
O : Type w
inst✝¹ : CommRing O
inst✝ : Algebra O F
hv : v.Integers O
x : F
h : v x⁻¹ ≤ 1
a : O
ha : (algebraMap O F) a = x⁻¹
⊢ ∃ a, x = (algebraMap O F) a ∨ x⁻¹ = (algebraMap O F) a

Tactic:
exacts [⟨a, Or.inl ha.symm⟩, ⟨a, Or.inr ha.symm⟩]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_append (f : α → β → β) (b) (l l' : Array α) :
    (l ++ l').foldr f b = l.foldr f (l'.foldr f b)

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
b : β
l l' : Array α
⊢ foldr f b (l ++ l') = foldr f (foldr f b l') l

Tactic:
simp [foldr_eq_foldrM]

Result:
no goals
-- Mathlib/AlgebraicTopology/ModelCategory/CategoryWithCofibrations.lean
lemma mem_trivialCofibrations_iff :
    trivialCofibrations C f ↔ Cofibration f ∧ WeakEquivalence f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithCofibrations C
inst✝ : CategoryWithWeakEquivalences C
⊢ trivialCofibrations C f ↔ Cofibration f ∧ WeakEquivalence f

Tactic:
rw [cofibration_iff, weakEquivalence_iff]

Result:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithCofibrations C
inst✝ : CategoryWithWeakEquivalences C
⊢ trivialCofibrations C f ↔ cofibrations C f ∧ weakEquivalences C f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithCofibrations C
inst✝ : CategoryWithWeakEquivalences C
⊢ trivialCofibrations C f ↔ cofibrations C f ∧ weakEquivalences C f

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Presheaf.lean
lemma map_smul {X Y : Cᵒᵖ} (f : X ⟶ Y) (r : R.obj X) (m : M.obj X) :
    M.map f (r • m) = R.map f r • M.map f m

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X Y : Cᵒᵖ
f : X ⟶ Y
r : ↑(R.obj X)
m : ↑(M.obj X)
⊢ (ConcreteCategory.hom (M.map f)) (r • m) = (ConcreteCategory.hom (R.map f)) r • (ConcreteCategory.hom (M.map f)) m

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/MvPolynomial.lean
lemma rTensor_apply_monomial_tmul (e : σ →₀ ℕ) (s : S) (n : N) (d : σ →₀ ℕ) :
    rTensor (monomial e s ⊗ₜ[R] n) d = if e = d then s ⊗ₜ[R] n else 0

Proof state:
R : Type u
N : Type v
inst✝⁵ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
inst✝² : DecidableEq σ
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
e : σ →₀ ℕ
s : S
n : N
d : σ →₀ ℕ
⊢ (rTensor ((monomial e) s ⊗ₜ[R] n)) d = if e = d then s ⊗ₜ[R] n else 0

Tactic:
simp only [rTensor_apply_tmul_apply, coeff_monomial, ite_tmul]

Result:
no goals
-- Mathlib/Order/Closure.lean
theorem IsClosed.closure_le_iff (hy : c.IsClosed y) : c x ≤ y ↔ x ≤ y

Proof state:
α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
x y : α
hy : c.IsClosed y
⊢ c x ≤ y ↔ x ≤ y

Tactic:
rw [← hy.closure_eq, ← le_closure_iff]

Result:
no goals