harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Finiteness/Defs.lean
theorem fg_iff_exists_fin_generating_family {N : Submodule R M} :
    N.FG ↔ ∃ (n : ℕ) (s : Fin n → M), span R (range s) = N

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ S, S.Finite ∧ span R S = N) ↔ ∃ n s, span R (range s) = N

Tactic:
constructor

Result:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ S, S.Finite ∧ span R S = N) → ∃ n s, span R (range s) = N

case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ n s, span R (range s) = N) → ∃ S, S.Finite ∧ span R S = N

Proof state:
case mp.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
n : ℕ
f : Fin n ↪ M
Sfin : (range ⇑f).Finite
hS : span R (range ⇑f) = N
⊢ ∃ n s, span R (range s) = N

Tactic:
exact ⟨n, f, hS⟩

Result:
no goals

Proof state:
case mpr.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
n : ℕ
s : Fin n → M
hs : span R (range s) = N
⊢ ∃ S, S.Finite ∧ span R S = N

Tactic:
exact ⟨range s, finite_range s, hs⟩

Result:
no goals

Proof state:
case mp.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
S : Set M
Sfin : S.Finite
hS : span R S = N
⊢ ∃ n s, span R (range s) = N

Tactic:
obtain ⟨n, f, rfl⟩ := Sfin.fin_embedding

Result:
case mp.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
n : ℕ
f : Fin n ↪ M
Sfin : (range ⇑f).Finite
hS : span R (range ⇑f) = N
⊢ ∃ n s, span R (range s) = N

Proof state:
case mpr
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ n s, span R (range s) = N) → ∃ S, S.Finite ∧ span R S = N

Tactic:
rintro ⟨n, s, hs⟩

Result:
case mpr.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
n : ℕ
s : Fin n → M
hs : span R (range s) = N
⊢ ∃ S, S.Finite ∧ span R S = N

Proof state:
case mp
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ S, S.Finite ∧ span R S = N) → ∃ n s, span R (range s) = N

Tactic:
rintro ⟨S, Sfin, hS⟩

Result:
case mp.intro.intro
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
S : Set M
Sfin : S.Finite
hS : span R S = N
⊢ ∃ n s, span R (range s) = N

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ N.FG ↔ ∃ n s, span R (range s) = N

