harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Erase.lean
theorem getElem_eraseIdx_of_ge (l : Vector α n) (i : Nat) (w : i < n) (j : Nat) (h : j < n - 1) (h' : i ≤ j) :
    (l.eraseIdx i)[j] = l[j + 1]

Proof state:
case mk
α : Type u_1
i j : Nat
h' : i ≤ j
l : Array α
w : i < l.size
h : j < l.size - 1
⊢ ({ toArray := l, size_toArray := ⋯ }.eraseIdx i w)[j] = { toArray := l, size_toArray := ⋯ }[j + 1]

Tactic:
simp [Array.getElem_eraseIdx_of_ge, *]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
w : i < n
j : Nat
h : j < n - 1
h' : i ≤ j
⊢ (l.eraseIdx i w)[j] = l[j + 1]

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
i j : Nat
h' : i ≤ j
l : Array α
w : i < l.size
h : j < l.size - 1
⊢ ({ toArray := l, size_toArray := ⋯ }.eraseIdx i w)[j] = { toArray := l, size_toArray := ⋯ }[j + 1]
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem mul_div_mul_cancel {a b c : R} (ha : a ≠ 0) (hcb : c ∣ b) : a * b / (a * c) = b / c

Proof state:
case pos
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : c = 0
⊢ a * b / (a * c) = b / c

Tactic:
simp [hc]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * (c * (a * b / (a * c))) = a * b

Tactic:
rw [← mul_assoc, ← mul_div_assoc _ (mul_dvd_mul_left a hcb),
  mul_div_cancel_left₀ _ (mul_ne_zero ha hc)]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * b / (a * c) = b / c

Tactic:
refine eq_div_of_mul_eq_right hc (mul_left_cancel₀ ha ?_)

Result:
case neg
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * (c * (a * b / (a * c))) = a * b

Proof state:
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
⊢ a * b / (a * c) = b / c

Tactic:
by_cases hc : c = 0

Result:
case pos
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : c = 0
⊢ a * b / (a * c) = b / c

case neg
R : Type u
inst✝ : EuclideanDomain R
a b c : R
ha : a ≠ 0
hcb : c ∣ b
hc : ¬c = 0
⊢ a * b / (a * c) = b / c
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem succ_le_iff' {a b : Ordinal} : a + 1 ≤ b ↔ a < b

Proof state:
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : r ≺i s
⊢ ∀ (a b : α ⊕ PUnit.{u_1 + 1}),
    Sum.Lex r EmptyRelation a b →
      s ((fun x => Sum.recOn x ⇑f.toRelEmbedding fun x => f.top) a)
        ((fun x => Sum.recOn x ⇑f.toRelEmbedding fun x => f.top) b)

Tactic:
simpa [f.map_rel_iff] using f.lt_top

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
⊢ a + 1 ≤ b ↔ a < b

Tactic:
refine inductionOn₂ a b fun α r _ β s _ ↦ ⟨?_, ?_⟩ <;> rintro ⟨f⟩

Result:
case refine_1.intro
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : Sum.Lex r EmptyRelation ≼i s
⊢ type r < type s

case refine_2.intro
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : r ≺i s
⊢ type r + 1 ≤ type s

Proof state:
case refine_1.intro
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : Sum.Lex r EmptyRelation ≼i s
⊢ type r < type s

Tactic:
refine ⟨((InitialSeg.leAdd _ _).trans f).toPrincipalSeg fun h ↦ ?_⟩

Result:
case refine_1.intro
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : Sum.Lex r EmptyRelation ≼i s
h : Surjective ⇑((InitialSeg.leAdd r EmptyRelation).trans f)
⊢ False

Proof state:
case refine_1.intro
a b : Ordinal.{u_1}
α : Type u_1
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_1
s : β → β → Prop
x✝ : IsWellOrder β s
f : Sum.Lex r EmptyRelation ≼i s
h : Surjective ⇑((InitialSeg.leAdd r EmptyRelation).trans f)
⊢ False

Tactic:
simpa using h (f (Sum.inr PUnit.unit))

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem fin_app {n} : Primrec₂ (@id (Fin n → σ)) :=
  (vector_get.comp (vector_ofFn'.comp fst) snd).of_eq fun ⟨v, i⟩ => by simp

Proof state:
σ : Type u_3
inst✝ : Primcodable σ
n : ℕ
x✝ : (Fin n → σ) × Fin n
v : Fin n → σ
i : Fin n
⊢ (List.Vector.ofFn (v, i).1).get (v, i).2 = id (v, i).1 (v, i).2

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Distributions/Pareto.lean
/-- The Pareto pdf is nonnegative. -/
lemma paretoPDFReal_nonneg (ht : 0 ≤ t) (hr : 0 ≤ r) (x : ℝ) :
    0 ≤ paretoPDFReal t r x

Proof state:
case pos.inl
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : t ≤ x
ht0 : 0 = t
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))

Tactic:
rw [← ht0] at h

Result:
case pos.inl
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : 0 ≤ x
ht0 : 0 = t
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))

