harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasFDerivAt.multiset_prod [DecidableEq ι] {u : Multiset ι} {x : E}
    (h : ∀ i ∈ u, HasFDerivAt (g i ·) (g' i) x) :
    HasFDerivAt (fun x ↦ (u.map (g · x)).prod)
      (u.map fun i ↦ ((u.erase i).map (g · x)).prod • g' i).sum x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasFDerivAt (fun x => g i x) (g' i) x
⊢ HasFDerivAt (fun x => (Multiset.map (fun x_1 => g x_1 x) u).prod)
    (Multiset.map (fun i => (Multiset.map (fun x_1 => g x_1 x) (u.erase i)).prod • g' i) u).sum x

Tactic:
simp only [← Multiset.attach_map_val u, Multiset.map_map]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasFDerivAt (fun x => g i x) (g' i) x
⊢ HasFDerivAt (fun x => (Multiset.map ((fun x_1 => g x_1 x) ∘ Subtype.val) u.attach).prod)
    (Multiset.map
        ((fun x_1 =>
            (Multiset.map (fun x_2 => g x_2 x) ((Multiset.map Subtype.val u.attach).erase x_1)).prod • g' x_1) ∘
          Subtype.val)
        u.attach).sum
    x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasFDerivAt (fun x => g i x) (g' i) x
⊢ (Multiset.map (fun i => (Multiset.map (fun i => g (↑i) x) (u.attach.erase i)).prod • proj i) u.attach).sum.comp
      (pi fun i => g' ↑i) =
    (Multiset.map
        ((fun x_1 =>
            (Multiset.map (fun x_2 => g x_2 x) ((Multiset.map Subtype.val u.attach).erase x_1)).prod • g' x_1) ∘
          Subtype.val)
        u.attach).sum

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
u : Multiset ι
x : E
h : ∀ i ∈ u, HasFDerivAt (fun x => g i x) (g' i) x
x✝ : E
⊢ ((Multiset.map (fun i => (Multiset.map (fun i => g (↑i) x) (u.attach.erase i)).prod • proj i) u.attach).sum.comp
        (pi fun i => g' ↑i))
      x✝ =
    (Multiset.map
          ((fun x_1 =>
              (Multiset.map (fun x_2 => g x_2 x) ((Multiset.map Subtype.val u.attach).erase x_1)).prod • g' x_1) ∘
            Subtype.val)
          u.attach).sum
      x✝
-- Mathlib/CategoryTheory/Subpresheaf/Equalizer.lean
@[simp]
lemma equalizer_self : Subpresheaf.equalizer f f = A

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f : A.toPresheaf ⟶ F₂
⊢ Subpresheaf.equalizer f f = A

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
@[reassoc]
lemma inlX_d' (i j : ι) (hij : c.Rel i j) (hj : ¬ c.Rel j (c.next j)) :
    inlX φ j i hij ≫ d φ i j = φ.f j ≫ inrX φ j

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ inlX φ j i hij ≫ d φ i j = φ.f j ≫ inrX φ j

Tactic:
apply ext_to_X' _ _ hj

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ (inlX φ j i hij ≫ d φ i j) ≫ sndX φ j = (φ.f j ≫ inrX φ j) ≫ sndX φ j

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ (inlX φ j i hij ≫ d φ i j) ≫ sndX φ j = (φ.f j ≫ inrX φ j) ≫ sndX φ j

Tactic:
simp [d_sndX φ i j hij]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem isCompl_iff_toSubmodule :
    IsCompl N N' ↔ IsCompl (N : Submodule R M) (N' : Submodule R M)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N' : LieSubmodule R L M
⊢ IsCompl N N' ↔ IsCompl ↑N ↑N'

Tactic:
simp only [isCompl_iff, disjoint_iff_toSubmodule, codisjoint_iff_toSubmodule]

Result:
no goals
-- Mathlib/Probability/Kernel/Basic.lean
@[simp]
lemma const_zero : const α (0 : Measure β) = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
⊢ const α 0 = 0

Tactic:
ext x s _

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
x : α
s : Set β
a✝ : MeasurableSet s
⊢ ((const α 0) x) s = (0 x) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
x : α
s : Set β
a✝ : MeasurableSet s
⊢ ((const α 0) x) s = (0 x) s

Tactic:
simp [const_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem exists_erase_eq [LawfulBEq α] {a : α} {l : List α} (h : a ∈ l) :
    ∃ l₁ l₂, a ∉ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.erase a = l₁ ++ l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
w✝ : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬(a == b) = true
e : (a == w✝) = true
h₂ : l = l₁ ++ w✝ :: l₂
h₃ : eraseP (BEq.beq a) l = l₁ ++ l₂
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.erase a = l₁ ++ l₂

Tactic:
rw [erase_eq_eraseP]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
w✝ : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬(a == b) = true
e : (a == w✝) = true
h₂ : l = l₁ ++ w✝ :: l₂
h₃ : eraseP (BEq.beq a) l = l₁ ++ l₂
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ eraseP (fun x => a == x) l = l₁ ++ l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
w✝ : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬(a == b) = true
e : (a == w✝) = true
h₂ : l = l₁ ++ w✝ :: l₂
h₃ : eraseP (BEq.beq a) l = l₁ ++ l₂
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ eraseP (fun x => a == x) l = l₁ ++ l₂

Tactic:
exact ⟨l₁, l₂, fun h => h₁ _ h (beq_self_eq_true _), eq_of_beq e ▸ h₂, h₃⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.erase a = l₁ ++ l₂

Tactic:
let ⟨_, l₁, l₂, h₁, e, h₂, h₃⟩ := exists_of_eraseP h (beq_self_eq_true _)

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
w✝ : α
l₁ l₂ : List α
h₁ : ∀ (b : α), b ∈ l₁ → ¬(a == b) = true
e : (a == w✝) = true
h₂ : l = l₁ ++ w✝ :: l₂
h₃ : eraseP (BEq.beq a) l = l₁ ++ l₂
⊢ ∃ l₁ l₂, ¬a ∈ l₁ ∧ l = l₁ ++ a :: l₂ ∧ l.erase a = l₁ ++ l₂
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem church_rosser : Red L₁ L₂ → Red L₁ L₃ → Join Red L₂ L₃ :=
  Relation.church_rosser fun _ b c hab hac =>
    match b, c, Red.Step.diamond hab hac rfl with
    | b, _, Or.inl rfl => ⟨b, by rfl, by rfl⟩
    | _, _, Or.inr ⟨d, hbd, hcd⟩ => ⟨d, ReflGen.single hbd, hcd.to_red⟩

Proof state:
α : Type u
L₁ L₂ L₃ x✝ b✝ c b : List (α × Bool)
hab hac : Step x✝ b
⊢ ReflTransGen Step b b

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
L₁ L₂ L₃ x✝ b✝ c b : List (α × Bool)
hab hac : Step x✝ b
⊢ ReflGen Step b b

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem inv_zero : (0 : ℝ≥0∞)⁻¹ = ∞ :=
  show sInf { b : ℝ≥0∞ | 1 ≤ 0 * b } = ∞ by simp

Proof state:
⊢ sInf {b | 1 ≤ 0 * b} = ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem imp_true_eq (p : Prop) : (p → True) = True

Proof state:
p : Prop
⊢ (p → True) = True

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem compact_covered_by_mul_left_translates {K V : Set G} (hK : IsCompact K)
    (hV : (interior V).Nonempty) : ∃ t : Finset G, K ⊆ ⋃ g ∈ t, (g * ·) ⁻¹' V

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
⊢ K ⊆ ⋃ i, (fun x => interior ((fun x_1 => x * x_1) ⁻¹' V)) i

Tactic:
obtain ⟨g₀, hg₀⟩ := hV

Result:
case intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
⊢ K ⊆ ⋃ i, (fun x => interior ((fun x_1 => x * x_1) ⁻¹' V)) i

Proof state:
case intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
t : Finset G
ht : K ⊆ ⋃ x ∈ t, interior ((fun x_1 => x * x_1) ⁻¹' V)
⊢ ∃ t, K ⊆ ⋃ g ∈ t, (fun x => g * x) ⁻¹' V

Tactic:
exact ⟨t, Subset.trans ht <| iUnion₂_mono fun g _ => interior_subset⟩

Result:
no goals

Proof state:
case intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
⊢ K ⊆ ⋃ i, (fun x => interior ((fun x_1 => x * x_1) ⁻¹' V)) i

Tactic:
refine fun g _ => mem_iUnion.2 ⟨g₀ * g⁻¹, ?_⟩

Result:
case intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ g ∈ interior ((fun x => g₀ * g⁻¹ * x) ⁻¹' V)

Proof state:
case intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ g ∈ interior ((fun x => g₀ * g⁻¹ * x) ⁻¹' V)

Tactic:
refine preimage_interior_subset_interior_preimage (continuous_const.mul continuous_id) ?_

Result:
case intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ g ∈ (fun x => g₀ * g⁻¹ * id x) ⁻¹' interior V

Proof state:
case intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ g ∈ (fun x => g₀ * g⁻¹ * id x) ⁻¹' interior V

Tactic:
rwa [mem_preimage, Function.id_def, inv_mul_cancel_right]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem mem_comap_iff {f : Filter β} {m : α → β} (inj : Injective m) (large : Set.range m ∈ f)
    {S : Set α} : S ∈ comap m f ↔ m '' S ∈ f

Proof state:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
inj : Injective m
large : range m ∈ f
S : Set α
⊢ S ∈ comap m f ↔ m '' S ∈ f

Tactic:
rw [← image_mem_map_iff inj, map_comap_of_mem large]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem Measurable.max {f g : δ → α} (hf : Measurable f) (hg : Measurable g) :
    Measurable fun a => max (f a) (g a)

Proof state:
α : Type u_1
δ : Type u_4
inst✝⁴ : TopologicalSpace α
mα : MeasurableSpace α
inst✝³ : OpensMeasurableSpace α
mδ : MeasurableSpace δ
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
inst✝ : SecondCountableTopology α
f g : δ → α
hf : Measurable f
hg : Measurable g
⊢ Measurable fun a => f a ⊔ g a

Tactic:
simpa only [max_def'] using hf.piecewise (measurableSet_le hg hf) hg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Basic.lean
theorem min?_eq_some_iff' {xs : List Nat} :
    xs.min? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, a ≤ b) :=
  min?_eq_some_iff
    (le_refl := Nat.le_refl)
    (min_eq_or := fun _ _ => Nat.min_def .. ▸ by split <;> simp)
    (le_min_iff := fun _ _ _ => Nat.le_min)

Proof state:
a : Nat
xs : List Nat
x✝¹ x✝ : Nat
⊢ (if x✝¹ ≤ x✝ then x✝¹ else x✝) = x✝¹ ∨ (if x✝¹ ≤ x✝ then x✝¹ else x✝) = x✝

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem diag_col_mul_row [Mul α] [AddCommMonoid α] [Unique ι] (a b : n → α) :
    diag (col ι a * row ι b) = a * b

Proof state:
n : Type u_3
α : Type v
ι : Type u_6
inst✝² : Mul α
inst✝¹ : AddCommMonoid α
inst✝ : Unique ι
a b : n → α
⊢ (col ι a * row ι b).diag = a * b

Tactic:
ext

Result:
case h
n : Type u_3
α : Type v
ι : Type u_6
inst✝² : Mul α
inst✝¹ : AddCommMonoid α
inst✝ : Unique ι
a b : n → α
x✝ : n
⊢ (col ι a * row ι b).diag x✝ = (a * b) x✝

Proof state:
case h
n : Type u_3
α : Type v
ι : Type u_6
inst✝² : Mul α
inst✝¹ : AddCommMonoid α
inst✝ : Unique ι
a b : n → α
x✝ : n
⊢ (col ι a * row ι b).diag x✝ = (a * b) x✝

Tactic:
simp [Matrix.mul_apply, col, row]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/AbelianImages.lean
theorem PreservesImage.factorThruImage_iso_hom :
    F.map (Abelian.factorThruImage f) ≫ (PreservesImage.iso F f).hom =
      Abelian.factorThruImage (F.map f)

Proof state:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasKernels C
inst✝⁷ : HasCokernels C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
inst✝⁴ : HasKernels D
inst✝³ : HasCokernels D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair F
inst✝ : PreservesColimitsOfShape WalkingParallelPair F
X Y : C
f : X ⟶ Y
⊢ F.map (Abelian.factorThruImage f) ≫ (iso F f).hom = Abelian.factorThruImage (F.map f)

Tactic:
ext

Result:
case h
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasKernels C
inst✝⁷ : HasCokernels C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
inst✝⁴ : HasKernels D
inst✝³ : HasCokernels D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair F
inst✝ : PreservesColimitsOfShape WalkingParallelPair F
X Y : C
f : X ⟶ Y
⊢ (F.map (Abelian.factorThruImage f) ≫ (iso F f).hom) ≫ equalizer.ι (cokernel.π (F.map f)) 0 =
    Abelian.factorThruImage (F.map f) ≫ equalizer.ι (cokernel.π (F.map f)) 0

Proof state:
case h
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasKernels C
inst✝⁷ : HasCokernels C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
inst✝⁴ : HasKernels D
inst✝³ : HasCokernels D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair F
inst✝ : PreservesColimitsOfShape WalkingParallelPair F
X Y : C
f : X ⟶ Y
⊢ (F.map (Abelian.factorThruImage f) ≫ (iso F f).hom) ≫ equalizer.ι (cokernel.π (F.map f)) 0 =
    Abelian.factorThruImage (F.map f) ≫ equalizer.ι (cokernel.π (F.map f)) 0

Tactic:
simp [iso]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean
theorem geometric_hahn_banach_point_point [T1Space E] (hxy : x ≠ y) :
    ∃ f : E →L[ℝ] ℝ, f x < f y

Proof state:
E : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
x y : E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
hxy : x ≠ y
⊢ ∃ f, f x < f y

Tactic:
obtain ⟨f, s, t, hs, st, ht⟩ :=
  geometric_hahn_banach_compact_closed (convex_singleton x) isCompact_singleton
    (convex_singleton y) isClosed_singleton (disjoint_singleton.2 hxy)

Result:
case intro.intro.intro.intro.intro
E : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
x y : E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
hxy : x ≠ y
f : E →L[ℝ] ℝ
s t : ℝ
hs : ∀ a ∈ {x}, f a < s
st : s < t
ht : ∀ b ∈ {y}, t < f b
⊢ ∃ f, f x < f y

Proof state:
case intro.intro.intro.intro.intro
E : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
x y : E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
hxy : x ≠ y
f : E →L[ℝ] ℝ
s t : ℝ
hs : ∀ a ∈ {x}, f a < s
st : s < t
ht : ∀ b ∈ {y}, t < f b
⊢ ∃ f, f x < f y

Tactic:
exact ⟨f, by linarith [hs x rfl, ht y rfl]⟩

Result:
no goals

Proof state:
E : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
x y : E
inst✝³ : IsTopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
hxy : x ≠ y
f : E →L[ℝ] ℝ
s t : ℝ
hs : ∀ a ∈ {x}, f a < s
st : s < t
ht : ∀ b ∈ {y}, t < f b
⊢ f x < f y

Tactic:
linarith [hs x rfl, ht y rfl]

Result:
no goals
-- Mathlib/CategoryTheory/Subterminal.lean
theorem isSubterminal_of_mono_isTerminal_from {T : C} (hT : IsTerminal T) [Mono (hT.from A)] :
    IsSubterminal A := fun Z f g => by
  rw [← cancel_mono (hT.from A)]
  apply hT.hom_ext

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A T : C
hT : IsTerminal T
inst✝ : Mono (hT.from A)
Z : C
f g : Z ⟶ A
⊢ f ≫ hT.from A = g ≫ hT.from A

Tactic:
apply hT.hom_ext

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A T : C
hT : IsTerminal T
inst✝ : Mono (hT.from A)
Z : C
f g : Z ⟶ A
⊢ f = g

Tactic:
rw [← cancel_mono (hT.from A)]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A T : C
hT : IsTerminal T
inst✝ : Mono (hT.from A)
Z : C
f g : Z ⟶ A
⊢ f ≫ hT.from A = g ≫ hT.from A
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem reverse_mkArray (n) (a : α) : reverse (mkArray n a) = mkArray n a

Proof state:
α : Type u_1
n : Nat
a : α
⊢ (mkArray n a).reverse = mkArray n a

Tactic:
rw [← toList_inj]

Result:
α : Type u_1
n : Nat
a : α
⊢ (mkArray n a).reverse.toList = (mkArray n a).toList

Proof state:
α : Type u_1
n : Nat
a : α
⊢ (mkArray n a).reverse.toList = (mkArray n a).toList

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem sub_pos_of_lt {a b : Int} (h : b < a) : 0 < a - b

Proof state:
a b : Int
h : b < a
⊢ 0 < a - b

Tactic:
have h := Int.add_lt_add_right h (-b)

Result:
a b : Int
h✝ : b < a
h : b + -b < a + -b
⊢ 0 < a - b

Proof state:
a b : Int
h✝ : b < a
h : b + -b < a + -b
⊢ 0 < a - b

Tactic:
rwa [Int.add_right_neg] at h

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem finSuccEquiv_X_zero : finSuccEquiv R n (X 0) = Polynomial.X

Proof state:
R : Type u
inst✝ : CommSemiring R
n : ℕ
⊢ (finSuccEquiv R n) (X 0) = Polynomial.X

Tactic:
simp [finSuccEquiv_apply]

Result:
no goals
-- Mathlib/Data/Fintype/EquivFin.lean
theorem card_le_one_iff : card α ≤ 1 ↔ ∀ a b : α, a = b :=
  let n := card α
  have hn : n = card α := rfl
  match n, hn with
  | 0, ha =>
    ⟨fun _h => fun a => (card_eq_zero_iff.1 ha.symm).elim a, fun _ => ha ▸ Nat.le_succ _⟩
  | 1, ha =>
    ⟨fun _h => fun a b => by
      let ⟨x, hx⟩ := card_eq_one_iff.1 ha.symm
      rw [hx a, hx b], fun _ => ha ▸ le_rfl⟩
  | n + 2, ha =>
    ⟨fun h => False.elim <| by rw [← ha] at h; cases h with | step h => cases h; , fun h =>
      card_unit ▸ card_le_of_injective (fun _ => ()) fun _ _ _ => h _ _⟩

Proof state:
α : Type u_1
inst✝ : Fintype α
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b : α
⊢ a = b

Tactic:
let ⟨x, hx⟩ := card_eq_one_iff.1 ha.symm

Result:
α : Type u_1
inst✝ : Fintype α
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b x : α
hx : ∀ (y : α), y = x
⊢ a = b

Proof state:
case step
α : Type u_1
inst✝ : Fintype α
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : (n + 2).le 0
⊢ False

Tactic:
cases h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Fintype α
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : n + 2 ≤ 1
⊢ False

Tactic:
cases h with | step h => cases h;

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Fintype α
n : ℕ := card α
hn : n = card α
ha : 1 = card α
_h : card α ≤ 1
a b x : α
hx : ∀ (y : α), y = x
⊢ a = b

Tactic:
rw [hx a, hx b]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Fintype α
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : card α ≤ 1
⊢ False

Tactic:
rw [← ha] at h

Result:
α : Type u_1
inst✝ : Fintype α
n✝ : ℕ := card α
hn : n✝ = card α
n : ℕ
ha : n + 2 = card α
h : n + 2 ≤ 1
⊢ False
-- Mathlib/Algebra/Module/LinearMap/Defs.lean
theorem isScalarTower_of_injective [SMul R S] [CompatibleSMul M M₂ R S] [IsScalarTower R S M₂]
    (f : M →ₗ[S] M₂) (hf : Function.Injective f) : IsScalarTower R S M where
  smul_assoc r s _ := hf <| by rw [f.map_smul_of_tower r, map_smul, map_smul, smul_assoc]

Proof state:
M : Type u_8
M₂ : Type u_10
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
R : Type u_14
S : Type u_15
inst✝⁷ : Semiring S
inst✝⁶ : SMul R M
inst✝⁵ : Module S M
inst✝⁴ : SMul R M₂
inst✝³ : Module S M₂
inst✝² : SMul R S
inst✝¹ : CompatibleSMul M M₂ R S
inst✝ : IsScalarTower R S M₂
f : M →ₗ[S] M₂
hf : Injective ⇑f
r : R
s : S
x✝ : M
⊢ f ((r • s) • x✝) = f (r • s • x✝)

Tactic:
rw [f.map_smul_of_tower r, map_smul, map_smul, smul_assoc]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma natAbs_add_of_nonpos {a b : Int} (ha : a ≤ 0) (hb : b ≤ 0) :
    natAbs (a + b) = natAbs a + natAbs b

Proof state:
a b : ℤ
ha : a ≤ 0
hb : b ≤ 0
⊢ (a + b).natAbs = a.natAbs + b.natAbs

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem X_pow_add_C_ne_one {n : ℕ} (hn : 0 < n) (a : R) : (X : R[X]) ^ n + C a ≠ 1 := fun h =>
  hn.ne' <| by simpa only [natDegree_X_pow_add_C, natDegree_one] using congr_arg natDegree h

Proof state:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
h : X ^ n + C a = 1
⊢ n = 0

Tactic:
simpa only [natDegree_X_pow_add_C, natDegree_one] using congr_arg natDegree h

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Matrix.lean
lemma l2_opNorm_conjTranspose [DecidableEq m] (A : Matrix m n 𝕜) : ‖Aᴴ‖ = ‖A‖

Proof state:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix m n 𝕜
⊢ ‖ContinuousLinearMap.adjoint
        (toContinuousLinearMap
          ((toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis) A))‖ =
    ‖A‖

Tactic:
exact ContinuousLinearMap.adjoint.norm_map _

Result:
no goals

Proof state:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix m n 𝕜
⊢ ‖Aᴴ‖ = ‖A‖

Tactic:
rw [l2_opNorm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
  toLin_conjTranspose, adjoint_toContinuousLinearMap]

Result:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : RCLike 𝕜
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
A : Matrix m n 𝕜
⊢ ‖ContinuousLinearMap.adjoint
        (toContinuousLinearMap
          ((toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis) A))‖ =
    ‖A‖
-- Mathlib/Data/Finset/PImage.lean
theorem pimage_eq_image_filter : s.pimage f =
    (filter (fun x => (f x).Dom) s).attach.image
      fun x : { x // x ∈ filter (fun x => (f x).Dom) s } =>
        (f x).get (mem_filter.mp x.coe_prop).2

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α →. β
inst✝ : (x : α) → Decidable (f x).Dom
s : Finset α
x : β
⊢ (∃ a ∈ s, ∃ (h : (f a).Dom), (f a).get h = x) ↔ ∃ a, ∃ (hp : a ∈ s) (hq : (f a).Dom), (f a).get ⋯ = x

Tactic:
simp only [← exists_prop]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α →. β
inst✝ : (x : α) → Decidable (f x).Dom
s : Finset α
⊢ pimage f s = image (fun x => (f ↑x).get ⋯) (filter (fun x => (f x).Dom) s).attach

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α →. β
inst✝ : (x : α) → Decidable (f x).Dom
s : Finset α
x : β
⊢ x ∈ pimage f s ↔ x ∈ image (fun x => (f ↑x).get ⋯) (filter (fun x => (f x).Dom) s).attach

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α →. β
inst✝ : (x : α) → Decidable (f x).Dom
s : Finset α
x : β
⊢ x ∈ pimage f s ↔ x ∈ image (fun x => (f ↑x).get ⋯) (filter (fun x => (f x).Dom) s).attach

Tactic:
simp [Part.mem_eq, And.exists]

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α →. β
inst✝ : (x : α) → Decidable (f x).Dom
s : Finset α
x : β
⊢ (∃ a ∈ s, ∃ (h : (f a).Dom), (f a).get h = x) ↔ ∃ a, ∃ (hp : a ∈ s) (hq : (f a).Dom), (f a).get ⋯ = x