harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Extension/Linear.lean
theorem extend_partialOrder {α : Type u} (r : α → α → Prop) [IsPartialOrder α r] :
    ∃ s : α → α → Prop, IsLinearOrder α s ∧ r ≤ s

Proof state:
case refine_3.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 => x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
⊢ x = y

Tactic:
haveI : IsPartialOrder _ _ := hc₁ h₁s₁

Result:
case refine_3.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 => x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this✝ : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this : IsPartialOrder α s₁
⊢ x = y

Proof state:
case refine_3
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 => x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∀ (a b : α), (∃ r ∈ c, r a b) → (∃ r ∈ c, r b a) → a = b

Tactic:
rintro x y ⟨s₁, h₁s₁, h₂s₁⟩ ⟨s₂, h₁s₂, h₂s₂⟩

Result:
case refine_3.intro.intro.intro.intro
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 => x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
⊢ x = y

Proof state:
case refine_2.inl.inl
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x => x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
s' : α → α → Prop := fun x' y' => s x' y' ∨ s x' x ∧ s y y'
a b : α
ab : s a b
ba : s b a
⊢ a = b

Tactic:
exact antisymm ab ba

Result:
no goals

Proof state:
case refine_3.intro.intro.intro.intro.inr
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 => x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this✝¹ : IsPreorder α s
x y : α
s₁ : α → α → Prop
h₁s₁ : s₁ ∈ c
h₂s₁ : s₁ x y
s₂ : α → α → Prop
h₁s₂ : s₂ ∈ c
h₂s₂ : s₂ y x
this✝ : IsPartialOrder α s₁
this : IsPartialOrder α s₂
h : s₂ ≤ s₁
⊢ x = y

Tactic:
apply antisymm h₂s₁ (h _ _ h₂s₂)

Result:
no goals
-- Mathlib/Algebra/Star/Unitary.lean
theorem star_mem {U : R} (hU : U ∈ unitary R) : star U ∈ unitary R :=
  ⟨by rw [star_star, mul_star_self_of_mem hU], by rw [star_star, star_mul_self_of_mem hU]⟩

Proof state:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U : R
hU : U ∈ unitary R
⊢ star (star U) * star U = 1

Tactic:
rw [star_star, mul_star_self_of_mem hU]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
U : R
hU : U ∈ unitary R
⊢ star U * star (star U) = 1

