harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
theorem cocyclesMap_comp_isoZeroCocycles_hom :
    cocyclesMap f φ 0 ≫ (isoZeroCocycles B).hom = (isoZeroCocycles A).hom ≫ H0Map f φ

Proof state:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
⊢ cocyclesMap f φ 0 ≫ (isoZeroCocycles B).hom = (isoZeroCocycles A).hom ≫ H0Map f φ

Tactic:
rw [← Iso.eq_comp_inv, Category.assoc, ← Iso.inv_comp_eq, ← cancel_mono (iCocycles _ _)]

Result:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
⊢ ((isoZeroCocycles A).inv ≫ cocyclesMap f φ 0) ≫ iCocycles B 0 = (H0Map f φ ≫ (isoZeroCocycles B).inv) ≫ iCocycles B 0

Proof state:
case hf.h.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑(H0 A)
x✝ : Fin 0 → G
this :
  (ConcreteCategory.hom ((zeroCochainsLequiv A).toModuleIso.inv ≫ (cochainsMap f φ).f 0)) ↑x =
    (ConcreteCategory.hom (φ.hom ≫ (zeroCochainsLequiv B).toModuleIso.inv)) ↑x
⊢ (ModuleCat.Hom.hom (((isoZeroCocycles A).inv ≫ cocyclesMap f φ 0) ≫ iCocycles B 0)) x x✝ =
    (ModuleCat.Hom.hom ((H0Map f φ ≫ (isoZeroCocycles B).inv) ≫ iCocycles B 0)) x x✝

Tactic:
simp_all

Result:
no goals

Proof state:
case hf.h.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑(H0 A)
x✝ : Fin 0 → G
⊢ (ModuleCat.Hom.hom (((isoZeroCocycles A).inv ≫ cocyclesMap f φ 0) ≫ iCocycles B 0)) x x✝ =
    (ModuleCat.Hom.hom ((H0Map f φ ≫ (isoZeroCocycles B).inv) ≫ iCocycles B 0)) x x✝

Tactic:
have := congr($((CommSq.vert_inv ⟨cochainsMap_f_0_comp_zeroCochainsLequiv f φ⟩).w.symm) x)

Result:
case hf.h.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑(H0 A)
x✝ : Fin 0 → G
this :
  (ConcreteCategory.hom ((zeroCochainsLequiv A).toModuleIso.inv ≫ (cochainsMap f φ).f 0)) ↑x =
    (ConcreteCategory.hom (φ.hom ≫ (zeroCochainsLequiv B).toModuleIso.inv)) ↑x
⊢ (ModuleCat.Hom.hom (((isoZeroCocycles A).inv ≫ cocyclesMap f φ 0) ≫ iCocycles B 0)) x x✝ =
    (ModuleCat.Hom.hom ((H0Map f φ ≫ (isoZeroCocycles B).inv) ≫ iCocycles B 0)) x x✝

Proof state:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
⊢ ((isoZeroCocycles A).inv ≫ cocyclesMap f φ 0) ≫ iCocycles B 0 = (H0Map f φ ≫ (isoZeroCocycles B).inv) ≫ iCocycles B 0

Tactic:
ext x

Result:
case hf.h.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑(H0 A)
x✝ : Fin 0 → G
⊢ (ModuleCat.Hom.hom (((isoZeroCocycles A).inv ≫ cocyclesMap f φ 0) ≫ iCocycles B 0)) x x✝ =
    (ModuleCat.Hom.hom ((H0Map f φ ≫ (isoZeroCocycles B).inv) ≫ iCocycles B 0)) x x✝
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem gcd_isUnit_iff (x y : R) : IsUnit (gcd x y) ↔ IsCoprime x y

Proof state:
R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
x y : R
⊢ IsUnit (gcd x y) ↔ IsCoprime x y

Tactic:
rw [IsCoprime, ← Ideal.mem_span_pair, ← span_gcd, ← span_singleton_eq_top, eq_top_iff_one]

