harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem comap_id {U V : Opens (PrimeSpectrum.Top R)} (hUV : U = V) :
    (comap (RingHom.id R) U V fun p hpV => by rwa [hUV, PrimeSpectrum.comap_id]) =
      (eqToHom (show (structureSheaf R).1.obj (op U) = _ by rw [hUV])).hom

Proof state:
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
p : ↑(PrimeSpectrum.Top R)
hpV : p ∈ V.carrier
⊢ p ∈ ⇑(PrimeSpectrum.comap (RingHom.id R)) ⁻¹' U.carrier

Tactic:
rwa [hUV, PrimeSpectrum.comap_id]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
⊢ comap (RingHom.id R) U V ⋯ = CommRingCat.Hom.hom (eqToHom ⋯)

Tactic:
rw [comap_id_eq_map U V (eqToHom hUV.symm), eqToHom_op, eqToHom_map]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
⊢ (structureSheaf R).val.obj (op U) = (structureSheaf R).val.obj (op V)

Tactic:
rw [hUV]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem bindOnSupport_pure (p : PMF α) : (p.bindOnSupport fun a _ => pure a) = p

Proof state:
α : Type u_1
p : PMF α
⊢ (p.bindOnSupport fun a x => pure a) = p

Tactic:
simp only [PMF.bind_pure, PMF.bindOnSupport_eq_bind]

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem contMDiff_zero_iff :
    ContMDiff I I' 0 f ↔ Continuous f

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
⊢ ContMDiff I I' 0 f ↔ Continuous f

Tactic:
rw [← contMDiffOn_univ, continuous_iff_continuousOn_univ, contMDiffOn_zero_iff]

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Exactness.lean
theorem injective_of_isLocalized_span
    (H : ∀ r : s, Function.Injective (map (.powers r.1) (f r) (g r) F)) :
    Function.Injective F :=
  fun x y eq ↦ Module.eq_of_isLocalized_span _ spn _ f _ _ fun P ↦ H P <| by simp [eq]

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
s : Set R
spn : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝⁵ : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝⁴ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝³ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (f r)
Nₚ : ↑s → Type u_6
inst✝² : (r : ↑s) → AddCommMonoid (Nₚ r)
inst✝¹ : (r : ↑s) → Module R (Nₚ r)
g : (r : ↑s) → N →ₗ[R] Nₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule (Submonoid.powers ↑r) (g r)
F : M →ₗ[R] N
H : ∀ (r : ↑s), Function.Injective ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)
x y : M
eq : F x = F y
P : ↑s
⊢ ((IsLocalizedModule.map (Submonoid.powers ↑P) (f P) (g P)) F) ((f P) x) =
    ((IsLocalizedModule.map (Submonoid.powers ↑P) (f P) (g P)) F) ((f P) y)

Tactic:
simp [eq]

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem neg (h : Irrational x) : Irrational (-x) :=
  of_neg <| by rwa [neg_neg]

Proof state:
x : ℝ
h : Irrational x
⊢ Irrational (- -x)

Tactic:
rwa [neg_neg]

Result:
no goals
-- Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean
theorem strictConcaveOn_sqrt_mul_log_Ioi :
    StrictConcaveOn ℝ (Set.Ioi 1) fun x => √x * log x

Proof state:
⊢ ContinuousOn (fun x => √x * log x) (Ioi 1)

Tactic:
exact continuous_sqrt.continuousOn.mul
  (continuousOn_log.mono fun x hx => ne_of_gt (zero_lt_one.trans hx))

Result:
no goals

Proof state:
x : ℝ
hx : x ∈ Ioi 1
⊢ -log x / (4 * √x ^ 3) < 0

Tactic:
exact div_neg_of_neg_of_pos (neg_neg_of_pos (log_pos hx))
  (mul_pos four_pos (pow_pos (sqrt_pos.mpr (zero_lt_one.trans hx)) 3))

