harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Game/Basic.lean
/-- A small family of games is bounded above. -/
lemma bddAbove_range_of_small {ι : Type*} [Small.{u} ι] (f : ι → Game.{u}) :
    BddAbove (Set.range f)

Proof state:
case intro
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Game
x : PGame
hx : x ∈ upperBounds (Set.range (Quotient.out ∘ f))
i : ι
⊢ f i ≤ ⟦x⟧

Tactic:
simpa [PGame.le_iff_game_le] using hx <| Set.mem_range_self i

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Game
⊢ BddAbove (Set.range f)

Tactic:
obtain ⟨x, hx⟩ := PGame.bddAbove_range_of_small (Quotient.out ∘ f)

Result:
case intro
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Game
x : PGame
hx : x ∈ upperBounds (Set.range (Quotient.out ∘ f))
⊢ BddAbove (Set.range f)

Proof state:
case intro
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Game
x : PGame
hx : x ∈ upperBounds (Set.range (Quotient.out ∘ f))
⊢ BddAbove (Set.range f)

Tactic:
refine ⟨⟦x⟧, Set.forall_mem_range.2 fun i ↦ ?_⟩

Result:
case intro
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Game
x : PGame
hx : x ∈ upperBounds (Set.range (Quotient.out ∘ f))
i : ι
⊢ f i ≤ ⟦x⟧
-- Mathlib/Algebra/Polynomial/Bivariate.lean
@[simp]
lemma evalEval_zero (x y : R) : (0 : R[X][Y]).evalEval x y = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
x y : R
⊢ evalEval x y 0 = 0

Tactic:
simp only [evalEval, eval_zero]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Contracting.lean
theorem dist_inequality (x y) : dist x y ≤ (dist x (f x) + dist y (f y)) / (1 - K) :=
  suffices dist x y ≤ dist x (f x) + dist y (f y) + K * dist x y by
    rwa [le_div_iff₀ hf.one_sub_K_pos, mul_comm, _root_.sub_mul, one_mul, sub_le_iff_le_add]
  calc
    dist x y ≤ dist x (f x) + dist y (f y) + dist (f x) (f y) := dist_triangle4_right _ _ _ _
    _ ≤ dist x (f x) + dist y (f y) + K * dist x y := add_le_add_left (hf.dist_le_mul _ _) _

Proof state:
α : Type u_1
inst✝ : MetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
this : dist x y ≤ dist x (f x) + dist y (f y) + ↑K * dist x y
⊢ dist x y ≤ (dist x (f x) + dist y (f y)) / (1 - ↑K)

Tactic:
rwa [le_div_iff₀ hf.one_sub_K_pos, mul_comm, _root_.sub_mul, one_mul, sub_le_iff_le_add]

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
theorem eraseLead_C_mul_X_pow (r : R) (n : ℕ) : eraseLead (C r * X ^ n) = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ (C r * X ^ n).eraseLead = 0

Tactic:
rw [C_mul_X_pow_eq_monomial, eraseLead_monomial]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallyInjective.lean
lemma isLocallyInjective_of_isLocallyInjective [IsLocallyInjective J (φ ≫ ψ)] :
    IsLocallyInjective J φ where
  equalizerSieve_mem {X} x y h := equalizerSieve_mem J (φ ≫ ψ) x y (by simp [h])

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
FD : D → D → Type u_1
CD : D → Type w
inst✝² : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝¹ : ConcreteCategory D FD
J : GrothendieckTopology C
F₁ F₂ F₃ : Cᵒᵖ ⥤ D
φ : F₁ ⟶ F₂
ψ : F₂ ⟶ F₃
inst✝ : IsLocallyInjective J (φ ≫ ψ)
X : Cᵒᵖ
x y : ToType (F₁.obj X)
h : (ConcreteCategory.hom (φ.app X)) x = (ConcreteCategory.hom (φ.app X)) y
⊢ (ConcreteCategory.hom ((φ ≫ ψ).app X)) x = (ConcreteCategory.hom ((φ ≫ ψ).app X)) y

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem support_nonempty {u v : V} (p : G.Walk u v) : { w | w ∈ p.support }.Nonempty :=
  ⟨u, by simp⟩

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ u ∈ {w | w ∈ p.support}

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Elementwise.lean
theorem hom_elementwise {C : Type*} [Category C] [HasForget C]
    {X Y : C} {f g : X ⟶ Y} (h : f = g) (x : X) : f x = g x

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasForget C
X Y : C
f g : X ⟶ Y
h : f = g
x : (forget C).obj X
⊢ f x = g x

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/SmoothTransition.lean
theorem pos_of_pos {x : ℝ} (hx : 0 < x) : 0 < expNegInvGlue x

