harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma map_add : (z + z').map Φ = z.map Φ + z'.map Φ

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
z z' : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
⊢ (z + z').map Φ = z.map Φ + z'.map Φ

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
@[simp] lemma lt_singleton : s < {a} ↔ s = 0

Proof state:
α : Type u_1
s : Multiset α
a : α
⊢ s < {a} ↔ s = 0

Tactic:
simp only [lt_iff_le_and_ne, le_singleton, or_and_right, Ne, and_not_self, or_false,
  and_iff_left_iff_imp]

Result:
α : Type u_1
s : Multiset α
a : α
⊢ s = 0 → ¬s = {a}

Proof state:
α : Type u_1
a : α
⊢ ¬0 = {a}

Tactic:
exact (singleton_ne_zero _).symm

Result:
no goals

Proof state:
α : Type u_1
s : Multiset α
a : α
⊢ s = 0 → ¬s = {a}

Tactic:
rintro rfl

Result:
α : Type u_1
a : α
⊢ ¬0 = {a}
-- Mathlib/Topology/Inseparable.lean
theorem ker_nhds_eq_specializes : (𝓝 x).ker = {y | y ⤳ x}

Proof state:
case h
X : Type u_1
inst✝ : TopologicalSpace X
x x✝ : X
⊢ x✝ ∈ (𝓝 x).ker ↔ x✝ ∈ {y | y ⤳ x}

Tactic:
simp [specializes_iff_pure, le_def]

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ (𝓝 x).ker = {y | y ⤳ x}

Tactic:
ext

Result:
case h
X : Type u_1
inst✝ : TopologicalSpace X
x x✝ : X
⊢ x✝ ∈ (𝓝 x).ker ↔ x✝ ∈ {y | y ⤳ x}
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem not_step_singleton : ∀ {p : α × Bool}, ¬Step [p] L
  | (a, b) => by simp [Step.cons_left_iff, not_step_nil]

Proof state:
α : Type u
L : List (α × Bool)
a : α
b : Bool
⊢ ¬Step [(a, b)] L

Tactic:
simp [Step.cons_left_iff, not_step_nil]

Result:
no goals
-- Mathlib/Order/OrderIsoNat.lean
theorem exists_covBy_seq_of_wellFoundedLT_wellFoundedGT (α) [Preorder α]
    [Nonempty α] [wfl : WellFoundedLT α] [wfg : WellFoundedGT α] :
    ∃ a : ℕ → α, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Proof state:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
a : ℕ → α := fun t => Nat.rec (⋯.min Set.univ hα) (fun _n a => if ha : IsMax a then a else next ha) t
⊢ ∃ a, IsMin (a 0) ∧ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
refine ⟨a, isMin_iff_forall_not_lt.mpr fun _ ↦ wfl.wf.not_lt_min _ hα trivial, ?_⟩

Result:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
a : ℕ → α := fun t => Nat.rec (⋯.min Set.univ hα) (fun _n a => if ha : IsMax a then a else next ha) t
⊢ ∃ n, IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Proof state:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
a : ℕ → α := fun t => Nat.rec (⋯.min Set.univ hα) (fun _n a => if ha : IsMax a then a else next ha) t
n : ℕ
hn : ¬IsMax (a n)
⊢ a n ⋖ if ha : IsMax (a n) then a n else next ha

Tactic:
rw [dif_neg hn]

Result:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → ¬IsMax a → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.univ.Nonempty
a : ℕ → α := fun t => Nat.rec (⋯.min Set.univ hα) (fun _n a => if ha : IsMax a then a else next ha) t
n : ℕ
hn : ¬IsMax (a n)
⊢ a n ⋖ next hn
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem eval_πs' {l : Products I} {o₁ o₂ : Ordinal} (h : o₁ ≤ o₂)
    (hlt : ∀ i ∈ l.val, ord I i < o₁) :
    πs' C h (l.eval (π C (ord I · < o₁))) = l.eval (π C (ord I · < o₂))

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hlt : ∀ i ∈ ↑l, ord I i < o₁
⊢ ((πs' C h) (eval (π C fun x => ord I x < o₁) l)).toFun = ⇑(eval (π C fun x => ord I x < o₂) l)

Tactic:
exact evalFacProps C (fun (i : I) ↦ ord I i < o₁) (fun (i : I) ↦ ord I i < o₂) hlt
  (fun _ hh ↦ lt_of_lt_of_le hh h)

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hlt : ∀ i ∈ ↑l, ord I i < o₁
⊢ (πs' C h) (eval (π C fun x => ord I x < o₁) l) = eval (π C fun x => ord I x < o₂) l

Tactic:
rw [← LocallyConstant.coe_inj, ← LocallyConstant.toFun_eq_coe]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hlt : ∀ i ∈ ↑l, ord I i < o₁
⊢ ((πs' C h) (eval (π C fun x => ord I x < o₁) l)).toFun = ⇑(eval (π C fun x => ord I x < o₂) l)
-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
@[simp]
lemma specTensorTo_base_fst (p : Spec T.tensor) :
    (pullback.fst f g).base (T.SpecTensorTo.base p) = T.x

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (ConcreteCategory.hom (pullback.fst f g).base) ((ConcreteCategory.hom T.SpecTensorTo.base) p) = T.x

Tactic:
simp only [SpecTensorTo, residueFieldCongr_inv]

Result:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (ConcreteCategory.hom (pullback.fst f g).base)
      ((ConcreteCategory.hom
          (pullback.lift (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x)
              (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y) ⋯).base)
        p) =
    T.x

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (ConcreteCategory.hom
        (pullback.lift (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x)
              (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y) ⋯ ≫
            pullback.fst f g).base)
      p =
    T.x

Tactic:
simp

Result:
no goals

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (ConcreteCategory.hom (pullback.fst f g).base)
      ((ConcreteCategory.hom
          (pullback.lift (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x)
              (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y) ⋯).base)
        p) =
    T.x

Tactic:
rw [← Scheme.comp_base_apply]

Result:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↑↑(Spec T.tensor).toPresheafedSpace
⊢ (ConcreteCategory.hom
        (pullback.lift (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x)
              (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y) ⋯ ≫
            pullback.fst f g).base)
      p =
    T.x
-- Mathlib/Algebra/Module/Submodule/Ker.lean
theorem ker_comp_of_ker_eq_bot (f : M →ₛₗ[τ₁₂] M₂) {g : M₂ →ₛₗ[τ₂₃] M₃} (hg : ker g = ⊥) :
    ker (g.comp f : M →ₛₗ[τ₁₃] M₃) = ker f

Proof state:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
M : Type u_5
M₂ : Type u_7
M₃ : Type u_8
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hg : ker g = ⊥
⊢ ker (g.comp f) = ker f

Tactic:
rw [ker_comp, hg, Submodule.comap_bot]

Result:
no goals
-- Mathlib/Data/Fintype/Order.lean
lemma Finset.exists_minimal_le (s : Finset α) (h : a ∈ s) : ∃ b, b ≤ a ∧ Minimal (· ∈ s) b

Proof state:
case intro.mk.intro
α : Type u_1
inst✝ : PartialOrder α
a : α
s : Finset α
h : a ∈ s
b : α
property✝ : b ∈ s
lb : ⟨b, property✝⟩ ≤ ⟨a, h⟩
minb : Minimal (fun x => ↑x ∈ s) ⟨b, property✝⟩
⊢ ∃ b ≤ a, Minimal (fun x => x ∈ s) b

Tactic:
use b, lb

Result:
case right
α : Type u_1
inst✝ : PartialOrder α
a : α
s : Finset α
h : a ∈ s
b : α
property✝ : b ∈ s
lb : ⟨b, property✝⟩ ≤ ⟨a, h⟩
minb : Minimal (fun x => ↑x ∈ s) ⟨b, property✝⟩
⊢ Minimal (fun x => x ∈ s) b

Proof state:
case right
α : Type u_1
inst✝ : PartialOrder α
a : α
s : Finset α
h : a ∈ s
b : α
property✝ : b ∈ s
lb : ⟨b, property✝⟩ ≤ ⟨a, h⟩
minb : Minimal (fun x => ↑x ∈ s) ⟨b, property✝⟩
⊢ Minimal (fun x => x ∈ s) b

Tactic:
rwa [minimal_subtype, inf_idem] at minb

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem normalize_gcd : normalize (s.gcd f) = s.gcd f

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
⊢ normalize (s.gcd f) = s.gcd f

Tactic:
simp [gcd_def]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LinearMap.lean
theorem comp_smul [LinearMap.CompatibleSMul N₂ N₃ S R] (hₗ : N₂ →L[R] N₃) (c : S)
    (fₗ : M →L[R] N₂) : hₗ.comp (c • fₗ) = c • hₗ.comp fₗ

Proof state:
R : Type u_1
S : Type u_4
inst✝¹⁷ : Semiring R
inst✝¹⁶ : Monoid S
M : Type u_6
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
N₂ : Type u_9
inst✝¹² : TopologicalSpace N₂
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R N₂
N₃ : Type u_10
inst✝⁹ : TopologicalSpace N₃
inst✝⁸ : AddCommMonoid N₃
inst✝⁷ : Module R N₃
inst✝⁶ : DistribMulAction S N₃
inst✝⁵ : SMulCommClass R S N₃
inst✝⁴ : ContinuousConstSMul S N₃
inst✝³ : DistribMulAction S N₂
inst✝² : ContinuousConstSMul S N₂
inst✝¹ : SMulCommClass R S N₂
inst✝ : LinearMap.CompatibleSMul N₂ N₃ S R
hₗ : N₂ →L[R] N₃
c : S
fₗ : M →L[R] N₂
⊢ hₗ.comp (c • fₗ) = c • hₗ.comp fₗ

Tactic:
ext x

Result:
case h
R : Type u_1
S : Type u_4
inst✝¹⁷ : Semiring R
inst✝¹⁶ : Monoid S
M : Type u_6
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
N₂ : Type u_9
inst✝¹² : TopologicalSpace N₂
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R N₂
N₃ : Type u_10
inst✝⁹ : TopologicalSpace N₃
inst✝⁸ : AddCommMonoid N₃
inst✝⁷ : Module R N₃
inst✝⁶ : DistribMulAction S N₃
inst✝⁵ : SMulCommClass R S N₃
inst✝⁴ : ContinuousConstSMul S N₃
inst✝³ : DistribMulAction S N₂
inst✝² : ContinuousConstSMul S N₂
inst✝¹ : SMulCommClass R S N₂
inst✝ : LinearMap.CompatibleSMul N₂ N₃ S R
hₗ : N₂ →L[R] N₃
c : S
fₗ : M →L[R] N₂
x : M
⊢ (hₗ.comp (c • fₗ)) x = (c • hₗ.comp fₗ) x

Proof state:
case h
R : Type u_1
S : Type u_4
inst✝¹⁷ : Semiring R
inst✝¹⁶ : Monoid S
M : Type u_6
inst✝¹⁵ : TopologicalSpace M
inst✝¹⁴ : AddCommMonoid M
inst✝¹³ : Module R M
N₂ : Type u_9
inst✝¹² : TopologicalSpace N₂
inst✝¹¹ : AddCommMonoid N₂
inst✝¹⁰ : Module R N₂
N₃ : Type u_10
inst✝⁹ : TopologicalSpace N₃
inst✝⁸ : AddCommMonoid N₃
inst✝⁷ : Module R N₃
inst✝⁶ : DistribMulAction S N₃
inst✝⁵ : SMulCommClass R S N₃
inst✝⁴ : ContinuousConstSMul S N₃
inst✝³ : DistribMulAction S N₂
inst✝² : ContinuousConstSMul S N₂
inst✝¹ : SMulCommClass R S N₂
inst✝ : LinearMap.CompatibleSMul N₂ N₃ S R
hₗ : N₂ →L[R] N₃
c : S
fₗ : M →L[R] N₂
x : M
⊢ (hₗ.comp (c • fₗ)) x = (c • hₗ.comp fₗ) x

Tactic:
exact hₗ.map_smul_of_tower c (fₗ x)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem eraseKey_of_containsKey_eq_false [BEq α] {l : List ((a : α) × β a)} {k : α}
    (h : containsKey k l = false) : eraseKey k l = l

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : containsKey k t = false → eraseKey k t = t
h : (k' == k) = false ∧ containsKey k t = false
⊢ eraseKey k (⟨k', v'⟩ :: t) = ⟨k', v'⟩ :: t

Tactic:
rw [eraseKey_cons_of_false h.1, ih h.2]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
h : containsKey k l = false
⊢ eraseKey k l = l

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
k : α
h : containsKey k [] = false
⊢ eraseKey k [] = []

case cons
α : Type u
β : α → Type v
inst✝ : BEq α
k k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : containsKey k tail✝ = false → eraseKey k tail✝ = tail✝
h : containsKey k (⟨k✝, v✝⟩ :: tail✝) = false
⊢ eraseKey k (⟨k✝, v✝⟩ :: tail✝) = ⟨k✝, v✝⟩ :: tail✝

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
k : α
h : containsKey k [] = false
⊢ eraseKey k [] = []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : containsKey k t = false → eraseKey k t = t
h : containsKey k (⟨k', v'⟩ :: t) = false
⊢ eraseKey k (⟨k', v'⟩ :: t) = ⟨k', v'⟩ :: t

Tactic:
simp only [containsKey_cons, Bool.or_eq_false_iff] at h

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
k k' : α
v' : β k'
t : List ((a : α) × β a)
ih : containsKey k t = false → eraseKey k t = t
h : (k' == k) = false ∧ containsKey k t = false
⊢ eraseKey k (⟨k', v'⟩ :: t) = ⟨k', v'⟩ :: t

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
k k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : containsKey k tail✝ = false → eraseKey k tail✝ = tail✝
h : containsKey k (⟨k✝, v✝⟩ :: tail✝) = false
⊢ eraseKey k (⟨k✝, v✝⟩ :: tail✝) = ⟨k✝, v✝⟩ :: tail✝

Tactic:
next k' v' t ih =>
simp only [containsKey_cons, Bool.or_eq_false_iff] at h
rw [eraseKey_cons_of_false h.1, ih h.2]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCastD_eq_fallback [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
    {fallback : β a} (h : containsKey a l = false) : getValueCastD a l fallback = fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
a : α
fallback : β a
h : getValueCast? a l = none
⊢ getValueCastD a l fallback = fallback

Tactic:
rw [getValueCastD_eq_getValueCast?, h, Option.getD_none]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
a : α
fallback : β a
h : containsKey a l = false
⊢ getValueCastD a l fallback = fallback

Tactic:
rw [containsKey_eq_isSome_getValueCast?, Bool.eq_false_iff, ne_eq,
  Option.not_isSome_iff_eq_none] at h

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
a : α
fallback : β a
h : getValueCast? a l = none
⊢ getValueCastD a l fallback = fallback
-- Mathlib/Topology/UniformSpace/Ascoli.lean
theorem EquicontinuousOn.comap_uniformOnFun_eq {𝔖 : Set (Set X)} (𝔖_compact : ∀ K ∈ 𝔖, IsCompact K)
    (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) :
    (UniformOnFun.uniformSpace X α 𝔖).comap F =
    (Pi.uniformSpace _).comap ((⋃₀ 𝔖).restrict ∘ F)

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict ∘ F) (UniformFun.uniformSpace (↑K) α)
⊢ UniformSpace.comap ((⋃₀ 𝔖).restrict ∘ F) (Pi.uniformSpace fun i => α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict ∘ F) (Pi.uniformSpace fun i => α)

Tactic:
simp_rw [UniformSpace.comap_comap, Pi.uniformSpace_comap_restrict_sUnion (fun _ ↦ α) 𝔖,
  UniformSpace.comap_iInf]

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict ∘ F) (UniformFun.uniformSpace (↑K) α)
H2 :
  UniformSpace.comap ((⋃₀ 𝔖).restrict ∘ F) (Pi.uniformSpace fun i => α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict ∘ F) (Pi.uniformSpace fun i => α)
H3 :
  ∀ K ∈ 𝔖,
    UniformSpace.comap (K.restrict ∘ F) (UniformFun.uniformSpace (↑K) α) =
      UniformSpace.comap (K.restrict ∘ F) (Pi.uniformSpace fun i => α)
⊢ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    UniformSpace.comap ((⋃₀ 𝔖).restrict ∘ F) (Pi.uniformSpace fun i => α)

Tactic:
simp_rw [H1, H2, iInf_congr fun K ↦ iInf_congr fun hK ↦ H3 K hK]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem Frequently.and_eventually {p q : α → Prop} {f : Filter α} (hp : ∃ᶠ x in f, p x)
    (hq : ∀ᶠ x in f, q x) : ∃ᶠ x in f, p x ∧ q x

Proof state:
α : Type u
p q : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
hq : ∀ᶠ (x : α) in f, q x
⊢ ∃ᶠ (x : α) in f, p x ∧ q x

Tactic:
refine mt (fun h => hq.mp <| h.mono ?_) hp

Result:
α : Type u
p q : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
hq : ∀ᶠ (x : α) in f, q x
h : ∀ᶠ (x : α) in f, ¬(fun x => p x ∧ q x) x
⊢ ∀ (x : α), ¬(fun x => p x ∧ q x) x → q x → ¬(fun x => p x) x

Proof state:
α : Type u
p q : α → Prop
f : Filter α
hp : ∃ᶠ (x : α) in f, p x
hq : ∀ᶠ (x : α) in f, q x
h : ∀ᶠ (x : α) in f, ¬(fun x => p x ∧ q x) x
⊢ ∀ (x : α), ¬(fun x => p x ∧ q x) x → q x → ¬(fun x => p x) x

Tactic:
exact fun x hpq hq hp => hpq ⟨hp, hq⟩

Result:
no goals
-- Mathlib/MeasureTheory/Order/Lattice.lean
theorem Finset.measurable_range_sup' {f : ℕ → δ → α} {n : ℕ} (hf : ∀ k ≤ n, Measurable (f k)) :
    Measurable ((range (n + 1)).sup' nonempty_range_succ f)

Proof state:
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k < n.succ, Measurable (f k)
⊢ Measurable ((range (n + 1)).sup' ⋯ f)

Tactic:
refine Finset.measurable_sup' _ ?_

Result:
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k < n.succ, Measurable (f k)
⊢ ∀ n_1 ∈ range (n + 1), Measurable (f n_1)

Proof state:
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k < n.succ, Measurable (f k)
⊢ ∀ n_1 ∈ range (n + 1), Measurable (f n_1)

Tactic:
simpa [Finset.mem_range]

Result:
no goals

Proof state:
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k ≤ n, Measurable (f k)
⊢ Measurable ((range (n + 1)).sup' ⋯ f)

Tactic:
simp_rw [← Nat.lt_succ_iff] at hf

Result:
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k < n.succ, Measurable (f k)
⊢ Measurable ((range (n + 1)).sup' ⋯ f)
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_X_pow {n : ℕ} :
    (X ^ n : R[X]).smeval x = x ^ n

Proof state:
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : AddCommMonoid S
inst✝¹ : Pow S ℕ
inst✝ : MulActionWithZero R S
x : S
n : ℕ
⊢ (X ^ n).smeval x = x ^ n

Tactic:
simp only [smeval_eq_sum, smul_pow, X_pow_eq_monomial, zero_smul, sum_monomial_index, one_smul]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Turan.lean
lemma degree_eq_card_sub_part_card [DecidableEq V] :
    G.degree s = Fintype.card V - #(h.finpartition.part s) :=
  calc
    _ = #{t | G.Adj s t}

Proof state:
case e_a.e_s.h
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
a✝ : V
⊢ a✝ ∈ univ ∧ ¬G.Adj s a✝ ↔ a✝ ∈ h.finpartition.part s

Tactic:
convert Finpartition.mem_part_ofSetoid_iff_rel.symm

Result:
case h.e'_1.a
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
a✝ : V
⊢ a✝ ∈ univ ∧ ¬G.Adj s a✝ ↔ h.setoid s a✝

Proof state:
case h.e'_1.a
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
a✝ : V
⊢ a✝ ∈ univ ∧ ¬G.Adj s a✝ ↔ h.setoid s a✝

Tactic:
simp [setoid]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ G.degree s = #(filter (fun t => G.Adj s t) univ)

Tactic:
simp [← card_neighborFinset_eq_degree, neighborFinset]

Result:
no goals

Proof state:
case e_a.e_s
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ filter (fun t => ¬G.Adj s t) univ = h.finpartition.part s

Tactic:
ext

Result:
case e_a.e_s.h
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
a✝ : V
⊢ a✝ ∈ filter (fun t => ¬G.Adj s t) univ ↔ a✝ ∈ h.finpartition.part s

Proof state:
case e_a.e_s.h
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
a✝ : V
⊢ a✝ ∈ filter (fun t => ¬G.Adj s t) univ ↔ a✝ ∈ h.finpartition.part s

Tactic:
rw [mem_filter]

Result:
case e_a.e_s.h
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
a✝ : V
⊢ a✝ ∈ univ ∧ ¬G.Adj s a✝ ↔ a✝ ∈ h.finpartition.part s

Proof state:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ Fintype.card V - #(filter (fun t => ¬G.Adj s t) univ) = Fintype.card V - #(h.finpartition.part s)

Tactic:
congr

Result:
case e_a.e_s
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ filter (fun t => ¬G.Adj s t) univ = h.finpartition.part s
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_eq_sum_norm_sq_div_four (x y : E) :
    ⟪x, y⟫ = ((‖x + y‖ : 𝕜) ^ 2 - (‖x - y‖ : 𝕜) ^ 2 +
              ((‖x - IK • y‖ : 𝕜) ^ 2 - (‖x + IK • y‖ : 𝕜) ^ 2) * IK) / 4

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x, y⟫_𝕜 = (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - I • y‖ ^ 2 - ↑‖x + I • y‖ ^ 2) * I) / 4

Tactic:
rw [← re_add_im ⟪x, y⟫, re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four,
  im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ↑((‖x + y‖ * ‖x + y‖ - ‖x - y‖ * ‖x - y‖) / 4) + ↑((‖x - I • y‖ * ‖x - I • y‖ - ‖x + I • y‖ * ‖x + I • y‖) / 4) * I =
    (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - I • y‖ ^ 2 - ↑‖x + I • y‖ ^ 2) * I) / 4

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ↑((‖x + y‖ * ‖x + y‖ - ‖x - y‖ * ‖x - y‖) / 4) + ↑((‖x - I • y‖ * ‖x - I • y‖ - ‖x + I • y‖ * ‖x + I • y‖) / 4) * I =
    (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - I • y‖ ^ 2 - ↑‖x + I • y‖ ^ 2) * I) / 4

Tactic:
push_cast

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ (↑‖x + y‖ * ↑‖x + y‖ - ↑‖x - y‖ * ↑‖x - y‖) / 4 +
      (↑‖x - I • y‖ * ↑‖x - I • y‖ - ↑‖x + I • y‖ * ↑‖x + I • y‖) / 4 * I =
    (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - I • y‖ ^ 2 - ↑‖x + I • y‖ ^ 2) * I) / 4

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ (↑‖x + y‖ * ↑‖x + y‖ - ↑‖x - y‖ * ↑‖x - y‖) / 4 +
      (↑‖x - I • y‖ * ↑‖x - I • y‖ - ↑‖x + I • y‖ * ↑‖x + I • y‖) / 4 * I =
    (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - I • y‖ ^ 2 - ↑‖x + I • y‖ ^ 2) * I) / 4

Tactic:
simp only [sq, ← mul_div_right_comm, ← add_div]

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem Finite.partiallyWellOrderedOn (hs : s.Finite) : s.PartiallyWellOrderedOn r

Proof state:
case intro.intro.intro
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsRefl α r
hs : s.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
m n : ℕ
hmn : m < n
h : f m = f n
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
exact ⟨m, n, hmn, h.subst <| refl (f m)⟩

Result:
no goals

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsRefl α r
hs : s.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Tactic:
obtain ⟨m, n, hmn, h⟩ := hs.exists_lt_map_eq_of_forall_mem hf

Result:
case intro.intro.intro
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsRefl α r
hs : s.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
m n : ℕ
hmn : m < n
h : f m = f n
⊢ ∃ m n, m < n ∧ r (f m) (f n)

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsRefl α r
hs : s.Finite
⊢ s.PartiallyWellOrderedOn r

Tactic:
intro f hf

Result:
α : Type u_2
r : α → α → Prop
s : Set α
inst✝ : IsRefl α r
hs : s.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ r (f m) (f n)