Proof state:
case pos
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : t ≤ x
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))

Tactic:
cases le_iff_eq_or_lt.1 ht with
| inl ht0 =>
  rw [← ht0] at h
  positivity
| inr htp =>
  have := lt_of_lt_of_le htp h
  positivity

Result:
no goals

Proof state:
case neg
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : ¬t ≤ x
⊢ 0 ≤ 0

Tactic:
positivity

Result:
no goals

Proof state:
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
⊢ 0 ≤ paretoPDFReal t r x

Tactic:
unfold paretoPDFReal

Result:
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
⊢ 0 ≤ if t ≤ x then r * t ^ r * x ^ (-(r + 1)) else 0

Proof state:
case pos.inr
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : t ≤ x
htp : 0 < t
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))

Tactic:
have := lt_of_lt_of_le htp h

Result:
case pos.inr
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : t ≤ x
htp : 0 < t
this : 0 < x
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))

Proof state:
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
⊢ 0 ≤ if t ≤ x then r * t ^ r * x ^ (-(r + 1)) else 0

Tactic:
split_ifs with h

Result:
case pos
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : t ≤ x
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))

case neg
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : ¬t ≤ x
⊢ 0 ≤ 0

Proof state:
case pos.inl
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : 0 ≤ x
ht0 : 0 = t
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))

Tactic:
positivity

Result:
no goals

Proof state:
case pos.inr
t r : ℝ
ht : 0 ≤ t
hr : 0 ≤ r
x : ℝ
h : t ≤ x
htp : 0 < t
this : 0 < x
⊢ 0 ≤ r * t ^ r * x ^ (-(r + 1))

Tactic:
positivity

Result:
no goals
-- Mathlib/Computability/ContextFreeGrammar.lean
/-- Add extra prefix to context-free deriving. -/
lemma Derives.append_left {v w : List (Symbol T g.NT)}
    (hvw : g.Derives v w) (p : List (Symbol T g.NT)) :
    g.Derives (p ++ v) (p ++ w)

Proof state:
case tail
T : Type u_1
g : ContextFreeGrammar T
v w p b✝ c✝ : List (Symbol T g.NT)
a✝ : Relation.ReflTransGen g.Produces v b✝
last : g.Produces b✝ c✝
ih : g.Derives (p ++ v) (p ++ b✝)
⊢ g.Derives (p ++ v) (p ++ c✝)

Tactic:
exact ih.trans_produces <| last.append_left p

Result:
no goals

Proof state:
T : Type u_1
g : ContextFreeGrammar T
v w : List (Symbol T g.NT)
hvw : g.Derives v w
p : List (Symbol T g.NT)
⊢ g.Derives (p ++ v) (p ++ w)

Tactic:
induction hvw with
| refl => rfl
| tail _ last ih => exact ih.trans_produces <| last.append_left p

Result:
no goals

Proof state:
case refl
T : Type u_1
g : ContextFreeGrammar T
v w p : List (Symbol T g.NT)
⊢ g.Derives (p ++ v) (p ++ v)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
@[to_additive]
lemma eq_of_prod_take_eq [LeftCancelMonoid M] {L L' : List M} (h : L.length = L'.length)
    (h' : ∀ i ≤ L.length, (L.take i).prod = (L'.take i).prod) : L = L'