Proof state:
x : ℝ
hx : 0 < x
⊢ 0 < expNegInvGlue x

Tactic:
simp [expNegInvGlue, not_le.2 hx, exp_pos]

Result:
no goals
-- Mathlib/FieldTheory/Finite/GaloisField.lean
theorem _root_.FiniteField.splits_X_pow_nat_card_sub_X [Finite K] :
    Splits (algebraMap (ZMod p) K) (X ^ Nat.card K - X)

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : Algebra (ZMod p) K
inst✝ : Finite K
this : Fintype K
⊢ Splits (algebraMap (ZMod p) K) (X ^ Nat.card K - X)

Tactic:
rw [Nat.card_eq_fintype_card]

Result:
p : ℕ
h_prime : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : Algebra (ZMod p) K
inst✝ : Finite K
this : Fintype K
⊢ Splits (algebraMap (ZMod p) K) (X ^ Fintype.card K - X)

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : Algebra (ZMod p) K
inst✝ : Finite K
⊢ Splits (algebraMap (ZMod p) K) (X ^ Nat.card K - X)

Tactic:
haveI : Fintype K := Fintype.ofFinite K

Result:
p : ℕ
h_prime : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : Algebra (ZMod p) K
inst✝ : Finite K
this : Fintype K
⊢ Splits (algebraMap (ZMod p) K) (X ^ Nat.card K - X)

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : Algebra (ZMod p) K
inst✝ : Finite K
this : Fintype K
⊢ Splits (algebraMap (ZMod p) K) (X ^ Fintype.card K - X)

Tactic:
exact (FiniteField.isSplittingField_sub K (ZMod p)).splits

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem lift_relrank_comap (f : L →+* E) (B : Subfield L) :
    lift.{v} (relrank (A.comap f) B) = lift.{w} (relrank A (B.map f)) :=
  (lift_relrank_map_map _ _ f).symm.trans <| congr_arg lift <| relrank_eq_of_inf_eq <| by
    rw [map_comap_eq, f.fieldRange_eq_map, inf_assoc, ← map_inf, top_inf_eq]

Proof state:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A : Subfield E
f : L →+* E
B : Subfield L
⊢ map f (comap f A) ⊓ map f B = A ⊓ map f B

Tactic:
rw [map_comap_eq, f.fieldRange_eq_map, inf_assoc, ← map_inf, top_inf_eq]

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

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : (k == a) = false
⊢ getEntry? a (⟨k, v⟩ :: l) = getEntry? a l

Tactic:
simp [getEntry?, h]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_exchange (he : e ∈ M.closure (insert f X) \ M.closure X) :
    f ∈ M.closure (insert e X) \ M.closure X :=
  ⟨mem_closure_insert he.2 he.1, fun hf ↦ by
    rwa [closure_insert_eq_of_mem_closure hf, diff_self, iff_false_intro (not_mem_empty _)] at he⟩

Proof state:
α : Type u_2
M : Matroid α
X : Set α
e f : α
he : e ∈ M.closure (insert f X) \ M.closure X
hf : f ∈ M.closure X
⊢ False

Tactic:
rwa [closure_insert_eq_of_mem_closure hf, diff_self, iff_false_intro (not_mem_empty _)] at he

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem neg_eq_of_add_eq_zero {a b : Int} (h : a + b = 0) : -a = b

Proof state:
a b : Int
h : a + b = 0
⊢ -a = b

Tactic:
rw [← Int.add_zero (-a), ← h, ← Int.add_assoc, Int.add_left_neg, Int.zero_add]

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem image_coe_Icc : (some : α → WithBot α) '' Icc a b = Icc (a : WithBot α) b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' Icc a b = Icc ↑a ↑b

Tactic:
rw [← preimage_coe_Icc, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left
    (Subset.trans Icc_subset_Ici_self <| Ici_subset_Ioi.2 <| bot_lt_coe a)]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Basic.lean
