harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/ForwardDiff.lean
lemma fwdDiff_iter_choose_zero (m n : ℕ) :
    Δ_[1]^[n] (fun x ↦ x.choose m : ℕ → ℤ) 0 = if n = m then 1 else 0

Proof state:
case inl
m n : ℕ
hmn : m < n
⊢ Δ_[1]^[n] (fun x => ↑(x.choose m)) 0 = if n = m then 1 else 0

Tactic:
rcases Nat.exists_eq_add_of_lt hmn with ⟨k, rfl⟩

Result:
case inl.intro
m k : ℕ
hmn : m < m + k + 1
⊢ Δ_[1]^[m + k + 1] (fun x => ↑(x.choose m)) 0 = if m + k + 1 = m then 1 else 0

Proof state:
m n : ℕ
⊢ Δ_[1]^[n] (fun x => ↑(x.choose m)) 0 = if n = m then 1 else 0

Tactic:
rcases lt_trichotomy m n with hmn | rfl | hnm

Result:
case inl
m n : ℕ
hmn : m < n
⊢ Δ_[1]^[n] (fun x => ↑(x.choose m)) 0 = if n = m then 1 else 0

case inr.inl
m : ℕ
⊢ Δ_[1]^[m] (fun x => ↑(x.choose m)) 0 = if m = m then 1 else 0

case inr.inr
m n : ℕ
hnm : n < m
⊢ Δ_[1]^[n] (fun x => ↑(x.choose m)) 0 = if n = m then 1 else 0

Proof state:
case inr.inr
m n : ℕ
hnm : n < m
⊢ Δ_[1]^[n] (fun x => ↑(x.choose m)) 0 = if n = m then 1 else 0

Tactic:
rcases Nat.exists_eq_add_of_lt hnm with ⟨k, rfl⟩

Result:
case inr.inr.intro
n k : ℕ
hnm : n < n + k + 1
⊢ Δ_[1]^[n] (fun x => ↑(x.choose (n + k + 1))) 0 = if n = n + k + 1 then 1 else 0

Proof state:
case inr.inr.intro
n k : ℕ
hnm : n < n + k + 1
⊢ Δ_[1]^[n] (fun x => ↑(x.choose (n + k + 1))) 0 = if n = n + k + 1 then 1 else 0

Tactic:
simp_rw [hnm.ne, if_false, add_assoc n k 1, fwdDiff_iter_choose, choose_zero_succ, cast_zero]

Result:
no goals

Proof state:
m k : ℕ
hmn : m < m + k + 1
⊢ m + k + 1 = k + 1 + m

Tactic:
ring

Result:
no goals

Proof state:
case inr.inl
m : ℕ
⊢ Δ_[1]^[m] (fun x => ↑(x.choose m)) 0 = if m = m then 1 else 0

Tactic:
simp only [if_true, add_zero m ▸ fwdDiff_iter_choose 0 m, choose_zero_right, cast_one]

Result:
no goals

Proof state:
case inl.intro
m k : ℕ
hmn : m < m + k + 1
⊢ Δ_[1]^[m + k + 1] (fun x => ↑(x.choose m)) 0 = if m + k + 1 = m then 1 else 0

Tactic:
simp_rw [hmn.ne', if_false, (by ring : m + k + 1 = k + 1 + m), iterate_add_apply,
  add_zero m ▸ fwdDiff_iter_choose 0 m, choose_zero_right, iterate_one, cast_one, fwdDiff_const,
  fwdDiff_iter_eq_sum_shift, smul_zero, sum_const_zero]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/ZPow.lean
theorem hasStrictDerivAt_zpow (m : ℤ) (x : 𝕜) (h : x ≠ 0 ∨ 0 ≤ m) :
    HasStrictDerivAt (fun x => x ^ m) ((m : 𝕜) * x ^ (m - 1)) x

Proof state:
case intro
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m✝ : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m✝
m : ℕ
hm : 0 < ↑m
⊢ HasStrictDerivAt (fun x => x ^ m) (↑m * x ^ (↑m - 1)) x

Tactic:
convert hasStrictDerivAt_pow m x using 2