Result:
no goals
-- Mathlib/Analysis/Convex/Birkhoff.lean
/--
If M is a doubly stochastic matrix, then it is an convex combination of permutation matrices. Note
`doublyStochastic_eq_convexHull_permMatrix` shows `doublyStochastic n` is exactly the convex hull of
the permutation matrices, and this lemma is instead most useful for accessing the coefficients of
each permutation matrices directly.
-/
lemma exists_eq_sum_perm_of_mem_doublyStochastic (hM : M ∈ doublyStochastic R n) :
    ∃ w : Equiv.Perm n → R, (∀ σ, 0 ≤ w σ) ∧ ∑ σ, w σ = 1 ∧ ∑ σ, w σ • σ.permMatrix R = M

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
h✝ : Nonempty n
w : Equiv.Perm n → R
hw1 : ∀ (σ : Equiv.Perm n), 0 ≤ w σ
hw3 : ∑ σ : Equiv.Perm n, w σ • Equiv.Perm.permMatrix R σ = M
inhabited_h : Inhabited n
⊢ ∑ x : n, M default x = 1

Tactic:
rw [sum_row_of_mem_doublyStochastic hM]

Result:
no goals

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
h✝ : Nonempty n
⊢ 0 ≤ 1

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
h✝ : IsEmpty n
⊢ ∀ (σ : Equiv.Perm n), 0 ≤ (fun x => 1) σ

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : LinearOrderedField R
M : Matrix n n R
hM : M ∈ doublyStochastic R n
h✝ : IsEmpty n
⊢ ∑ σ : Equiv.Perm n, (fun x => 1) σ = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Cover.lean
/-- If `a < b` then there exist `a' > a` and `b' < b` such that `Set.Iio a'` is strictly to the left
of `Set.Ioi b'`. -/
lemma LT.lt.exists_disjoint_Iio_Ioi (h : a < b) :
    ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
h' : ¬a ⋖ b
⊢ ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y

Tactic:
rcases h.exists_lt_lt h' with ⟨c, ha, hb⟩

Result:
case neg.intro.intro
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
h' : ¬a ⋖ b
c : α
ha : a < c
hb : c < b
⊢ ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y

Proof state:
case neg.intro.intro
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
h' : ¬a ⋖ b
c : α
ha : a < c
hb : c < b
⊢ ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y

Tactic:
exact ⟨c, ha, c, hb, fun _ h₁ _ => lt_trans h₁⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y

Tactic:
by_cases h' : a ⋖ b

Result:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
h' : a ⋖ b
⊢ ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y

case neg
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
h' : ¬a ⋖ b
⊢ ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
h' : a ⋖ b
⊢ ∃ a' > a, ∃ b' < b, ∀ x < a', ∀ y > b', x < y

Tactic:
exact ⟨b, h, a, h, fun x hx y hy => hx.trans_le <| h'.ge_of_gt hy⟩

Result:
no goals
-- Mathlib/Topology/Bases.lean
lemma IsTopologicalBasis.subset_of_forall_subset {t : Set α} (hB : IsTopologicalBasis B)
    (hs : IsOpen s) (h : ∀ U ∈ B, U ⊆ s → U ⊆ t) : s ⊆ t

Proof state:
α : Type u
t✝ : TopologicalSpace α
B : Set (Set α)
s t : Set α
hB : IsTopologicalBasis B
hs : IsOpen s
h : ∀ U ∈ B, U ⊆ s → U ⊆ t
⊢ ⋃₀ {s_1 | s_1 ∈ B ∧ s_1 ⊆ s} ⊆ t

Tactic:
simpa [sUnion_subset_iff]

Result:
no goals

Proof state:
α : Type u
t✝ : TopologicalSpace α
B : Set (Set α)
s t : Set α
hB : IsTopologicalBasis B
hs : IsOpen s
h : ∀ U ∈ B, U ⊆ s → U ⊆ t
⊢ s ⊆ t