theorem Prime.eq_two_or_odd {p : ℕ} (hp : Prime p) : p = 2 ∨ p % 2 = 1 :=
  p.mod_two_eq_zero_or_one.imp_left fun h =>
    ((hp.eq_one_or_self_of_dvd 2 (dvd_of_mod_eq_zero h)).resolve_left (by decide)).symm

Proof state:
p : ℕ
hp : Prime p
h : p % 2 = 0
⊢ ¬2 = 1

Tactic:
decide

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
theorem rothNumberNat_add_le (M N : ℕ) :
    rothNumberNat (M + N) ≤ rothNumberNat M + rothNumberNat N

Proof state:
M N : ℕ
⊢ addRothNumber (range (M + N)) ≤ addRothNumber (range M) + addRothNumber (range N)

Tactic:
rw [range_add_eq_union, ← addRothNumber_map_add_left (range N) M]

Result:
M N : ℕ
⊢ addRothNumber (range M ∪ map (addLeftEmbedding M) (range N)) ≤
    addRothNumber (range M) + addRothNumber (map (addLeftEmbedding M) (range N))

Proof state:
M N : ℕ
⊢ rothNumberNat (M + N) ≤ rothNumberNat M + rothNumberNat N

Tactic:
simp_rw [rothNumberNat_def]

Result:
M N : ℕ
⊢ addRothNumber (range (M + N)) ≤ addRothNumber (range M) + addRothNumber (range N)

Proof state:
M N : ℕ
⊢ addRothNumber (range M ∪ map (addLeftEmbedding M) (range N)) ≤
    addRothNumber (range M) + addRothNumber (map (addLeftEmbedding M) (range N))

Tactic:
exact addRothNumber_union_le _ _

Result:
no goals
-- Mathlib/Algebra/Group/Units/Defs.lean
theorem isUnit_of_mul_isUnit_left [CommMonoid M] {x y : M} (hu : IsUnit (x * y)) : IsUnit x :=
  let ⟨z, hz⟩ := isUnit_iff_exists_inv.1 hu
  isUnit_iff_exists_inv.2 ⟨y * z, by rwa [← mul_assoc]⟩

Proof state:
M : Type u_1
inst✝ : CommMonoid M
x y : M
hu : IsUnit (x * y)
z : M
hz : x * y * z = 1
⊢ x * (y * z) = 1

