harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiff_infty_iff_fderiv :
    ContDiff 𝕜 ∞ f ↔ Differentiable 𝕜 f ∧ ContDiff 𝕜 ∞ (fderiv 𝕜 f)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ Differentiable 𝕜 f ∧ (∞ = ω → AnalyticOnNhd 𝕜 f univ) ∧ ContDiff 𝕜 ∞ (fderiv 𝕜 f) ↔
    Differentiable 𝕜 f ∧ ContDiff 𝕜 (∞ + 1) (fderiv 𝕜 f)

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ ContDiff 𝕜 ∞ f ↔ Differentiable 𝕜 f ∧ ContDiff 𝕜 ∞ (fderiv 𝕜 f)

Tactic:
rw [← ENat.coe_top_add_one, contDiff_succ_iff_fderiv]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
⊢ Differentiable 𝕜 f ∧ (∞ = ω → AnalyticOnNhd 𝕜 f univ) ∧ ContDiff 𝕜 ∞ (fderiv 𝕜 f) ↔
    Differentiable 𝕜 f ∧ ContDiff 𝕜 (∞ + 1) (fderiv 𝕜 f)
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean
theorem det_eq_prod_roots_charpoly_of_splits (hAps : A.charpoly.Splits (RingHom.id R)) :
    A.det = (Matrix.charpoly A).roots.prod

Proof state:
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Field R
A : Matrix n n R
hAps : Splits (RingHom.id R) A.charpoly
⊢ A.det = A.charpoly.roots.prod