Result:
case h.e'_9.h.e'_6
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m✝ : ℤ
x : 𝕜
h : x ≠ 0 ∨ 0 ≤ m✝
m : ℕ
hm : 0 < ↑m
⊢ x ^ (↑m - 1) = x ^ (m - 1)
-- Mathlib/FieldTheory/Separable.lean
theorem eq_X_sub_C_of_separable_of_root_eq {x : F} {h : F[X]} (h_sep : h.Separable)
    (h_root : h.eval x = 0) (h_splits : Splits i h) (h_roots : ∀ y ∈ (h.map i).roots, y = i x) :
    h = C (leadingCoeff h) * (X - C x)

Proof state:
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ y ∈ (map i h).roots, y = i x
⊢ h ≠ 0

Tactic:
rintro rfl

Result:
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h_sep : Separable 0
h_root : eval x 0 = 0
h_splits : Splits i 0
h_roots : ∀ y ∈ (map i 0).roots, y = i x
⊢ False

Proof state:
case x.right
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ y ∈ (map i h).roots, y = i x
h_ne_zero : h ≠ 0
⊢ ∀ x_1 ∈ { val := (map i h).roots, nodup := ⋯ }, x_1 = i x

Tactic:
exact h_roots

Result:
no goals

Proof state:
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ y ∈ (map i h).roots, y = i x
h_ne_zero : h ≠ 0
⊢ h = C h.leadingCoeff * (X - C x)

Tactic:
apply Polynomial.eq_X_sub_C_of_splits_of_single_root i h_splits