Tactic:
rw [star_star, star_mul_self_of_mem hU]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_preimage_eq_range_inter {f : α → β} {t : Set β} : f '' (f ⁻¹' t) = range f ∩ t :=
  ext fun x =>
    ⟨fun ⟨_, hx, HEq⟩ => HEq ▸ ⟨mem_range_self _, hx⟩, fun ⟨⟨y, h_eq⟩, hx⟩ =>
      h_eq ▸ mem_image_of_mem f <| show y ∈ f ⁻¹' t by rw [preimage, mem_setOf, h_eq]; exact hx⟩

Proof state:
α : Type u_1
β : Type u_2
f : α → β
t : Set β
x : β
x✝ : x ∈ range f ∩ t
y : α
h_eq : f y = x
hx : x ∈ t
⊢ x ∈ t

Tactic:
exact hx

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
t : Set β
x : β
x✝ : x ∈ range f ∩ t
y : α
h_eq : f y = x
hx : x ∈ t
⊢ y ∈ f ⁻¹' t

Tactic:
rw [preimage, mem_setOf, h_eq]

Result:
α : Type u_1
β : Type u_2
f : α → β
t : Set β
x : β
x✝ : x ∈ range f ∩ t
y : α
h_eq : f y = x
hx : x ∈ t
⊢ x ∈ t
-- Mathlib/Data/Fin/Tuple/Finset.lean
lemma insertNth_mem_piFinset_insertNth {x_pivot : α p} {x_remove : ∀ i, α (succAbove p i)}
    {s_pivot : Finset (α p)} {s_remove : ∀ i, Finset (α (succAbove p i))} :
    insertNth p x_pivot x_remove ∈ piFinset (insertNth p s_pivot s_remove) ↔
      x_pivot ∈ s_pivot ∧ x_remove ∈ piFinset s_remove

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
p : Fin (n + 1)
x_pivot : α p
x_remove : (i : Fin n) → α (p.succAbove i)
s_pivot : Finset (α p)
s_remove : (i : Fin n) → Finset (α (p.succAbove i))
⊢ p.insertNth x_pivot x_remove ∈ piFinset (p.insertNth s_pivot s_remove) ↔
    x_pivot ∈ s_pivot ∧ x_remove ∈ piFinset s_remove

Tactic:
simp [mem_piFinset_iff_pivot_removeNth p]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Basic.lean
theorem toSubalgebra_toIntermediateField (S : Subalgebra K L) (inv_mem : ∀ x ∈ S, x⁻¹ ∈ S) :
    (S.toIntermediateField inv_mem).toSubalgebra = S

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : Subalgebra K L
inv_mem : ∀ x ∈ S, x⁻¹ ∈ S
x✝ : L
⊢ x✝ ∈ (S.toIntermediateField inv_mem).toSubalgebra ↔ x✝ ∈ S

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : Subalgebra K L
inv_mem : ∀ x ∈ S, x⁻¹ ∈ S
⊢ (S.toIntermediateField inv_mem).toSubalgebra = S

Tactic:
ext

Result:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : Subalgebra K L
inv_mem : ∀ x ∈ S, x⁻¹ ∈ S
x✝ : L
⊢ x✝ ∈ (S.toIntermediateField inv_mem).toSubalgebra ↔ x✝ ∈ S
-- Mathlib/Order/Filter/Map.lean
theorem compl_mem_kernMap {s : Set β} : sᶜ ∈ kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = s

Proof state:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
⊢ sᶜ ∈ kernMap m f ↔ ∃ t, tᶜ ∈ f ∧ m '' t = s

Tactic:
simp_rw [mem_kernMap_iff_compl, compl_compl]

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma IsAffineOpen.fromSpec_image_zeroLocus {X : Scheme.{u}} {U : X.Opens}
    (hU : IsAffineOpen U) (s : Set Γ(X, U)) :
    hU.fromSpec.base '' PrimeSpectrum.zeroLocus s = X.zeroLocus s ∩ U

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⇑(ConcreteCategory.hom hU.fromSpec.base) '' PrimeSpectrum.zeroLocus s = X.zeroLocus s ∩ ↑U

Tactic:
rw [← hU.fromSpec_preimage_zeroLocus, Set.image_preimage_eq_inter_range, range_fromSpec]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem chaar_sup_eq {K₀ : PositiveCompacts G}
    {K₁ K₂ : Compacts G} (h : Disjoint K₁.1 K₂.1) (h₂ : IsClosed K₂.1) :
    chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂

Proof state:
case intro.intro.intro.intro.hU
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen U₁
h1U₂ : IsOpen U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ ↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ }.toOpens
h2U : IsOpen U
h3U : 1 ∈ U
⊢ U.Nonempty

Tactic:
exact ⟨1, h3U⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.h.refine_2
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₀ : PositiveCompacts G
K₁ K₂ : Compacts G
h : Disjoint K₁.carrier K₂.carrier
h₂ : IsClosed K₂.carrier
U₁ U₂ : Set G
h1U₁ : IsOpen U₁
h1U₂ : IsOpen U₂
h2U₁ : K₁.carrier ⊆ U₁
h2U₂ : K₂.carrier ⊆ U₂
hU : Disjoint U₁ U₂
L₁ : Set G
h1L₁ : L₁ ∈ 𝓝 1
V₁ : Set G
h1V₁ : V₁ ⊆ L₁
h2V₁ : IsOpen V₁
h3V₁ : 1 ∈ V₁
h2L₁ : K₁.carrier * V₁ ⊆ U₁
L₂ : Set G
h1L₂ : L₂ ∈ 𝓝 1
V₂ : Set G
h1V₂ : V₂ ⊆ L₂
h2V₂ : IsOpen V₂
h3V₂ : 1 ∈ V₂
h2L₂ : K₂.carrier * V₂ ⊆ U₂
eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)
this : Continuous eval
V : Set G := V₁ ∩ V₂
U : Set G
h1U : U ⊆ ↑{ carrier := V⁻¹, is_open' := ⋯, mem' := ⋯ }.toOpens
h2U : IsOpen U
h3U : 1 ∈ U
⊢ U⁻¹ ⊆ V₂

Tactic:
exact Subset.trans (inv_subset.mpr h1U) inter_subset_right