Tactic:
rwa [← mul_assoc]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem ContinuousWithinAt.preimage_mem_nhdsWithin'' {y : β} {s t : Set β}
    (h : ContinuousWithinAt f (f ⁻¹' s) x) (ht : t ∈ 𝓝[s] y) (hxy : y = f x) :
    f ⁻¹' t ∈ 𝓝[f ⁻¹' s] x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
y : β
s t : Set β
h : ContinuousWithinAt f (f ⁻¹' s) x
ht : t ∈ 𝓝[s] f x
hxy : y = f x
⊢ f ⁻¹' t ∈ 𝓝[f ⁻¹' s] x

Tactic:
exact h.preimage_mem_nhdsWithin' (nhdsWithin_mono _ (image_preimage_subset f s) ht)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
y : β
s t : Set β
h : ContinuousWithinAt f (f ⁻¹' s) x
ht : t ∈ 𝓝[s] y
hxy : y = f x
⊢ f ⁻¹' t ∈ 𝓝[f ⁻¹' s] x

Tactic:
rw [hxy] at ht

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
y : β
s t : Set β
h : ContinuousWithinAt f (f ⁻¹' s) x
ht : t ∈ 𝓝[s] f x
hxy : y = f x
⊢ f ⁻¹' t ∈ 𝓝[f ⁻¹' s] x
-- Mathlib/CategoryTheory/Triangulated/Subcategory.lean
lemma ext₂ [S.P.IsClosedUnderIsomorphisms]
    (T : Triangle C) (hT : T ∈ distTriang C) (h₁ : S.P T.obj₁)
    (h₃ : S.P T.obj₃) : S.P T.obj₂

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_2, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
S : Subcategory C
inst✝ : S.P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : S.P T.obj₁
h₃ : S.P T.obj₃
⊢ S.P T.obj₂

Tactic:
simpa only [ObjectProperty.isoClosure_eq_self] using S.ext₂' T hT h₁ h₃

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContDiff.contDiff_fderiv_apply {f : E → F} (hf : ContDiff 𝕜 n f) (hmn : m + 1 ≤ n) :
    ContDiff 𝕜 m fun p : E × E => (fderiv 𝕜 f p.1 : E →L[𝕜] F) p.2

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m n : WithTop ℕ∞
f : E → F
hf : ContDiff 𝕜 n f
hmn : m + 1 ≤ n
⊢ ContDiff 𝕜 m fun p => (fderiv 𝕜 f p.1) p.2

Tactic:
rw [← contDiffOn_univ] at hf ⊢

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m n : WithTop ℕ∞
f : E → F
hf : ContDiffOn 𝕜 n f univ
hmn : m + 1 ≤ n
⊢ ContDiffOn 𝕜 m (fun p => (fderiv 𝕜 f p.1) p.2) univ

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m n : WithTop ℕ∞
f : E → F
hf : ContDiffOn 𝕜 n f univ
hmn : m + 1 ≤ n
⊢ ContDiffOn 𝕜 m (fun p => (fderivWithin 𝕜 f univ p.1) p.2) (univ ×ˢ univ)

Tactic:
exact contDiffOn_fderivWithin_apply hf uniqueDiffOn_univ hmn

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m n : WithTop ℕ∞
f : E → F
hf : ContDiffOn 𝕜 n f univ
hmn : m + 1 ≤ n
⊢ ContDiffOn 𝕜 m (fun p => (fderiv 𝕜 f p.1) p.2) univ

Tactic:
rw [← fderivWithin_univ, ← univ_prod_univ]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
m n : WithTop ℕ∞
f : E → F
hf : ContDiffOn 𝕜 n f univ
hmn : m + 1 ≤ n
⊢ ContDiffOn 𝕜 m (fun p => (fderivWithin 𝕜 f univ p.1) p.2) (univ ×ˢ univ)
-- Mathlib/Analysis/Convex/Function.lean
theorem StrictConvexOn.add_convexOn (hf : StrictConvexOn 𝕜 s f) (hg : ConvexOn 𝕜 s g) :
    StrictConvexOn 𝕜 s (f + g) :=
  ⟨hf.1, fun x hx y hy hxy a b ha hb hab =>
    calc
      f (a • x + b • y) + g (a • x + b • y) < a • f x + b • f y + (a • g x + b • g y) :=
        add_lt_add_of_lt_of_le (hf.2 hx hy hxy ha hb hab) (hg.2 hx hy ha.le hb.le hab)
      _ = a • (f x + g x) + b • (f y + g y)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)

Tactic:
rw [smul_add, smul_add, add_add_add_comm]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem sup_le_inf : a ⊔ b ≤ a ⊓ b ↔ a = b

Proof state:
α : Type u
inst✝ : Lattice α
a b : α
⊢ a ⊔ b ≤ a ⊓ b ↔ a = b

Tactic:
simp [le_antisymm_iff, and_comm]

Result:
no goals
-- Mathlib/GroupTheory/CommutingProbability.lean
lemma commProb_cons (n : ℕ) (l : List ℕ) :
    commProb (Product (n :: l)) = commProb (DihedralGroup n) * commProb (Product l)

Proof state:
n : ℕ
l : List ℕ
⊢ commProb (Product (n :: l)) = commProb (DihedralGroup n) * commProb (Product l)

Tactic:
simp [Product, commProb_pi, Fin.prod_univ_succ]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/SmallDegree.lean
theorem zero_le_degree_iff : 0 ≤ degree p ↔ p ≠ 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ 0 ≤ p.degree ↔ p ≠ 0

Tactic:
rw [← not_lt, Nat.WithBot.lt_zero_iff, degree_eq_bot]

Result:
no goals
-- Mathlib/Data/Fintype/Units.lean
theorem Nat.card_eq_card_units_add_one [GroupWithZero α] [Finite α] :
    Nat.card α = Nat.card αˣ + 1

Proof state:
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : Finite α
⊢ Nat.card α = Nat.card αˣ + 1

Tactic:
rw [Nat.card_units, tsub_add_cancel_of_le Nat.card_pos]

Result:
no goals
-- Mathlib/Probability/Kernel/RadonNikodym.lean
@[fun_prop]
lemma measurable_rnDerivAux_right (κ η : Kernel α γ) (a : α) :
    Measurable (fun x : γ ↦ rnDerivAux κ η a x)

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
⊢ Measurable fun x => κ.rnDerivAux η a x