Result:
F : Type u
inst✝¹ : Field F
K : Type v
inst✝ : Field K
i : F →+* K
x : F
h : F[X]
h_sep : h.Separable
h_root : eval x h = 0
h_splits : Splits i h
h_roots : ∀ y ∈ (map i h).roots, y = i x
h_ne_zero : h ≠ 0
⊢ (map i h).roots = {i x}
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem continuous_from_bounded {p : SeminormFamily 𝕝 E ι} {q : SeminormFamily 𝕝₂ F ι'}
    {_ : TopologicalSpace E} (hp : WithSeminorms p) {_ : TopologicalSpace F} (hq : WithSeminorms q)
    (f : E →ₛₗ[τ₁₂] F) (hf : Seminorm.IsBounded p q f) : Continuous f

Proof state:
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι : Type u_8
ι' : Type u_9
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕝
inst✝⁶ : Module 𝕝 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : NormedField 𝕝₂
inst✝³ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝² : RingHomIsometric τ₁₂
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
⊢ Continuous ⇑((q i).comp f)

Tactic:
rcases hf i with ⟨s, C, hC⟩

Result:
case intro.intro
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι : Type u_8
ι' : Type u_9
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕝
inst✝⁶ : Module 𝕝 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : NormedField 𝕝₂
inst✝³ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝² : RingHomIsometric τ₁₂
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ C • s.sup p
⊢ Continuous ⇑((q i).comp f)

Proof state:
case intro.intro
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι : Type u_8
ι' : Type u_9
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕝
inst✝⁶ : Module 𝕝 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : NormedField 𝕝₂
inst✝³ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝² : RingHomIsometric τ₁₂
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
⊢ Continuous fun x => (coeFnAddMonoidHom 𝕝 E) (∑ i ∈ s, C • p i) x

Tactic:
simp_rw [map_sum, Finset.sum_apply]

Result:
case intro.intro
𝕝 : Type u_3
𝕝₂ : Type u_4
E : Type u_5
F : Type u_6
ι : Type u_8
ι' : Type u_9
inst✝⁸ : AddCommGroup E
inst✝⁷ : NormedField 𝕝
inst✝⁶ : Module 𝕝 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : NormedField 𝕝₂
inst✝³ : Module 𝕝₂ F
τ₁₂ : 𝕝 →+* 𝕝₂
inst✝² : RingHomIsometric τ₁₂
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
p : SeminormFamily 𝕝 E ι
q : SeminormFamily 𝕝₂ F ι'
x✝¹ : TopologicalSpace E
hp : WithSeminorms p
x✝ : TopologicalSpace F
hq : WithSeminorms q
f : E →ₛₗ[τ₁₂] F
hf : IsBounded p q f
this : IsTopologicalAddGroup E
i : ι'
s : Finset ι
C : ℝ≥0
hC : (q i).comp f ≤ s.sup (C • p)
⊢ Continuous fun x => ∑ c ∈ s, (coeFnAddMonoidHom 𝕝 E) (C • p c) x
-- Mathlib/Analysis/Convex/StrictConvexSpace.lean
theorem norm_combo_lt_of_ne (hx : ‖x‖ ≤ r) (hy : ‖y‖ ≤ r) (hne : x ≠ y) (ha : 0 < a) (hb : 0 < b)
    (hab : a + b = 1) : ‖a • x + b • y‖ < r

Proof state:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
a b r : ℝ
hx : ‖x‖ ≤ r
hy : ‖y‖ ≤ r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ‖a • x + b • y‖ < r

Tactic:
simp only [← mem_ball_zero_iff, ← mem_closedBall_zero_iff] at hx hy ⊢

Result:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
a b r : ℝ
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : x ∈ closedBall 0 r
hy : y ∈ closedBall 0 r
⊢ a • x + b • y ∈ ball 0 r

Proof state:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y : E
a b r : ℝ
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : x ∈ closedBall 0 r
hy : y ∈ closedBall 0 r
⊢ a • x + b • y ∈ ball 0 r

Tactic:
exact combo_mem_ball_of_ne hx hy hne ha hb hab

Result:
no goals
-- Mathlib/Algebra/CharP/Quotient.lean
theorem Ideal.Quotient.index_eq_zero {R : Type*} [CommRing R] (I : Ideal R) :
    (↑I.toAddSubgroup.index : R ⧸ I) = 0

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
this : Fintype (R ⧸ I) := Fintype.ofFinite (R ⧸ I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0

Tactic:
exact Nat.cast_card_eq_zero (R ⧸ I)

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0

Tactic:
letI : Fintype (R ⧸ I) := @Fintype.ofFinite _ hq

Result:
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
this : Fintype (R ⧸ I) := Fintype.ofFinite (R ⧸ I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0

case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : ¬Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑0 = 0

Tactic:
swap

Result:
case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : ¬Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑0 = 0

case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : ¬Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑0 = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ↑(if x : Finite (R ⧸ Submodule.toAddSubgroup I) then Fintype.card (R ⧸ Submodule.toAddSubgroup I) else 0) = 0

Tactic:
split_ifs with hq

Result:
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑(Fintype.card (R ⧸ Submodule.toAddSubgroup I)) = 0

case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hq : ¬Finite (R ⧸ Submodule.toAddSubgroup I)
⊢ ↑0 = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ↑(Submodule.toAddSubgroup I).index = 0

Tactic:
rw [AddSubgroup.index, Nat.card_eq]

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ↑(if x : Finite (R ⧸ Submodule.toAddSubgroup I) then Fintype.card (R ⧸ Submodule.toAddSubgroup I) else 0) = 0
-- Mathlib/RingTheory/Finiteness/Subalgebra.lean
theorem FG.pow (h : M.FG) (n : ℕ) : (M ^ n).FG :=
  Nat.recOn n ⟨{1}, by simp [one_eq_span]⟩ fun n ih => by simpa [pow_succ] using ih.mul h

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
h : M.FG
n : ℕ
⊢ span R ↑{1} = M ^ Nat.zero

Tactic:
simp [one_eq_span]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
M : Submodule R A
h : M.FG
n✝ n : ℕ
ih : (M ^ n).FG
⊢ (M ^ n.succ).FG

Tactic:
simpa [pow_succ] using ih.mul h

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_eq_zero_iff_neg_one [LinearOrderedRing α] (hn : n ≠ 0) :
    ∑ i ∈ range n, x ^ i = 0 ↔ x = -1 ∧ Even n

Proof state:
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
⊢ ∑ i ∈ range n, x ^ i = 0 ↔ x = -1 ∧ Even n

Tactic:
refine ⟨fun h => ?_, @fun ⟨h, hn⟩ => by simp only [h, hn, neg_one_geom_sum, if_true]⟩

Result:
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : ∑ i ∈ range n, x ^ i = 0
⊢ x = -1 ∧ Even n

Proof state:
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : ∑ i ∈ range n, x ^ i = 0
⊢ x = -1 ∧ Even n

Tactic:
contrapose! h

Result:
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
⊢ ∑ i ∈ range n, x ^ i ≠ 0

Proof state:
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
⊢ ∑ i ∈ range n, x ^ i ≠ 0

Tactic:
have hx := eq_or_ne x (-1)

Result:
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1 ∨ x ≠ -1
⊢ ∑ i ∈ range n, x ^ i ≠ 0

Proof state:
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn✝ : n ≠ 0
x✝ : x = -1 ∧ Even n
h : x = -1
hn : Even n
⊢ ∑ i ∈ range n, x ^ i = 0

Tactic:
simp only [h, hn, neg_one_geom_sum, if_true]

Result:
no goals

Proof state:
case inl
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ (if Even n then 0 else 1) ≠ 0

Tactic:
simp only [h hx, ite_false, ne_eq, one_ne_zero, not_false_eq_true]

Result:
no goals

Proof state:
case inr
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x ≠ -1
⊢ ∑ i ∈ range n, x ^ i ≠ 0

Tactic:
exact geom_sum_ne_zero hx hn

Result:
no goals

Proof state:
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1 ∨ x ≠ -1
⊢ ∑ i ∈ range n, x ^ i ≠ 0

Tactic:
rcases hx with hx | hx

Result:
case inl
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ ∑ i ∈ range n, x ^ i ≠ 0

case inr
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x ≠ -1
⊢ ∑ i ∈ range n, x ^ i ≠ 0

Proof state:
case inl
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ ∑ i ∈ range n, x ^ i ≠ 0

Tactic:
rw [hx, neg_one_geom_sum]

Result:
case inl
α : Type u
n : ℕ
x : α
inst✝ : LinearOrderedRing α
hn : n ≠ 0
h : x = -1 → ¬Even n
hx : x = -1
⊢ (if Even n then 0 else 1) ≠ 0
-- Mathlib/Topology/Baire/BaireMeasurable.lean
theorem _root_.MeasurableSet.baireMeasurableSet [MeasurableSpace α] [BorelSpace α]
    (h : MeasurableSet s) : BaireMeasurableSet s

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
h : MeasurableSet s
⊢ BaireMeasurableSet s

Tactic:
borelize α

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : BorelSpace α
h : MeasurableSet s
this✝ : MeasurableSpace α := borel α
⊢ BaireMeasurableSet s

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : BorelSpace α
h : MeasurableSet s
this✝ : MeasurableSpace α := borel α
⊢ BaireMeasurableSet s

Tactic:
exact h.eventuallyMeasurableSet

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[simp, norm_cast] lemma coe_lt_enorm : r < ‖x‖ₑ ↔ r < ‖x‖₊

Proof state:
E : Type u_8
inst✝ : NNNorm E
x : E
r : ℝ≥0
⊢ ↑r < ‖x‖ₑ ↔ r < ‖x‖₊

Tactic:
simp [enorm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} :
    (replicate n a).eraseIdx k = if k < n then replicate (n - 1) a else replicate n a

Proof state:
case isTrue
α : Type u_1
n : Nat
a : α
k : Nat
h : k < n
b : α
m : b ∈ replicate n a
⊢ b = a

Tactic:
simp only [mem_replicate] at m

Result:
case isTrue
α : Type u_1
n : Nat
a : α
k : Nat
h : k < n
b : α
m : n ≠ 0 ∧ b = a
⊢ b = a

Proof state:
case isTrue
α : Type u_1
n : Nat
a : α
k : Nat
h : k < n
⊢ (replicate n a).length - 1 = n - 1 ∧ ∀ (b : α), b ∈ (replicate n a).eraseIdx k → b = a

Tactic:
simp only [length_replicate, true_and]

Result:
case isTrue
α : Type u_1
n : Nat
a : α
k : Nat
h : k < n
⊢ ∀ (b : α), b ∈ (replicate n a).eraseIdx k → b = a

Proof state:
α : Type u_1
n : Nat
a : α
k : Nat
h : k < n
⊢ k < (replicate n a).length

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
k : Nat
⊢ (replicate n a).eraseIdx k = if k < n then replicate (n - 1) a else replicate n a

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
n : Nat
a : α
k : Nat
h : k < n
⊢ (replicate n a).eraseIdx k = replicate (n - 1) a

case isFalse
α : Type u_1
n : Nat
a : α
k : Nat
h : ¬k < n
⊢ (replicate n a).eraseIdx k = replicate n a

Proof state:
case isTrue
α : Type u_1
n : Nat
a : α
k : Nat
h : k < n
⊢ ∀ (b : α), b ∈ (replicate n a).eraseIdx k → b = a

Tactic:
intro b m

Result:
case isTrue
α : Type u_1
n : Nat
a : α
k : Nat
h : k < n
b : α
m : b ∈ (replicate n a).eraseIdx k
⊢ b = a

Proof state:
α : Type u_1
n : Nat
a : α
k : Nat
h : ¬k < n
⊢ (replicate n a).length ≤ k

Tactic:
simpa using h

Result:
no goals

Proof state:
case isTrue
α : Type u_1
n : Nat
a : α
k : Nat
h : k < n
b : α
m : n ≠ 0 ∧ b = a
⊢ b = a

Tactic:
exact m.2

Result:
no goals

Proof state:
case isFalse
α : Type u_1
n : Nat
a : α
k : Nat
h : ¬k < n
⊢ (replicate n a).eraseIdx k = replicate n a

Tactic:
rw [eraseIdx_of_length_le (by simpa using h)]

Result:
no goals

Proof state:
case isTrue
α : Type u_1
n : Nat
a : α
k : Nat
h : k < n
b : α
m : b ∈ (replicate n a).eraseIdx k
⊢ b = a

Tactic:
replace m := mem_of_mem_eraseIdx m

Result:
case isTrue
α : Type u_1
n : Nat
a : α
k : Nat
h : k < n
b : α
m : b ∈ replicate n a
⊢ b = a

Proof state:
case isTrue
α : Type u_1
n : Nat
a : α
k : Nat
h : k < n
⊢ (replicate n a).eraseIdx k = replicate (n - 1) a

Tactic:
rw [eq_replicate_iff, length_eraseIdx_of_lt (by simpa using h)]

Result:
case isTrue
α : Type u_1
n : Nat
a : α
k : Nat
h : k < n
⊢ (replicate n a).length - 1 = n - 1 ∧ ∀ (b : α), b ∈ (replicate n a).eraseIdx k → b = a
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem attach_affineCombination_of_injective [DecidableEq P] (s : Finset P) (w : P → k) (f : s → P)
    (hf : Function.Injective f) :
    s.attach.affineCombination k f (w ∘ f) = (image f univ).affineCombination k id w

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice ⋯)
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice ⋯)
⊢ univ.sum g₁ = (image f univ).sum g₂

Tactic:
have hgf : g₁ = g₂ ∘ f := by
  ext
  simp [g₁, g₂]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
inst✝ : DecidableEq P
s : Finset P
w : P → k
f : { x // x ∈ s } → P
hf : Function.Injective f
g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice ⋯)
g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice ⋯)
hgf : g₁ = g₂ ∘ f
⊢ univ.sum g₁ = (image f univ).sum g₂
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem U_two : U R 2 = 4 * X ^ 2 - 1