Result:
no goals
-- Mathlib/CategoryTheory/Equivalence.lean
theorem changeFunctor_refl (e : C ≌ D) : e.changeFunctor (Iso.refl _) = e

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
⊢ e.changeFunctor (Iso.refl e.functor) = e

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
private lemma toAffine_negAddY_of_eq {P : Fin 3 → F} (hPz : P z ≠ 0) {n d : F} (hd : d ≠ 0) :
    W.toAffine.negAddY (P x / P z) (P x / P z) (P y / P z) (-n / P z / d) =
      (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2
          - P x * P z * d ^ 2) + P y * P z ^ 2 * d ^ 3) / P z ^ 2 / (P z * d ^ 3)

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ -n / P z / d *
        ((n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2) * d / P z / (P z * d ^ 3) -
          P x / P z) +
      P y / P z =
    (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2 - P x * P z * d ^ 2) +
          P y * P z ^ 2 * d ^ 3) /
        P z ^ 2 /
      (P z * d ^ 3)

Tactic:
field_simp [mul_ne_zero hPz <| mul_ne_zero hPz <| pow_ne_zero 3 hd]

Result:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ (-(n *
              ((n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2) * d * P z -
                P z * (P z * d ^ 3) * P x) *
            P z) +
        P y * (P z * d * (P z * (P z * d ^ 3) * P z))) *
      (P z ^ 2 * (P z * d ^ 3)) =
    (-(n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2 - P x * P z * d ^ 2)) +
        P y * P z ^ 2 * d ^ 3) *
      (P z * d * (P z * (P z * d ^ 3) * P z) * P z)

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ (toAffine W).negAddY (P x / P z) (P x / P z) (P y / P z) (-n / P z / d) =
    (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2 - P x * P z * d ^ 2) +
          P y * P z ^ 2 * d ^ 3) /
        P z ^ 2 /
      (P z * d ^ 3)

Tactic:
rw [Affine.negAddY, toAffine_addX_of_eq hPz hd]

Result:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ -n / P z / d *
        ((n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2) * d / P z / (P z * d ^ 3) -
          P x / P z) +
      P y / P z =
    (-n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2 - P x * P z * d ^ 2) +
          P y * P z ^ 2 * d ^ 3) /
        P z ^ 2 /
      (P z * d ^ 3)

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
n d : F
hd : d ≠ 0
⊢ (-(n *
              ((n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2) * d * P z -
                P z * (P z * d ^ 3) * P x) *
            P z) +
        P y * (P z * d * (P z * (P z * d ^ 3) * P z))) *
      (P z ^ 2 * (P z * d ^ 3)) =
    (-(n * (n ^ 2 - W.a₁ * n * P z * d - W.a₂ * P z ^ 2 * d ^ 2 - 2 * P x * P z * d ^ 2 - P x * P z * d ^ 2)) +
        P y * P z ^ 2 * d ^ 3) *
      (P z * d * (P z * (P z * d ^ 3) * P z) * P z)

Tactic:
ring1

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem adjugate_fin_succ_eq_det_submatrix {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) α) (i j) :
    adjugate A i j = (-1) ^ (j + i : ℕ) * det (A.submatrix j.succAbove i.succAbove)