Proof state:
M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
this : (take i L').prod * L[i] = (take i L').prod * L'[i]
⊢ L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩

Tactic:
convert mul_left_cancel this

Result:
no goals

Proof state:
M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
⊢ L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩

Tactic:
have : (L.take (i + 1)).prod = (L'.take (i + 1)).prod := h' _ (Nat.succ_le_of_lt h₁)

Result:
M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
this : (take (i + 1) L).prod = (take (i + 1) L').prod
⊢ L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩

Proof state:
M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
this : (take (i + 1) L).prod = (take (i + 1) L').prod
⊢ L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩

Tactic:
rw [prod_take_succ L i h₁, prod_take_succ L' i h₂, h' i (le_of_lt h₁)] at this

Result:
M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
this : (take i L').prod * L[i] = (take i L').prod * L'[i]
⊢ L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩

Proof state:
M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
⊢ L = L'

Tactic:
refine ext_get h fun i h₁ h₂ => ?_

Result:
M : Type u_4
inst✝ : LeftCancelMonoid M
L L' : List M
h : L.length = L'.length
h' : ∀ (i : ℕ), i ≤ L.length → (take i L).prod = (take i L').prod
i : ℕ
h₁ : i < L.length
h₂ : i < L'.length
⊢ L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩
-- Mathlib/Algebra/Order/Group/Defs.lean
theorem inv_lt_self_iff : a⁻¹ < a ↔ 1 < a

Proof state:
α : Type u
inst✝ : LinearOrderedCommGroup α
a : α
⊢ a⁻¹ < a ↔ 1 < a

Tactic:
simp [inv_lt_iff_one_lt_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Sublist.lean
theorem isSuffix_iff : l₁ <:+ l₂ ↔
    l₁.length ≤ l₂.length ∧ ∀ i (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i]

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
le : l₁.length ≤ l₂.length
w : ∀ (i : Nat) (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i]
i : Nat
h : i < l₁.length
⊢ l₁.length - 1 - i < l₁.length

Tactic:
omega

Result:
no goals

Proof state:
case mp
α✝ : Type u_1
l₁ l₂ : List α✝
this :
  l₁.length ≤ l₂.length ∧ l₁ <:+ l₂ ↔
    l₁.length ≤ l₂.length ∧ ∀ (i : Nat) (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i]
h : l₁ <:+ l₂
⊢ l₁.length ≤ l₂.length ∧ ∀ (i : Nat) (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i]

Tactic:
exact this.mp ⟨h.length_le, h⟩

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
lemma equalizerCondition_w' (P : Cᵒᵖ ⥤ Type*) {X B : C} (π : X ⟶ B)
    [HasPullback π π] : P.map π.op ≫ P.map (pullback.fst π π).op =
    P.map π.op ≫ P.map (pullback.snd π π).op

Proof state:
C : Type u_1
inst✝¹ : Category.{u_5, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
⊢ P.map π.op ≫ P.map (pullback.fst π π).op = P.map π.op ≫ P.map (pullback.snd π π).op

Tactic:
simp only [← Functor.map_comp, ← op_comp, pullback.condition]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean
theorem integral_comp_neg_Ioi {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    (c : ℝ) (f : ℝ → E) : (∫ x in Ioi c, f (-x)) = ∫ x in Iic (-c), f x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
⊢ ∫ (x : ℝ) in Iic (-c), f (- -x) = ∫ (x : ℝ) in Iic (- - -c), f x

Tactic:
simp only [neg_neg]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
⊢ ∫ (x : ℝ) in Ioi c, f (-x) = ∫ (x : ℝ) in Iic (-c), f x

Tactic:
rw [← neg_neg c, ← integral_comp_neg_Iic]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
c : ℝ
f : ℝ → E
⊢ ∫ (x : ℝ) in Iic (-c), f (- -x) = ∫ (x : ℝ) in Iic (- - -c), f x
-- Mathlib/Data/Complex/Norm.lean
theorem abs_re_lt_norm {z : ℂ} : |z.re| < ‖z‖ ↔ z.im ≠ 0

Proof state:
z : ℂ
⊢ |z.re| < ‖z‖ ↔ z.im ≠ 0

Tactic:
rw [norm_def, Real.lt_sqrt (abs_nonneg _), normSq_apply, sq_abs, ← sq, lt_add_iff_pos_right,
  mul_self_pos]

Result:
no goals
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive] lemma leOnePart_eq_ite : a⁻ᵐ = if a ≤ 1 then a⁻¹ else 1

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = if a ≤ 1 then a⁻¹ else 1

Tactic:
simp_rw [← one_le_inv']

Result:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = if 1 ≤ a⁻¹ then a⁻¹ else 1

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻¹ ⊔ 1 = (fun x1 x2 => x1 ⊔ x2) 1 a⁻¹

Tactic:
simp_rw [sup_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻ᵐ = if 1 ≤ a⁻¹ then a⁻¹ else 1

Tactic:
rw [leOnePart_def, ← maxDefault, ← sup_eq_maxDefault]

Result:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : Group α
a : α
inst✝ : MulLeftMono α
⊢ a⁻¹ ⊔ 1 = (fun x1 x2 => x1 ⊔ x2) 1 a⁻¹
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
lemma image_insert_memberSubfamily (𝒜 : Finset (Finset α)) (a : α) :
    (𝒜.memberSubfamily a).image (insert a) = {s ∈ 𝒜 | a ∈ s}

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
⊢ (∃ a_1, (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) ↔ s ∈ 𝒜 ∧ a ∈ s

Tactic:
refine ⟨?_, fun ⟨hs, ha⟩ ↦ ⟨erase s a, ⟨?_, not_mem_erase _ _⟩, insert_erase ha⟩⟩

Result:
case h.refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
⊢ (∃ a_1, (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) → s ∈ 𝒜 ∧ a ∈ s

case h.refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
x✝ : s ∈ 𝒜 ∧ a ∈ s
hs : s ∈ 𝒜
ha : a ∈ s
⊢ insert a (s.erase a) ∈ 𝒜

Proof state:
case h.refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
⊢ (∃ a_1, (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) → s ∈ 𝒜 ∧ a ∈ s

Tactic:
rintro ⟨s, ⟨hs, -⟩, rfl⟩

Result:
case h.refine_1.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
hs : insert a s ∈ 𝒜
⊢ insert a s ∈ 𝒜 ∧ a ∈ insert a s

Proof state:
case h.refine_1.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
hs : insert a s ∈ 𝒜
⊢ insert a s ∈ 𝒜 ∧ a ∈ insert a s

Tactic:
exact ⟨hs, mem_insert_self _ _⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ image (insert a) (memberSubfamily a 𝒜) = filter (fun s => a ∈ s) 𝒜

Tactic:
ext s

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
⊢ s ∈ image (insert a) (memberSubfamily a 𝒜) ↔ s ∈ filter (fun s => a ∈ s) 𝒜

Proof state:
case h.refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
x✝ : s ∈ 𝒜 ∧ a ∈ s
hs : s ∈ 𝒜
ha : a ∈ s
⊢ insert a (s.erase a) ∈ 𝒜

Tactic:
rwa [insert_erase ha]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
⊢ s ∈ image (insert a) (memberSubfamily a 𝒜) ↔ s ∈ filter (fun s => a ∈ s) 𝒜

Tactic:
simp only [mem_memberSubfamily, mem_image, mem_filter]

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
⊢ (∃ a_1, (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) ↔ s ∈ 𝒜 ∧ a ∈ s
-- Mathlib/Topology/Algebra/GroupCompletion.lean
theorem AddMonoidHom.completion_zero :
    AddMonoidHom.completion (0 : α →+ β) continuous_const = 0

Proof state:
case h.refine_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
a : α
⊢ (completion 0 ⋯) ↑a = 0 ↑a

Tactic:
simp [(0 : α →+ β).completion_coe continuous_const, coe_zero]

Result:
no goals

Proof state:
case h.refine_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
⊢ ∀ (a : α), (completion 0 ⋯) ↑a = 0 ↑a

Tactic:
intro a

Result:
case h.refine_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
a : α
⊢ (completion 0 ⋯) ↑a = 0 ↑a

Proof state:
case h.refine_1
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
⊢ IsClosed {a | (completion 0 ⋯) a = 0 a}

Tactic:
apply isClosed_eq (AddMonoidHom.continuous_completion (0 : α →+ β) continuous_const)

Result:
case h.refine_1
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
⊢ Continuous ⇑0

Proof state:
case h
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
⊢ (completion 0 ⋯) x = 0 x

Tactic:
refine Completion.induction_on x ?_ ?_

Result:
case h.refine_1
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
⊢ IsClosed {a | (completion 0 ⋯) a = 0 a}

case h.refine_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
⊢ ∀ (a : α), (completion 0 ⋯) ↑a = 0 ↑a

Proof state:
case h.refine_1
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
⊢ Continuous ⇑0

Tactic:
exact continuous_const

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
⊢ completion 0 ⋯ = 0

Tactic:
ext x

Result:
case h
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
⊢ (completion 0 ⋯) x = 0 x
-- Mathlib/Data/List/InsertIdx.lean
theorem get_insertIdx_add_succ (l : List α) (x : α) (n k : ℕ) (hk' : n + k < l.length)
    (hk : n + k + 1 < (insertIdx n x l).length := (by
      rwa [length_insertIdx_of_le_length (by omega), Nat.succ_lt_succ_iff])) :
    (insertIdx n x l).get ⟨n + k + 1, hk⟩ = get l ⟨n + k, hk'⟩

Proof state:
α : Type u
β : Type v
a : α
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
⊢ n + k + 1 < (insertIdx n x l).length

Tactic:
rwa [length_insertIdx_of_le_length (by omega), Nat.succ_lt_succ_iff]

Result:
no goals

Proof state:
α : Type u
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
hk : optParam (n + k + 1 < (insertIdx n x l).length) ⋯
⊢ (insertIdx n x l).get ⟨n + k + 1, hk⟩ = l.get ⟨n + k, hk'⟩

Tactic:
simp [getElem_insertIdx_add_succ, hk, hk']

Result:
no goals

Proof state:
α : Type u
β : Type v
a : α
l : List α
x : α
n k : ℕ
hk' : n + k < l.length
⊢ n ≤ l.length

Tactic:
omega

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/DoubleCounting.lean
theorem card_nsmul_lt_card_nsmul_of_lt_of_le [∀ a b, Decidable (r a b)] (hs : s.Nonempty)
    (hm : ∀ a ∈ s, m < #(t.bipartiteAbove r a))
    (hn : ∀ b ∈ t, #(s.bipartiteBelow r b) ≤ n) : #s • m < #t • n :=
  calc
    _ = ∑ _a ∈ s, m

Proof state:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : StrictOrderedSemiring R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hs : s.Nonempty
hm : ∀ a ∈ s, m < ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ ∑ x ∈ s, #(bipartiteAbove r t x) = ∑ x ∈ t, #(bipartiteBelow r s x)

Tactic:
rw [sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow]

Result:
no goals

Proof state:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : StrictOrderedSemiring R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hs : s.Nonempty
hm : ∀ a ∈ s, m < ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ #s • m = ∑ _a ∈ s, m

Tactic:
rw [sum_const]

Result:
no goals

Proof state:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : StrictOrderedSemiring R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hs : s.Nonempty
hm : ∀ a ∈ s, m < ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ ∑ a ∈ s, ↑(#(bipartiteAbove r t a)) = ∑ b ∈ t, ↑(#(bipartiteBelow r s b))

Tactic:
norm_cast

Result:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : StrictOrderedSemiring R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hs : s.Nonempty
hm : ∀ a ∈ s, m < ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ ∑ x ∈ s, #(bipartiteAbove r t x) = ∑ x ∈ t, #(bipartiteBelow r s x)
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem induction_on' {M : R[X] → Prop} (p : R[X]) (h_add : ∀ p q, M p → M q → M (p + q))
    (h_monomial : ∀ (n : ℕ) (a : R), M (monomial n a)) : M p :=
  Polynomial.induction_on p (h_monomial 0) h_add fun n a _h =>
    by rw [C_mul_X_pow_eq_monomial]; exact h_monomial _ _

Proof state:
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
p : R[X]
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M ((monomial n) a)
n : ℕ
a : R
_h : M (C a * X ^ n)
⊢ M ((monomial (n + 1)) a)

Tactic:
exact h_monomial _ _

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
p : R[X]
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M ((monomial n) a)
n : ℕ
a : R
_h : M (C a * X ^ n)
⊢ M (C a * X ^ (n + 1))

Tactic:
rw [C_mul_X_pow_eq_monomial]

Result:
R : Type u
inst✝ : Semiring R
M : R[X] → Prop
p : R[X]
h_add : ∀ (p q : R[X]), M p → M q → M (p + q)
h_monomial : ∀ (n : ℕ) (a : R), M ((monomial n) a)
n : ℕ
a : R
_h : M (C a * X ^ n)
⊢ M ((monomial (n + 1)) a)
-- Mathlib/Probability/Independence/Basic.lean
lemma iIndepSets.isProbabilityMeasure (h : iIndepSets π μ) : IsProbabilityMeasure μ :=
  ⟨by simpa using h ∅ (f := fun _ ↦ univ)⟩

Proof state:
Ω : Type u_1
ι : Type u_2
π : ι → Set (Set Ω)
x✝ : MeasurableSpace Ω
μ : Measure Ω
h : iIndepSets π μ
⊢ μ univ = 1

Tactic:
simpa using h ∅ (f := fun _ ↦ univ)

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem ascFactorial_lt_pow_add (n : ℕ) : ∀ {k : ℕ}, 2 ≤ k → (n + 1).ascFactorial k < (n + k) ^ k
  | 0 => by rintro ⟨⟩
  | 1 => by intro; contradiction
  | k + 2 => fun _ => by
    rw [Nat.pow_succ, Nat.mul_comm, ascFactorial_succ, succ_add_eq_add_succ n (k + 1)]
    exact Nat.mul_lt_mul_of_le_of_lt (le_refl _) (Nat.lt_of_le_of_lt (ascFactorial_le_pow_add n _)
      (Nat.pow_lt_pow_left (Nat.lt_succ_self _) k.succ_ne_zero)) (succ_pos _)

Proof state:
n : ℕ
⊢ 2 ≤ 1 → (n + 1).ascFactorial 1 < (n + 1) ^ 1

Tactic:
intro

Result:
n : ℕ
a✝ : 2 ≤ 1
⊢ (n + 1).ascFactorial 1 < (n + 1) ^ 1

Proof state:
n : ℕ
a✝ : 2 ≤ 1
⊢ (n + 1).ascFactorial 1 < (n + 1) ^ 1

Tactic:
contradiction

Result:
no goals

Proof state:
n : ℕ
⊢ 2 ≤ 0 → (n + 1).ascFactorial 0 < (n + 0) ^ 0

Tactic:
rintro ⟨⟩

Result:
no goals

Proof state:
n k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n + 1).ascFactorial (k + 2) < (n + (k + 2)) ^ (k + 2)

Tactic:
rw [Nat.pow_succ, Nat.mul_comm, ascFactorial_succ, succ_add_eq_add_succ n (k + 1)]

Result:
n k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n + (k + 1).succ) * (n + 1).ascFactorial (k + 1) < (n + (k + 2)) * (n + (k + 2)) ^ (k + 1)

Proof state:
n k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n + (k + 1).succ) * (n + 1).ascFactorial (k + 1) < (n + (k + 2)) * (n + (k + 2)) ^ (k + 1)

Tactic:
exact Nat.mul_lt_mul_of_le_of_lt (le_refl _) (Nat.lt_of_le_of_lt (ascFactorial_le_pow_add n _)
  (Nat.pow_lt_pow_left (Nat.lt_succ_self _) k.succ_ne_zero)) (succ_pos _)

Result:
no goals