Proof state:
R : Type u_1
inst✝ : CommRing R
this : U R (0 + 2) = 2 * X * U R (0 + 1) - U R 0
⊢ U R 2 = 4 * X ^ 2 - 1

Tactic:
simp only [zero_add, U_one, U_zero] at this

Result:
R : Type u_1
inst✝ : CommRing R
this : U R 2 = 2 * X * (2 * X) - 1
⊢ U R 2 = 4 * X ^ 2 - 1

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ U R 2 = 4 * X ^ 2 - 1

Tactic:
have := U_add_two R 0

Result:
R : Type u_1
inst✝ : CommRing R
this : U R (0 + 2) = 2 * X * U R (0 + 1) - U R 0
⊢ U R 2 = 4 * X ^ 2 - 1

Proof state:
R : Type u_1
inst✝ : CommRing R
this : U R 2 = 2 * X * (2 * X) - 1
⊢ U R 2 = 4 * X ^ 2 - 1

Tactic:
linear_combination this

Result:
no goals
-- Mathlib/MeasureTheory/Order/UpperLower.lean
theorem IsAntichain.volume_eq_zero [Nonempty ι] (hs : IsAntichain (· ≤ ·) s) : volume s = 0

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
s : Set (ι → ℝ)
inst✝ : Nonempty ι
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
⊢ s ⊆ frontier s