Tactic:
rw [fg_def]

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
⊢ (∃ S, S.Finite ∧ span R S = N) ↔ ∃ n s, span R (range s) = N
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem mul_inv_rev (φ ψ : MvPowerSeries σ k) :
    (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

Proof state:
case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬(constantCoeff σ k) φ = 0 ∧ ¬(constantCoeff σ k) ψ = 0
⊢ ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1

Tactic:
rw [← mul_assoc, mul_assoc _⁻¹, MvPowerSeries.inv_mul_cancel _ h.left, mul_one,
  MvPowerSeries.inv_mul_cancel _ h.right]

Result:
no goals

Proof state:
case pos
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : (constantCoeff σ k) φ = 0 ∨ (constantCoeff σ k) ψ = 0
⊢ 0 = ψ⁻¹ * φ⁻¹

Tactic:
rcases h with h | h <;> simp [inv_eq_zero.mpr h]

Result:
no goals

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

Tactic:
by_cases h : constantCoeff σ k (φ * ψ) = 0

Result:
case pos
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : (constantCoeff σ k) (φ * ψ) = 0
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬(constantCoeff σ k) (φ * ψ) = 0
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

Proof state:
case pos
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : (constantCoeff σ k) (φ * ψ) = 0
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

Tactic:
rw [inv_eq_zero.mpr h]

Result:
case pos
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : (constantCoeff σ k) (φ * ψ) = 0
⊢ 0 = ψ⁻¹ * φ⁻¹

Proof state:
case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬(constantCoeff σ k) (φ * ψ) = 0
⊢ ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1

Tactic:
simp only [not_or, map_mul, mul_eq_zero] at h

Result:
case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬(constantCoeff σ k) φ = 0 ∧ ¬(constantCoeff σ k) ψ = 0
⊢ ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1

Proof state:
case pos
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : (constantCoeff σ k) (φ * ψ) = 0
⊢ 0 = ψ⁻¹ * φ⁻¹

Tactic:
simp only [map_mul, mul_eq_zero] at h

Result:
case pos
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : (constantCoeff σ k) φ = 0 ∨ (constantCoeff σ k) ψ = 0
⊢ 0 = ψ⁻¹ * φ⁻¹

Proof state:
case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬(constantCoeff σ k) (φ * ψ) = 0
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

Tactic:
rw [MvPowerSeries.inv_eq_iff_mul_eq_one h]

Result:
case neg
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ ψ : MvPowerSeries σ k
h : ¬(constantCoeff σ k) (φ * ψ) = 0
⊢ ψ⁻¹ * φ⁻¹ * (φ * ψ) = 1
-- Mathlib/Probability/UniformOn.lean
/-- See `uniformOn_eq_zero` for a version assuming `MeasurableSingletonClass Ω` instead of
`MeasurableSet s`. -/
@[simp] lemma uniformOn_eq_zero' (hs : MeasurableSet s) : uniformOn s = 0 ↔ s.Infinite ∨ s = ∅

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
s : Set Ω
hs : MeasurableSet s
⊢ uniformOn s = 0 ↔ s.Infinite ∨ s = ∅

Tactic:
simp [uniformOn, hs]

Result:
no goals
-- Mathlib/Order/Filter/Finite.lean
lemma _root_.Set.Finite.eventuallyLE_iUnion {ι : Type*} {s : Set ι} (hs : s.Finite)
    {f g : ι → Set α} (hle : ∀ i ∈ s, f i ≤ᶠ[l] g i) : (⋃ i ∈ s, f i) ≤ᶠ[l] (⋃ i ∈ s, g i)

Proof state:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i

Tactic:
rw [biUnion_eq_iUnion, biUnion_eq_iUnion]

Result:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋃ x, f ↑x ≤ᶠ[l] ⋃ x, g ↑x

Proof state:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋃ x, f ↑x ≤ᶠ[l] ⋃ x, g ↑x

Tactic:
exact .iUnion fun i ↦ hle i.1 i.2

Result:
no goals

Proof state:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
⊢ ⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i

Tactic:
have := hs.to_subtype

Result:
α : Type u
l : Filter α
ι : Type u_2
s : Set ι
hs : s.Finite
f g : ι → Set α
hle : ∀ i ∈ s, f i ≤ᶠ[l] g i
this : Finite ↑s
⊢ ⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i
-- Mathlib/Analysis/Analytic/Composition.lean
theorem HasFPowerSeriesWithinAt.comp {g : F → G} {f : E → F} {q : FormalMultilinearSeries 𝕜 F G}
    {p : FormalMultilinearSeries 𝕜 E F} {x : E} {t : Set F} {s : Set E}
    (hg : HasFPowerSeriesWithinAt g q t (f x)) (hf : HasFPowerSeriesWithinAt f p s x)
    (hs : Set.MapsTo f s t) : HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
this✝ : insert (f x) t ∩ EMetric.ball (f x) rg ∈ 𝓝[insert (f x) t] f x
this : insert (f x) t ∩ EMetric.ball (f x) rg ∈ Filter.map f (𝓝[insert x s] x)
⊢ ∃ δ, 0 < δ ∧ ∀ {z : E}, z ∈ insert x s ∩ EMetric.ball x δ → f z ∈ insert (f x) t ∩ EMetric.ball (f x) rg

Tactic:
rcases EMetric.mem_nhdsWithin_iff.1 this with ⟨δ, δpos, Hδ⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
g : F → G
f : E → F
q : FormalMultilinearSeries 𝕜 F G
p : FormalMultilinearSeries 𝕜 E F
x : E
t : Set F
s : Set E
hs : Set.MapsTo f s t
rg : ℝ≥0∞
Hg : HasFPowerSeriesWithinOnBall g q t (f x) rg
rf : ℝ≥0∞
Hf : HasFPowerSeriesWithinOnBall f p s x rf
r : ℝ≥0
r_pos : 0 < r
hr : Summable fun i => ‖q.compAlongComposition p i.snd‖₊ * r ^ i.fst
this✝ : insert (f x) t ∩ EMetric.ball (f x) rg ∈ 𝓝[insert (f x) t] f x
this : insert (f x) t ∩ EMetric.ball (f x) rg ∈ Filter.map f (𝓝[insert x s] x)
δ : ℝ≥0∞
δpos : δ > 0
Hδ : EMetric.ball x δ ∩ insert x s ⊆ f ⁻¹' (insert (f x) t ∩ EMetric.ball (f x) rg)
⊢ ∃ δ, 0 < δ ∧ ∀ {z : E}, z ∈ insert x s ∩ EMetric.ball x δ → f z ∈ insert (f x) t ∩ EMetric.ball (f x) rg
-- Mathlib/Combinatorics/Hall/Finite.lean
theorem hall_hard_inductive_step_A {n : ℕ} (hn : Fintype.card ι = n + 1)
    (ht : ∀ s : Finset ι, #s ≤ #(s.biUnion t))
    (ih :
      ∀ {ι' : Type u} [Fintype ι'] (t' : ι' → Finset α),
        Fintype.card ι' ≤ n →
          (∀ s' : Finset ι', #s' ≤ #(s'.biUnion t')) →
            ∃ f : ι' → α, Function.Injective f ∧ ∀ x, f x ∈ t' x)
    (ha : ∀ s : Finset ι, s.Nonempty → s ≠ univ → #s < #(s.biUnion t)) :
    ∃ f : ι → α, Function.Injective f ∧ ∀ x, f x ∈ t x

Proof state:
case neg
ι : Type u
α : Type v
inst✝¹ : DecidableEq α
t : ι → Finset α
inst✝ : Fintype ι
n : ℕ
hn : Fintype.card ι = n + 1
ht : ∀ (s : Finset ι), #s ≤ #(s.biUnion t)
ih :
  ∀ {ι' : Type u} [inst : Fintype ι'] (t' : ι' → Finset α),
    Fintype.card ι' ≤ n →
      (∀ (s' : Finset ι'), #s' ≤ #(s'.biUnion t')) → ∃ f, Function.Injective f ∧ ∀ (x : ι'), f x ∈ t' x
ha : ∀ (s : Finset ι), s.Nonempty → s ≠ univ → #s < #(s.biUnion t)
this✝ : Nonempty ι
this : DecidableEq ι
x : ι := Classical.arbitrary ι
y : α
hy : y ∈ t x
ι' : Set ι := {x' | x' ≠ x}
t' : ↑ι' → Finset α := fun x' => (t ↑x').erase y
card_ι' : Fintype.card ↑ι' = n
f' : ↑ι' → α
hfinj : Function.Injective f'
z : ι
hz : ¬z = x
hfr : f' ⟨z, hz⟩ ≠ y ∧ f' ⟨z, hz⟩ ∈ t ↑⟨z, hz⟩
⊢ f' ⟨z, hz⟩ ∈ t z

Tactic:
exact hfr.2

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ToNat.lean
theorem toNat_lift (c : Cardinal.{v}) : toNat (lift.{u, v} c) = toNat c

Proof state:
c : Cardinal.{v}
⊢ toNat (lift.{u, v} c) = toNat c

Tactic:
simp only [← toNat_toENat, toENat_lift]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_filterMap (f : α → Option β) : ∀ (l : List α),
    (filterMap f l).eraseP p = filterMap f (l.eraseP (fun x => match f x with | some y => p y | none => false))
  | [] => rfl
  | a::l => by
    rw [filterMap_cons, eraseP_cons]
    split <;> rename_i h
    · simp [h, eraseP_filterMap]
    · rename_i b
      rw [h, eraseP_cons]
      by_cases w : p b
      · simp [w]
      · simp only [w, cond_false]
        rw [filterMap_cons_some h, eraseP_filterMap]

Proof state:
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
a : α
l : List α
⊢ eraseP p (filterMap f (a :: l)) =
    filterMap f
      (eraseP
        (fun x =>
          match f x with
          | some y => p y
          | none => false)
        (a :: l))

Tactic:
rw [filterMap_cons, eraseP_cons]

Result:
α : Type u_1
β : Type u_2
p : β → Bool
f : α → Option β
a : α
l : List α
⊢ eraseP p
      (match f a with
      | none => filterMap f l
      | some b => b :: filterMap f l) =
    filterMap f
      (bif
          match f a with
          | some y => p y
          | none => false then
        l
      else
        a ::
          eraseP
            (fun x =>
              match f x with
              | some y => p y
              | none => false)
            l)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem push_inj_left {a : α} {xs ys : Vector α n} : xs.push a = ys.push a ↔ xs = ys :=
  ⟨pop_eq_of_push_eq, fun h => by simp [h]⟩

Proof state:
α : Type u_1
n : Nat
a : α
xs ys : Vector α n
h : xs = ys
⊢ xs.push a = ys.push a

Tactic:
simp [h]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Basic.lean
theorem algHom_eq (f : B →ₐ[A] B') (hf : Function.Injective f) (x : B) :
    minpoly A (f x) = minpoly A x

Proof state:
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
f : B →ₐ[A] B'
hf : Injective ⇑f
x : B
⊢ minpoly A (f x) = minpoly A x

Tactic:
classical
simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,
  AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
B' : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Ring B
inst✝² : Ring B'
inst✝¹ : Algebra A B
inst✝ : Algebra A B'
f : B →ₐ[A] B'
hf : Injective ⇑f
x : B
⊢ minpoly A (f x) = minpoly A x

Tactic:
simp_rw [minpoly, isIntegral_algHom_iff _ hf, ← Polynomial.aeval_def, aeval_algHom,
  AlgHom.comp_apply, _root_.map_eq_zero_iff f hf]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem integral_eq_sum_filter [DecidablePred fun x : F => x ≠ 0] {m : MeasurableSpace α}
    (f : α →ₛ F) (μ : Measure α) :
    f.integral μ = ∑ x ∈ {x ∈ f.range | x ≠ 0}, (μ (f ⁻¹' {x})).toReal • x

Proof state:
α : Type u_1
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : DecidablePred fun x => x ≠ 0
m : MeasurableSpace α
f : α →ₛ F
μ : Measure α
⊢ integral μ f = ∑ x ∈ filter (fun x => x ≠ 0) f.range, (μ (⇑f ⁻¹' {x})).toReal • x

Tactic:
simp_rw [integral_def, setToSimpleFunc_eq_sum_filter, weightedSMul_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem MemLp.neg {f : α → E} (hf : MemLp f p μ) : MemLp (-f) p μ :=
  ⟨AEStronglyMeasurable.neg hf.1, by simp [hf.right]⟩

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
f : α → E
hf : MemLp f p μ
⊢ eLpNorm (-f) p μ < ⊤

Tactic:
simp [hf.right]

Result:
no goals
-- Mathlib/RingTheory/LocalRing/LocalSubring.lean
lemma le_ofPrime : A ≤ (ofPrime A P).toSubring

Proof state:
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
⊢ A ≤ (ofPrime A P).toSubring

Tactic:
intro x hx

Result:
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : K
hx : x ∈ A
⊢ x ∈ (ofPrime A P).toSubring

Proof state:
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : K
hx : x ∈ A
⊢ x ∈ (ofPrime A P).toSubring

Tactic:
exact ⟨algebraMap A _ ⟨x, hx⟩, by simp⟩

Result:
no goals

Proof state:
K : Type u_3
inst✝¹ : Field K
A : Subring K
P : Ideal ↥A
inst✝ : P.IsPrime
x : K
hx : x ∈ A
⊢ (IsLocalization.lift ⋯) ((algebraMap (↥A) (Localization.AtPrime P)) ⟨x, hx⟩) = x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Flatten.lean
theorem take_sum_flatten' (L : List (List α)) (i : ℕ) :
    L.flatten.take (Nat.sum ((L.map length).take i)) = (L.take i).flatten

Proof state:
case cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), take (Nat.sum (take i (map length tail✝))) tail✝.flatten = (take i tail✝).flatten
i : ℕ
⊢ take (Nat.sum (take i (map length (head✝ :: tail✝)))) (head✝ :: tail✝).flatten = (take i (head✝ :: tail✝)).flatten

Tactic:
cases i <;> simp [take_append, *]

Result:
no goals

Proof state:
case nil
α : Type u_1
i : ℕ
⊢ take (Nat.sum (take i (map length []))) [].flatten = (take i []).flatten

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
L : List (List α)
i : ℕ
⊢ take (Nat.sum (take i (map length L))) L.flatten = (take i L).flatten

Tactic:
induction L generalizing i

Result:
case nil
α : Type u_1
i : ℕ
⊢ take (Nat.sum (take i (map length []))) [].flatten = (take i []).flatten

case cons
α : Type u_1
head✝ : List α
tail✝ : List (List α)
tail_ih✝ : ∀ (i : ℕ), take (Nat.sum (take i (map length tail✝))) tail✝.flatten = (take i tail✝).flatten
i : ℕ
⊢ take (Nat.sum (take i (map length (head✝ :: tail✝)))) (head✝ :: tail✝).flatten = (take i (head✝ :: tail✝)).flatten
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq α]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
    {not_contains : (toInsert.map Prod.fst).contains k = false}
    {h} :
    getValue k (insertListConst l toInsert) h =
    getValue k l (containsKey_of_containsKey_insertListConst h not_contains)

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k : α
not_contains : (List.map Prod.fst toInsert).contains k = false
h : containsKey k (insertListConst l toInsert) = true
⊢ getValue k (insertListConst l toInsert) h = getValue k l ⋯

Tactic:
rw [← Option.some_inj, ← getValue?_eq_some_getValue, ← getValue?_eq_some_getValue,
  getValue?_insertListConst_of_contains_eq_false not_contains]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem _root_.HasCompactSupport.integral_Iic_deriv_eq (hf : ContDiff ℝ 1 f)
    (h2f : HasCompactSupport f) (b : ℝ) : ∫ x in Iic b, deriv f x = f b

Proof state:
case hf
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atBot (𝓝 0)

Tactic:
rw [hasCompactSupport_iff_eventuallyEq, Filter.coclosedCompact_eq_cocompact] at h2f

Result:
case hf
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : f =ᶠ[cocompact ℝ] 0
b : ℝ
this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atBot (𝓝 0)

Proof state:
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
⊢ ∫ (x : ℝ) in Iic b, deriv f x = f b

Tactic:
have := fun x (_ : x ∈ Iio b) ↦ hf.differentiable le_rfl x |>.hasDerivAt

Result:
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ ∫ (x : ℝ) in Iic b, deriv f x = f b

Proof state:
case hf
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : f =ᶠ[cocompact ℝ] 0
b : ℝ
this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atBot (𝓝 0)

Tactic:
exact h2f.filter_mono _root_.atBot_le_cocompact |>.tendsto

Result:
no goals

Proof state:
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ ∫ (x : ℝ) in Iic b, deriv f x = f b

Tactic:
rw [integral_Iic_of_hasDerivAt_of_tendsto hf.continuous.continuousWithinAt this, sub_zero]

Result:
case f'int
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ IntegrableOn (deriv f) (Iic b) volume

case hf
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atBot (𝓝 0)

Proof state:
case f'int
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ IntegrableOn (deriv f) (Iic b) volume

Tactic:
refine hf.continuous_deriv le_rfl |>.integrable_of_hasCompactSupport h2f.deriv |>.integrableOn

Result:
no goals
-- Mathlib/GroupTheory/Coset/Card.lean
theorem card_subgroup_dvd_card (s : Subgroup α) : Nat.card s ∣ Nat.card α

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Nat.card ↥s ∣ Nat.card α

Tactic:
simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_left ℕ]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Nat.card ↥s ∣ Nat.card α

Tactic:
classical simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_left ℕ]

Result:
no goals
-- Mathlib/Algebra/Group/Conj.lean
theorem map_surjective {f : α →* β} (hf : Function.Surjective f) :
    Function.Surjective (ConjClasses.map f)

Proof state:
case intro
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ⇑f
b : β
⊢ ∃ a, map f a = ConjClasses.mk b

Tactic:
obtain ⟨a, rfl⟩ := hf b

Result:
case intro.intro
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ⇑f
a : α
⊢ ∃ a_1, map f a_1 = ConjClasses.mk (f a)

Proof state:
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ⇑f
b : ConjClasses β
⊢ ∃ a, map f a = b

Tactic:
obtain ⟨b, rfl⟩ := ConjClasses.mk_surjective b

Result:
case intro
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ⇑f
b : β
⊢ ∃ a, map f a = ConjClasses.mk b

Proof state:
case intro.intro
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ⇑f
a : α
⊢ ∃ a_1, map f a_1 = ConjClasses.mk (f a)

Tactic:
exact ⟨ConjClasses.mk a, rfl⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ⇑f
⊢ Function.Surjective (map f)

Tactic:
intro b

Result:
α : Type u
β : Type v
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
hf : Function.Surjective ⇑f
b : ConjClasses β
⊢ ∃ a, map f a = b
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem transpose_le_iff {μ ν : YoungDiagram} : μ.transpose ≤ ν.transpose ↔ μ ≤ ν :=
  ⟨fun h => by
    convert YoungDiagram.le_of_transpose_le h
    simp, fun h => by
    rw [← transpose_transpose μ] at h
    exact YoungDiagram.le_of_transpose_le h ⟩

Proof state:
μ ν : YoungDiagram
h : μ.transpose.transpose ≤ ν
⊢ μ.transpose ≤ ν.transpose

Tactic:
exact YoungDiagram.le_of_transpose_le h

Result:
no goals

Proof state:
μ ν : YoungDiagram
h : μ.transpose ≤ ν.transpose
⊢ μ ≤ ν

Tactic:
convert YoungDiagram.le_of_transpose_le h

Result:
case h.e'_4
μ ν : YoungDiagram
h : μ.transpose ≤ ν.transpose
⊢ ν = ν.transpose.transpose

Proof state:
case h.e'_4
μ ν : YoungDiagram
h : μ.transpose ≤ ν.transpose
⊢ ν = ν.transpose.transpose

Tactic:
simp

Result:
no goals

Proof state:
μ ν : YoungDiagram
h : μ ≤ ν
⊢ μ.transpose ≤ ν.transpose

Tactic:
rw [← transpose_transpose μ] at h

Result:
μ ν : YoungDiagram
h : μ.transpose.transpose ≤ ν
⊢ μ.transpose ≤ ν.transpose
-- Mathlib/Order/GameAdd.lean
theorem GameAdd.snd_fst {a₁ a₂ b : α} (h : rα a₁ a₂) : GameAdd rα s(b, a₁) s(a₂, b)

Proof state:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα s(b, a₁) s(a₂, b)

Tactic:
rw [Sym2.eq_swap]

Result:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα s(a₁, b) s(a₂, b)

Proof state:
α : Type u_1
rα : α → α → Prop
a₁ a₂ b : α
h : rα a₁ a₂
⊢ GameAdd rα s(a₁, b) s(a₂, b)

Tactic:
exact GameAdd.fst h

Result:
no goals