Tactic:
rw [det_eq_sign_charpoly_coeff, ← charpoly_natDegree_eq_dim A,
  Polynomial.prod_roots_eq_coeff_zero_of_monic_of_splits A.charpoly_monic hAps, ← mul_assoc,
  ← pow_two, pow_right_comm, neg_one_sq, one_pow, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem merge_stable : ∀ (xs ys) (_ : ∀ x y, x ∈ xs → y ∈ ys → x.2 ≤ y.2),
    (merge xs ys (zipIdxLE le)).map (·.1) = merge (xs.map (·.1)) (ys.map (·.1)) le
  | [], ys, _ => by simp [merge]
  | xs, [], _ => by simp [merge]
  | (i, x) :: xs, (j, y) :: ys, h => by
    simp only [merge, zipIdxLE, map_cons]
    split <;> rename_i w
    · rw [if_pos (by simp [h _ _ (mem_cons_self ..) (mem_cons_self ..)])]
      simp only [map_cons, cons.injEq, true_and]
      rw [merge_stable, map_cons]
      exact fun x' y' mx my => h x' y' (mem_cons_of_mem (i, x) mx) my
    · simp only [↓reduceIte, map_cons, cons.injEq, true_and, reduceCtorEq]
      rw [merge_stable, map_cons]
      exact fun x' y' mx my => h x' y' mx (mem_cons_of_mem (j, y) my)

Proof state:
case isFalse
α : Type u_1
le : α → α → Bool
i : α
x : Nat
xs : List (α × Nat)
j : α
y : Nat
ys : List (α × Nat)
h : ∀ (x_1 y_1 : α × Nat), x_1 ∈ (i, x) :: xs → y_1 ∈ (j, y) :: ys → x_1.snd ≤ y_1.snd
w : ¬le i j = true
⊢ map (fun x => x.fst)
      (if false = true then (i, x) :: xs.merge ((j, y) :: ys) (zipIdxLE le)
      else (j, y) :: ((i, x) :: xs).merge ys (zipIdxLE le)) =
    j :: (i :: map (fun x => x.fst) xs).merge (map (fun x => x.fst) ys) le

Tactic:
simp only [↓reduceIte, map_cons, cons.injEq, true_and, reduceCtorEq]

Result:
case isFalse
α : Type u_1
le : α → α → Bool
i : α
x : Nat
xs : List (α × Nat)
j : α
y : Nat
ys : List (α × Nat)
h : ∀ (x_1 y_1 : α × Nat), x_1 ∈ (i, x) :: xs → y_1 ∈ (j, y) :: ys → x_1.snd ≤ y_1.snd
w : ¬le i j = true
⊢ map (fun x => x.fst) (((i, x) :: xs).merge ys (zipIdxLE le)) =
    (i :: map (fun x => x.fst) xs).merge (map (fun x => x.fst) ys) le

Proof state:
case isTrue.x
α : Type u_1
le : α → α → Bool
i : α
x : Nat
xs : List (α × Nat)
j : α
y : Nat
ys : List (α × Nat)
h : ∀ (x_1 y_1 : α × Nat), x_1 ∈ (i, x) :: xs → y_1 ∈ (j, y) :: ys → x_1.snd ≤ y_1.snd
w : le i j = true
⊢ ∀ (x y_1 : α × Nat), x ∈ xs → y_1 ∈ (j, y) :: ys → x.snd ≤ y_1.snd

Tactic:
exact fun x' y' mx my => h x' y' (mem_cons_of_mem (i, x) mx) my

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem setIntegral_condExpL1CLM_of_measure_ne_top (f : α →₁[μ] F') (hs : MeasurableSet[m] s)
    (hμs : μ s ≠ ∞) : ∫ x in s, condExpL1CLM F' hm μ f x ∂μ = ∫ x in s, f x ∂μ

Proof state:
case refine_2
α : Type u_1
F' : Type u_3
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
s : Set α
f✝ : ↥(Lp F' 1 μ)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f g : α → F'
hf_Lp : MemLp f 1 μ
hg_Lp : MemLp g 1 μ
a✝ : Disjoint (Function.support f) (Function.support g)
hf : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x ∂μ
hg : ∫ (x : α) in s, ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ = ∫ (x : α) in s, ↑↑(MemLp.toLp g hg_Lp) x ∂μ
⊢ ∫ (x : α) in s,
      ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp f hf_Lp)) x + ↑↑((condExpL1CLM F' hm μ) (MemLp.toLp g hg_Lp)) x ∂μ =
    ∫ (x : α) in s, ↑↑(MemLp.toLp f hf_Lp) x + ↑↑(MemLp.toLp g hg_Lp) x ∂μ

Tactic:
rw [integral_add (L1.integrable_coeFn _).integrableOn (L1.integrable_coeFn _).integrableOn,
  integral_add (L1.integrable_coeFn _).integrableOn (L1.integrable_coeFn _).integrableOn, hf,
  hg]

Result:
no goals
-- Mathlib/Algebra/Homology/QuasiIso.lean
@[simp]
lemma mem_quasiIso_iff (f : K ⟶ L) : quasiIso C c f ↔ QuasiIso f

Proof state:
ι : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : CategoryWithHomology C
f : K ⟶ L
⊢ quasiIso C c f ↔ QuasiIso f

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
theorem tendstoInMeasure_of_tendsto_eLpNorm_top {E} [NormedAddCommGroup E] {f : ι → α → E}
    {g : α → E} {l : Filter ι} (hfg : Tendsto (fun n => eLpNorm (f n - g) ∞ μ) l (𝓝 0)) :
    TendstoInMeasure μ f l g

Proof state:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
hfg : ∀ ε > 0, ∀ᶠ (x : ι) in l, essSup (fun x_1 => ‖(f x - g) x_1‖ₑ) μ ≤ ε
⊢ ∀ ε > 0, ∀ᶠ (x : ι) in l, μ {x_1 | δ ≤ dist (f x x_1) (g x_1)} ≤ ε

Tactic:
intro ε hε

Result:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
hfg : ∀ ε > 0, ∀ᶠ (x : ι) in l, essSup (fun x_1 => ‖(f x - g) x_1‖ₑ) μ ≤ ε
ε : ℝ≥0∞
hε : ε > 0
⊢ ∀ᶠ (x : ι) in l, μ {x_1 | δ ≤ dist (f x x_1) (g x_1)} ≤ ε

Proof state:
case h.e_6.h.h
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ‖f x x_1 - g x_1‖ₑ) μ ≤ ENNReal.ofReal δ / 2
n : ι
hn : essSup (fun x => ‖f n x - g x‖ₑ) μ ≤ ENNReal.ofReal δ / 2
hε : 0 < ε
this : essSup (fun x => ↑‖f n x - g x‖₊) μ < ENNReal.ofReal δ
x : α
⊢ x ∈ {x | δ ≤ dist (f n x) (g x)} ↔ x ∈ {x | (fun y => ↑‖f n y - g y‖₊ < ENNReal.ofReal δ) x}ᶜ

Tactic:
simp only [ENNReal.ofReal_le_iff_le_toReal ENNReal.coe_lt_top.ne, ENNReal.coe_toReal, not_lt,
  coe_nnnorm, Set.mem_setOf_eq, Set.mem_compl_iff]

Result:
case h.e_6.h.h
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ‖f x x_1 - g x_1‖ₑ) μ ≤ ENNReal.ofReal δ / 2
n : ι
hn : essSup (fun x => ‖f n x - g x‖ₑ) μ ≤ ENNReal.ofReal δ / 2
hε : 0 < ε
this : essSup (fun x => ↑‖f n x - g x‖₊) μ < ENNReal.ofReal δ
x : α
⊢ δ ≤ dist (f n x) (g x) ↔ δ ≤ ‖f n x - g x‖

Proof state:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
hfg : Tendsto (fun n => essSup (fun x => ‖(f n - g) x‖ₑ) μ) l (𝓝 0)
⊢ Tendsto (fun i => μ {x | δ ≤ dist (f i x) (g x)}) l (𝓝 0)

Tactic:
rw [ENNReal.tendsto_nhds_zero] at hfg ⊢

Result:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
hfg : ∀ ε > 0, ∀ᶠ (x : ι) in l, essSup (fun x_1 => ‖(f x - g) x_1‖ₑ) μ ≤ ε
⊢ ∀ ε > 0, ∀ᶠ (x : ι) in l, μ {x_1 | δ ≤ dist (f x x_1) (g x_1)} ≤ ε
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem ordProj_dvd (n p : ℕ) : ordProj[p] n ∣ n

Proof state:
n p : ℕ
hp : Prime p
q : ℕ
hq : q ∈ replicate (count p n.primeFactorsList) p
⊢ count q (replicate (count p n.primeFactorsList) p) ≤ count q n.primeFactorsList

Tactic:
simp [List.eq_of_mem_replicate hq]

Result:
no goals

Proof state:
n p : ℕ
⊢ p ^ n.factorization p ∣ n

Tactic:
if hp : p.Prime then ?_ else simp [hp]

Result:
n p : ℕ
hp : Prime p
⊢ p ^ n.factorization p ∣ n

Proof state:
n p : ℕ
hp : ¬Prime p
⊢ p ^ n.factorization p ∣ n

Tactic:
simp [hp]

Result:
no goals

Proof state:
n p : ℕ
hp : Prime p
⊢ ∀ x ∈ replicate (count p n.primeFactorsList) p,
    count x (replicate (count p n.primeFactorsList) p) ≤ count x n.primeFactorsList

Tactic:
intro q hq

Result:
n p : ℕ
hp : Prime p
q : ℕ
hq : q ∈ replicate (count p n.primeFactorsList) p
⊢ count q (replicate (count p n.primeFactorsList) p) ≤ count q n.primeFactorsList

Proof state:
n p : ℕ
hp : Prime p
⊢ p ^ n.factorization p ∣ n

Tactic:
rw [← primeFactorsList_count_eq]

Result:
n p : ℕ
hp : Prime p
⊢ p ^ count p n.primeFactorsList ∣ n

Proof state:
n p : ℕ
hp : Prime p
⊢ (p ^ count p n.primeFactorsList).primeFactorsList <+~ n.primeFactorsList

Tactic:
rw [hp.primeFactorsList_pow, List.subperm_ext_iff]

Result:
n p : ℕ
hp : Prime p
⊢ ∀ x ∈ replicate (count p n.primeFactorsList) p,
    count x (replicate (count p n.primeFactorsList) p) ≤ count x n.primeFactorsList

Proof state:
n p : ℕ
hp : Prime p
⊢ p ^ count p n.primeFactorsList ∣ n

Tactic:
apply dvd_of_primeFactorsList_subperm (pow_ne_zero _ hp.ne_zero)

Result:
n p : ℕ
hp : Prime p
⊢ (p ^ count p n.primeFactorsList).primeFactorsList <+~ n.primeFactorsList
-- Mathlib/MeasureTheory/Function/Jacobian.lean
theorem addHaar_image_le_lintegral_abs_det_fderiv (hs : MeasurableSet s)
    (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :
    μ (f '' s) ≤ ∫⁻ x in s, ENNReal.ofReal |(f' x).det| ∂μ

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
u : ℕ → Set E := fun n => disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
⊢ μ (f '' s) ≤ ∑' (n : ℕ), μ (f '' (s ∩ u n))

Tactic:
conv_lhs => rw [A, image_iUnion]

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
u : ℕ → Set E := fun n => disjointed (spanningSets μ) n
u_meas : ∀ (n : ℕ), MeasurableSet (u n)
A : s = ⋃ n, s ∩ u n
⊢ μ (⋃ i, f '' (s ∩ u i)) ≤ ∑' (n : ℕ), μ (f '' (s ∩ u n))
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem kerParam_range_eq :
    (kerParam g).range = (toPermHom g).ker.map (Subgroup.subtype _)

Proof state:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), x ∈ c.support ↔ ↑p x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c) := fun c => ⟨ofSubtype ((↑p).subtypePerm ⋯), ⋯⟩
x : α
hx✝ : g.cycleOf x ∈ g.cycleFactorsFinset
hx : g x ≠ x
⊢ ↑(v ⟨g.cycleOf x, hx✝⟩) x = ↑p x

Tactic:
rw [ofSubtype_apply_of_mem, subtypePerm_apply]

Result:
case pos.ha
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), x ∈ c.support ↔ ↑p x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
v : (c : { x // x ∈ g.cycleFactorsFinset }) → ↥(zpowers ↑c) := fun c => ⟨ofSubtype ((↑p).subtypePerm ⋯), ⋯⟩
x : α
hx✝ : g.cycleOf x ∈ g.cycleFactorsFinset
hx : g x ≠ x
⊢ x ∈ (↑⟨g.cycleOf x, hx✝⟩).support

Proof state:
case a.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
hp : p ∈ ↑(toPermHom g).ker
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
⊢ ↑p ∈ (kerParam g).range

Tactic:
simp only [SetLike.mem_coe, mem_ker_toPermHom_iff, IsCycle.forall_commute_iff] at hp

Result:
case a.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
p : ↥(centralizer {g})
u : Perm ↑(Function.fixedPoints ⇑g) := (↑p).subtypePerm ⋯
hp :
  ∀ c ∈ g.cycleFactorsFinset,
    ∃ (hc : ∀ (x : α), x ∈ c.support ↔ ↑p x ∈ c.support), ofSubtype ((↑p).subtypePerm hc) ∈ zpowers c
⊢ ↑p ∈ (kerParam g).range
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToL1_add_left' (hT : DominatedFinMeasAdditive μ T C)
    (hT' : DominatedFinMeasAdditive μ T' C') (hT'' : DominatedFinMeasAdditive μ T'' C'')
    (h_add : ∀ s, MeasurableSet s → μ s < ∞ → T'' s = T s + T' s) (f : α →₁[μ] E) :
    setToL1 hT'' f = setToL1 hT f + setToL1 hT' f

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' T'' : Set α → E →L[ℝ] F
C C' C'' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
hT'' : DominatedFinMeasAdditive μ T'' C''
h_add : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s
f✝ : ↥(Lp E 1 μ)
f : ↥(simpleFunc E 1 μ)
this : (setToL1 hT) ↑f + (setToL1 hT') ↑f = (setToL1SCLM α E μ hT'') f
⊢ ((setToL1 hT + setToL1 hT').comp (coeToLp α E ℝ)) f = (setToL1 hT) ↑f + (setToL1 hT') ↑f

Tactic:
congr

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem mem_affineSpan_iff_eq_affineCombination [Nontrivial k] {p1 : P} {p : ι → P} :
    p1 ∈ affineSpan k (Set.range p) ↔
      ∃ (s : Finset ι) (w : ι → k), ∑ i ∈ s, w i = 1 ∧ p1 = s.affineCombination k p w

Proof state:
case mpr.intro.intro.intro
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 1
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)

Tactic:
exact affineCombination_mem_affineSpan hw p

Result:
no goals

Proof state:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
p1 : P
p : ι → P
⊢ p1 ∈ affineSpan k (Set.range p) ↔ ∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w

Tactic:
constructor

Result:
case mp
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
p1 : P
p : ι → P
⊢ p1 ∈ affineSpan k (Set.range p) → ∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w

case mpr
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
p1 : P
p : ι → P
⊢ (∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w) → p1 ∈ affineSpan k (Set.range p)

Proof state:
case mpr
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
p1 : P
p : ι → P
⊢ (∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w) → p1 ∈ affineSpan k (Set.range p)

Tactic:
rintro ⟨s, w, hw, rfl⟩

Result:
case mpr.intro.intro.intro
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
p : ι → P
s : Finset ι
w : ι → k
hw : ∑ i ∈ s, w i = 1
⊢ (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)

Proof state:
case mp
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝⁴ : Ring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Nontrivial k
p1 : P
p : ι → P
⊢ p1 ∈ affineSpan k (Set.range p) → ∃ s w, ∑ i ∈ s, w i = 1 ∧ p1 = (Finset.affineCombination k s p) w

Tactic:
exact eq_affineCombination_of_mem_affineSpan

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem ofStream_cons (a : α) (s) : ofStream (a::s) = cons a (ofStream s)

Proof state:
case a
α : Type u
a : α
s : Stream' α
⊢ ↑↑(a :: s) = ↑(cons a ↑s)

Tactic:
simp only [ofStream, cons]

Result:
case a
α : Type u
a : α
s : Stream' α
⊢ Stream'.map some (a :: s) = some a :: Stream'.map some s

Proof state:
case a
α : Type u
a : α
s : Stream' α
⊢ Stream'.map some (a :: s) = some a :: Stream'.map some s

Tactic:
rw [Stream'.map_cons]

Result:
no goals

Proof state:
α : Type u
a : α
s : Stream' α
⊢ ↑(a :: s) = cons a ↑s

Tactic:
apply Subtype.eq

Result:
case a
α : Type u
a : α
s : Stream' α
⊢ ↑↑(a :: s) = ↑(cons a ↑s)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapFinIdx_singleton {a : α} {f : (i : Nat) → α → (h : i < 1) → β} :
    #v[a].mapFinIdx f = #v[f 0 a (by simp)]

Proof state:
α : Type ?u.27712
β : Type ?u.27753
a : α
f : (i : Nat) → α → i < 1 → β
⊢ 0 < 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
f : (i : Nat) → α → i < 1 → β
⊢ { toArray := #[a], size_toArray := ⋯ }.mapFinIdx f = { toArray := #[f 0 a ⋯], size_toArray := ⋯ }

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/UrysohnsLemma.lean
theorem approx_le_one (c : CU P) (n : ℕ) (x : X) : c.approx n x ≤ 1

Proof state:
case zero
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
c : CU P
⊢ approx 0 c x ≤ 1

Tactic:
exact indicator_apply_le' (fun _ => le_rfl) fun _ => zero_le_one

Result:
no goals

Proof state:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ≤ 1
c : CU P
⊢ (approx n c.left x + approx n c.right x) / 2 ≤ 1

Tactic:
have := add_le_add (ihn (left c)) (ihn (right c))

Result:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ≤ 1
c : CU P
this : approx n c.left x + approx n c.right x ≤ 1 + 1
⊢ (approx n c.left x + approx n c.right x) / 2 ≤ 1

Proof state:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ≤ 1
c : CU P
⊢ approx (n + 1) c x ≤ 1

Tactic:
simp only [approx, midpoint_eq_smul_add, invOf_eq_inv, smul_eq_mul, ← div_eq_inv_mul]

Result:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ≤ 1
c : CU P
⊢ (approx n c.left x + approx n c.right x) / 2 ≤ 1

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c : CU P
n : ℕ
x : X
⊢ approx n c x ≤ 1

Tactic:
induction n generalizing c with
| zero => exact indicator_apply_le' (fun _ => le_rfl) fun _ => zero_le_one
| succ n ihn =>
  simp only [approx, midpoint_eq_smul_add, invOf_eq_inv, smul_eq_mul, ← div_eq_inv_mul]
  have := add_le_add (ihn (left c)) (ihn (right c))
  norm_num at this
  exact Iff.mpr (div_le_one zero_lt_two) this

Result:
no goals

Proof state:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ≤ 1
c : CU P
this : approx n c.left x + approx n c.right x ≤ 2
⊢ (approx n c.left x + approx n c.right x) / 2 ≤ 1

Tactic:
exact Iff.mpr (div_le_one zero_lt_two) this

Result:
no goals

Proof state:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ≤ 1
c : CU P
this : approx n c.left x + approx n c.right x ≤ 1 + 1
⊢ (approx n c.left x + approx n c.right x) / 2 ≤ 1

Tactic:
norm_num at this

Result:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), approx n c x ≤ 1
c : CU P
this : approx n c.left x + approx n c.right x ≤ 2
⊢ (approx n c.left x + approx n c.right x) / 2 ≤ 1
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem chromaticNumber_le_iff_colorable {n : ℕ} : G.chromaticNumber ≤ n ↔ G.Colorable n

Proof state:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ ↑n
this : ∃ n, G.Colorable n
⊢ G.Colorable n

Tactic:
obtain ⟨m, hm⟩ := this

Result:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ ↑n
m : ℕ
hm : G.Colorable m
⊢ G.Colorable n

Proof state:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ ↑n
m : ℕ
hm : G.Colorable m
⊢ G.Colorable n

Tactic:
rw [hm.chromaticNumber_eq_sInf, Nat.cast_le] at h

Result:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
h : sInf {n' | G.Colorable n'} ≤ n
m : ℕ
hm : G.Colorable m
⊢ G.Colorable n

Proof state:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
h : sInf {n' | G.Colorable n'} ≤ n
m : ℕ
hm : G.Colorable m
this : G.Colorable (sInf {n' | G.Colorable n'})
⊢ G.Colorable n

Tactic:
exact this.mono h

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ ↑n
⊢ G.Colorable n

Tactic:
have : G.chromaticNumber ≠ ⊤ := (trans h (WithTop.coe_lt_top n)).ne

Result:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ ↑n
this : G.chromaticNumber ≠ ⊤
⊢ G.Colorable n

Proof state:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
h : sInf {n' | G.Colorable n'} ≤ n
m : ℕ
hm : G.Colorable m
this : sInf {n' | G.Colorable n'} ∈ {n' | G.Colorable n'}
⊢ G.Colorable n

Tactic:
rw [Set.mem_setOf_eq] at this

Result:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
h : sInf {n' | G.Colorable n'} ≤ n
m : ℕ
hm : G.Colorable m
this : G.Colorable (sInf {n' | G.Colorable n'})
⊢ G.Colorable n

Proof state:
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.chromaticNumber ≤ ↑n ↔ G.Colorable n

Tactic:
refine ⟨fun h ↦ ?_, Colorable.chromaticNumber_le⟩

Result:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ ↑n
⊢ G.Colorable n

Proof state:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
h : sInf {n' | G.Colorable n'} ≤ n
m : ℕ
hm : G.Colorable m
⊢ G.Colorable n

Tactic:
have := Nat.sInf_mem (⟨m, hm⟩ : {n' | G.Colorable n'}.Nonempty)

Result:
case intro
V : Type u
G : SimpleGraph V
n : ℕ
h : sInf {n' | G.Colorable n'} ≤ n
m : ℕ
hm : G.Colorable m
this : sInf {n' | G.Colorable n'} ∈ {n' | G.Colorable n'}
⊢ G.Colorable n

Proof state:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ ↑n
this : G.chromaticNumber ≠ ⊤
⊢ G.Colorable n

Tactic:
rw [chromaticNumber_ne_top_iff_exists] at this

Result:
V : Type u
G : SimpleGraph V
n : ℕ
h : G.chromaticNumber ≤ ↑n
this : ∃ n, G.Colorable n
⊢ G.Colorable n