Tactic:
rw [← closure_diff_interior, hs.interior_eq_empty, diff_empty]

Result:
ι : Type u_1
inst✝¹ : Fintype ι
s : Set (ι → ℝ)
inst✝ : Nonempty ι
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
⊢ s ⊆ closure s

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
s : Set (ι → ℝ)
inst✝ : Nonempty ι
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
⊢ s ⊆ closure s

Tactic:
exact subset_closure

Result:
no goals

Proof state:
ι : Type u_1
inst✝¹ : Fintype ι
s : Set (ι → ℝ)
inst✝ : Nonempty ι
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
⊢ volume s = 0

Tactic:
refine measure_mono_null ?_ hs.ordConnected.null_frontier

Result:
ι : Type u_1
inst✝¹ : Fintype ι
s : Set (ι → ℝ)
inst✝ : Nonempty ι
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
⊢ s ⊆ frontier s
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem Biprod.ofComponents_fst :
    Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ biprod.fst = biprod.fst ≫ f₁₁ + biprod.snd ≫ f₂₁

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
⊢ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ biprod.fst = biprod.fst ≫ f₁₁ + biprod.snd ≫ f₂₁

Tactic:
simp [Biprod.ofComponents]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Killing.lean
lemma coe_corootSpace_eq_span_singleton' (α : Weight K H L) :
    (corootSpace α).toSubmodule = K ∙ (cartanEquivDual H).symm α

