harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem tsum_mul_right [T2Space α] : ∑' x, f x * a = (∑' x, f x) * a

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
hf : ¬Summable f
ha : a = 0
⊢ ∑' (x : ι), f x * a = (∑' (x : ι), f x) * a

Tactic:
simp [ha]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
hf : ¬Summable f
ha : ¬a = 0
⊢ ∑' (x : ι), f x * a = (∑' (x : ι), f x) * a

Tactic:
rw [tsum_eq_zero_of_not_summable hf,
    tsum_eq_zero_of_not_summable (mt (summable_mul_right_iff ha).mp hf), zero_mul]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
⊢ ∑' (x : ι), f x * a = (∑' (x : ι), f x) * a

Tactic:
classical
exact if hf : Summable f then hf.tsum_mul_right a
else if ha : a = 0 then by simp [ha]
else by rw [tsum_eq_zero_of_not_summable hf,
            tsum_eq_zero_of_not_summable (mt (summable_mul_right_iff ha).mp hf), zero_mul]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalSemiring α
f : ι → α
a : α
inst✝ : T2Space α
⊢ ∑' (x : ι), f x * a = (∑' (x : ι), f x) * a

Tactic:
exact if hf : Summable f then hf.tsum_mul_right a
else if ha : a = 0 then by simp [ha]
else by rw [tsum_eq_zero_of_not_summable hf,
            tsum_eq_zero_of_not_summable (mt (summable_mul_right_iff ha).mp hf), zero_mul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/OrdinaryHypergeometric.lean
theorem ordinaryHypergeometric_radius_top_of_neg_nat₁ {k : ℕ} :
    (ordinaryHypergeometricSeries 𝔸 (-(k : 𝕂)) b c).radius = ⊤

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
b c : 𝕂
k : ℕ
⊢ (ordinaryHypergeometricSeries 𝔸 (-↑k) b c).radius = ⊤

Tactic:
refine FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero _ (1 + k) fun n ↦ ?_

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
b c : 𝕂
k n : ℕ
⊢ ordinaryHypergeometricSeries 𝔸 (-↑k) b c (n + (1 + k)) = 0

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
b c : 𝕂
k n : ℕ
⊢ ordinaryHypergeometricSeries 𝔸 (-↑k) b c (n + (1 + k)) = 0

Tactic:
exact ordinaryHypergeometricSeries_eq_zero_of_neg_nat (-(k : 𝕂)) b c (by aesop) (by omega)

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
b c : 𝕂
k n : ℕ
⊢ k < n + (1 + k)

Tactic:
omega

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedDivisionRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
b c : 𝕂
k n : ℕ
⊢ ↑?m.64878 = - -↑k ∨ ↑?m.64878 = -b ∨ ↑?m.64878 = -c

Tactic:
aesop

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem zneg_succ (n : ZNum) : -n.succ = (-n).pred

Proof state:
n : ZNum
⊢ -n.succ = (-n).pred

Tactic:
cases n <;> try { rfl }

Result:
case neg
a✝ : PosNum
⊢ -(neg a✝).succ = (-neg a✝).pred

Proof state:
case neg
a✝ : PosNum
⊢ -(neg a✝).succ = (-neg a✝).pred

Tactic:
rw [succ, Num.zneg_toZNumNeg]

Result:
case neg
a✝ : PosNum
⊢ a✝.pred'.toZNum = (-neg a✝).pred

Proof state:
case pos
a✝ : PosNum
⊢ -(pos a✝).succ = (-pos a✝).pred

Tactic:
rfl

Result:
no goals

Proof state:
case neg
a✝ : PosNum
⊢ a✝.pred'.toZNum = (-neg a✝).pred

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/ODE/Gronwall.lean
theorem gronwallBound_ε0_δ0 (K x : ℝ) : gronwallBound 0 K 0 x = 0

Proof state:
K x : ℝ
⊢ gronwallBound 0 K 0 x = 0

Tactic:
simp only [gronwallBound_ε0, zero_mul]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean
theorem iSup_sInfGen_nonempty {m : Set (OuterMeasure α)} (h : m.Nonempty) (t : Set α) :
    ⨆ _ : t.Nonempty, sInfGen m t = ⨅ (μ : OuterMeasure α) (_ : μ ∈ m), μ t

Proof state:
case inr
α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
t : Set α
ht : t.Nonempty
⊢ ⨆ (_ : t.Nonempty), sInfGen m t = ⨅ μ ∈ m, μ t

Tactic:
simp [ht, sInfGen_def]

Result:
no goals

Proof state:
α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
t : Set α
⊢ ⨆ (_ : t.Nonempty), sInfGen m t = ⨅ μ ∈ m, μ t

Tactic:
rcases t.eq_empty_or_nonempty with (rfl | ht)

Result:
case inl
α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
⊢ ⨆ (_ : ∅.Nonempty), sInfGen m ∅ = ⨅ μ ∈ m, μ ∅

case inr
α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
t : Set α
ht : t.Nonempty
⊢ ⨆ (_ : t.Nonempty), sInfGen m t = ⨅ μ ∈ m, μ t

Proof state:
case inl
α : Type u_1
m : Set (OuterMeasure α)
h : m.Nonempty
⊢ ⨆ (_ : ∅.Nonempty), sInfGen m ∅ = ⨅ μ ∈ m, μ ∅

Tactic:
simp [biInf_const h]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem integralPowerBasis'_gen [hcycl : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p) :
    hζ.integralPowerBasis'.gen = hζ.toInteger :=
  integralPowerBasis_gen (hcycl

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ 1} ℚ K

Tactic:
rwa [pow_one]

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsPrimitiveRoot ζ ↑(p ^ 1)

Tactic:
rwa [pow_one]

Result:
no goals
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upperCrossingTime_lt_bddAbove (hab : a < b) :
    BddAbove {n | upperCrossingTime a b f N n ω < N}

Proof state:
case intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
k : ℕ
hk : upperCrossingTime a b f N k ω = N
n : ℕ
hn : upperCrossingTime a b f N n ω < N
⊢ n ≤ k

Tactic:
by_contra hn'

Result:
case intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
k : ℕ
hk : upperCrossingTime a b f N k ω = N
n : ℕ
hn : upperCrossingTime a b f N n ω < N
hn' : ¬n ≤ k
⊢ False

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
⊢ BddAbove {n | upperCrossingTime a b f N n ω < N}

Tactic:
obtain ⟨k, hk⟩ := exists_upperCrossingTime_eq f N ω hab

Result:
case intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
k : ℕ
hk : upperCrossingTime a b f N k ω = N
⊢ BddAbove {n | upperCrossingTime a b f N n ω < N}

Proof state:
case intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
k : ℕ
hk : upperCrossingTime a b f N k ω = N
n : ℕ
hn : upperCrossingTime a b f N n ω < N
hn' : ¬n ≤ k
⊢ False

Tactic:
exact hn.ne (upperCrossingTime_stabilize (not_le.1 hn').le hk)

Result:
no goals

Proof state:
case intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
k : ℕ
hk : upperCrossingTime a b f N k ω = N
⊢ BddAbove {n | upperCrossingTime a b f N n ω < N}

Tactic:
refine ⟨k, fun n (hn : upperCrossingTime a b f N n ω < N) => ?_⟩

Result:
case intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
k : ℕ
hk : upperCrossingTime a b f N k ω = N
n : ℕ
hn : upperCrossingTime a b f N n ω < N
⊢ n ≤ k
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero (x y : F) :
    ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ 2 = 0 ∨ re ⟪x, y⟫_ℝ = 0 ↔ ⟪x, y⟫_ℝ = 0

Tactic:
norm_num

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ ⟪x, y⟫_ℝ = 0

Tactic:
rw [@norm_add_mul_self ℝ, add_right_cancel_iff, add_right_eq_self, mul_eq_zero]

Result:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ 2 = 0 ∨ re ⟪x, y⟫_ℝ = 0 ↔ ⟪x, y⟫_ℝ = 0
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
/-- Negating a matrix partitioned by columns is equivalent to negating each of the columns. -/
@[simp]
lemma fromCols_neg (A₁ : Matrix n m₁ R) (A₂ : Matrix n m₂ R) :
    -fromCols A₁ A₂ = fromCols (-A₁) (-A₂)

Proof state:
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝ : Neg R
A₁ : Matrix n m₁ R
A₂ : Matrix n m₂ R
⊢ -A₁.fromCols A₂ = (-A₁).fromCols (-A₂)

Tactic:
ext i (j | j) <;> simp

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Period.lean
theorem period_dvd_exponent (m : M) (a : α) : period m a ∣ Monoid.exponent M

Proof state:
α : Type v
M : Type u
inst✝¹ : Monoid M
inst✝ : MulAction M α
m : M
a : α
⊢ period m a ∣ Monoid.exponent M

Tactic:
rw [← pow_smul_eq_iff_period_dvd, Monoid.pow_exponent_eq_one, one_smul]

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
@[simp]
lemma map_stdBasisMatrix (i : m) (j : n) (a : α) {β : Type*} [Zero β]
    {F : Type*} [FunLike F α β] [ZeroHomClass F α β] (f : F) :
    (stdBasisMatrix i j a).map f = stdBasisMatrix i j (f a)

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
i : m
j : n
a : α
β : Type u_7
inst✝² : Zero β
F : Type u_8
inst✝¹ : FunLike F α β
inst✝ : ZeroHomClass F α β
f : F
⊢ (stdBasisMatrix i j a).map ⇑f = stdBasisMatrix i j (f a)

Tactic:
aesop (add unsafe unfold stdBasisMatrix)

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBase.isBasis_of_subset (hX : X ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
B X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
hB : M.IsBase B
hBX : B ⊆ X
⊢ ∀ (J : Set α), M.Indep J → B ⊆ J → J ⊆ X → B = J

Tactic:
exact fun J hJ hBJ _ ↦ hB.eq_of_subset_indep hJ hBJ

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
B X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
hB : M.IsBase B
hBX : B ⊆ X
⊢ M.IsBasis B X

Tactic:
rw [isBasis_iff, and_iff_right hB.indep, and_iff_right hBX]

Result:
α : Type u_1
M : Matroid α
B X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
hB : M.IsBase B
hBX : B ⊆ X
⊢ ∀ (J : Set α), M.Indep J → B ⊆ J → J ⊆ X → B = J
-- Mathlib/Combinatorics/Derangements/Finite.lean
theorem card_derangements_fin_add_two (n : ℕ) :
    card (derangements (Fin (n + 2))) =
      (n + 1) * card (derangements (Fin n)) + (n + 1) * card (derangements (Fin (n + 1)))

Proof state:
n : ℕ
⊢ card ↑(derangements (Fin (n + 2))) =
    (n + 1) * card ↑(derangements (Fin n)) + (n + 1) * card ↑(derangements (Fin (n + 1)))

Tactic:
have h1 : ∀ a : Fin (n + 1), card ({a}ᶜ : Set (Fin (n + 1))) = card (Fin n) := by
  intro a
  simp only
    [card_ofFinset (s := Finset.filter (fun x => x ∈ ({a}ᶜ : Set (Fin (n + 1)))) Finset.univ),
    Set.mem_compl_singleton_iff, Finset.filter_ne' _ a,
    Finset.card_erase_of_mem (Finset.mem_univ a), Finset.card_fin, add_tsub_cancel_right,
    card_fin]

Result:
n : ℕ
h1 : ∀ (a : Fin (n + 1)), card ↑{a}ᶜ = card (Fin n)
⊢ card ↑(derangements (Fin (n + 2))) =
    (n + 1) * card ↑(derangements (Fin n)) + (n + 1) * card ↑(derangements (Fin (n + 1)))

Proof state:
n : ℕ
⊢ ∀ (a : Fin (n + 1)), card ↑{a}ᶜ = card (Fin n)

Tactic:
intro a

Result:
n : ℕ
a : Fin (n + 1)
⊢ card ↑{a}ᶜ = card (Fin n)

Proof state:
n : ℕ
h1 : ∀ (a : Fin (n + 1)), card ↑{a}ᶜ = card (Fin n)
⊢ card ↑(derangements (Fin (n + 2))) =
    (n + 1) * card ↑(derangements (Fin n)) + (n + 1) * card ↑(derangements (Fin (n + 1)))

Tactic:
have h2 : card (Fin (n + 2)) = card (Option (Fin (n + 1))) := by simp only [card_fin, card_option]

Result:
n : ℕ
h1 : ∀ (a : Fin (n + 1)), card ↑{a}ᶜ = card (Fin n)
h2 : card (Fin (n + 2)) = card (Option (Fin (n + 1)))
⊢ card ↑(derangements (Fin (n + 2))) =
    (n + 1) * card ↑(derangements (Fin n)) + (n + 1) * card ↑(derangements (Fin (n + 1)))

Proof state:
n : ℕ
h1 : ∀ (a : Fin (n + 1)), card ↑{a}ᶜ = card (Fin n)
h2 : card (Fin (n + 2)) = card (Option (Fin (n + 1)))
⊢ card ↑(derangements (Fin (n + 2))) =
    (n + 1) * card ↑(derangements (Fin n)) + (n + 1) * card ↑(derangements (Fin (n + 1)))

Tactic:
simp only [card_derangements_invariant h2,
  card_congr
    (@derangementsRecursionEquiv (Fin (n + 1))
      _),card_sigma,
  card_sum, card_derangements_invariant (h1 _), Finset.sum_const, nsmul_eq_mul, Finset.card_fin,
  mul_add, Nat.cast_id]

Result:
no goals

Proof state:
n : ℕ
a : Fin (n + 1)
⊢ card ↑{a}ᶜ = card (Fin n)

Tactic:
simp only
  [card_ofFinset (s := Finset.filter (fun x => x ∈ ({a}ᶜ : Set (Fin (n + 1)))) Finset.univ),
  Set.mem_compl_singleton_iff, Finset.filter_ne' _ a,
  Finset.card_erase_of_mem (Finset.mem_univ a), Finset.card_fin, add_tsub_cancel_right,
  card_fin]

Result:
no goals

Proof state:
n : ℕ
h1 : ∀ (a : Fin (n + 1)), card ↑{a}ᶜ = card (Fin n)
⊢ card (Fin (n + 2)) = card (Option (Fin (n + 1)))

Tactic:
simp only [card_fin, card_option]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem toJordanDecomposition_spec (s : SignedMeasure α) :
    ∃ (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0),
      s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ ∧
        s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ hi₁.compl hi₃

Proof state:
case intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α := ⋯.choose
hi₁ : MeasurableSet ⋯.choose
hi₂ : 0 ≤[⋯.choose] s
hi₃ : s ≤[⋯.chooseᶜ] 0
⊢ ∃ i,
    ∃ (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0),
      s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ ∧
        s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃

Tactic:
exact ⟨i, hi₁, hi₂, hi₃, rfl, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α := ⋯.choose
⊢ ∃ i,
    ∃ (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0),
      s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ ∧
        s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃

Tactic:
obtain ⟨hi₁, hi₂, hi₃⟩ := s.exists_compl_positive_negative.choose_spec

Result:
case intro.intro
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α := ⋯.choose
hi₁ : MeasurableSet ⋯.choose
hi₂ : 0 ≤[⋯.choose] s
hi₃ : s ≤[⋯.chooseᶜ] 0
⊢ ∃ i,
    ∃ (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0),
      s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ ∧
        s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
⊢ ∃ i,
    ∃ (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0),
      s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ ∧
        s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃

Tactic:
set i := s.exists_compl_positive_negative.choose

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
i : Set α := ⋯.choose
⊢ ∃ i,
    ∃ (hi₁ : MeasurableSet i) (hi₂ : 0 ≤[i] s) (hi₃ : s ≤[iᶜ] 0),
      s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ ∧
        s.toJordanDecomposition.negPart = s.toMeasureOfLEZero iᶜ ⋯ hi₃
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem factors_span_eq {p : K[X]} : factors (span {p}) = (factors p).map (fun q ↦ span {q})

Proof state:
case inr
K : Type u_3
inst✝ : Field K
p : K[X]
hp : p ≠ 0
⊢ factors (span {p}) = Multiset.map (fun q => span {q}) (factors p)

Tactic:
have : ∀ q ∈ (factors p).map (fun q ↦ span {q}), Prime q := fun q hq ↦ by
  obtain ⟨r, hr, rfl⟩ := Multiset.mem_map.mp hq
  exact prime_span_singleton_iff.mpr <| prime_of_factor r hr

Result:
case inr
K : Type u_3
inst✝ : Field K
p : K[X]
hp : p ≠ 0
this : ∀ q ∈ Multiset.map (fun q => span {q}) (factors p), Prime q
⊢ factors (span {p}) = Multiset.map (fun q => span {q}) (factors p)

Proof state:
case intro.intro
K : Type u_3
inst✝ : Field K
p : K[X]
hp : p ≠ 0
r : K[X]
hr : r ∈ factors p
hq : span {r} ∈ Multiset.map (fun q => span {q}) (factors p)
⊢ Prime (span {r})

Tactic:
exact prime_span_singleton_iff.mpr <| prime_of_factor r hr

Result:
no goals

Proof state:
K : Type u_3
inst✝ : Field K
p : K[X]
⊢ factors (span {p}) = Multiset.map (fun q => span {q}) (factors p)

Tactic:
rcases eq_or_ne p 0 with rfl | hp

Result:
case inl
K : Type u_3
inst✝ : Field K
⊢ factors (span {0}) = Multiset.map (fun q => span {q}) (factors 0)

case inr
K : Type u_3
inst✝ : Field K
p : K[X]
hp : p ≠ 0
⊢ factors (span {p}) = Multiset.map (fun q => span {q}) (factors p)

Proof state:
case inl
K : Type u_3
inst✝ : Field K
⊢ factors (span {0}) = Multiset.map (fun q => span {q}) (factors 0)

Tactic:
simpa [Set.singleton_zero] using normalizedFactors_zero

Result:
no goals

Proof state:
K : Type u_3
inst✝ : Field K
p : K[X]
hp : p ≠ 0
q : Ideal K[X]
hq : q ∈ Multiset.map (fun q => span {q}) (factors p)
⊢ Prime q

Tactic:
obtain ⟨r, hr, rfl⟩ := Multiset.mem_map.mp hq

Result:
case intro.intro
K : Type u_3
inst✝ : Field K
p : K[X]
hp : p ≠ 0
r : K[X]
hr : r ∈ factors p
hq : span {r} ∈ Multiset.map (fun q => span {q}) (factors p)
⊢ Prime (span {r})

Proof state:
case inr
K : Type u_3
inst✝ : Field K
p : K[X]
hp : p ≠ 0
this : ∀ q ∈ Multiset.map (fun q => span {q}) (factors p), Prime q
⊢ factors (span {p}) = Multiset.map (fun q => span {q}) (factors p)

Tactic:
rw [← span_singleton_eq_span_singleton.mpr (factors_prod hp), ← multiset_prod_span_singleton,
  factors_eq_normalizedFactors, normalizedFactors_prod_of_prime this]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem thickening_iUnion (δ : ℝ) (f : ι → Set α) :
    thickening δ (⋃ i, f i) = ⋃ i, thickening δ (f i)

Proof state:
ι : Sort u_1
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
f : ι → Set α
⊢ thickening δ (⋃ i, f i) = ⋃ i, thickening δ (f i)

Tactic:
simp_rw [thickening, infEdist_iUnion, iInf_lt_iff, setOf_exists]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem vadd_mem_iff_mem_direction {s : AffineSubspace k P} (v : V) {p : P} (hp : p ∈ s) :
    v +ᵥ p ∈ s ↔ v ∈ s.direction :=
  ⟨fun h => by simpa using vsub_mem_direction h hp, fun h => vadd_mem_of_mem_direction h hp⟩

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
p : P
hp : p ∈ s
h : v +ᵥ p ∈ s
⊢ v ∈ s.direction

Tactic:
simpa using vsub_mem_direction h hp

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem le_of_span_le_span [Nontrivial R] {s t u : Set M} (hl : LinearIndepOn R id u)
    (hsu : s ⊆ u) (htu : t ⊆ u) (hst : span R s ≤ span R t) : s ⊆ t

Proof state:
R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t u : Set M
hl : LinearIndepOn R id u
hsu : s ⊆ u
htu : t ⊆ u
hst : span R s ≤ span R t
this : s ∪ t = t
⊢ s ⊆ s ∪ t

Tactic:
apply Set.subset_union_left

Result:
no goals

Proof state:
R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t u : Set M
hl : LinearIndepOn R id u
hsu : s ⊆ u
htu : t ⊆ u
hst : span R s ≤ span R t
this : s ∪ t = t
⊢ s ⊆ t

Tactic:
rw [← this]

Result:
R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t u : Set M
hl : LinearIndepOn R id u
hsu : s ⊆ u
htu : t ⊆ u
hst : span R s ≤ span R t
this : s ∪ t = t
⊢ s ⊆ s ∪ t

Proof state:
R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t u : Set M
hl : LinearIndepOn R id u
hsu : s ⊆ u
htu : t ⊆ u
hst : span R s ≤ span R t
⊢ s ⊆ t

Tactic:
have :=
  eq_of_linearIndepOn_id_of_span_subtype (hl.mono (Set.union_subset hsu htu))
    Set.subset_union_right (Set.union_subset (Set.Subset.trans subset_span hst) subset_span)

Result:
R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t u : Set M
hl : LinearIndepOn R id u
hsu : s ⊆ u
htu : t ⊆ u
hst : span R s ≤ span R t
this : s ∪ t = t
⊢ s ⊆ t
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKeyD_insertList_of_contains_eq_false [BEq α] [EquivBEq α]
    {l toInsert : List ((a : α) × β a)} {k fallback : α}
    (not_contains : (toInsert.map Sigma.fst).contains k = false) :
    getKeyD k (insertList l toInsert) fallback = getKeyD k l fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l toInsert : List ((a : α) × β a)
k fallback : α
not_contains : (List.map Sigma.fst toInsert).contains k = false
⊢ getKeyD k (insertList l toInsert) fallback = getKeyD k l fallback

Tactic:
rw [getKeyD_eq_getKey?, getKey?_insertList_of_contains_eq_false not_contains, getKeyD_eq_getKey?]

Result:
no goals
-- Mathlib/Analysis/Calculus/SmoothSeries.lean
theorem deriv_tsum (hu : Summable u) (hg : ∀ n, Differentiable 𝕜 (g n))
    (hg' : ∀ n y, ‖deriv (g n) y‖ ≤ u n) (hg0 : Summable fun n => g n y₀) :
    (deriv fun y => ∑' n, g n y) = fun y => ∑' n, deriv (g n) y

Proof state:
case h
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g : α → 𝕜 → F
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α), Differentiable 𝕜 (g n)
hg' : ∀ (n : α) (y : 𝕜), ‖deriv (g n) y‖ ≤ u n
hg0 : Summable fun n => g n y₀
x : 𝕜
⊢ deriv (fun y => ∑' (n : α), g n y) x = ∑' (n : α), deriv (g n) x

Tactic:
exact deriv_tsum_apply hu hg hg' hg0 x

Result:
no goals

Proof state:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g : α → 𝕜 → F
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α), Differentiable 𝕜 (g n)
hg' : ∀ (n : α) (y : 𝕜), ‖deriv (g n) y‖ ≤ u n
hg0 : Summable fun n => g n y₀
⊢ (deriv fun y => ∑' (n : α), g n y) = fun y => ∑' (n : α), deriv (g n) y

Tactic:
ext1 x

Result:
case h
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g : α → 𝕜 → F
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α), Differentiable 𝕜 (g n)
hg' : ∀ (n : α) (y : 𝕜), ‖deriv (g n) y‖ ≤ u n
hg0 : Summable fun n => g n y₀
x : 𝕜
⊢ deriv (fun y => ∑' (n : α), g n y) x = ∑' (n : α), deriv (g n) x
-- Mathlib/Data/List/Nodup.lean
theorem Nodup.getElem_inj_iff {l : List α} (h : Nodup l)
    {i : Nat} {hi : i < l.length} {j : Nat} {hj : j < l.length} :
    l[i] = l[j] ↔ i = j

Proof state:
α : Type u
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
⊢ l[i] = l[j] ↔ i = j

Tactic:
have := @Nodup.get_inj_iff _ _ h ⟨i, hi⟩ ⟨j, hj⟩

Result:
α : Type u
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
this : l.get ⟨i, hi⟩ = l.get ⟨j, hj⟩ ↔ ⟨i, hi⟩ = ⟨j, hj⟩
⊢ l[i] = l[j] ↔ i = j

Proof state:
α : Type u
l : List α
h : l.Nodup
i : ℕ
hi : i < l.length
j : ℕ
hj : j < l.length
this : l.get ⟨i, hi⟩ = l.get ⟨j, hj⟩ ↔ ⟨i, hi⟩ = ⟨j, hj⟩
⊢ l[i] = l[j] ↔ i = j

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem pmap_attach (l : Array α) {p : {x // x ∈ l} → Prop} (f : ∀ a, p a → β) (H) :
    pmap f l.attach H =
      l.pmap (P := fun a => ∃ h : a ∈ l, p ⟨a, h⟩)
        (fun a h => f ⟨a, h.1⟩ h.2) (fun a h => ⟨h, H ⟨a, h⟩ (by simp)⟩)

Proof state:
α : Type ?u.39637
β : Type ?u.39681
l : Array α
p : { x // x ∈ l } → Prop
f : (a : { x // x ∈ l }) → p a → β
H : ∀ (a : { x // x ∈ l }), a ∈ l.attach → p a
a : α
h : a ∈ l
⊢ ⟨a, h⟩ ∈ l.attach

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
p : { x // x ∈ l } → Prop
f : (a : { x // x ∈ l }) → p a → β
H : ∀ (a : { x // x ∈ l }), a ∈ l.attach → p a
⊢ pmap f l.attach H = pmap (fun a h => f ⟨a, ⋯⟩ ⋯) l ⋯

Tactic:
ext <;> simp

Result:
no goals