Result:
no goals

Proof state:
x : ℝ
hx : x ∈ Ioi 1
⊢ deriv^[2] (fun x => √x * log x) x < 0

Tactic:
rw [deriv2_sqrt_mul_log x]

Result:
x : ℝ
hx : x ∈ Ioi 1
⊢ -log x / (4 * √x ^ 3) < 0

Proof state:
⊢ StrictConcaveOn ℝ (Ioi 1) fun x => √x * log x

Tactic:
apply strictConcaveOn_of_deriv2_neg' (convex_Ioi 1) _ fun x hx => ?_

Result:
⊢ ContinuousOn (fun x => √x * log x) (Ioi 1)

x : ℝ
hx : x ∈ Ioi 1
⊢ deriv^[2] (fun x => √x * log x) x < 0
-- Mathlib/Logic/Equiv/Fin.lean
theorem coe_finRotate (i : Fin n.succ) :
    (finRotate n.succ i : ℕ) = if i = Fin.last n then (0 : ℕ) else i + 1

Proof state:
n : ℕ
i : Fin n.succ
⊢ ↑((finRotate n.succ) i) = if i = Fin.last n then 0 else ↑i + 1

Tactic:
rw [finRotate_succ_apply, Fin.val_add_one i]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem DifferentiableWithinAt.hasFDerivWithinAt (h : DifferentiableWithinAt 𝕜 f s x) :
    HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s 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
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
⊢ HasFDerivWithinAt f (if HasFDerivWithinAt f 0 s x then 0 else Classical.choose h) s x

Tactic:
split_ifs with h₀

Result:
case pos
𝕜 : 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
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
h₀ : HasFDerivWithinAt f 0 s x
⊢ HasFDerivWithinAt f 0 s x

case neg
𝕜 : 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
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
h₀ : ¬HasFDerivWithinAt f 0 s x
⊢ HasFDerivWithinAt f (Classical.choose h) s 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
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x

Tactic:
simp only [fderivWithin, dif_pos h]

Result:
𝕜 : 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
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
⊢ HasFDerivWithinAt f (if HasFDerivWithinAt f 0 s x then 0 else Classical.choose h) s x

Proof state:
case pos
𝕜 : 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
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
h₀ : HasFDerivWithinAt f 0 s x
⊢ HasFDerivWithinAt f 0 s x

case neg
𝕜 : 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
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
h₀ : ¬HasFDerivWithinAt f 0 s x
⊢ HasFDerivWithinAt f (Classical.choose h) s x

