harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem lift_comp_reindex (e : ι ≃ ι₂) (φ : MultilinearMap R (fun i ↦ s (e.symm i)) E) :
    lift φ ∘ₗ (reindex R s e) = lift ((domDomCongrLinearEquiv' R R s _ e).symm φ)

Proof state:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
e : ι ≃ ι₂
φ : MultilinearMap R (fun i => s (e.symm i)) E
⊢ lift φ ∘ₗ ↑(reindex R s e) = lift ((domDomCongrLinearEquiv' R R s E e).symm φ)

Tactic:
ext

Result:
case H.H
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
e : ι ≃ ι₂
φ : MultilinearMap R (fun i => s (e.symm i)) E
x✝ : (i : ι) → s i
⊢ ((lift φ ∘ₗ ↑(reindex R s e)).compMultilinearMap (tprod R)) x✝ =
    ((lift ((domDomCongrLinearEquiv' R R s E e).symm φ)).compMultilinearMap (tprod R)) x✝

Proof state:
case H.H
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
e : ι ≃ ι₂
φ : MultilinearMap R (fun i => s (e.symm i)) E
x✝ : (i : ι) → s i
⊢ ((lift φ ∘ₗ ↑(reindex R s e)).compMultilinearMap (tprod R)) x✝ =
    ((lift ((domDomCongrLinearEquiv' R R s E e).symm φ)).compMultilinearMap (tprod R)) x✝

Tactic:
simp [reindex]

Result:
no goals
-- Mathlib/Topology/Order/T5.lean
theorem compl_ordConnectedSection_ordSeparatingSet_mem_nhds (hd : Disjoint s (closure t))
    (ha : a ∈ s) : (ordConnectedSection <| ordSeparatingSet s t)ᶜ ∈ 𝓝 a

Proof state:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure t)
ha : a ∈ s
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a ∧ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a

Tactic:
exact ⟨compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE hd ha,
  compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE hd ha⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure t)
ha : a ∈ s
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝 a

Tactic:
rw [← nhdsLE_sup_nhdsGE, mem_sup]

Result:
X : Type u_1
inst✝² : LinearOrder X
inst✝¹ : TopologicalSpace X
inst✝ : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure t)
ha : a ∈ s
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≤] a ∧ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem cos_sq_add_sin_sq (θ : Real.Angle) : cos θ ^ 2 + sin θ ^ 2 = 1

Proof state:
case h
x✝ : ℝ
⊢ (↑x✝).cos ^ 2 + (↑x✝).sin ^ 2 = 1

Tactic:
exact Real.cos_sq_add_sin_sq _

Result:
no goals

Proof state:
θ : Angle
⊢ θ.cos ^ 2 + θ.sin ^ 2 = 1

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ (↑x✝).cos ^ 2 + (↑x✝).sin ^ 2 = 1
-- Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean
theorem re_exp (q : ℍ[ℝ]) : (exp ℝ q).re = exp ℝ q.re * Real.cos ‖q - q.re‖

Proof state:
q : ℍ
⊢ (exp ℝ q).re = exp ℝ q.re * Real.cos ‖q - ↑q.re‖

Tactic:
simp [exp_eq]

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
lemma ceil_lt_two_mul (ha : 2⁻¹ < a) : ⌈a⌉₊ < 2 * a :=
  ceil_lt_mul one_lt_two (by norm_num at ha ⊢; exact ha)

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a : α
ha : 1 / 2 < a
⊢ 1 / 2 < a

Tactic:
exact ha

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a : α
ha : 2⁻¹ < a
⊢ ↑⌈(2 - 1)⁻¹⌉₊ / 2 < a

Tactic:
norm_num at ha ⊢

Result:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorSemiring α
a : α
ha : 1 / 2 < a
⊢ 1 / 2 < a
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem lift_comp_kernelIsoOfEq_inv {Z} {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g)
    (e : Z ⟶ X) (he) :
    kernel.lift _ e he ≫ (kernelIsoOfEq h).inv = kernel.lift _ e (by simp [h, he])

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
e : Z ⟶ X
he : e ≫ g = 0
⊢ kernel.lift g e he ≫ (kernelIsoOfEq h).inv = kernel.lift f e ⋯

Tactic:
cases h

Result:
case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasKernel f
e : Z ⟶ X
inst✝ : HasKernel f
he : e ≫ f = 0
⊢ kernel.lift f e he ≫ (kernelIsoOfEq ⋯).inv = kernel.lift f e ⋯

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
X Y : C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
Z : C
f g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
e : Z ⟶ X
he : e ≫ g = 0
⊢ e ≫ f = 0

Tactic:
simp [h, he]

Result:
no goals

Proof state:
case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasKernel f
e : Z ⟶ X
inst✝ : HasKernel f
he : e ≫ f = 0
⊢ kernel.lift f e he ≫ (kernelIsoOfEq ⋯).inv = kernel.lift f e ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
theorem measurable_injection_nat_bool_of_countablySeparated [MeasurableSpace α]
    [CountablySeparated α] : ∃ f : α → ℕ → Bool, Measurable f ∧ Injective f

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
⊢ ∃ f, Measurable f ∧ Injective f

Tactic:
rcases exists_countablyGenerated_le_of_countablySeparated α with ⟨m', _, _, m'le⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
m' : MeasurableSpace α
left✝¹ : CountablyGenerated α
left✝ : SeparatesPoints α
m'le : m' ≤ inst✝¹
⊢ ∃ f, Measurable f ∧ Injective f

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
m' : MeasurableSpace α
left✝¹ : CountablyGenerated α
left✝ : SeparatesPoints α
m'le : m' ≤ inst✝¹
⊢ Measurable (mapNatBool α)

Tactic:
exact (measurable_mapNatBool _).mono m'le le_rfl

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
m' : MeasurableSpace α
left✝¹ : CountablyGenerated α
left✝ : SeparatesPoints α
m'le : m' ≤ inst✝¹
⊢ ∃ f, Measurable f ∧ Injective f

Tactic:
refine ⟨mapNatBool α, ?_, injective_mapNatBool _⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : CountablySeparated α
m' : MeasurableSpace α
left✝¹ : CountablyGenerated α
left✝ : SeparatesPoints α
m'le : m' ≤ inst✝¹
⊢ Measurable (mapNatBool α)
-- Mathlib/Data/Finset/Basic.lean
theorem filter_mem_eq_inter {s t : Finset α} [∀ i, Decidable (i ∈ t)] :
    (s.filter fun i => i ∈ t) = s ∩ t :=
  ext fun i => by simp [mem_filter, mem_inter]

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
s t : Finset α
inst✝ : (i : α) → Decidable (i ∈ t)
i : α
⊢ i ∈ filter (fun i => i ∈ t) s ↔ i ∈ s ∩ t

Tactic:
simp [mem_filter, mem_inter]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem IsOpen.ite (hs : IsOpen s) (hs' : IsOpen s')
    (ht : s ∩ frontier t = s' ∩ frontier t) : IsOpen (t.ite s s') :=
  hs.ite' hs' fun x hx => by simpa [hx] using Set.ext_iff.1 ht x

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
hs : IsOpen s
hs' : IsOpen s'
ht : s ∩ frontier t = s' ∩ frontier t
x : α
hx : x ∈ frontier t
⊢ x ∈ s ↔ x ∈ s'

Tactic:
simpa [hx] using Set.ext_iff.1 ht x

Result:
no goals
-- Mathlib/Combinatorics/Schnirelmann.lean
/-- The Schnirelmann density is unaffected by removing `0`. -/
lemma schnirelmannDensity_diff_singleton_zero [DecidablePred (· ∈ A \ {0})] :
    schnirelmannDensity (A \ {0}) = schnirelmannDensity A :=
  schnirelmannDensity_congr' (by aesop)

Proof state:
A : Set ℕ
inst✝¹ : DecidablePred fun x => x ∈ A
inst✝ : DecidablePred fun x => x ∈ A \ {0}
⊢ ∀ n > 0, n ∈ A \ {0} ↔ n ∈ A

Tactic:
aesop

Result:
no goals
-- Mathlib/Analysis/Calculus/BumpFunction/Basic.lean
theorem tsupport_eq : tsupport f = closedBall c f.rOut

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : HasContDiffBump E
c : E
f : ContDiffBump c
⊢ tsupport ↑f = closedBall c f.rOut

Tactic:
simp_rw [tsupport, f.support_eq, closure_ball _ f.rOut_pos.ne']

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
theorem Parallel.direction_eq {s₁ s₂ : AffineSubspace k P} (h : s₁ ∥ s₂) :
    s₁.direction = s₂.direction

Proof state:
case intro
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
⊢ s₁.direction = (map (↑(constVAdd k P v)) s₁).direction

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₁ s₂ : AffineSubspace k P
h : s₁ ∥ s₂
⊢ s₁.direction = s₂.direction

Tactic:
rcases h with ⟨v, rfl⟩

Result:
case intro
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
⊢ s₁.direction = (map (↑(constVAdd k P v)) s₁).direction
-- Mathlib/Algebra/CharP/Lemmas.lean
theorem add_pow_prime_eq (h : Commute x y) :
    (x + y) ^ p =
      x ^ p + y ^ p + p * ∑ k ∈ Finset.Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p)

Proof state:
R : Type u_1
inst✝ : Semiring R
p : ℕ
hp : Nat.Prime p
x y : R
h : Commute x y
⊢ (x + y) ^ p = x ^ p + y ^ p + ↑p * ∑ k ∈ Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p)

Tactic:
simpa using h.add_pow_prime_pow_eq hp 1

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem pow_apply_mem_support {n : ℕ} {x : α} : (f ^ n) x ∈ f.support ↔ x ∈ f.support

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
n : ℕ
x : α
⊢ (f ^ n) x ∈ f.support ↔ x ∈ f.support

Tactic:
simp only [mem_support, ne_eq, apply_pow_apply_eq_iff]

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
theorem trans_refl (e : α ≃ β) : e.trans (Equiv.refl β) = e

Proof state:
α : Sort u
β : Sort v
e : α ≃ β
⊢ e.trans (Equiv.refl β) = e

Tactic:
cases e

Result:
case mk
α : Sort u
β : Sort v
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
⊢ { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.trans (Equiv.refl β) =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Proof state:
case mk
α : Sort u
β : Sort v
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
⊢ { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.trans (Equiv.refl β) =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Projection.lean
theorem ofIsCompl_smul {R : Type*} [CommRing R] {E : Type*} [AddCommGroup E] [Module R E]
    {F : Type*} [AddCommGroup F] [Module R F] {p q : Submodule R E} (h : IsCompl p q)
    {φ : p →ₗ[R] F} {ψ : q →ₗ[R] F} (c : R) : ofIsCompl h (c • φ) (c • ψ) = c • ofIsCompl h φ ψ :=
  ofIsCompl_eq _ (by simp) (by simp)

Proof state:
R : Type u_7
inst✝⁴ : CommRing R
E : Type u_8
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_9
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
c : R
⊢ ∀ (u : ↥p), (c • φ) u = (c • ofIsCompl h φ ψ) ↑u

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_7
inst✝⁴ : CommRing R
E : Type u_8
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_9
inst✝¹ : AddCommGroup F
inst✝ : Module R F
p q : Submodule R E
h : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
c : R
⊢ ∀ (u : ↥q), (c • ψ) u = (c • ofIsCompl h φ ψ) ↑u

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Limits.lean
theorem isSheaf_of_isLimit (F : K ⥤ Sheaf J D) (E : Cone (F ⋙ sheafToPresheaf J D))
    (hE : IsLimit E) : Presheaf.IsSheaf J E.pt

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
⊢ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork E.pt))

Tactic:
intro X S

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
S : J.Cover X
⊢ Nonempty (IsLimit (S.multifork E.pt))

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
X : C
S : J.Cover X
⊢ Nonempty (IsLimit (S.multifork E.pt))

Tactic:
exact ⟨isLimitMultiforkOfIsLimit _ _ hE _ _⟩

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
⊢ Presheaf.IsSheaf J E.pt

Tactic:
rw [Presheaf.isSheaf_iff_multifork]

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasLimitsOfShape K D
F : K ⥤ Sheaf J D
E : Cone (F ⋙ sheafToPresheaf J D)
hE : IsLimit E
⊢ ∀ (X : C) (S : J.Cover X), Nonempty (IsLimit (S.multifork E.pt))
-- Mathlib/Data/Matroid/Restrict.lean
theorem isBasis_restrict_iff (hR : R ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
R I X : Set α
hR : autoParam (R ⊆ M.E) _auto✝
hXR : X ⊆ R
⊢ M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I X

Tactic:
rw [← isBasis'_iff_isBasis_inter_ground, isBasis'_iff_isBasis]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
R I X : Set α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ X ⊆ R → (M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I X)

Tactic:
intro hXR

Result:
α : Type u_1
M : Matroid α
R I X : Set α
hR : autoParam (R ⊆ M.E) _auto✝
hXR : X ⊆ R
⊢ M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I X

Proof state:
α : Type u_1
M : Matroid α
R I X : Set α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ (M ↾ R).IsBasis I X ↔ M.IsBasis I X ∧ X ⊆ R

Tactic:
rw [isBasis_restrict_iff', and_congr_left_iff]

Result:
α : Type u_1
M : Matroid α
R I X : Set α
hR : autoParam (R ⊆ M.E) _auto✝
⊢ X ⊆ R → (M.IsBasis I (X ∩ M.E) ↔ M.IsBasis I X)
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
lemma integrable_cexp_mul_of_re_mem_integrableExpSet (hX : AEMeasurable X μ)
    (hz : z.re ∈ integrableExpSet X μ) :
    Integrable (fun ω ↦ cexp (z * X ω)) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
hz : z.re ∈ integrableExpSet X μ
⊢ Integrable (fun a => ‖cexp (z * ↑(X a))‖) μ

Tactic:
simpa [Complex.norm_exp] using hz

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
hz : z.re ∈ integrableExpSet X μ
⊢ AEStronglyMeasurable (fun ω => cexp (z * ↑(X ω))) μ

Tactic:
exact AEMeasurable.aestronglyMeasurable (by fun_prop)

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
hz : z.re ∈ integrableExpSet X μ
⊢ Integrable (fun ω => cexp (z * ↑(X ω))) μ

Tactic:
rw [← integrable_norm_iff]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
hz : z.re ∈ integrableExpSet X μ
⊢ Integrable (fun a => ‖cexp (z * ↑(X a))‖) μ

Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
hz : z.re ∈ integrableExpSet X μ
⊢ AEStronglyMeasurable (fun ω => cexp (z * ↑(X ω))) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
hz : z.re ∈ integrableExpSet X μ
⊢ AEMeasurable (fun ω => cexp (z * ↑(X ω))) μ

Tactic:
fun_prop

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem inl_isoIsPushout_inv (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') :
    inl' ≫ (h.isoIsPushout _ _ h').inv = inl

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
P' : C
inl' : X ⟶ P'
inr' : Y ⟶ P'
h : IsPushout f g inl inr
h' : IsPushout f g inl' inr'
⊢ inl' ≫ (isoIsPushout X Y h h').inv = inl

Tactic:
simp only [Iso.comp_inv_eq, inl_isoIsPushout_hom]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/GramSchmidtOrtho.lean
theorem gramSchmidt_def' (f : ι → E) (n : ι) :
    f n = gramSchmidt 𝕜 f n + ∑ i ∈ Iio n, orthogonalProjection (𝕜 ∙ gramSchmidt 𝕜 f i) (f n)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
ι : Type u_3
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : WellFoundedLT ι
f : ι → E
n : ι
⊢ f n = gramSchmidt 𝕜 f n + ∑ i ∈ Iio n, ↑((orthogonalProjection (span 𝕜 {gramSchmidt 𝕜 f i})) (f n))

Tactic:
rw [gramSchmidt_def, sub_add_cancel]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem mem_span_set {m : M} {s : Set M} :
    m ∈ Submodule.span R s ↔
      ∃ c : M →₀ R, (c.support : Set M) ⊆ s ∧ (c.sum fun mi r => r • mi) = m

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
s : Set M
⊢ m ∈ span R s ↔ ∃ c, ↑c.support ⊆ s ∧ (c.sum fun mi r => r • mi) = m

Tactic:
conv_lhs => rw [← Set.image_id s]

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
s : Set M
⊢ m ∈ span R (_root_.id '' s) ↔ ∃ c, ↑c.support ⊆ s ∧ (c.sum fun mi r => r • mi) = m

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
s : Set M
⊢ m ∈ span R (_root_.id '' s) ↔ ∃ c, ↑c.support ⊆ s ∧ (c.sum fun mi r => r • mi) = m

Tactic:
exact Finsupp.mem_span_image_iff_linearCombination R (v := _root_.id (α := M))

Result:
no goals
-- Mathlib/Topology/Bases.lean
theorem _root_.Topology.IsQuotientMap.secondCountableTopology [SecondCountableTopology X]
    (h' : IsQuotientMap π) (h : IsOpenMap π) : SecondCountableTopology Y where
  is_open_generated_countable

Proof state:
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
π : X → Y
inst✝ : SecondCountableTopology X
h' : IsQuotientMap π
h : IsOpenMap π
⊢ ∃ b, b.Countable ∧ inst✝¹ = generateFrom b

Tactic:
obtain ⟨V, V_countable, -, V_generates⟩ := exists_countable_basis X

Result:
case intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
π : X → Y
inst✝ : SecondCountableTopology X
h' : IsQuotientMap π
h : IsOpenMap π
V : Set (Set X)
V_countable : V.Countable
V_generates : IsTopologicalBasis V
⊢ ∃ b, b.Countable ∧ inst✝¹ = generateFrom b

Proof state:
case intro.intro.intro
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : TopologicalSpace Y
π : X → Y
inst✝ : SecondCountableTopology X
h' : IsQuotientMap π
h : IsOpenMap π
V : Set (Set X)
V_countable : V.Countable
V_generates : IsTopologicalBasis V
⊢ ∃ b, b.Countable ∧ inst✝¹ = generateFrom b

Tactic:
exact ⟨Set.image π '' V, V_countable.image (Set.image π),
  (V_generates.isQuotientMap h' h).eq_generateFrom⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem decide_ite (u : Prop) [du : Decidable u] (p q : Prop)
      [dpq : Decidable (ite u p q)] [dp : Decidable p] [dq : Decidable q] :
    decide (ite u p q) = ite u (decide p) (decide q)

Proof state:
u : Prop
du : Decidable u
p q : Prop
dpq : Decidable (if u then p else q)
dp : Decidable p
dq : Decidable q
⊢ decide (if u then p else q) = if u then decide p else decide q

Tactic:
cases du <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem extract.go₁_cons_addChar (c : Char) (cs : List Char) (b e : Pos) :
    go₁ (c :: cs) 0 (b + c) (e + c) = go₁ cs 0 b e

Proof state:
c : Char
cs : List Char
b e : Pos
⊢ go₁ (c :: cs) 0 (b + c) (e + c) = go₁ cs 0 b e

Tactic:
simp only [go₁, Pos.ext_iff, Pos.byteIdx_zero, pos_add_char, Nat.ne_of_lt add_utf8Size_pos,
  ↓reduceIte]

Result:
c : Char
cs : List Char
b e : Pos
⊢ go₁ cs (0 + c) (b + c) (e + c) = go₁ cs 0 b e

Proof state:
c : Char
cs : List Char
b e : Pos
⊢ go₁ cs (0 + c) (b + c) (e + c) = go₁ cs 0 b e

Tactic:
apply go₁_add_right_cancel

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem of_ne_one_ne_zero {z : ℤ} (hp : p ≠ 1) (hz : z ≠ 0) :
    padicValInt p z = multiplicity (p : ℤ) z

Proof state:
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ padicValInt p z = multiplicity (↑p) z

Tactic:
rw [padicValInt, padicValNat_def' hp (Int.natAbs_pos.mpr hz)]

Result:
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ multiplicity p z.natAbs = multiplicity (↑p) z

Proof state:
p : ℕ
z : ℤ
hp : p ≠ 1
hz : z ≠ 0
⊢ multiplicity p z.natAbs = multiplicity (↑p) z

Tactic:
apply Int.multiplicity_natAbs

Result:
no goals
-- Mathlib/Computability/Reduce.lean
theorem manyOneEquiv_toNat (p : Set α) (q : Set β) :
    ManyOneEquiv (toNat p) (toNat q) ↔ ManyOneEquiv p q

Proof state:
α : Type u
inst✝³ : Primcodable α
inst✝² : Inhabited α
β : Type v
inst✝¹ : Primcodable β
inst✝ : Inhabited β
p : Set α
q : Set β
⊢ ManyOneEquiv (toNat p) (toNat q) ↔ ManyOneEquiv p q

Tactic:
simp [ManyOneEquiv]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Basic.lean
theorem charmatrix_reindex (e : n ≃ m) :
    charmatrix (reindex e e M) = reindex e e (charmatrix M)

Proof state:
case neg
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M : Matrix n n R
e : n ≃ m
i j : m
x : ℕ
h : ¬i = j
⊢ (((reindex e e) M).charmatrix i j).coeff x = ((reindex e e) M.charmatrix i j).coeff x

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M : Matrix n n R
e : n ≃ m
⊢ ((reindex e e) M).charmatrix = (reindex e e) M.charmatrix

Tactic:
ext i j x

Result:
case a.a
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M : Matrix n n R
e : n ≃ m
i j : m
x : ℕ
⊢ (((reindex e e) M).charmatrix i j).coeff x = ((reindex e e) M.charmatrix i j).coeff x

Proof state:
case a.a
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M : Matrix n n R
e : n ≃ m
i j : m
x : ℕ
⊢ (((reindex e e) M).charmatrix i j).coeff x = ((reindex e e) M.charmatrix i j).coeff x

Tactic:
by_cases h : i = j

Result:
case pos
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M : Matrix n n R
e : n ≃ m
i j : m
x : ℕ
h : i = j
⊢ (((reindex e e) M).charmatrix i j).coeff x = ((reindex e e) M.charmatrix i j).coeff x

case neg
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M : Matrix n n R
e : n ≃ m
i j : m
x : ℕ
h : ¬i = j
⊢ (((reindex e e) M).charmatrix i j).coeff x = ((reindex e e) M.charmatrix i j).coeff x

Proof state:
case pos
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M : Matrix n n R
e : n ≃ m
i j : m
x : ℕ
h : i = j
⊢ (((reindex e e) M).charmatrix i j).coeff x = ((reindex e e) M.charmatrix i j).coeff x

case neg
R : Type u_1
inst✝⁴ : CommRing R
m : Type u_3
n : Type u_4
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : Fintype n
M : Matrix n n R
e : n ≃ m
i j : m
x : ℕ
h : ¬i = j
⊢ (((reindex e e) M).charmatrix i j).coeff x = ((reindex e e) M.charmatrix i j).coeff x

Tactic:
all_goals simp [h]

Result:
no goals