Tactic:
rw [hB.open_eq_sUnion' hs]

Result:
α : Type u
t✝ : TopologicalSpace α
B : Set (Set α)
s t : Set α
hB : IsTopologicalBasis B
hs : IsOpen s
h : ∀ U ∈ B, U ⊆ s → U ⊆ t
⊢ ⋃₀ {s_1 | s_1 ∈ B ∧ s_1 ⊆ s} ⊆ t
-- Mathlib/CategoryTheory/Subobject/Comma.lean
theorem lift_projectQuotient [HasFiniteColimits C] [PreservesFiniteColimits S]
    {A : CostructuredArrow S T} :
    ∀ (P : Subobject (op A)) {q} (hq : S.map (projectQuotient P).arrow.unop ≫ q = A.hom),
      liftQuotient (projectQuotient P) hq = P :=
  Subobject.ind _
    (by
      intro P f hf q hq
      fapply Subobject.mk_eq_mk_of_comm
      · refine (Iso.op (isoMk ?_ ?_) : _ ≅ op (unop P))
        · exact (Subobject.underlyingIso f.unop.left.op).unop
        · refine (cancel_epi (S.map f.unop.left)).1 ?_
          simpa [← Category.assoc, ← S.map_comp] using hq
      · exact Quiver.Hom.unop_inj (by simp))

Proof state:
case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
hf : Mono f
q : S.obj (unop (Subobject.underlying.obj (projectQuotient (Subobject.mk f)))) ⟶ (Functor.fromPUnit T).obj A.right
hq : S.map (projectQuotient (Subobject.mk f)).arrow.unop ≫ q = A.hom
⊢ (isoMk (Subobject.underlyingIso f.unop.left.op).unop ⋯).op.hom ≫ f =
    (homMk (projectQuotient (Subobject.mk f)).arrow.unop hq).op

Tactic:
exact Quiver.Hom.unop_inj (by simp)

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem blockTriangular_stdBasisMatrix {i j : m} (hij : b i ≤ b j) (c : R) :
    BlockTriangular (stdBasisMatrix i j c) b

Proof state:
case h.intro
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq m
i j : m
hij : b i ≤ b j
c : R
hrs : b j < b i
⊢ False

Tactic:
exact (hij.trans_lt hrs).false

Result:
no goals

Proof state:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq m
i j : m
hij : b i ≤ b j
c : R
⊢ (stdBasisMatrix i j c).BlockTriangular b

Tactic:
intro r s hrs

Result:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq m
i j : m
hij : b i ≤ b j
c : R
r s : m
hrs : b s < b r
⊢ stdBasisMatrix i j c r s = 0

Proof state:
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq m
i j : m
hij : b i ≤ b j
c : R
r s : m
hrs : b s < b r
⊢ stdBasisMatrix i j c r s = 0

Tactic:
apply StdBasisMatrix.apply_of_ne

Result:
case h
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq m
i j : m
hij : b i ≤ b j
c : R
r s : m
hrs : b s < b r
⊢ ¬(i = r ∧ j = s)

Proof state:
case h
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq m
i j : m
hij : b i ≤ b j
c : R
r s : m
hrs : b s < b r
⊢ ¬(i = r ∧ j = s)

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case h.intro
α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq m
i j : m
hij : b i ≤ b j
c : R
hrs : b j < b i
⊢ False
-- Mathlib/Data/Fintype/Defs.lean
theorem coe_univ : ↑(univ : Finset α) = (Set.univ : Set α)

Proof state:
α : Type u_1
inst✝ : Fintype α
⊢ ↑univ = Set.univ

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : Fintype α
x✝ : α
⊢ x✝ ∈ ↑univ ↔ x✝ ∈ Set.univ

Proof state:
case h
α : Type u_1
inst✝ : Fintype α
x✝ : α
⊢ x✝ ∈ ↑univ ↔ x✝ ∈ Set.univ

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/FiniteType.lean
nonrec lemma LocallyOfFiniteType.jacobsonSpace
  (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace Y] : JacobsonSpace X

Proof state:
case intro
R : CommRingCat
inst✝¹ : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
S : CommRingCat
f : Spec S ⟶ Spec R
inst✝ : LocallyOfFiniteType f
⊢ JacobsonSpace ↑↑(Spec S).toPresheafedSpace

Tactic:
obtain ⟨φ, rfl : Spec.map φ = f⟩ := Spec.homEquiv.symm.surjective f

Result:
case intro.intro
R : CommRingCat
inst✝¹ : JacobsonSpace ↑↑(Spec R).toPresheafedSpace
S : CommRingCat
φ : R ⟶ S
inst✝ : LocallyOfFiniteType (Spec.map φ)
⊢ JacobsonSpace ↑↑(Spec S).toPresheafedSpace
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem parallel_bot_iff_eq_bot {s : AffineSubspace k P} : s ∥ ⊥ ↔ s = ⊥

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : s ∥ ⊥
⊢ s = ⊥

Tactic:
rcases h with ⟨v, h⟩

Result:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
h : ⊥ = map (↑(constVAdd k P v)) s
⊢ s = ⊥

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
⊢ s ∥ ⊥ ↔ s = ⊥

Tactic:
refine ⟨fun h => ?_, fun h => h ▸ Parallel.refl _⟩

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : s ∥ ⊥
⊢ s = ⊥

Proof state:
case intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
h : ⊥ = map (↑(constVAdd k P v)) s
⊢ s = ⊥

Tactic:
rwa [eq_comm, map_eq_bot_iff] at h

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem pos_of_not_mem_negAt_plusPart (hx : x ∈ negAt s '' (plusPart A)) {w : {w // IsReal w}}
    (hw : w ∉ s) : 0 < x.1 w

Proof state:
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
x : mixedSpace K
hx : x ∈ ⇑(negAt s) '' plusPart A
w : { w // w.IsReal }
hw : w ∉ s
⊢ 0 < x.1 w

Tactic:
obtain ⟨y, hy, rfl⟩ := hx

Result:
case intro.intro
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
w : { w // w.IsReal }
hw : w ∉ s
y : mixedSpace K
hy : y ∈ plusPart A
⊢ 0 < ((negAt s) y).1 w

Proof state:
case intro.intro
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
w : { w // w.IsReal }
hw : w ∉ s
y : mixedSpace K
hy : y ∈ plusPart A
⊢ 0 < y.1 w

Tactic:
exact hy.2 w

Result:
no goals

Proof state:
case intro.intro
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
w : { w // w.IsReal }
hw : w ∉ s
y : mixedSpace K
hy : y ∈ plusPart A
⊢ 0 < ((negAt s) y).1 w

Tactic:
rw [negAt_apply_isReal_and_not_mem _ hw]

Result:
case intro.intro
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
A : Set (mixedSpace K)
w : { w // w.IsReal }
hw : w ∉ s
y : mixedSpace K
hy : y ∈ plusPart A
⊢ 0 < y.1 w
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem aroots_mul [CommRing S] [IsDomain S] [Algebra T S]
    [NoZeroSMulDivisors T S] {p q : T[X]} (hpq : p * q ≠ 0) :
    (p * q).aroots S = p.aroots S + q.aroots S

Proof state:
S : Type v
T : Type w
inst✝⁴ : CommRing T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : NoZeroSMulDivisors T S
p q : T[X]
hpq : p * q ≠ 0
⊢ (p * q).aroots S = p.aroots S + q.aroots S

Tactic:
suffices map (algebraMap T S) p * map (algebraMap T S) q ≠ 0 by
  rw [aroots_def, Polynomial.map_mul, roots_mul this]

Result:
S : Type v
T : Type w
inst✝⁴ : CommRing T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : NoZeroSMulDivisors T S
p q : T[X]
hpq : p * q ≠ 0
⊢ map (algebraMap T S) p * map (algebraMap T S) q ≠ 0

Proof state:
S : Type v
T : Type w
inst✝⁴ : CommRing T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : NoZeroSMulDivisors T S
p q : T[X]
hpq : p * q ≠ 0
this : map (algebraMap T S) p * map (algebraMap T S) q ≠ 0
⊢ (p * q).aroots S = p.aroots S + q.aroots S

Tactic:
rw [aroots_def, Polynomial.map_mul, roots_mul this]

Result:
no goals

Proof state:
S : Type v
T : Type w
inst✝⁴ : CommRing T
inst✝³ : CommRing S
inst✝² : IsDomain S
inst✝¹ : Algebra T S
inst✝ : NoZeroSMulDivisors T S
p q : T[X]
hpq : p * q ≠ 0
⊢ map (algebraMap T S) p * map (algebraMap T S) q ≠ 0

Tactic:
rwa [← Polynomial.map_mul, Polynomial.map_ne_zero_iff
  (FaithfulSMul.algebraMap_injective T S)]

Result:
no goals
-- Mathlib/Data/Multiset/FinsetOps.lean
theorem ndinter_cons_of_not_mem {a : α} (s : Multiset α) {t : Multiset α} (h : a ∉ t) :
    ndinter (a ::ₘ s) t = ndinter s t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Multiset α
h : a ∉ t
⊢ (a ::ₘ s).ndinter t = s.ndinter t

Tactic:
simp [ndinter, h]

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/Basic.lean
theorem convexHull_toCone_isLeast (s : Set E) :
    IsLeast { t : ConvexCone 𝕜 E | s ⊆ t } ((convex_convexHull 𝕜 s).toCone _)

Proof state:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ {t | s ⊆ ↑t} = {t | (convexHull 𝕜) s ⊆ ↑t}

Tactic:
ext t

Result:
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
t : ConvexCone 𝕜 E
⊢ t ∈ {t | s ⊆ ↑t} ↔ t ∈ {t | (convexHull 𝕜) s ⊆ ↑t}

Proof state:
case h.e'_3.h
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
t : ConvexCone 𝕜 E
⊢ t ∈ {t | s ⊆ ↑t} ↔ t ∈ {t | (convexHull 𝕜) s ⊆ ↑t}

Tactic:
exact ⟨fun h => convexHull_min h t.convex, (subset_convexHull 𝕜 s).trans⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ IsLeast {t | s ⊆ ↑t} (Convex.toCone ((convexHull 𝕜) s) ⋯)

Tactic:
convert (convex_convexHull 𝕜 s).toCone_isLeast using 1

Result:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ {t | s ⊆ ↑t} = {t | (convexHull 𝕜) s ⊆ ↑t}
-- Mathlib/Logic/Encodable/Basic.lean
theorem decode_prod_val (n : ℕ) :
    (@decode (α × β) _ n : Option (α × β))
      = (decode n.unpair.1).bind fun a => (decode n.unpair.2).map <| Prod.mk a

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β))
      ((decode (unpair n).1).bind fun a => Option.map (Sigma.mk a) (decode (unpair n).2)) =
    (decode (unpair n).1).bind fun a => Option.map (Prod.mk a) (decode (unpair n).2)

Tactic:
cases (decode n.unpair.1 : Option α) <;> cases (decode n.unpair.2 : Option β)
<;> rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ decode n = (decode (unpair n).1).bind fun a => Option.map (Prod.mk a) (decode (unpair n).2)

Tactic:
simp only [decode_ofEquiv, Equiv.symm_symm, decode_sigma_val]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
n : ℕ
⊢ Option.map (⇑(Equiv.sigmaEquivProd α β))
      ((decode (unpair n).1).bind fun a => Option.map (Sigma.mk a) (decode (unpair n).2)) =
    (decode (unpair n).1).bind fun a => Option.map (Prod.mk a) (decode (unpair n).2)
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem le_prod_of_submultiplicative_on_pred (f : M → N) (p : M → Prop) (h_one : f 1 = 1)
    (h_mul : ∀ x y, p x → p y → f (x * y) ≤ f x * f y) (hp_mul : ∀ x y, p x → p y → p (x * y))
    (g : ι → M) {s : Finset ι} (hs : ∀ i ∈ s, p (g i)) : f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Proof state:
case inr
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_one : f 1 = 1
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs : ∀ i ∈ s, p (g i)
hs_nonempty : s.Nonempty
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Tactic:
exact le_prod_nonempty_of_submultiplicative_on_pred f p h_mul hp_mul g s hs_nonempty hs

Result:
no goals

Proof state:
case inl
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_one : f 1 = 1
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
hs : ∀ i ∈ ∅, p (g i)
⊢ f (∏ i ∈ ∅, g i) ≤ ∏ i ∈ ∅, f (g i)

Tactic:
simp [h_one]

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_one : f 1 = 1
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs : ∀ i ∈ s, p (g i)
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hs_nonempty)

Result:
case inl
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_one : f 1 = 1
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
hs : ∀ i ∈ ∅, p (g i)
⊢ f (∏ i ∈ ∅, g i) ≤ ∏ i ∈ ∅, f (g i)

case inr
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
p : M → Prop
h_one : f 1 = 1
h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y
hp_mul : ∀ (x y : M), p x → p y → p (x * y)
g : ι → M
s : Finset ι
hs : ∀ i ∈ s, p (g i)
hs_nonempty : s.Nonempty
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_concat {w : Nat} {b : Bool} {x : BitVec w} :
    (x.concat b).msb = if 0 < w then x.msb else b

Proof state:
w : Nat
b : Bool
x : BitVec w
⊢ (x.concat b).msb = if 0 < w then x.msb else b

Tactic:
simp only [BitVec.msb, getMsbD_eq_getLsbD, Nat.zero_lt_succ, decide_true, Nat.add_one_sub_one,
  Nat.sub_zero, Bool.true_and]

Result:
w : Nat
b : Bool
x : BitVec w
⊢ (x.concat b).getLsbD w = if 0 < w then decide (0 < w) && x.getLsbD (w - 1) else b

Proof state:
case pos
w : Nat
b : Bool
x : BitVec w
h₀ : 0 < w
⊢ w = 0 → b = x.getLsbD (w - 1)

Tactic:
intro

Result:
case pos
w : Nat
b : Bool
x : BitVec w
h₀ : 0 < w
a✝ : w = 0
⊢ b = x.getLsbD (w - 1)

Proof state:
case neg
w : Nat
b : Bool
x : BitVec w
h₀ : ¬0 < w
⊢ (x.concat b).getLsbD w = if 0 < w then decide (0 < w) && x.getLsbD (w - 1) else b

Tactic:
simp [h₀, show w = 0 by omega]

Result:
no goals

Proof state:
w : Nat
b : Bool
x : BitVec w
⊢ (x.concat b).getLsbD w = if 0 < w then decide (0 < w) && x.getLsbD (w - 1) else b

Tactic:
by_cases h₀ : 0 < w

Result:
case pos
w : Nat
b : Bool
x : BitVec w
h₀ : 0 < w
⊢ (x.concat b).getLsbD w = if 0 < w then decide (0 < w) && x.getLsbD (w - 1) else b

case neg
w : Nat
b : Bool
x : BitVec w
h₀ : ¬0 < w
⊢ (x.concat b).getLsbD w = if 0 < w then decide (0 < w) && x.getLsbD (w - 1) else b

Proof state:
case pos
w : Nat
b : Bool
x : BitVec w
h₀ : 0 < w
a✝ : w = 0
⊢ b = x.getLsbD (w - 1)

Tactic:
omega

Result:
no goals

Proof state:
case pos
w : Nat
b : Bool
x : BitVec w
h₀ : 0 < w
⊢ (x.concat b).getLsbD w = if 0 < w then decide (0 < w) && x.getLsbD (w - 1) else b

Tactic:
simp only [Nat.lt_add_one, getLsbD_eq_getElem, getElem_concat, h₀, ↓reduceIte, decide_true,
  Bool.true_and, ite_eq_right_iff]

Result:
case pos
w : Nat
b : Bool
x : BitVec w
h₀ : 0 < w
⊢ w = 0 → b = x.getLsbD (w - 1)

Proof state:
w : Nat
b : Bool
x : BitVec w
h₀ : ¬0 < w
⊢ w = 0

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem ceil_add_le (a b : α) : ⌈a + b⌉₊ ≤ ⌈a⌉₊ + ⌈b⌉₊

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
⊢ ⌈a + b⌉₊ ≤ ⌈a⌉₊ + ⌈b⌉₊

Tactic:
rw [ceil_le, Nat.cast_add]

Result:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
⊢ a + b ≤ ↑⌈a⌉₊ + ↑⌈b⌉₊

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a b : α
⊢ a + b ≤ ↑⌈a⌉₊ + ↑⌈b⌉₊

Tactic:
gcongr <;> apply le_ceil

Result:
no goals
-- Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean
@[simp]
lemma re_extendTo𝕜'ₗ [ContinuousConstSMul 𝕜 E] (g : E →L[ℝ] ℝ) (x : E) : re ((extendTo𝕜'ₗ g) x : 𝕜)
    = g x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : RCLike 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
g : E →L[ℝ] ℝ
x : E
⊢ re ((extendTo𝕜'ₗ g) x) = g x

Tactic:
have h g (x : E) : extendTo𝕜'ₗ g x = ((g x : 𝕜) - (I : 𝕜) * (g ((I : 𝕜) • x) : 𝕜)) := rfl

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : RCLike 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
g : E →L[ℝ] ℝ
x : E
h : ∀ (g : E →L[ℝ] ℝ) (x : E), (extendTo𝕜'ₗ g) x = ↑(g x) - I * ↑(g (I • x))
⊢ re ((extendTo𝕜'ₗ g) x) = g x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : RCLike 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : IsScalarTower ℝ 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 E
g : E →L[ℝ] ℝ
x : E
h : ∀ (g : E →L[ℝ] ℝ) (x : E), (extendTo𝕜'ₗ g) x = ↑(g x) - I * ↑(g (I • x))
⊢ re ((extendTo𝕜'ₗ g) x) = g x

Tactic:
simp only [h , map_sub, ofReal_re, mul_re, I_re, zero_mul, ofReal_im, mul_zero,
  sub_self, sub_zero]

Result:
no goals