Tactic:
exacts [h₀, Classical.choose_spec h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
lemma log_pos_of_isNat {n : ℕ} (h : NormNum.IsNat e n) (w : Nat.blt 1 n = true) :
    0 < Real.log (e : ℝ)

Proof state:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 0 < Real.log e

Tactic:
rw [NormNum.IsNat.to_eq h rfl]

Result:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 0 < Real.log ↑n

Proof state:
case hx
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 1 < ↑n

Tactic:
simpa using w

Result:
no goals

Proof state:
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 0 < Real.log ↑n

Tactic:
apply Real.log_pos

Result:
case hx
e : ℝ
n : ℕ
h : NormNum.IsNat e n
w : Nat.blt 1 n = true
⊢ 1 < ↑n
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_modifyKey (k : α) (f : β → β) (l : List ((_ : α) × β)) :
    (modifyKey k f l).isEmpty = l.isEmpty

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
l : List ((_ : α) × β)
a : (_ : α) × β
as : List ((_ : α) × β)
⊢ (match getValue? k (a :: as) with
      | none => a :: as
      | some v => if (a.fst == k) = true then ⟨k, f v⟩ :: as else ⟨a.fst, a.snd⟩ :: replaceEntry k (f v) as).isEmpty =
    (a :: as).isEmpty

Tactic:
repeat' split <;> simp

Result:
no goals

Proof state:
case h_2
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
l : List ((_ : α) × β)
a : (_ : α) × β
as : List ((_ : α) × β)
x✝ : Option β
v✝ : β
heq✝ : getValue? k (a :: as) = some v✝
⊢ (if (a.fst == k) = true then ⟨k, f v✝⟩ :: as else ⟨a.fst, a.snd⟩ :: replaceEntry k (f v✝) as).isEmpty = false

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
l : List ((_ : α) × β)
⊢ (modifyKey k f l).isEmpty = l.isEmpty

Tactic:
match l with
| [] => simp [modifyKey]
| a :: as =>
  simp only [modifyKey, replaceEntry, cond_eq_if]
  repeat' split <;> simp

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
l : List ((_ : α) × β)
⊢ (modifyKey k f []).isEmpty = [].isEmpty

Tactic:
simp [modifyKey]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
l : List ((_ : α) × β)
a : (_ : α) × β
as : List ((_ : α) × β)
⊢ (modifyKey k f (a :: as)).isEmpty = (a :: as).isEmpty

Tactic:
simp only [modifyKey, replaceEntry, cond_eq_if]

Result:
α : Type u
β : Type v
inst✝ : BEq α
k : α
f : β → β
l : List ((_ : α) × β)
a : (_ : α) × β
as : List ((_ : α) × β)
⊢ (match getValue? k (a :: as) with
      | none => a :: as
      | some v => if (a.fst == k) = true then ⟨k, f v⟩ :: as else ⟨a.fst, a.snd⟩ :: replaceEntry k (f v) as).isEmpty =
    (a :: as).isEmpty
-- Mathlib/Topology/Algebra/Group/Basic.lean
@[to_additive]
lemma Subgroup.coe_topologicalClosure_bot :
    ((⊥ : Subgroup G).topologicalClosure : Set G) = _root_.closure ({1} : Set G)

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
⊢ ↑⊥.topologicalClosure = _root_.closure {1}

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem disconnect_le : S.disconnect ≤ S

Proof state:
case intro
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c✝ d✝ : C
a✝ : c✝ ⟶ d✝
left✝ : c✝ = d✝
right✝ : a✝ ∈ S.arrows c✝ d✝
⊢ a✝ ∈ S.arrows c✝ d✝

Tactic:
assumption

Result:
no goals

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ S.disconnect ≤ S

Tactic:
rw [le_iff]

Result:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ {c d : C}, S.disconnect.arrows c d ⊆ S.arrows c d

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
⊢ ∀ {c d : C}, S.disconnect.arrows c d ⊆ S.arrows c d

Tactic:
rintro _ _ _ ⟨⟩

Result:
case intro
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c✝ d✝ : C
a✝ : c✝ ⟶ d✝
left✝ : c✝ = d✝
right✝ : a✝ ∈ S.arrows c✝ d✝
⊢ a✝ ∈ S.arrows c✝ d✝
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[simp]
lemma ofEpiOfIsIsoOfMono'_f' (φ : S₁ ⟶ S₂) (h : LeftHomologyData S₂)
    [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] : (ofEpiOfIsIsoOfMono' φ h).f' = φ.τ₁ ≫ h.f'

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono' φ h).f' = φ.τ₁ ≫ h.f'

Tactic:
rw [← cancel_mono (ofEpiOfIsIsoOfMono' φ h).i, f'_i, ofEpiOfIsIsoOfMono'_i,
  assoc, f'_i_assoc, φ.comm₁₂_assoc, IsIso.hom_inv_id, comp_id]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sheaf.lean
theorem isSheaf_comp_of_isSheaf (s : A ⥤ B) [PreservesLimitsOfSize.{v₁, max v₁ u₁} s]
    (h : IsSheaf J P) : IsSheaf J (P ⋙ s)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
B : Type u₃
inst✝¹ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝ : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit (P.mapCone S.arrows.cocone.op))
⊢ ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit ((P ⋙ s).mapCone S.arrows.cocone.op))

Tactic:
apply fun X S hS ↦ (h S hS).map fun t ↦ isLimitOfPreserves s t

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
B : Type u₃
inst✝¹ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝ : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : IsSheaf J P
⊢ IsSheaf J (P ⋙ s)

Tactic:
rw [isSheaf_iff_isLimit] at h ⊢

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
B : Type u₃
inst✝¹ : Category.{v₃, u₃} B
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ A
s : A ⥤ B
inst✝ : PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s
h : ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit (P.mapCone S.arrows.cocone.op))
⊢ ∀ ⦃X : C⦄, ∀ S ∈ J X, Nonempty (IsLimit ((P ⋙ s).mapCone S.arrows.cocone.op))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem insertEntry_cons_of_beq [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'}
    (h : k' == k) : insertEntry k v (⟨k', v'⟩ :: l) = ⟨k, v⟩ :: l

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

Tactic:
simp_all only [insertEntry, containsKey_cons, Bool.true_or, cond_true, replaceEntry_cons_of_true]

Result:
no goals
-- Mathlib/Algebra/Group/Even.lean
@[to_additive]
lemma IsSquare.map {a : α} (f : F) : IsSquare a → IsSquare (f a) :=
  fun ⟨r, _⟩ => ⟨f r, by simp_all⟩

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : MulOneClass α
inst✝² : MulOneClass β
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
a : α
f : F
x✝ : IsSquare a
r : α
h✝ : a = r * r
⊢ f a = f r * f r

Tactic:
simp_all

Result:
no goals
-- Mathlib/RingTheory/Localization/Cardinality.lean
theorem lift_cardinalMk_le (S : Submonoid R) [IsLocalization S L] :
    Cardinal.lift.{u} #L ≤ Cardinal.lift.{v} #R

Proof state:
R : Type u
inst✝³ : CommSemiring R
L : Type v
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
⊢ Cardinal.lift.{u, v} #L ≤ Cardinal.lift.{v, u} #R

Tactic:
have := Localization.cardinalMk_le S

Result:
R : Type u
inst✝³ : CommSemiring R
L : Type v
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
this : #(Localization S) ≤ #R
⊢ Cardinal.lift.{u, v} #L ≤ Cardinal.lift.{v, u} #R

Proof state:
R : Type u
inst✝³ : CommSemiring R
L : Type v
inst✝² : CommSemiring L
inst✝¹ : Algebra R L
S : Submonoid R
inst✝ : IsLocalization S L
this : #(Localization S) ≤ #R
⊢ Cardinal.lift.{u, v} #L ≤ Cardinal.lift.{v, u} #R

Tactic:
rwa [← lift_le.{v}, lift_mk_eq'.2 ⟨(Localization.algEquiv S L).toEquiv⟩] at this

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem cons_merge_cons (s : α → α → Bool) (a b l r) :
    merge (a::l) (b::r) s = if s a b then a :: merge l (b::r) s else b :: merge (a::l) r s

Proof state:
α : Type u_1
s : α → α → Bool
a b : α
l r : List α
⊢ (a :: l).merge (b :: r) s = if s a b = true then a :: l.merge (b :: r) s else b :: (a :: l).merge r s

Tactic:
simp only [merge]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
theorem evenOdd_map_involute (n : ZMod 2) :
    (evenOdd Q n).map (involute : CliffordAlgebra Q →ₐ[R] CliffordAlgebra Q).toLinearMap =
      evenOdd Q n

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
n : ZMod 2
⊢ Submodule.map involute.toLinearMap (evenOdd Q n) = evenOdd Q n

Tactic:
simp_rw [evenOdd, Submodule.map_iSup, Submodule.map_pow, ι_range_map_involute]

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
theorem equivCongr_symm {δ} (ab : α ≃ β) (cd : γ ≃ δ) :
    (ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm

Proof state:
case H.H
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
x✝¹ : β ≃ δ
x✝ : α
⊢ ((ab.equivCongr cd).symm x✝¹) x✝ = ((ab.symm.equivCongr cd.symm) x✝¹) x✝

Tactic:
rfl

Result:
no goals

Proof state:
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
⊢ (ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm

Tactic:
ext

Result:
case H.H
α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
x✝¹ : β ≃ δ
x✝ : α
⊢ ((ab.equivCongr cd).symm x✝¹) x✝ = ((ab.symm.equivCongr cd.symm) x✝¹) x✝
-- Mathlib/Algebra/Homology/DifferentialObject.lean
theorem d_eqToHom (X : HomologicalComplex V (ComplexShape.up' b)) {x y z : β} (h : y = z) :
    X.d x y ≫ eqToHom (congr_arg X.X h) = X.d x z

Proof state:
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V (ComplexShape.up' b)
x y z : β
h : y = z
⊢ X.d x y ≫ eqToHom ⋯ = X.d x z

Tactic:
cases h

Result:
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V (ComplexShape.up' b)
x y : β
⊢ X.d x y ≫ eqToHom ⋯ = X.d x y

Proof state:
case refl
β : Type u_1
inst✝² : AddCommGroup β
b : β
V : Type u_2
inst✝¹ : Category.{u_3, u_2} V
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V (ComplexShape.up' b)
x y : β
⊢ X.d x y ≫ eqToHom ⋯ = X.d x y

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem pow_mul_divByMonic_rootMultiplicity_eq (p : R[X]) (a : R) :
    (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = p

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
⊢ (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = p

Tactic:
have : Monic ((X - C a) ^ rootMultiplicity a p) := (monic_X_sub_C _).pow _

Result:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : ((X - C a) ^ rootMultiplicity a p).Monic
⊢ (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = p

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : ((X - C a) ^ rootMultiplicity a p).Monic
⊢ (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) = p

Tactic:
conv_rhs =>
    rw [← modByMonic_add_div p this,
      (modByMonic_eq_zero_iff_dvd this).2 (pow_rootMultiplicity_dvd _ _)]

Result:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : ((X - C a) ^ rootMultiplicity a p).Monic
⊢ (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) =
    0 + (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p)

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
this : ((X - C a) ^ rootMultiplicity a p).Monic
⊢ (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p) =
    0 + (X - C a) ^ rootMultiplicity a p * (p /ₘ (X - C a) ^ rootMultiplicity a p)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem isBasis_ground_iff : M.IsBasis B M.E ↔ M.IsBase B

Proof state:
α : Type u_1
M : Matroid α
B : Set α
⊢ M.IsBasis B M.E ↔ M.IsBase B

Tactic:
rw [IsBasis, and_iff_left rfl.subset, isBase_iff_maximal_indep,
  maximal_and_iff_right_of_imp (fun _ h ↦ h.subset_ground),
  and_iff_left_of_imp (fun h ↦ h.1.subset_ground)]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Flag.lean
theorem flag_last (b : Basis (Fin n) R M) : b.flag (.last n) = ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
b : Basis (Fin n) R M
⊢ b.flag (Fin.last n) = ⊤

Tactic:
simp [flag, Fin.castSucc_lt_last]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem _root_.Continuous.memLp_of_hasCompactSupport [OpensMeasurableSpace X]
    {f : X → E} (hf : Continuous f) (h'f : HasCompactSupport f) : MemLp f p μ

Proof state:
E : Type u_4
p : ℝ≥0∞
inst✝⁴ : NormedAddCommGroup E
X : Type u_7
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : OpensMeasurableSpace X
f : X → E
hf : Continuous f
h'f : HasCompactSupport f
this : MemLp f ⊤ μ
⊢ MemLp f p μ

Tactic:
exact this.mono_exponent_of_measure_support_ne_top
  (fun x ↦ image_eq_zero_of_nmem_tsupport) (h'f.measure_lt_top.ne) le_top

Result:
no goals

Proof state:
E : Type u_4
p : ℝ≥0∞
inst✝⁴ : NormedAddCommGroup E
X : Type u_7
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : OpensMeasurableSpace X
f : X → E
hf : Continuous f
h'f : HasCompactSupport f
⊢ MemLp f p μ

Tactic:
have := hf.memLp_top_of_hasCompactSupport h'f μ

Result:
E : Type u_4
p : ℝ≥0∞
inst✝⁴ : NormedAddCommGroup E
X : Type u_7
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasureOnCompacts μ
inst✝ : OpensMeasurableSpace X
f : X → E
hf : Continuous f
h'f : HasCompactSupport f
this : MemLp f ⊤ μ
⊢ MemLp f p μ
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem order_add_of_order_eq (φ ψ : R⟦X⟧) (h : order φ ≠ order ψ) :
    order (φ + ψ) = order φ ⊓ order ψ

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
⊢ (φ + ψ).order ≤ φ.order ⊓ ψ.order

Tactic:
by_cases H₁ : order φ < order ψ

Result:
case pos
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
H₁ : φ.order < ψ.order
⊢ (φ + ψ).order ≤ φ.order ⊓ ψ.order

case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
H₁ : ¬φ.order < ψ.order
⊢ (φ + ψ).order ≤ φ.order ⊓ ψ.order

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
H₁ : φ.order < ψ.order
⊢ (φ + ψ).order ≤ φ.order ⊓ ψ.order

Tactic:
apply order_add_of_order_eq.aux _ _ h H₁

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
⊢ (φ + ψ).order = φ.order ⊓ ψ.order

Tactic:
refine le_antisymm ?_ (min_order_le_order_add _ _)

Result:
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
⊢ (φ + ψ).order ≤ φ.order ⊓ ψ.order

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
H₁ : ¬φ.order < ψ.order
H₂ : ψ.order < φ.order
⊢ (φ + ψ).order ≤ φ.order ⊓ ψ.order

Tactic:
simpa only [add_comm, inf_comm] using order_add_of_order_eq.aux _ _ h.symm H₂

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
H₁ : ¬φ.order < ψ.order
H₂ : ¬ψ.order < φ.order
⊢ False

Tactic:
exact h (le_antisymm (not_lt.1 H₂) (not_lt.1 H₁))

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
H₁ : ¬φ.order < ψ.order
H₂ : ¬ψ.order < φ.order
⊢ (φ + ψ).order ≤ φ.order ⊓ ψ.order

Tactic:
exfalso

Result:
case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
H₁ : ¬φ.order < ψ.order
H₂ : ¬ψ.order < φ.order
⊢ False

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
H₁ : ¬φ.order < ψ.order
⊢ (φ + ψ).order ≤ φ.order ⊓ ψ.order

Tactic:
by_cases H₂ : order ψ < order φ

Result:
case pos
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
H₁ : ¬φ.order < ψ.order
H₂ : ψ.order < φ.order
⊢ (φ + ψ).order ≤ φ.order ⊓ ψ.order

case neg
R : Type u_1
inst✝ : Semiring R
φ ψ : R⟦X⟧
h : φ.order ≠ ψ.order
H₁ : ¬φ.order < ψ.order
H₂ : ¬ψ.order < φ.order
⊢ (φ + ψ).order ≤ φ.order ⊓ ψ.order
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem degree_derivative_le {p : R[X]} : p.derivative.degree ≤ p.degree :=
  letI := Classical.decEq R
  if H : p = 0 then le_of_eq <| by rw [H, derivative_zero] else (degree_derivative_lt H).le

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
this : DecidableEq R := Classical.decEq R
H : p = 0
⊢ (derivative p).degree = p.degree

Tactic:
rw [H, derivative_zero]

Result:
no goals