harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/Combination.lean
theorem Finset.centroid_mem_convexHull (s : Finset E) (hs : s.Nonempty) :
    s.centroid R id ∈ convexHull R (s : Set E)

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
hs : s.Nonempty
⊢ s.centerMass (centroidWeights R s) id ∈ (convexHull R) ↑s

Tactic:
apply s.centerMass_id_mem_convexHull

Result:
case hw₀
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
hs : s.Nonempty
⊢ ∀ i ∈ s, 0 ≤ centroidWeights R s i

case hws
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
hs : s.Nonempty
⊢ 0 < ∑ i ∈ s, centroidWeights R s i

Proof state:
case hws
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
hs : s.Nonempty
hs_card : ↑(#s) ≠ 0
⊢ 0 < ∑ i ∈ s, centroidWeights R s i

Tactic:
simp only [hs_card, Finset.sum_const, nsmul_eq_mul, mul_inv_cancel₀, Ne, not_false_iff,
  Finset.centroidWeights_apply, zero_lt_one]

Result:
no goals

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
hs : s.Nonempty
⊢ centroid R s id ∈ (convexHull R) ↑s

Tactic:
rw [s.centroid_eq_centerMass hs]

Result:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
hs : s.Nonempty
⊢ s.centerMass (centroidWeights R s) id ∈ (convexHull R) ↑s

Proof state:
case hws
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
hs : s.Nonempty
⊢ 0 < ∑ i ∈ s, centroidWeights R s i

Tactic:
have hs_card : (#s : R) ≠ 0 := by simp [Finset.nonempty_iff_ne_empty.mp hs]

Result:
case hws
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
hs : s.Nonempty
hs_card : ↑(#s) ≠ 0
⊢ 0 < ∑ i ∈ s, centroidWeights R s i

Proof state:
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
hs : s.Nonempty
⊢ ↑(#s) ≠ 0

Tactic:
simp [Finset.nonempty_iff_ne_empty.mp hs]

Result:
no goals

Proof state:
case hw₀
R : Type u_1
E : Type u_3
inst✝² : LinearOrderedField R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
s : Finset E
hs : s.Nonempty
⊢ ∀ i ∈ s, 0 ≤ centroidWeights R s i

Tactic:
simp only [inv_nonneg, imp_true_iff, Nat.cast_nonneg, Finset.centroidWeights_apply]

Result:
no goals
-- Mathlib/Order/SuccPred/Archimedean.lean
lemma strictAnti_of_succ_lt (hf : ∀ a, ¬ IsMax a → f (succ a) < f a) : StrictAnti f

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) < f a
⊢ ∀ (a : α), ¬IsMax a → a ∈ Set.univ → succ a ∈ Set.univ → f (succ a) < f a

Tactic:
simpa using hf

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f (succ a) < f a
⊢ StrictAnti f

Tactic:
simpa using strictAntiOn_of_succ_lt Set.ordConnected_univ (by simpa using hf)

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_updateCol_smul_left (M : Matrix n n R) (j : n) (s : R) (u : n → R) :
    det (updateCol (s • M) j u) = s ^ (Fintype.card n - 1) * det (updateCol M j u)

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
s : R
u : n → R
⊢ ((s • M).updateCol j u).det = s ^ (Fintype.card n - 1) * (M.updateCol j u).det

Tactic:
rw [← det_transpose, ← updateRow_transpose, transpose_smul, det_updateRow_smul_left]

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
s : R
u : n → R
⊢ s ^ (Fintype.card n - 1) * (Mᵀ.updateRow j u).det = s ^ (Fintype.card n - 1) * (M.updateCol j u).det

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
s : R
u : n → R
⊢ s ^ (Fintype.card n - 1) * (Mᵀ.updateRow j u).det = s ^ (Fintype.card n - 1) * (M.updateCol j u).det

Tactic:
simp [updateRow_transpose, det_transpose]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiff_iff_contDiffAt : ContDiff 𝕜 n f ↔ ∀ x, ContDiffAt 𝕜 n f x

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
n : WithTop ℕ∞
⊢ ContDiff 𝕜 n f ↔ ∀ (x : E), ContDiffAt 𝕜 n f x

Tactic:
simp [← contDiffOn_univ, ContDiffOn, ContDiffAt]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem dist_le_infDist_add_diam (hs : IsBounded s) (hy : y ∈ s) :
    dist x y ≤ infDist x s + diam s

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
hs : Bornology.IsBounded s
hy : y ∈ s
⊢ dist x y ≤ infDist x s + diam s

Tactic:
rw [infDist, diam, dist_edist]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
hs : Bornology.IsBounded s
hy : y ∈ s
⊢ (edist x y).toReal ≤ (infEdist x s).toReal + (EMetric.diam s).toReal

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
hs : Bornology.IsBounded s
hy : y ∈ s
⊢ (edist x y).toReal ≤ (infEdist x s).toReal + (EMetric.diam s).toReal

Tactic:
exact toReal_le_add (edist_le_infEdist_add_ediam hy) (infEdist_ne_top ⟨y, hy⟩) hs.ediam_ne_top

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem interedges_disjoint_left {s s' : Finset α} (hs : Disjoint s s') (t : Finset β) :
    Disjoint (interedges r s t) (interedges r s' t)

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : Disjoint s s'
t : Finset β
⊢ Disjoint (interedges r s t) (interedges r s' t)

Tactic:
rw [Finset.disjoint_left] at hs ⊢

Result:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'
t : Finset β
⊢ ∀ ⦃a : α × β⦄, a ∈ interedges r s t → a ∉ interedges r s' t

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'
t : Finset β
a✝ : α × β
hx : a✝.1 ∈ s ∧ a✝.2 ∈ t ∧ r a✝.1 a✝.2
hy : a✝.1 ∈ s' ∧ a✝.2 ∈ t ∧ r a✝.1 a✝.2
⊢ False

Tactic:
exact hs hx.1 hy.1

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'
t : Finset β
⊢ ∀ ⦃a : α × β⦄, a ∈ interedges r s t → a ∉ interedges r s' t

Tactic:
intro _ hx hy

Result:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'
t : Finset β
a✝ : α × β
hx : a✝ ∈ interedges r s t
hy : a✝ ∈ interedges r s' t
⊢ False

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'
t : Finset β
a✝ : α × β
hx : a✝ ∈ interedges r s t
hy : a✝ ∈ interedges r s' t
⊢ False

Tactic:
rw [mem_interedges_iff] at hx hy

Result:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'
t : Finset β
a✝ : α × β
hx : a✝.1 ∈ s ∧ a✝.2 ∈ t ∧ r a✝.1 a✝.2
hy : a✝.1 ∈ s' ∧ a✝.2 ∈ t ∧ r a✝.1 a✝.2
⊢ False
-- Mathlib/Order/SupClosed.lean
/-- The semilatice generated by a finite set is finite. -/
protected lemma Set.Finite.infClosure (hs : s.Finite) : (infClosure s).Finite

Proof state:
case intro.intro.intro.intro
α : Type u_3
inst✝ : SemilatticeInf α
s t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ ↑s
⊢ t.inf' ht id ∈ ↑(Finset.image (fun t => (↑t).inf' ⋯ id) (filter (fun t => t.Nonempty) s.powerset).attach)

Tactic:
simp only [id_eq, coe_image, mem_image, mem_coe, mem_attach, true_and, Subtype.exists,
  Finset.mem_powerset, Finset.not_nonempty_iff_eq_empty, mem_filter]

Result:
case intro.intro.intro.intro
α : Type u_3
inst✝ : SemilatticeInf α
s t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ ↑s
⊢ ∃ a, ∃ (h : a ⊆ s ∧ a.Nonempty), (a.inf' ⋯ fun x => x) = t.inf' ⋯ fun x => x

Proof state:
case intro.intro.intro.intro
α : Type u_3
inst✝ : SemilatticeInf α
s t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ ↑s
⊢ ∃ a, ∃ (h : a ⊆ s ∧ a.Nonempty), (a.inf' ⋯ fun x => x) = t.inf' ⋯ fun x => x

Tactic:
exact ⟨t, ⟨hts, ht⟩, rfl⟩

Result:
no goals

Proof state:
case intro
α : Type u_3
inst✝ : SemilatticeInf α
s : Finset α
⊢ (infClosure ↑s).Finite

Tactic:
classical
refine ({t ∈ s.powerset | t.Nonempty}.attach.image
  fun t ↦ t.1.inf' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_
rintro _ ⟨t, ht, hts, rfl⟩
simp only [id_eq, coe_image, mem_image, mem_coe, mem_attach, true_and, Subtype.exists,
  Finset.mem_powerset, Finset.not_nonempty_iff_eq_empty, mem_filter]
exact ⟨t, ⟨hts, ht⟩, rfl⟩

Result:
no goals

Proof state:
case intro
α : Type u_3
inst✝ : SemilatticeInf α
s : Finset α
⊢ infClosure ↑s ⊆ ↑(Finset.image (fun t => (↑t).inf' ⋯ id) (filter (fun t => t.Nonempty) s.powerset).attach)

Tactic:
rintro _ ⟨t, ht, hts, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_3
inst✝ : SemilatticeInf α
s t : Finset α
ht : t.Nonempty
hts : ↑t ⊆ ↑s
⊢ t.inf' ht id ∈ ↑(Finset.image (fun t => (↑t).inf' ⋯ id) (filter (fun t => t.Nonempty) s.powerset).attach)

Proof state:
case intro
α : Type u_3
inst✝ : SemilatticeInf α
s : Finset α
⊢ (infClosure ↑s).Finite

Tactic:
refine ({t ∈ s.powerset | t.Nonempty}.attach.image
  fun t ↦ t.1.inf' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_

Result:
case intro
α : Type u_3
inst✝ : SemilatticeInf α
s : Finset α
⊢ infClosure ↑s ⊆ ↑(Finset.image (fun t => (↑t).inf' ⋯ id) (filter (fun t => t.Nonempty) s.powerset).attach)

Proof state:
α : Type u_3
inst✝ : SemilatticeInf α
s : Set α
hs : s.Finite
⊢ (infClosure s).Finite

Tactic:
lift s to Finset α using hs

Result:
case intro
α : Type u_3
inst✝ : SemilatticeInf α
s : Finset α
⊢ (infClosure ↑s).Finite
-- Mathlib/GroupTheory/GroupAction/FixedPoints.lean
theorem smul_mem_fixedBy_iff_mem_fixedBy {a : α} {g : G} :
    g • a ∈ fixedBy α g ↔ a ∈ fixedBy α g

Proof state:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g : G
⊢ g • a ∈ fixedBy α g ↔ a ∈ fixedBy α g

Tactic:
rw [mem_fixedBy, smul_left_cancel_iff]

Result:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g : G
⊢ g • a = a ↔ a ∈ fixedBy α g

Proof state:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a : α
g : G
⊢ g • a = a ↔ a ∈ fixedBy α g

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/MeanErgodic.lean
theorem LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure [NormedSpace 𝕜 E]
    (f : E →ₗ[𝕜] E) (hf : LipschitzWith 1 f) (g : E →L[𝕜] LinearMap.eqLocus f 1)
    (hg_proj : ∀ x : LinearMap.eqLocus f 1, g x = x)
    (hg_ker : (LinearMap.ker g : Set E) ⊆ closure (LinearMap.range (f - 1))) (x : E) :
    Tendsto (birkhoffAverage 𝕜 f _root_.id · x) atTop (𝓝 (g x))

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : E →ₗ[𝕜] E
hf : LipschitzWith 1 ⇑f
g : E →L[𝕜] ↥(eqLocus f 1)
hg_proj : ∀ (x : ↥(eqLocus f 1)), g ↑x = x
hg_ker : ↑(ker g) ⊆ closure ↑(range (f - 1))
y : E
hy : g y = 0
z : E
hz : IsFixedPt (⇑f) z
this✝ : IsClosed {x | Tendsto (fun x_1 => birkhoffAverage 𝕜 (⇑f) _root_.id x_1 x) atTop (𝓝 0)}
x : E
this : Bornology.IsBounded (Set.range fun x_1 => _root_.id ((⇑f)^[x_1] x))
H : ∀ (n : ℕ) (x y : E), (⇑f)^[n] (x - y) = (⇑f)^[n] x - (⇑f)^[n] y
⊢ (f - 1) x ∈ {x | Tendsto (fun x_1 => birkhoffAverage 𝕜 (⇑f) _root_.id x_1 x) atTop (𝓝 0)}

Tactic:
simpa [birkhoffAverage, birkhoffSum, Finset.sum_sub_distrib, smul_sub, H]
  using tendsto_birkhoffAverage_apply_sub_birkhoffAverage 𝕜 this

Result:
no goals
-- Mathlib/Data/Matroid/Sum.lean
lemma Indep.eq_union_image_of_disjointSum {h I} (hI : (disjointSum M N h).Indep I) :
    ∃ IM IN, M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN

Proof state:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ ∃ IM IN, M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN

Tactic:
refine ⟨_, _, hI.1, hI.2.1, h.mono inter_subset_right inter_subset_right, ?_⟩

Result:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ I = I ∩ M.E ∪ I ∩ N.E

Proof state:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ I = I ∩ M.E ∪ I ∩ N.E

Tactic:
rw [← inter_union_distrib_left, inter_eq_self_of_subset_left hI.2.2]

Result:
no goals

Proof state:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : (M.disjointSum N h).Indep I
⊢ ∃ IM IN, M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN

Tactic:
rw [disjointSum_indep_iff] at hI

Result:
α : Type u_1
M N : Matroid α
h : Disjoint M.E N.E
I : Set α
hI : M.Indep (I ∩ M.E) ∧ N.Indep (I ∩ N.E) ∧ I ⊆ M.E ∪ N.E
⊢ ∃ IM IN, M.Indep IM ∧ N.Indep IN ∧ Disjoint IM IN ∧ I = IM ∪ IN
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem ne_iff_lt_or_gt {a b : Int} : a ≠ b ↔ a < b ∨ b < a

Proof state:
a b : Int
⊢ a ≠ b ↔ a < b ∨ b < a

Tactic:
constructor

Result:
case mp
a b : Int
⊢ a ≠ b → a < b ∨ b < a

case mpr
a b : Int
⊢ a < b ∨ b < a → a ≠ b

Proof state:
case mpr
a b : Int
⊢ a < b ∨ b < a → a ≠ b

Tactic:
intro h

Result:
case mpr
a b : Int
h : a < b ∨ b < a
⊢ a ≠ b

Proof state:
case mpr.inr
a b : Int
h✝ : b < a
⊢ a ≠ b

Tactic:
case inr gt => exact Int.ne_of_gt gt

Result:
no goals

Proof state:
a b : Int
h✝ : a ≠ b
h : a = b ∨ b < a
⊢ a < b ∨ b < a

Tactic:
cases h

Result:
case inl
a b : Int
h : a ≠ b
h✝ : a = b
⊢ a < b ∨ b < a

case inr
a b : Int
h : a ≠ b
h✝ : b < a
⊢ a < b ∨ b < a

Proof state:
case mpr.inl
a b : Int
h✝ : a < b
⊢ a ≠ b

case mpr.inr
a b : Int
h✝ : b < a
⊢ a ≠ b

Tactic:
case inl lt => exact Int.ne_of_lt lt

Result:
case mpr.inr
a b : Int
h✝ : b < a
⊢ a ≠ b

Proof state:
a b : Int
h : a ≠ b
gt : b < a
⊢ a < b ∨ b < a

Tactic:
exact Or.inr gt

Result:
no goals

Proof state:
case inl
a b : Int
h : a ≠ b
h✝ : a = b
⊢ a < b ∨ b < a

case inr
a b : Int
h : a ≠ b
h✝ : b < a
⊢ a < b ∨ b < a

Tactic:
case inl =>simp_all

Result:
case inr
a b : Int
h : a ≠ b
h✝ : b < a
⊢ a < b ∨ b < a

Proof state:
case mp
a b : Int
h : a ≠ b
⊢ a < b ∨ b < a

Tactic:
cases Int.lt_trichotomy a b

Result:
case mp.inl
a b : Int
h : a ≠ b
h✝ : a < b
⊢ a < b ∨ b < a

case mp.inr
a b : Int
h : a ≠ b
h✝ : a = b ∨ b < a
⊢ a < b ∨ b < a

Proof state:
case mp.inl
a b : Int
h : a ≠ b
h✝ : a < b
⊢ a < b ∨ b < a

case mp.inr
a b : Int
h : a ≠ b
h✝ : a = b ∨ b < a
⊢ a < b ∨ b < a

Tactic:
case inl lt => exact Or.inl lt

Result:
case mp.inr
a b : Int
h : a ≠ b
h✝ : a = b ∨ b < a
⊢ a < b ∨ b < a

Proof state:
case inr
a b : Int
h : a ≠ b
h✝ : b < a
⊢ a < b ∨ b < a

Tactic:
case inr gt => exact Or.inr gt

Result:
no goals

Proof state:
case mpr
a b : Int
h : a < b ∨ b < a
⊢ a ≠ b

Tactic:
cases h

Result:
case mpr.inl
a b : Int
h✝ : a < b
⊢ a ≠ b

case mpr.inr
a b : Int
h✝ : b < a
⊢ a ≠ b

Proof state:
case mp
a b : Int
⊢ a ≠ b → a < b ∨ b < a

Tactic:
intro h

Result:
case mp
a b : Int
h : a ≠ b
⊢ a < b ∨ b < a

Proof state:
case mp.inr
a b : Int
h : a ≠ b
h✝ : a = b ∨ b < a
⊢ a < b ∨ b < a

Tactic:
case inr h =>
  cases h
  case inl =>simp_all
  case inr gt => exact Or.inr gt

Result:
no goals

Proof state:
a b : Int
lt : a < b
⊢ a ≠ b

Tactic:
exact Int.ne_of_lt lt

Result:
no goals

Proof state:
a b : Int
h : a ≠ b
h✝ : a = b
⊢ a < b ∨ b < a

Tactic:
simp_all

Result:
no goals

Proof state:
a b : Int
h : a ≠ b
lt : a < b
⊢ a < b ∨ b < a

Tactic:
exact Or.inl lt

Result:
no goals

Proof state:
a b : Int
gt : b < a
⊢ a ≠ b

Tactic:
exact Int.ne_of_gt gt

Result:
no goals
-- Mathlib/Data/Multiset/Powerset.lean
theorem powersetCardAux_zero (l : List α) : powersetCardAux 0 l = [0]

Proof state:
α : Type u_1
l : List α
⊢ powersetCardAux 0 l = [0]

Tactic:
simp [powersetCardAux_eq_map_coe]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem t1Space_TFAE (X : Type u) [TopologicalSpace X] :
    List.TFAE [T1Space X,
      ∀ x, IsClosed ({ x } : Set X),
      ∀ x, IsOpen ({ x }ᶜ : Set X),
      Continuous (@CofiniteTopology.of X),
      ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ y ∉ U,
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y),
      ∀ ⦃x y : X⦄, x ⤳ y → x = y]

Proof state:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed {x}) ↔ ∀ (x : X), IsOpen {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space X → Continuous ⇑CofiniteTopology.of
tfae_4_to_2 : Continuous ⇑CofiniteTopology.of → ∀ (x : X), IsClosed {x}
⊢ [T1Space X, ∀ (x : X), IsClosed {x}, ∀ (x : X), IsOpen {x}ᶜ, Continuous ⇑CofiniteTopology.of,
      ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : X⦄, x ⤳ y → x = y].TFAE

Tactic:
tfae_have 2 ↔ 10 := by
  simp only [← closure_subset_iff_isClosed, specializes_iff_mem_closure, subset_def,
    mem_singleton_iff, eq_comm]

Result:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_2 : T1Space X ↔ ∀ (x : X), IsClosed {x}
tfae_2_iff_3 : (∀ (x : X), IsClosed {x}) ↔ ∀ (x : X), IsOpen {x}ᶜ
tfae_5_iff_3 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ (x : X), IsOpen {x}ᶜ
tfae_5_iff_6 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s
tfae_5_iff_7 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U
tfae_5_iff_8 : (∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)
tfae_8_iff_9 : (∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y)) ↔ ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y)
tfae_1_to_4 : T1Space X → Continuous ⇑CofiniteTopology.of
tfae_4_to_2 : Continuous ⇑CofiniteTopology.of → ∀ (x : X), IsClosed {x}
tfae_2_iff_10 : (∀ (x : X), IsClosed {x}) ↔ ∀ ⦃x y : X⦄, x ⤳ y → x = y
⊢ [T1Space X, ∀ (x : X), IsClosed {x}, ∀ (x : X), IsOpen {x}ᶜ, Continuous ⇑CofiniteTopology.of,
      ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ 𝓝 x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ 𝓝 x, y ∉ s,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (𝓝 x) (pure y),
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (𝓝 y), ∀ ⦃x y : X⦄, x ⤳ y → x = y].TFAE
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
lemma deriv_qaryEntropy (hp₀ : p ≠ 0) (hp₁ : p ≠ 1) :
    deriv (qaryEntropy q) p = log (q - 1) + log (1 - p) - log p

Proof state:
case funProp.discharger
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ p ≠ 1

Tactic:
assumption

Result:
no goals

Proof state:
case hg
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ binEntropy p

Tactic:
fun_prop (disch := assumption)

Result:
no goals

Proof state:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ deriv (qaryEntropy q) p = log (↑q - 1) + log (1 - p) - log p

Tactic:
unfold qaryEntropy

Result:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ deriv (fun p => p * log ↑(↑q - 1) + binEntropy p) p = log (↑q - 1) + log (1 - p) - log p

Proof state:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ deriv (fun p => p * log ↑(↑q - 1) + binEntropy p) p = log (↑q - 1) + log (1 - p) - log p

Tactic:
rw [deriv_add]

Result:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ deriv (fun p => p * log ↑(↑q - 1)) p + deriv binEntropy p = log (↑q - 1) + log (1 - p) - log p

case hf
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ (fun p => p * log ↑(↑q - 1)) p

case hg
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ binEntropy p

Proof state:
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ deriv (fun p => p * log ↑(↑q - 1)) p + deriv binEntropy p = log (↑q - 1) + log (1 - p) - log p

Tactic:
simp only [Int.cast_sub, Int.cast_natCast, Int.cast_one, differentiableAt_id', deriv_mul_const,
  deriv_id'', one_mul, deriv_binEntropy, add_sub_assoc]

Result:
no goals

Proof state:
case hf
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ (fun p => p * log ↑(↑q - 1)) p

case hg
q : ℕ
p : ℝ
hp₀ : p ≠ 0
hp₁ : p ≠ 1
⊢ DifferentiableAt ℝ binEntropy p

Tactic:
all_goals fun_prop (disch := assumption)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem all_succ {n : Nat} (f : (i : Nat) → i < n + 1 → Bool) :
  all (n + 1) f = (all n (fun i h => f i (by omega)) && f n (by omega))

Proof state:
n : Nat
f : (i : Nat) → i < n + 1 → Bool
⊢ n < n + 1

Tactic:
omega

Result:
no goals

Proof state:
n : Nat
f : (i : Nat) → i < n + 1 → Bool
⊢ (n + 1).all f = ((n.all fun i h => f i ⋯) && f n ⋯)

Tactic:
simp [all]

Result:
no goals

Proof state:
n : Nat
f : (i : Nat) → i < n + 1 → Bool
i : Nat
h : i < n
⊢ i < n + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem mem_ofLe (x : K') : x ∈ ofLe h ↔ (x : L) ∈ K

Proof state:
case mp.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
y : ↥K
⊢ ↑⟨↑y, ⋯⟩ ∈ K

Tactic:
exact y.property

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K'
⊢ (∃ y, ⟨↑y, ⋯⟩ = x) ↔ ↑x ∈ K

Tactic:
constructor

Result:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K'
⊢ (∃ y, ⟨↑y, ⋯⟩ = x) → ↑x ∈ K

case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K'
⊢ ↑x ∈ K → ∃ y, ⟨↑y, ⋯⟩ = x

Proof state:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h✝ : K ≤ K'
x : ↥K'
h : ↑x ∈ K
⊢ ∃ y, ⟨↑y, ⋯⟩ = x

Tactic:
use ⟨(x : L), h⟩

Result:
no goals

Proof state:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K'
⊢ ↑x ∈ K → ∃ y, ⟨↑y, ⋯⟩ = x

Tactic:
intro h

Result:
case mpr
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h✝ : K ≤ K'
x : ↥K'
h : ↑x ∈ K
⊢ ∃ y, ⟨↑y, ⋯⟩ = x

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K'
⊢ x ∈ ofLe h ↔ ↑x ∈ K

Tactic:
simp only [ofLe, inclusion_apply, LieHom.mem_range]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K'
⊢ (∃ y, ⟨↑y, ⋯⟩ = x) ↔ ↑x ∈ K

Proof state:
case mp
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
x : ↥K'
⊢ (∃ y, ⟨↑y, ⋯⟩ = x) → ↑x ∈ K

Tactic:
rintro ⟨y, rfl⟩

Result:
case mp.intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K K' : LieSubalgebra R L
h : K ≤ K'
y : ↥K
⊢ ↑⟨↑y, ⋯⟩ ∈ K