harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem direction_affineSpan_insert {s : AffineSubspace k P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s) :
    (affineSpan k (insert p₂ (s : Set P))).direction =
    Submodule.span k {p₂ -ᵥ p₁} ⊔ s.direction

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
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ (affineSpan k (↑s ∪ ↑(affineSpan k {p₂}))).direction = s.direction ⊔ Submodule.span k {p₂ -ᵥ p₁}

Tactic:
change (s ⊔ affineSpan k {p₂}).direction = _

Result:
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
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ (s ⊔ affineSpan k {p₂}).direction = s.direction ⊔ Submodule.span k {p₂ -ᵥ p₁}

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
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ s.direction ⊔ vectorSpan k {p₂} ⊔ Submodule.span k {p₂ -ᵥ p₁} = s.direction ⊔ Submodule.span k {p₂ -ᵥ p₁}

Tactic:
simp

Result:
no goals

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
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ (affineSpan k (insert p₂ ↑s)).direction = Submodule.span k {p₂ -ᵥ p₁} ⊔ s.direction

Tactic:
rw [sup_comm, ← Set.union_singleton, ← coe_affineSpan_singleton k V p₂]

Result:
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
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ (affineSpan k (↑s ∪ ↑(affineSpan k {p₂}))).direction = s.direction ⊔ Submodule.span k {p₂ -ᵥ p₁}

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
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ (s ⊔ affineSpan k {p₂}).direction = s.direction ⊔ Submodule.span k {p₂ -ᵥ p₁}

Tactic:
rw [direction_sup hp₁ (mem_affineSpan k (Set.mem_singleton _)), direction_affineSpan]

Result:
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
p₁ p₂ : P
hp₁ : p₁ ∈ s
⊢ s.direction ⊔ vectorSpan k {p₂} ⊔ Submodule.span k {p₂ -ᵥ p₁} = s.direction ⊔ Submodule.span k {p₂ -ᵥ p₁}
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem dist_lt_add_of_nonempty_ball_inter_closedBall (h : (ball x ε₁ ∩ closedBall y ε₂).Nonempty) :
    dist x y < ε₁ + ε₂

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (ball x ε₁ ∩ closedBall y ε₂).Nonempty
⊢ dist x y < ε₁ + ε₂

Tactic:
rw [inter_comm] at h

Result:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (closedBall y ε₂ ∩ ball x ε₁).Nonempty
⊢ dist x y < ε₁ + ε₂

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (closedBall y ε₂ ∩ ball x ε₁).Nonempty
⊢ dist x y < ε₁ + ε₂

Tactic:
rw [add_comm, dist_comm]

Result:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (closedBall y ε₂ ∩ ball x ε₁).Nonempty
⊢ dist y x < ε₂ + ε₁

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
ε₁ ε₂ : ℝ
h : (closedBall y ε₂ ∩ ball x ε₁).Nonempty
⊢ dist y x < ε₂ + ε₁

Tactic:
exact dist_lt_add_of_nonempty_closedBall_inter_ball h

Result:
no goals
-- Mathlib/Order/Partition/Finpartition.lean
theorem card_parts_le_card : #P.parts ≤ #s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ #P.parts ≤ #⊥.parts

Tactic:
exact card_mono bot_le

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ #P.parts ≤ #s

Tactic:
rw [← card_bot s]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
⊢ #P.parts ≤ #⊥.parts
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem isLE_iff_eq_lt_or_eq_eq {o : Ordering} : o.isLE ↔ o = .lt ∨ o = .eq

Proof state:
o : Ordering
⊢ o.isLE = true ↔ o = lt ∨ o = eq

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Covering/Besicovitch.lean
theorem ae_tendsto_measure_inter_div (μ : Measure β) [IsLocallyFiniteMeasure μ] (s : Set β) :
    ∀ᵐ x ∂μ.restrict s,
      Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)

Proof state:
β : Type u
inst✝⁵ : MetricSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
inst✝² : SecondCountableTopology β
inst✝¹ : HasBesicovitchCovering β
μ : Measure β
inst✝ : IsLocallyFiniteMeasure μ
s : Set β
⊢ ∀ᵐ (x : β) ∂μ.restrict s, Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)

Tactic:
filter_upwards [VitaliFamily.ae_tendsto_measure_inter_div (Besicovitch.vitaliFamily μ) s] with x
  hx using hx.comp (tendsto_filterAt μ x)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem getLast_filter (p : α → Bool) (l : List α) (h) :
    (l.filter p).getLast h = (l.reverse.find? p).get (by simp_all [Option.isSome_iff_ne_none])