Proof state:
α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j : Fin n.succ
⊢ A.adjugate i j = (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det

Tactic:
simp_rw [adjugate_apply, det_succ_row _ j, updateRow_self, submatrix_updateRow_succAbove]

Result:
α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j : Fin n.succ
⊢ ∑ x : Fin n.succ, (-1) ^ (↑j + ↑x) * Pi.single i 1 x * (A.submatrix j.succAbove x.succAbove).det =
    (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det

Proof state:
α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j : Fin n.succ
⊢ ∑ x : Fin n.succ, (-1) ^ (↑j + ↑x) * Pi.single i 1 x * (A.submatrix j.succAbove x.succAbove).det =
    (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det

Tactic:
rw [Fintype.sum_eq_single i fun h hjk => ?_, Pi.single_eq_same, mul_one]

Result:
α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j h : Fin n.succ
hjk : h ≠ i
⊢ (-1) ^ (↑j + ↑h) * Pi.single i 1 h * (A.submatrix j.succAbove h.succAbove).det = 0

Proof state:
α : Type w
inst✝ : CommRing α
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) α
i j h : Fin n.succ
hjk : h ≠ i
⊢ (-1) ^ (↑j + ↑h) * Pi.single i 1 h * (A.submatrix j.succAbove h.succAbove).det = 0

Tactic:
rw [Pi.single_eq_of_ne hjk, mul_zero, zero_mul]

Result:
no goals
-- Mathlib/Analysis/Convex/Basic.lean
theorem convex_stdSimplex : Convex 𝕜 (stdSimplex 𝕜 ι)

Proof state:
case refine_2
𝕜 : Type u_1
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x : ι, (a • f + b • g) x = 1

Tactic:
erw [Finset.sum_add_distrib]

Result:
case refine_2
𝕜 : Type u_1
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x : ι, (a • f) x + ∑ x : ι, (b • g) x = 1

Proof state:
case refine_2
𝕜 : Type u_1
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x : ι, (a • f) x + ∑ x : ι, (b • g) x = 1

Tactic:
simp only [Pi.smul_apply]

Result:
case refine_2
𝕜 : Type u_1
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x : ι, a • f x + ∑ x : ι, b • g x = 1

Proof state:
𝕜 : Type u_1
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
⊢ Convex 𝕜 (stdSimplex 𝕜 ι)

Tactic:
refine fun f hf g hg a b ha hb hab => ⟨fun x => ?_, ?_⟩

Result:
case refine_1
𝕜 : Type u_1
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x : ι
⊢ 0 ≤ (a • f + b • g) x

case refine_2
𝕜 : Type u_1
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x : ι, (a • f + b • g) x = 1

Proof state:
case refine_2
𝕜 : Type u_1
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∑ x : ι, a • f x + ∑ x : ι, b • g x = 1

Tactic:
rw [← Finset.smul_sum, ← Finset.smul_sum, hf.2, hg.2, smul_eq_mul,
  smul_eq_mul, mul_one, mul_one]

Result:
case refine_2
𝕜 : Type u_1
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a + b = 1

Proof state:
case refine_1
𝕜 : Type u_1
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
x : ι
⊢ 0 ≤ (a • f + b • g) x

Tactic:
apply_rules [add_nonneg, mul_nonneg, hf.1, hg.1]

Result:
no goals

Proof state:
case refine_2
𝕜 : Type u_1
ι : Type u_5
inst✝¹ : OrderedSemiring 𝕜
inst✝ : Fintype ι
f : ι → 𝕜
hf : f ∈ stdSimplex 𝕜 ι
g : ι → 𝕜
hg : g ∈ stdSimplex 𝕜 ι
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a + b = 1

Tactic:
exact hab

Result:
no goals
-- Mathlib/Order/OrdContinuous.lean
theorem comp (hg : LeftOrdContinuous g) (hf : LeftOrdContinuous f) : LeftOrdContinuous (g ∘ f) :=
  fun s x h => by simpa only [image_image] using hg (hf h)

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
g : β → γ
f : α → β
hg : LeftOrdContinuous g
hf : LeftOrdContinuous f
s : Set α
x : α
h : IsLUB s x
⊢ IsLUB (g ∘ f '' s) ((g ∘ f) x)

Tactic:
simpa only [image_image] using hg (hf h)

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/InnerDual.lean
theorem innerDualCone_univ : (univ : Set H).innerDualCone = 0

Proof state:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
this : ∀ x ∈ univ.innerDualCone, x = 0
⊢ univ.innerDualCone = 0

Tactic:
apply SetLike.coe_injective

Result:
case a
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
this : ∀ x ∈ univ.innerDualCone, x = 0
⊢ ↑univ.innerDualCone = ↑0

Proof state:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
⊢ ∀ x ∈ univ.innerDualCone, x = 0

Tactic:
exact fun x hx => by simpa [← real_inner_self_nonpos] using hx (-x) (mem_univ _)

Result:
no goals

Proof state:
case a
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
this : ∀ x ∈ univ.innerDualCone, x = 0
⊢ ↑univ.innerDualCone = ↑0

Tactic:
exact eq_singleton_iff_unique_mem.mpr ⟨fun x _ => (inner_zero_right _).ge, this⟩

Result:
no goals

Proof state:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
x : H
hx : x ∈ univ.innerDualCone
⊢ x = 0

Tactic:
simpa [← real_inner_self_nonpos] using hx (-x) (mem_univ _)

Result:
no goals

Proof state:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
⊢ univ.innerDualCone = 0

Tactic:
suffices ∀ x : H, x ∈ (univ : Set H).innerDualCone → x = 0 by
  apply SetLike.coe_injective
  exact eq_singleton_iff_unique_mem.mpr ⟨fun x _ => (inner_zero_right _).ge, this⟩

Result:
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
⊢ ∀ x ∈ univ.innerDualCone, x = 0
-- Mathlib/Algebra/Category/Grp/Zero.lean
theorem isZero_of_subsingleton (G : CommGrp) [Subsingleton G] : IsZero G

Proof state:
G : CommGrp
inst✝ : Subsingleton ↑G
⊢ IsZero G

Tactic:
refine ⟨fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨1⟩, fun f => ?_⟩⟩⟩

Result:
case refine_1
G : CommGrp
inst✝ : Subsingleton ↑G
X : CommGrp
f : G ⟶ X
⊢ f = default

case refine_2
G : CommGrp
inst✝ : Subsingleton ↑G
X : CommGrp
f : X ⟶ G
⊢ f = default

Proof state:
case refine_1.hf.h
G : CommGrp
inst✝ : Subsingleton ↑G
X : CommGrp
f : G ⟶ X
x : ↑G
this : x = 1
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
rw [this, map_one, map_one]

Result:
no goals

Proof state:
case refine_1.hf.h
G : CommGrp
inst✝ : Subsingleton ↑G
X : CommGrp
f : G ⟶ X
x : ↑G
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
have : x = 1 := Subsingleton.elim _ _

Result:
case refine_1.hf.h
G : CommGrp
inst✝ : Subsingleton ↑G
X : CommGrp
f : G ⟶ X
x : ↑G
this : x = 1
⊢ (Hom.hom f) x = (Hom.hom default) x

Proof state:
case refine_2
G : CommGrp
inst✝ : Subsingleton ↑G
X : CommGrp
f : X ⟶ G
⊢ f = default

Tactic:
ext

Result:
case refine_2.hf.h
G : CommGrp
inst✝ : Subsingleton ↑G
X : CommGrp
f : X ⟶ G
x✝ : ↑X
⊢ (Hom.hom f) x✝ = (Hom.hom default) x✝

Proof state:
case refine_2.hf.h
G : CommGrp
inst✝ : Subsingleton ↑G
X : CommGrp
f : X ⟶ G
x✝ : ↑X
⊢ (Hom.hom f) x✝ = (Hom.hom default) x✝

Tactic:
subsingleton

Result:
no goals

Proof state:
case refine_1
G : CommGrp
inst✝ : Subsingleton ↑G
X : CommGrp
f : G ⟶ X
⊢ f = default

Tactic:
ext x

Result:
case refine_1.hf.h
G : CommGrp
inst✝ : Subsingleton ↑G
X : CommGrp
f : G ⟶ X
x : ↑G
⊢ (Hom.hom f) x = (Hom.hom default) x
-- Mathlib/Order/Basic.lean
lemma mk_lt_mk_of_le_of_lt (h₁ : a₁ ≤ a₂) (h₂ : b₁ < b₂) : (a₁, b₁) < (a₂, b₂)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
h₁ : a₁ ≤ a₂
h₂ : b₁ < b₂
⊢ (a₁, b₁) < (a₂, b₂)

Tactic:
simp [lt_iff, *]

Result:
no goals
-- Mathlib/Order/Monotone/Basic.lean
theorem StrictMonoOn.eq_iff_eq (hf : StrictMonoOn f s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) :
    f a = f b ↔ a = b :=
  ⟨fun h ↦ le_antisymm ((hf.le_iff_le ha hb).mp h.le) ((hf.le_iff_le hb ha).mp h.ge), by
    rintro rfl
    rfl⟩

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a : α
ha hb : a ∈ s
⊢ f a = f a

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b → f a = f b

Tactic:
rintro rfl

Result:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a : α
ha hb : a ∈ s
⊢ f a = f a
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/LawfulVecOperator.lean
theorem isPrefix_aig (aig : AIG α) (input : β aig len) :
    IsPrefix aig.decls (f aig input).aig.decls

Proof state:
case idx_eq
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (f aig input).aig.decls[idx] = aig.decls[idx]

Tactic:
intro idx h

Result:
case idx_eq
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
idx : Nat
h : idx < aig.decls.size
⊢ (f aig input).aig.decls[idx] = aig.decls[idx]

Proof state:
case idx_eq
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
idx : Nat
h : idx < aig.decls.size
⊢ (f aig input).aig.decls[idx] = aig.decls[idx]

Tactic:
apply decl_eq

Result:
no goals

Proof state:
case size_le
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ aig.decls.size ≤ (f aig input).aig.decls.size

Tactic:
apply le_size

Result:
no goals

Proof state:
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ IsPrefix aig.decls (f aig input).aig.decls

Tactic:
apply IsPrefix.of

Result:
case idx_eq
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (f aig input).aig.decls[idx] = aig.decls[idx]

case size_le
α : Type
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Nat → Type
f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len
inst✝ : LawfulVecOperator α β fun {len} => f
len : Nat
aig : AIG α
input : β aig len
⊢ aig.decls.size ≤ (f aig input).aig.decls.size