Proof state:
case refine_1
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
α : Weight K (↥H) L
x : L
hx : x ∈ H
hx' : x ∈ span K {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x}
this : ∃ a, a • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) = x
⊢ ∃ a, a • (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α) = ⟨x, hx⟩

Tactic:
obtain ⟨t, rfl⟩ := this

Result:
case refine_1.intro
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
α : Weight K (↥H) L
t : K
hx : t • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) ∈ H
hx' :
  t • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) ∈
    span K {x | ∃ y ∈ rootSpace H ⇑α, ∃ z ∈ rootSpace H (-⇑α), ⁅y, z⁆ = x}
⊢ ∃ a,
    a • (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α) =
      ⟨t • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)), hx⟩

Proof state:
case refine_2
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
α : Weight K (↥H) L
⊢ (cartanEquivDual H).symm (Weight.toLinear K (↥H) L α) ∈ corootSpace ⇑α

Tactic:
exact cartanEquivDual_symm_apply_mem_corootSpace α

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean
theorem isCaratheodory_union (h₁ : IsCaratheodory m s₁) (h₂ : IsCaratheodory m s₂) :
    IsCaratheodory m (s₁ ∪ s₂) := fun t => by
  rw [h₁ t, h₂ (t ∩ s₁), h₂ (t \ s₁), h₁ (t ∩ (s₁ ∪ s₂)), inter_diff_assoc _ _ s₁,
    Set.inter_assoc _ _ s₁, inter_eq_self_of_subset_right Set.subset_union_left,
    union_diff_left, h₂ (t ∩ s₁)]
  simp [diff_eq, add_assoc]

Proof state:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
t : Set α
⊢ m (t ∩ s₁ ∩ s₂) + m ((t ∩ s₁) \ s₂) + (m (t \ s₁ ∩ s₂) + m ((t \ s₁) \ s₂)) =
    m (t ∩ s₁ ∩ s₂) + m ((t ∩ s₁) \ s₂) + m (t ∩ (s₂ \ s₁)) + m (t \ (s₁ ∪ s₂))

Tactic:
simp [diff_eq, add_assoc]

Result:
no goals

Proof state:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
t : Set α
⊢ m t = m (t ∩ (s₁ ∪ s₂)) + m (t \ (s₁ ∪ s₂))

Tactic:
rw [h₁ t, h₂ (t ∩ s₁), h₂ (t \ s₁), h₁ (t ∩ (s₁ ∪ s₂)), inter_diff_assoc _ _ s₁,
  Set.inter_assoc _ _ s₁, inter_eq_self_of_subset_right Set.subset_union_left,
  union_diff_left, h₂ (t ∩ s₁)]

Result:
α : Type u
m : OuterMeasure α
s₁ s₂ : Set α
h₁ : m.IsCaratheodory s₁
h₂ : m.IsCaratheodory s₂
t : Set α
⊢ m (t ∩ s₁ ∩ s₂) + m ((t ∩ s₁) \ s₂) + (m (t \ s₁ ∩ s₂) + m ((t \ s₁) \ s₂)) =
    m (t ∩ s₁ ∩ s₂) + m ((t ∩ s₁) \ s₂) + m (t ∩ (s₂ \ s₁)) + m (t \ (s₁ ∪ s₂))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Instances.lean
theorem bind_pure_comp [Monad m] (f : α → β) (x : ExceptT ε m α) : x >>= pure ∘ f = f <$> x

Proof state:
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝ : Monad m
f : α → β
x : ExceptT ε m α
⊢ x >>= pure ∘ f = f <$> x

Tactic:
rfl

Result:
no goals