harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/PowerBasis.lean
theorem leftMulMatrix (pb : PowerBasis A S) : Algebra.leftMulMatrix pb.basis pb.gen =
    @Matrix.of (Fin pb.dim) (Fin pb.dim) _ fun i j =>
      if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if (i : ℕ) = j + 1 then 1 else 0

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ (Algebra.leftMulMatrix pb.basis) pb.gen =
    Matrix.of fun i j => if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0

Tactic:
cases subsingleton_or_nontrivial A

Result:
case inl
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Subsingleton A
⊢ (Algebra.leftMulMatrix pb.basis) pb.gen =
    Matrix.of fun i j => if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0

case inr
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
⊢ (Algebra.leftMulMatrix pb.basis) pb.gen =
    Matrix.of fun i j => if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0

Proof state:
case neg
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
⊢ ∀ (x : Fin pb.dim), x ≠ ⟨↑k + 1, ⋯⟩ → (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x = 0

Tactic:
intro x hx

Result:
case neg
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
h✝ : Nontrivial A
k : Fin pb.dim
h : ¬↑k + 1 = pb.dim
x : Fin pb.dim
hx : x ≠ ⟨↑k + 1, ⋯⟩
⊢ (if ↑x = ↑k + 1 then 1 else 0) • pb.gen ^ ↑x = 0
-- Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean
/-- If each component of the unit is a split epimorphism, then the left adjoint is full. -/
lemma full_L_of_isSplitEpi_unit_app [∀ X, IsSplitEpi (h.unit.app X)] : L.Full where
  map_surjective {X Y} f

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ L.map (section_ (h.unit.app Y)) = h.counit.app (L.obj Y)

Tactic:
rw [← comp_id (L.map (section_ (h.unit.app Y)))]

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ L.map (section_ (h.unit.app Y)) ≫ 𝟙 (L.obj ((𝟭 C).obj Y)) = h.counit.app (L.obj Y)

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ L.map ((h.homEquiv X (L.obj Y)) f ≫ section_ (h.unit.app Y)) = f

Tactic:
suffices L.map (section_ (h.unit.app Y)) = h.counit.app (L.obj Y) by simp [this]

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ L.map (section_ (h.unit.app Y)) = h.counit.app (L.obj Y)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ ∃ a, L.map a = f

Tactic:
use ((h.homEquiv X (L.obj Y)) f ≫ section_ (h.unit.app Y))

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ L.map ((h.homEquiv X (L.obj Y)) f ≫ section_ (h.unit.app Y)) = f

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
this : L.map (section_ (h.unit.app Y)) = h.counit.app (L.obj Y)
⊢ L.map ((h.homEquiv X (L.obj Y)) f ≫ section_ (h.unit.app Y)) = f

Tactic:
simp [this]

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝ : ∀ (X : C), IsSplitEpi (h.unit.app X)
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ L.map (section_ (h.unit.app Y)) ≫ 𝟙 (L.obj ((𝟭 C).obj Y)) = h.counit.app (L.obj Y)

Tactic:
simp only [Functor.comp_obj, Functor.id_obj, comp_id, ← h.left_triangle_components Y,
  ← assoc, ← Functor.map_comp, IsSplitEpi.id, Functor.map_id, id_comp]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem pred'_to_nat : ∀ n, (pred' n : ℕ) = Nat.pred n
  | 1 => rfl
  | bit0 n =>
    have : Nat.succ ↑(pred' n) = ↑n

Proof state:
n : PosNum
this : (↑n.pred').succ = ↑n
h : ↑1 = ↑n
⊢ ↑(Num.casesOn 0 1 bit1) = (↑1 + ↑1).pred

Tactic:
rfl

Result:
no goals

Proof state:
n : PosNum
this : (↑n.pred').succ = ↑n
p : PosNum
h : (↑p).succ = ↑n
⊢ ↑(Num.casesOn (pos p) 1 bit1) = (↑n + ↑n).pred

Tactic:
rw [← h]

Result:
n : PosNum
this : (↑n.pred').succ = ↑n
p : PosNum
h : (↑p).succ = ↑n
⊢ ↑(Num.casesOn (pos p) 1 bit1) = ((↑p).succ + (↑p).succ).pred

Proof state:
n : PosNum
this : (↑n.pred').succ = ↑n
h : ↑1 = ↑n
⊢ ↑(Num.casesOn 0 1 bit1) = (↑n + ↑n).pred

Tactic:
rw [← to_nat_inj.1 h]

Result:
n : PosNum
this : (↑n.pred').succ = ↑n
h : ↑1 = ↑n
⊢ ↑(Num.casesOn 0 1 bit1) = (↑1 + ↑1).pred

Proof state:
n : PosNum
⊢ (↑n.pred').succ = ↑n

Tactic:
rw [pred'_to_nat n, Nat.succ_pred_eq_of_pos (to_nat_pos n)]

Result:
no goals

Proof state:
n : PosNum
this : (↑n.pred').succ = ↑n
p : PosNum
h : (↑p).succ = ↑n
⊢ ↑(Num.casesOn (pos p) 1 bit1) = ((↑p).succ + (↑p).succ).pred

Tactic:
exact (Nat.succ_add p p).symm

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Real.lean
theorem interior_sphere' (x : E) (r : ℝ) : interior (sphere x r) = ∅

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : Nontrivial E
x : E
r : ℝ
⊢ interior (sphere x r) = ∅

Tactic:
rw [← frontier_closedBall' x, interior_frontier isClosed_closedBall]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Predicate.lean
lemma areEqualizedByLocalization_iff [L.IsLocalization W] :
    AreEqualizedByLocalization W f g ↔ L.map f = L.map g

Proof state:
case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
L : C ⥤ D
W : MorphismProperty C
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
⊢ L.map f = L.map g → W.Q.map f = W.Q.map g

Tactic:
intro h

Result:
case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{u_4, u_1} C
inst✝¹ : Category.{u_5, u_2} D
L : C ⥤ D
W : MorphismProperty C
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
h : L.map f = L.map g
⊢ W.Q.map f = W.Q.map g
-- Mathlib/Algebra/BigOperators/Option.lean
theorem prod_insertNone (f : Option α → M) (s : Finset α) :
    ∏ x ∈ insertNone s, f x = f none * ∏ x ∈ s, f (some x)

Proof state:
α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : Option α → M
s : Finset α
⊢ ∏ x ∈ insertNone s, f x = f none * ∏ x ∈ s, f (some x)

Tactic:
simp [insertNone]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiffOn.differentiableOn_iteratedFDerivWithin {m : ℕ} (h : ContDiffOn 𝕜 n f s)
    (hmn : m < n) (hs : UniqueDiffOn 𝕜 s) :
    DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 s
⊢ DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 m f s) s

Tactic:
intro x hx

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
⊢ DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
this : ↑(m + 1) ≤ n
⊢ DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x

Tactic:
apply (((h.of_le this).ftaylorSeriesWithin hs).fderivWithin m ?_ x hx).differentiableWithinAt

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
this : ↑(m + 1) ≤ n
⊢ ↑m < ↑(m + 1)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
⊢ DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x

Tactic:
have : (m + 1 : ℕ) ≤ n := ENat.add_one_natCast_le_withTop_of_lt hmn

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
this : ↑(m + 1) ≤ n
⊢ DifferentiableWithinAt 𝕜 (iteratedFDerivWithin 𝕜 m f s) s x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : WithTop ℕ∞
m : ℕ
h : ContDiffOn 𝕜 n f s
hmn : ↑m < n
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
this : ↑(m + 1) ≤ n
⊢ ↑m < ↑(m + 1)

Tactic:
exact_mod_cast lt_add_one m

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem δ_comp_σ_succ' {n} {j : Fin (n + 2)} {i : Fin (n + 1)} (H : j = i.succ) :
    δ j ≫ σ i = 𝟙 ⦋n⦌

Proof state:
n : ℕ
i : Fin (n + 1)
⊢ δ i.succ ≫ σ i = 𝟙 ⦋n⦌

Tactic:
rw [δ_comp_σ_succ]

Result:
no goals

Proof state:
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.succ
⊢ δ j ≫ σ i = 𝟙 ⦋n⦌

Tactic:
subst H

Result:
n : ℕ
i : Fin (n + 1)
⊢ δ i.succ ≫ σ i = 𝟙 ⦋n⦌
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem aux_uniformity_eq : 𝓤 (PiLp p β) = 𝓤[Pi.uniformSpace _]

Proof state:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
A : IsUniformInducing ⇑(WithLp.equiv p ((i : ι) → β i))
⊢ (fun x => ((WithLp.equiv p ((i : ι) → β i)) x.1, (WithLp.equiv p ((i : ι) → β i)) x.2)) = id

Tactic:
ext i <;> rfl

Result:
no goals

Proof state:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
A : IsUniformInducing ⇑(WithLp.equiv p ((i : ι) → β i))
this : (fun x => ((WithLp.equiv p ((i : ι) → β i)) x.1, (WithLp.equiv p ((i : ι) → β i)) x.2)) = id
⊢ 𝓤 (PiLp p β) = 𝓤 ((i : ι) → β i)

Tactic:
rw [← A.comap_uniformity, this, comap_id]

Result:
no goals

Proof state:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
A : IsUniformInducing ⇑(WithLp.equiv p ((i : ι) → β i))
⊢ 𝓤 (PiLp p β) = 𝓤 ((i : ι) → β i)

Tactic:
have : (fun x : PiLp p β × PiLp p β => (WithLp.equiv p _ x.fst, WithLp.equiv p _ x.snd)) = id :=
  by ext i <;> rfl

Result:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
A : IsUniformInducing ⇑(WithLp.equiv p ((i : ι) → β i))
this : (fun x => ((WithLp.equiv p ((i : ι) → β i)) x.1, (WithLp.equiv p ((i : ι) → β i)) x.2)) = id
⊢ 𝓤 (PiLp p β) = 𝓤 ((i : ι) → β i)

Proof state:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
⊢ 𝓤 (PiLp p β) = 𝓤 ((i : ι) → β i)

Tactic:
have A : IsUniformInducing (WithLp.equiv p (∀ i, β i)) :=
  (antilipschitzWith_equiv_aux p β).isUniformInducing
    (lipschitzWith_equiv_aux p β).uniformContinuous

Result:
p : ℝ≥0∞
ι : Type u_2
β : ι → Type u_4
inst✝² : Fact (1 ≤ p)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
A : IsUniformInducing ⇑(WithLp.equiv p ((i : ι) → β i))
⊢ 𝓤 (PiLp p β) = 𝓤 ((i : ι) → β i)
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem cycleType_prime_order {σ : Perm α} (hσ : (orderOf σ).Prime) :
    ∃ n : ℕ, σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)

Proof state:
case refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
n : ℕ
hn : n ∈ σ.cycleType
⊢ n = orderOf σ

Tactic:
exact (hσ.eq_one_or_self_of_dvd n (dvd_of_mem_cycleType hn)).resolve_left
  (one_lt_of_mem_cycleType hn).ne'

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ ¬orderOf σ = 1

Tactic:
exact hσ.ne_one

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ 1 ≤ σ.cycleType.card

Tactic:
rw [Nat.succ_le_iff, card_cycleType_pos, Ne, ← orderOf_eq_one_iff]

Result:
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ ¬orderOf σ = 1

Proof state:
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ σ.cycleType.card = σ.cycleType.card - 1 + 1

Tactic:
rw [tsub_add_cancel_of_le]

Result:
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ 1 ≤ σ.cycleType.card

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ ∃ n, σ.cycleType = Multiset.replicate (n + 1) (orderOf σ)

Tactic:
refine ⟨Multiset.card σ.cycleType - 1, eq_replicate.2 ⟨?_, fun n hn ↦ ?_⟩⟩

Result:
case refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
⊢ σ.cycleType.card = σ.cycleType.card - 1 + 1

case refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : Nat.Prime (orderOf σ)
n : ℕ
hn : n ∈ σ.cycleType
⊢ n = orderOf σ
-- Mathlib/Analysis/Fourier/Inversion.lean
theorem Continuous.fourier_inversion (h : Continuous f)
    (hf : Integrable f) (h'f : Integrable (𝓕 f)) :
    𝓕⁻ (𝓕 f) = f

Proof state:
case h
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
h : Continuous f
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
v : V
⊢ 𝓕⁻ (𝓕 f) v = f v

Tactic:
exact hf.fourier_inversion h'f h.continuousAt

Result:
no goals

Proof state:
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
h : Continuous f
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
⊢ 𝓕⁻ (𝓕 f) = f

Tactic:
ext v

Result:
case h
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
h : Continuous f
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
v : V
⊢ 𝓕⁻ (𝓕 f) v = f v
-- Mathlib/Algebra/Module/Submodule/Bilinear.lean
theorem map₂_flip (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) :
    map₂ f.flip q p = map₂ f p q

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ map₂ f.flip q p = map₂ f p q

Tactic:
rw [map₂_eq_span_image2, map₂_eq_span_image2, Set.image2_swap]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ span R (image2 (fun a b => (f.flip b) a) ↑p ↑q) = span R (image2 (fun m n => (f m) n) ↑p ↑q)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ span R (image2 (fun a b => (f.flip b) a) ↑p ↑q) = span R (image2 (fun m n => (f m) n) ↑p ↑q)

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/SuccPred/Archimedean.lean
lemma monotone_of_le_succ (hf : ∀ a, ¬ IsMax a → f a ≤ f (succ a)) : Monotone f

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a ≤ f (succ a)
⊢ Monotone f

Tactic:
simpa using monotoneOn_of_le_succ Set.ordConnected_univ (by simpa using hf)

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMax a → f a ≤ f (succ a)
⊢ ∀ (a : α), ¬IsMax a → a ∈ Set.univ → succ a ∈ Set.univ → f a ≤ f (succ a)

Tactic:
simpa using hf

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem exists_mem_nhdsWithin_lt_dimH_of_lt_dimH {s : Set X} {r : ℝ≥0∞} (h : r < dimH s) :
    ∃ x ∈ s, ∀ t ∈ 𝓝[s] x, r < dimH t

Proof state:
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, dimH t ≤ r
⊢ dimH s ≤ r

Tactic:
choose! t htx htr using h

Result:
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
t : X → Set X
htx : ∀ x ∈ s, t x ∈ 𝓝[s] x
htr : ∀ x ∈ s, dimH (t x) ≤ r
⊢ dimH s ≤ r

Proof state:
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
t : X → Set X
htx : ∀ x ∈ s, t x ∈ 𝓝[s] x
htr : ∀ x ∈ s, dimH (t x) ≤ r
⊢ dimH s ≤ r

Tactic:
rcases countable_cover_nhdsWithin htx with ⟨S, hSs, hSc, hSU⟩

Result:
case intro.intro.intro
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
t : X → Set X
htx : ∀ x ∈ s, t x ∈ 𝓝[s] x
htr : ∀ x ∈ s, dimH (t x) ≤ r
S : Set X
hSs : S ⊆ s
hSc : S.Countable
hSU : s ⊆ ⋃ x ∈ S, t x
⊢ dimH s ≤ r

Proof state:
case intro.intro.intro
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
t : X → Set X
htx : ∀ x ∈ s, t x ∈ 𝓝[s] x
htr : ∀ x ∈ s, dimH (t x) ≤ r
S : Set X
hSs : S ⊆ s
hSc : S.Countable
hSU : s ⊆ ⋃ x ∈ S, t x
⊢ dimH s ≤ r

Tactic:
calc
  dimH s ≤ dimH (⋃ x ∈ S, t x) := dimH_mono hSU
  _ = ⨆ x ∈ S, dimH (t x) := dimH_bUnion hSc _
  _ ≤ r := iSup₂_le fun x hx => htr x <| hSs hx

Result:
no goals

Proof state:
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
h : r < dimH s
⊢ ∃ x ∈ s, ∀ t ∈ 𝓝[s] x, r < dimH t

Tactic:
contrapose! h

Result:
X : Type u_2
inst✝¹ : EMetricSpace X
inst✝ : SecondCountableTopology X
s : Set X
r : ℝ≥0∞
h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, dimH t ≤ r
⊢ dimH s ≤ r
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_shiftLeftZeroExtend {x : BitVec m} {n : Nat} (h : i < m + n) :
    (shiftLeftZeroExtend x n)[i] = ((! decide (i < n)) && getLsbD x (i - n))

Proof state:
m i : Nat
x : BitVec m
n : Nat
h : i < m + n
⊢ (x.shiftLeftZeroExtend n)[i] = (!decide (i < n) && x.getLsbD (i - n))

Tactic:
rw [shiftLeftZeroExtend_eq, getLsbD]

Result:
m i : Nat
x : BitVec m
n : Nat
h : i < m + n
⊢ (setWidth (m + n) x <<< n)[i] = (!decide (i < n) && x.toNat.testBit (i - n))

Proof state:
m i : Nat
x : BitVec m
n : Nat
h : i < m + n
⊢ (setWidth (m + n) x <<< n)[i] = (!decide (i < n) && x.toNat.testBit (i - n))

Tactic:
simp only [getElem_eq_testBit_toNat, getLsbD_shiftLeft, getLsbD_setWidth]

Result:
m i : Nat
x : BitVec m
n : Nat
h : i < m + n
⊢ (setWidth (m + n) x <<< n).toNat.testBit i = (!decide (i < n) && x.toNat.testBit (i - n))

Proof state:
m i : Nat
x : BitVec m
n : Nat
h : i < m + n
⊢ (setWidth (m + n) x <<< n).toNat.testBit i = (!decide (i < n) && x.toNat.testBit (i - n))

Tactic:
cases h₁ : decide (i < n) <;> cases h₂ : decide (i - n < m + n)
  <;> simp_all [h]
  <;> omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem exists_of_findSome?_eq_some {f : α → Option β} {l : Array α} (w : l.findSome? f = some b) :
    ∃ a, a ∈ l ∧ f a = b

Proof state:
case mk
α : Type u_1
β : Type u_2
b : β
f : α → Option β
toList✝ : List α
w : findSome? f { toList := toList✝ } = some b
⊢ ∃ a, a ∈ { toList := toList✝ } ∧ f a = some b

Tactic:
simp_all [List.exists_of_findSome?_eq_some]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
b : β
f : α → Option β
l : Array α
w : findSome? f l = some b
⊢ ∃ a, a ∈ l ∧ f a = some b

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
b : β
f : α → Option β
toList✝ : List α
w : findSome? f { toList := toList✝ } = some b
⊢ ∃ a, a ∈ { toList := toList✝ } ∧ f a = some b
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem zero : FinMeasAdditive μ (0 : Set α → β) := fun _ _ _ _ _ _ _ => by simp

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : AddCommMonoid β
x✝⁶ x✝⁵ : Set α
x✝⁴ : MeasurableSet x✝⁶
x✝³ : MeasurableSet x✝⁵
x✝² : μ x✝⁶ ≠ ⊤
x✝¹ : μ x✝⁵ ≠ ⊤
x✝ : Disjoint x✝⁶ x✝⁵
⊢ 0 (x✝⁶ ∪ x✝⁵) = 0 x✝⁶ + 0 x✝⁵

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Real/Pi/Wallis.lean
theorem W_pos (k : ℕ) : 0 < W k

Proof state:
k : ℕ
⊢ 0 < W k

Tactic:
induction' k with k hk

Result:
case zero

⊢ 0 < W 0

case succ
k : ℕ
hk : 0 < W k
⊢ 0 < W (k + 1)

Proof state:
case succ
k : ℕ
hk : 0 < W k
⊢ 0 < W (k + 1)

Tactic:
rw [W_succ]

Result:
case succ
k : ℕ
hk : 0 < W k
⊢ 0 < W k * ((2 * ↑k + 2) / (2 * ↑k + 1) * ((2 * ↑k + 2) / (2 * ↑k + 3)))

Proof state:
case succ
k : ℕ
hk : 0 < W k
⊢ 0 < W k * ((2 * ↑k + 2) / (2 * ↑k + 1) * ((2 * ↑k + 2) / (2 * ↑k + 3)))

Tactic:
refine mul_pos hk (mul_pos (div_pos ?_ ?_) (div_pos ?_ ?_)) <;> positivity

Result:
no goals

Proof state:
case zero

⊢ 0 < ∏ i ∈ range 0, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3))

Tactic:
simp

Result:
no goals

Proof state:
case zero

⊢ 0 < W 0

Tactic:
unfold W

Result:
case zero

⊢ 0 < ∏ i ∈ range 0, (2 * ↑i + 2) / (2 * ↑i + 1) * ((2 * ↑i + 2) / (2 * ↑i + 3))
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem smeval_congr : f = g → x = y → f.smeval x = g.smeval y

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
f g : R[T;T⁻¹]
x y : Sˣ
⊢ f = g → x = y → f.smeval x = g.smeval y

Tactic:
rintro rfl rfl

Result:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
f : R[T;T⁻¹]
x : Sˣ
⊢ f.smeval x = f.smeval x

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid S
inst✝¹ : SMulWithZero R S
inst✝ : Monoid S
f : R[T;T⁻¹]
x : Sˣ
⊢ f.smeval x = f.smeval x

Tactic:
rfl

Result:
no goals