Tactic:
fun_prop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_alter_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β]
    {f : Option β → Option β} (h : m.WF) :
    Const.get! (Const.alter m k f) k = (f (Const.get? m k)).get!

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
k : α
inst✝ : Inhabited β
f : Option β → Option β
h : m.WF
⊢ get! (alter m k f) k = (f (get? m k)).get!

Tactic:
simp [get!_alter h]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem fderiv_neg : fderiv 𝕜 (fun y => -f y) x = -fderiv 𝕜 f 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
f : E → F
x : E
⊢ fderiv 𝕜 (fun y => -f y) x = -fderiv 𝕜 f x

Tactic:
simp only [← fderivWithin_univ, fderivWithin_neg uniqueDiffWithinAt_univ]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem domRestrict_le {f : E →ₗ.[R] F} {S : Submodule R E} : f.domRestrict S ≤ f :=
  ⟨by simp, fun _ _ hxy => domRestrict_apply hxy⟩

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
S : Submodule R E
⊢ (f.domRestrict S).domain ≤ f.domain

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma map_Ψ (n : ℤ) : (W.map f).Ψ n = (W.Ψ n).map (mapRingHom f)

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (C ((mapRingHom f) (W.preΨ n)) * if Even n then (mapRingHom (mapRingHom f)) W.ψ₂ else 1) =
    (mapRingHom (mapRingHom f)) (C (W.preΨ n) * if Even n then W.ψ₂ else 1)

Tactic:
map_simp

Result:
no goals

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (W.map f).Ψ n = Polynomial.map (mapRingHom f) (W.Ψ n)

Tactic:
simp only [Ψ, map_preΨ, map_ψ₂, ← coe_mapRingHom]

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (C ((mapRingHom f) (W.preΨ n)) * if Even n then (mapRingHom (mapRingHom f)) W.ψ₂ else 1) =
    (mapRingHom (mapRingHom f)) (C (W.preΨ n) * if Even n then W.ψ₂ else 1)
-- Mathlib/RingTheory/HopfAlgebra/Basic.lean
theorem antipode_one :
    HopfAlgebra.antipode (R := R) (1 : A) = 1

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
⊢ antipode 1 = 1

Tactic:
simpa [Algebra.TensorProduct.one_def] using mul_antipode_rTensor_comul_apply (R := R) (1 : A)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem eq_zero_rpow_iff {x : ℝ} {a : ℝ} : a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Proof state:
x a : ℝ
⊢ a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1