Proof state:
α : Type ?u.62032
p : α → Bool
l : List α
h : filter p l ≠ []
⊢ (find? p l.reverse).isSome = true

Tactic:
simp_all [Option.isSome_iff_ne_none]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
h : filter p l ≠ []
⊢ (filter p l).getLast h = (find? p l.reverse).get ⋯

Tactic:
simp [getLast_eq_iff_getLast_eq_some]

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem LeftInverse.eq_rightInverse {f : α → β} {g₁ g₂ : β → α} (h₁ : LeftInverse g₁ f)
    (h₂ : RightInverse g₂ f) : g₁ = g₂ :=
  calc
    g₁ = g₁ ∘ f ∘ g₂

Proof state:
α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ g₁ = g₁ ∘ f ∘ g₂

Tactic:
rw [h₂.comp_eq_id, comp_id]

Result:
no goals

Proof state:
α : Sort u_1
β : Sort u_2
f : α → β
g₁ g₂ : β → α
h₁ : LeftInverse g₁ f
h₂ : RightInverse g₂ f
⊢ g₁ ∘ f ∘ g₂ = g₂

Tactic:
rw [← comp_assoc, h₁.comp_eq_id, id_comp]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem reflect_C_mul_X_pow (N n : ℕ) {c : R} : reflect N (C c * X ^ n) = C c * X ^ revAt N n

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
n✝ : ℕ
⊢ (reflect N (C c * X ^ n)).coeff n✝ = (C c * X ^ (revAt N) n).coeff n✝

Tactic:
rw [reflect_C_mul, coeff_C_mul, coeff_C_mul, coeff_X_pow, coeff_reflect]

Result:
case a
R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
n✝ : ℕ
⊢ c * (X ^ n).coeff ((revAt N) n✝) = c * if n✝ = (revAt N) n then 1 else 0

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
n✝ : ℕ
⊢ c * (X ^ n).coeff ((revAt N) n✝) = c * if n✝ = (revAt N) n then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
n✝ : ℕ
h : n✝ = (revAt N) n
⊢ c * (X ^ n).coeff ((revAt N) n✝) = c * 1

case neg
R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = (revAt N) n
⊢ c * (X ^ n).coeff ((revAt N) n✝) = c * 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = (revAt N) n
a : (revAt N) n✝ ∈ (C 1 * X ^ n).support
⊢ n✝ = (revAt N) n

Tactic:
rw [← mem_support_C_mul_X_pow a, revAt_invol]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
⊢ reflect N (C c * X ^ n) = C c * X ^ (revAt N) n

Tactic:
ext

Result:
case a
R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
n✝ : ℕ
⊢ (reflect N (C c * X ^ n)).coeff n✝ = (C c * X ^ (revAt N) n).coeff n✝

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = (revAt N) n
a : (revAt N) n✝ ∈ (C 1 * X ^ n).support
⊢ False

Tactic:
apply h

Result:
case neg
R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = (revAt N) n
a : (revAt N) n✝ ∈ (C 1 * X ^ n).support
⊢ n✝ = (revAt N) n

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
n✝ : ℕ
h : n✝ = (revAt N) n
⊢ c * (X ^ n).coeff ((revAt N) n✝) = c * 1

Tactic:
rw [h, revAt_invol, coeff_X_pow_self]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = (revAt N) n
⊢ c * (X ^ n).coeff ((revAt N) n✝) = c * 0

Tactic:
rw [not_mem_support_iff.mp]

Result:
case neg
R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = (revAt N) n
⊢ (revAt N) n✝ ∉ (X ^ n).support

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = (revAt N) n
⊢ (revAt N) n✝ ∉ (X ^ n).support

Tactic:
intro a

Result:
case neg
R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = (revAt N) n
a : (revAt N) n✝ ∈ (X ^ n).support
⊢ False

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = (revAt N) n
a : (revAt N) n✝ ∈ (X ^ n).support
⊢ False

Tactic:
rw [← one_mul (X ^ n), ← C_1] at a

Result:
case neg
R : Type u_1
inst✝ : Semiring R
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = (revAt N) n
a : (revAt N) n✝ ∈ (C 1 * X ^ n).support
⊢ False
-- Mathlib/GroupTheory/HNNExtension.lean
theorem prod_smul_empty (w : NormalWord d) :
    (w.prod φ) • empty = w

Proof state:
case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ g • cons (↑((toSubgroupEquiv φ u) (⋯.equiv w.head).1)) u ((↑(⋯.equiv w.head).2 * w.head⁻¹) • w) ⋯ ⋯ = cons g u w h1 h2