Tactic:
rw [← zero_rpow_eq_iff, eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_some (l : Array α) : filterMap some l = l

Proof state:
case mk
α : Type u_1
toList✝ : List α
⊢ filterMap some { toList := toList✝ } = { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : Array α
⊢ filterMap some l = l

Tactic:
cases l

Result:
case mk
α : Type u_1
toList✝ : List α
⊢ filterMap some { toList := toList✝ } = { toList := toList✝ }
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem c₄_of_isCharThreeJNeZeroNF_of_char_three : W.c₄ = W.a₂ ^ 2

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ W.c₄ = W.a₂ ^ 2

Tactic:
rw [c₄_of_isCharThreeJNeZeroNF]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ 16 * W.a₂ ^ 2 = W.a₂ ^ 2

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ 16 * W.a₂ ^ 2 = W.a₂ ^ 2

Tactic:
linear_combination 5 * W.a₂ ^ 2 * CharP.cast_eq_zero R 3

Result:
no goals
-- Mathlib/AlgebraicGeometry/ResidueField.lean
@[reassoc]
lemma residue_residueFieldCongr (X : Scheme) {x y : X} (h : x = y) :
    X.residue x ≫ (X.residueFieldCongr h).hom =
      (X.presheaf.stalkCongr (.of_eq h)).hom ≫ X.residue y

Proof state:
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ X.residue x ≫ (residueFieldCongr ⋯).hom = (X.presheaf.stalkCongr ⋯).hom ≫ X.residue x

Tactic:
simp

Result:
no goals

Proof state:
X : Scheme
x y : ↑↑X.toPresheafedSpace
h : x = y
⊢ X.residue x ≫ (residueFieldCongr h).hom = (X.presheaf.stalkCongr ⋯).hom ≫ X.residue y

Tactic:
subst h

Result:
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ X.residue x ≫ (residueFieldCongr ⋯).hom = (X.presheaf.stalkCongr ⋯).hom ≫ X.residue x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem not_beq_eq_true_eq (a b : Nat) : ((!(a == b)) = true) = ¬(a = b)

Proof state:
a b : Nat
⊢ ((!a == b) = true) = ¬a = b

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem not_subset_iff_exists_mem_not_mem {α : Type*} {s t : Set α} :
    ¬s ⊆ t ↔ ∃ x, x ∈ s ∧ x ∉ t

Proof state:
α : Type u_1
s t : Set α
⊢ ¬s ⊆ t ↔ ∃ x ∈ s, x ∉ t

Tactic:
simp [subset_def]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem map_pointwise_smul (r : R) (N : Submodule R M) (f : M →ₗ[R] M') :
    (r • N).map f = r • N.map f

Proof state:
R : Type u
M : Type v
M' : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
r : R
N : Submodule R M
f : M →ₗ[R] M'
⊢ map f (r • N) = r • map f N

Tactic:
simp_rw [← ideal_span_singleton_smul, map_smul'']

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLintegral_eq_top_of_measure_eq_top_ne_zero {f : α → ℝ≥0∞} {s : Set α}
    (hf : AEMeasurable f (μ.restrict s)) (hμf : μ ({x ∈ s | f x = ∞}) ≠ 0) :
    ∫⁻ x in s, f x ∂μ = ∞ :=
  lintegral_eq_top_of_measure_eq_top_ne_zero hf <|
    mt (eq_bot_mono <| by rw [← setOf_inter_eq_sep]; exact Measure.le_restrict_apply _ _) hμf

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
hμf : μ {x | x ∈ s ∧ f x = ⊤} ≠ 0
⊢ μ ({a | f a = ⊤} ∩ s) ≤ (μ.restrict s) {x | f x = ⊤}

Tactic:
exact Measure.le_restrict_apply _ _

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
hμf : μ {x | x ∈ s ∧ f x = ⊤} ≠ 0
⊢ μ {x | x ∈ s ∧ f x = ⊤} ≤ (μ.restrict s) {x | f x = ⊤}

Tactic:
rw [← setOf_inter_eq_sep]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f (μ.restrict s)
hμf : μ {x | x ∈ s ∧ f x = ⊤} ≠ 0
⊢ μ ({a | f a = ⊤} ∩ s) ≤ (μ.restrict s) {x | f x = ⊤}
-- Mathlib/CategoryTheory/Shift/Adjunction.lean
@[reassoc]
lemma shift_unit_app [adj.CommShift A] (a : A) (X : C) :
    (adj.unit.app X)⟦a⟧' =
      adj.unit.app (X⟦a⟧) ≫
        G.map ((F.commShiftIso a).hom.app X) ≫
          (G.commShiftIso a).hom.app (F.obj X)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_4, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
inst✝ : adj.CommShift A
a : A
X : C
⊢ (shiftFunctor C a).map (adj.unit.app X) =
    adj.unit.app ((shiftFunctor C a).obj X) ≫
      G.map ((F.commShiftIso a).hom.app X) ≫ (G.commShiftIso a).hom.app (F.obj X)

Tactic:
simpa [Functor.commShiftIso_comp_hom_app] using NatTrans.shift_app_comm adj.unit a X

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
lemma restrictSubtype_isBase_iff {B : Set X} : (M.restrictSubtype X).IsBase B ↔ M.IsBasis' B X

Proof state:
α : Type u_1
X : Set α
M : Matroid α
B : Set ↑X
⊢ (M ↾ X).IsBasis ↑B ↑(X ↓∩ (M ↾ X).E) ∧ InjOn Subtype.val B ∧ B ⊆ X ↓∩ (M ↾ X).E ↔ M.IsBasis' (Subtype.val '' B) X

Tactic:
simp [Subtype.val_injective.injOn, Subset.rfl, isBasis_restrict_iff',
  isBasis'_iff_isBasis_inter_ground]

Result:
no goals

Proof state:
α : Type u_1
X : Set α
M : Matroid α
B : Set ↑X
⊢ (M.restrictSubtype X).IsBase B ↔ M.IsBasis' (Subtype.val '' B) X

Tactic:
rw [restrictSubtype, comap_isBase_iff]

Result:
α : Type u_1
X : Set α
M : Matroid α
B : Set ↑X
⊢ (M ↾ X).IsBasis ↑B ↑(X ↓∩ (M ↾ X).E) ∧ InjOn Subtype.val B ∧ B ⊆ X ↓∩ (M ↾ X).E ↔ M.IsBasis' (Subtype.val '' B) X