Tactic:
erw [(d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1]

Result:
case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ g • cons (↑((toSubgroupEquiv φ u) ⟨1, ⋯⟩)) u ((↑(⋯.equiv w.head).2 * w.head⁻¹) • w) ⋯ ⋯ = cons g u w h1 h2
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
@[simp]
lemma mk₀_comp_mk₀ (f : X ⟶ Y) (g : Y ⟶ Z) :
    (mk₀ f).comp (mk₀ g) (zero_add 0) = mk₀ (f ≫ g)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (mk₀ f).comp (mk₀ g) ⋯ = mk₀ (f ≫ g)

Tactic:
ext

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ ((mk₀ f).comp (mk₀ g) ⋯).hom = (mk₀ (f ≫ g)).hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (mk₀ f).comp (mk₀ g) ⋯ = mk₀ (f ≫ g)

Tactic:
letI := HasDerivedCategory.standard C

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (mk₀ f).comp (mk₀ g) ⋯ = mk₀ (f ≫ g)

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ ((mk₀ f).comp (mk₀ g) ⋯).hom = (mk₀ (f ≫ g)).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fintype/Fin.lean
theorem Ioi_zero_eq_map : Ioi (0 : Fin n.succ) = univ.map (Fin.succEmb _) :=
  coe_injective <| by ext; simp [pos_iff_ne_zero]

Proof state:
n : ℕ
⊢ ↑(Ioi 0) = ↑(map (succEmb n) univ)

Tactic:
ext

Result:
case h
n : ℕ
x✝ : Fin n.succ
⊢ x✝ ∈ ↑(Ioi 0) ↔ x✝ ∈ ↑(map (succEmb n) univ)

Proof state:
case h
n : ℕ
x✝ : Fin n.succ
⊢ x✝ ∈ ↑(Ioi 0) ↔ x✝ ∈ ↑(map (succEmb n) univ)

Tactic:
simp [pos_iff_ne_zero]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem equiv_snd_eq_one_of_mem_of_one_mem {g : G} (h1 : 1 ∈ T) (hg : g ∈ S) :
    (hST.equiv g).snd = ⟨1, h1⟩

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ (hST.equiv g).2 = ⟨1, h1⟩

Tactic:
ext

Result:
case a
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ ↑(hST.equiv g).2 = ↑⟨1, h1⟩

Proof state:
case a
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ T
hg : g ∈ S
⊢ ↑(hST.equiv g).2 = ↑⟨1, h1⟩

Tactic:
rw [equiv_snd_eq_inv_mul, equiv_fst_eq_self_of_mem_of_one_mem _ h1 hg, inv_mul_cancel]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem ContinuousInv.induced {α : Type*} {β : Type*} {F : Type*} [FunLike F α β] [Group α]
    [Group β] [MonoidHomClass F α β] [tβ : TopologicalSpace β] [ContinuousInv β] (f : F) :
    @ContinuousInv α (tβ.induced f) _

Proof state:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MonoidHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousInv β
f : F
⊢ ContinuousInv α

Tactic:
let _tα := tβ.induced f

Result:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MonoidHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousInv β
f : F
_tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ
⊢ ContinuousInv α

Proof state:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MonoidHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousInv β
f : F
_tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ
⊢ ContinuousInv α

Tactic:
refine ⟨continuous_induced_rng.2 ?_⟩

Result:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MonoidHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousInv β
f : F
_tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ
⊢ Continuous (⇑f ∘ fun a => a⁻¹)

Proof state:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MonoidHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousInv β
f : F
_tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ
⊢ Continuous fun x => (f x)⁻¹

Tactic:
fun_prop

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MonoidHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousInv β
f : F
_tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ
⊢ Continuous (⇑f ∘ fun a => a⁻¹)

Tactic:
simp only [Function.comp_def, map_inv]

Result:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝⁴ : FunLike F α β
inst✝³ : Group α
inst✝² : Group β
inst✝¹ : MonoidHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousInv β
f : F
_tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ
⊢ Continuous fun x => (f x)⁻¹
-- Mathlib/Order/Partition/Equipartition.lean
theorem IsEquipartition.filter_ne_average_add_one_eq_average (hP : P.IsEquipartition) :
    {p ∈ P.parts | ¬#p = #s / #P.parts + 1} = {p ∈ P.parts | #p = #s / #P.parts}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
⊢ filter (fun p => ¬#p = #s / #P.parts + 1) P.parts = filter (fun p => #p = #s / #P.parts) P.parts

Tactic:
ext p

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
p : Finset α
⊢ p ∈ filter (fun p => ¬#p = #s / #P.parts + 1) P.parts ↔ p ∈ filter (fun p => #p = #s / #P.parts) P.parts

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
p : Finset α
⊢ p ∈ P.parts → (¬#p = #s / #P.parts + 1 ↔ #p = #s / #P.parts)

Tactic:
exact fun hp ↦ (hP.card_part_eq_average_iff hp).symm

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
p : Finset α
⊢ p ∈ filter (fun p => ¬#p = #s / #P.parts + 1) P.parts ↔ p ∈ filter (fun p => #p = #s / #P.parts) P.parts

Tactic:
simp only [mem_filter, and_congr_right_iff]

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
p : Finset α
⊢ p ∈ P.parts → (¬#p = #s / #P.parts + 1 ↔ #p = #s / #P.parts)
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem _root_.MeasureTheory.memLp_re_im_iff {f : α → K} :
    MemLp (fun x ↦ RCLike.re (f x)) p μ ∧ MemLp (fun x ↦ RCLike.im (f x)) p μ ↔
      MemLp f p μ

Proof state:
case h.e'_6.h
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst✝ : RCLike K
f : α → K
hre : MemLp (fun x => RCLike.re (f x)) p μ
him : MemLp (fun x => RCLike.im (f x)) p μ
x : α
⊢ f x = ((fun x => ↑(RCLike.re (f x))) + fun x => RCLike.I * ↑(RCLike.im (f x))) x

Tactic:
rw [Pi.add_apply, mul_comm, RCLike.re_add_im]

Result:
no goals

Proof state:
case intro
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst✝ : RCLike K
f : α → K
hre : MemLp (fun x => RCLike.re (f x)) p μ
him : MemLp (fun x => RCLike.im (f x)) p μ
⊢ MemLp f p μ

Tactic:
convert MeasureTheory.MemLp.add (E := K) hre.ofReal (him.ofReal.const_mul RCLike.I)

Result:
case h.e'_6
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst✝ : RCLike K
f : α → K
hre : MemLp (fun x => RCLike.re (f x)) p μ
him : MemLp (fun x => RCLike.im (f x)) p μ
⊢ f = (fun x => ↑(RCLike.re (f x))) + fun x => RCLike.I * ↑(RCLike.im (f x))

Proof state:
case h.e'_6
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst✝ : RCLike K
f : α → K
hre : MemLp (fun x => RCLike.re (f x)) p μ
him : MemLp (fun x => RCLike.im (f x)) p μ
⊢ f = (fun x => ↑(RCLike.re (f x))) + fun x => RCLike.I * ↑(RCLike.im (f x))

Tactic:
ext1 x

Result:
case h.e'_6.h
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst✝ : RCLike K
f : α → K
hre : MemLp (fun x => RCLike.re (f x)) p μ
him : MemLp (fun x => RCLike.im (f x)) p μ
x : α
⊢ f x = ((fun x => ↑(RCLike.re (f x))) + fun x => RCLike.I * ↑(RCLike.im (f x))) x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst✝ : RCLike K
f : α → K
⊢ MemLp (fun x => RCLike.re (f x)) p μ ∧ MemLp (fun x => RCLike.im (f x)) p μ ↔ MemLp f p μ

Tactic:
refine ⟨?_, fun hf => ⟨hf.re, hf.im⟩⟩

Result:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst✝ : RCLike K
f : α → K
⊢ MemLp (fun x => RCLike.re (f x)) p μ ∧ MemLp (fun x => RCLike.im (f x)) p μ → MemLp f p μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst✝ : RCLike K
f : α → K
⊢ MemLp (fun x => RCLike.re (f x)) p μ ∧ MemLp (fun x => RCLike.im (f x)) p μ → MemLp f p μ

Tactic:
rintro ⟨hre, him⟩

Result:
case intro
α : Type u_1
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
K : Type u_8
inst✝ : RCLike K
f : α → K
hre : MemLp (fun x => RCLike.re (f x)) p μ
him : MemLp (fun x => RCLike.im (f x)) p μ
⊢ MemLp f p μ
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem isRegular_aleph_one : IsRegular ℵ₁

Proof state:
⊢ (succ ℵ₀).IsRegular

Tactic:
exact isRegular_succ le_rfl

Result:
no goals

Proof state:
⊢ (ℵ_ 1).IsRegular

Tactic:
rw [← succ_aleph0]

Result:
⊢ (succ ℵ₀).IsRegular
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
/-- The function `oddKernel a` has exponential decay at `+∞`, for any `a`. -/
lemma isBigO_atTop_oddKernel (a : UnitAddCircle) :
    ∃ p, 0 < p ∧ IsBigO atTop (oddKernel a) (fun x ↦ Real.exp (-p * x))

Proof state:
case H.intro.intro
b p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_int 1 ↑b =O[atTop] fun t => rexp (-p * t)
⊢ ∀ᶠ (x : ℝ) in atTop, ‖oddKernel (↑b) x‖ ≤ HurwitzKernelBounds.F_int 1 (↑b) x

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht

Result:
case h
b p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_int 1 ↑b =O[atTop] fun t => rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ‖oddKernel (↑b) t‖ ≤ HurwitzKernelBounds.F_int 1 (↑b) t

Proof state:
case H
b : ℝ
⊢ ∃ p, 0 < p ∧ oddKernel ↑b =O[atTop] fun x => rexp (-p * x)

Tactic:
obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_int_one b

Result:
case H.intro.intro
b p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_int 1 ↑b =O[atTop] fun t => rexp (-p * t)
⊢ ∃ p, 0 < p ∧ oddKernel ↑b =O[atTop] fun x => rexp (-p * x)

Proof state:
case H.intro.intro
b p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_int 1 ↑b =O[atTop] fun t => rexp (-p * t)
⊢ ∃ p, 0 < p ∧ oddKernel ↑b =O[atTop] fun x => rexp (-p * x)

Tactic:
refine ⟨p, hp, (Eventually.isBigO ?_).trans hp'⟩

Result:
case H.intro.intro
b p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_int 1 ↑b =O[atTop] fun t => rexp (-p * t)
⊢ ∀ᶠ (x : ℝ) in atTop, ‖oddKernel (↑b) x‖ ≤ HurwitzKernelBounds.F_int 1 (↑b) x

Proof state:
case h
b p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_int 1 ↑b =O[atTop] fun t => rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ‖oddKernel (↑b) t‖ ≤ HurwitzKernelBounds.F_int 1 (↑b) t

Tactic:
simpa [← (hasSum_int_oddKernel b ht).tsum_eq, HurwitzKernelBounds.F_int,
  HurwitzKernelBounds.f_int, abs_of_nonneg (exp_pos _).le] using
  norm_tsum_le_tsum_norm (hasSum_int_oddKernel b ht).summable.norm

Result:
no goals

Proof state:
a : UnitAddCircle
⊢ ∃ p, 0 < p ∧ oddKernel a =O[atTop] fun x => rexp (-p * x)

Tactic:
induction a using QuotientAddGroup.induction_on with | H b =>
obtain ⟨p, hp, hp'⟩ := HurwitzKernelBounds.isBigO_atTop_F_int_one b
refine ⟨p, hp, (Eventually.isBigO ?_).trans hp'⟩
filter_upwards [eventually_gt_atTop 0] with t ht
simpa [← (hasSum_int_oddKernel b ht).tsum_eq, HurwitzKernelBounds.F_int,
  HurwitzKernelBounds.f_int, abs_of_nonneg (exp_pos _).le] using
  norm_tsum_le_tsum_norm (hasSum_int_oddKernel b ht).summable.norm

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem prod_apply_inl_snd (i) : (b.prod b' (Sum.inl i)).2 = 0 :=
  b'.repr.injective <| by
    ext j
    simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply, LinearEquiv.prod_symm,
      LinearEquiv.prod_apply, b'.repr.apply_symm_apply, LinearEquiv.symm_symm, repr_self,
      Equiv.toFun_as_coe, Finsupp.snd_sumFinsuppLEquivProdFinsupp, LinearEquiv.map_zero,
      Finsupp.zero_apply]
    apply Finsupp.single_eq_of_ne Sum.inl_ne_inr

Proof state:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι
j : ι'
⊢ (single (Sum.inl i) 1) (Sum.inr j) = 0

Tactic:
apply Finsupp.single_eq_of_ne Sum.inl_ne_inr

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι
⊢ b'.repr ((b.prod b') (Sum.inl i)).2 = b'.repr 0

Tactic:
ext j

Result:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι
j : ι'
⊢ (b'.repr ((b.prod b') (Sum.inl i)).2) j = (b'.repr 0) j

Proof state:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι
j : ι'
⊢ (b'.repr ((b.prod b') (Sum.inl i)).2) j = (b'.repr 0) j

Tactic:
simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply, LinearEquiv.prod_symm,
  LinearEquiv.prod_apply, b'.repr.apply_symm_apply, LinearEquiv.symm_symm, repr_self,
  Equiv.toFun_as_coe, Finsupp.snd_sumFinsuppLEquivProdFinsupp, LinearEquiv.map_zero,
  Finsupp.zero_apply]

Result:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι
j : ι'
⊢ (single (Sum.inl i) 1) (Sum.inr j) = 0