harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem affineSpan_coe (s : AffineSubspace k P) : affineSpan k (s : Set P) = s

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
⊢ affineSpan k ↑s ≤ s

Tactic:
rintro p ⟨p₁, hp₁, v, hv, rfl⟩

Result:
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
v : V
hv : v ∈ vectorSpan k ↑s
⊢ v +ᵥ p₁ ∈ ↑s

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
⊢ affineSpan k ↑s = s

Tactic:
refine le_antisymm ?_ (subset_spanPoints _ _)

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
⊢ affineSpan k ↑s ≤ s

Proof state:
case intro.intro.intro.intro
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : AffineSubspace k P
p₁ : P
hp₁ : p₁ ∈ ↑s
v : V
hv : v ∈ vectorSpan k ↑s
⊢ v +ᵥ p₁ ∈ ↑s

Tactic:
exact vadd_mem_of_mem_direction hv hp₁

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive (attr := simp) nsmul_empty]
lemma empty_pow (hn : n ≠ 0) : (∅ : Finset α) ^ n = ∅ := match n with | n + 1 => by simp [pow_succ]

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
n✝ n : ℕ
hn : n + 1 ≠ 0
⊢ ∅ ^ (n + 1) = ∅

Tactic:
simp [pow_succ]

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem grundyValue_add (G H : PGame) [G.Impartial] [H.Impartial] :
    grundyValue (G + H) = grundyValue G + grundyValue H

Proof state:
G H : PGame
inst✝¹ : G.Impartial
inst✝ : H.Impartial
⊢ G + H ≈ nim (toOrdinal G.grundyValue) + nim (toOrdinal H.grundyValue)

Tactic:
exact add_congr (equiv_nim_grundyValue G) (equiv_nim_grundyValue H)

Result:
no goals

Proof state:
G H : PGame
inst✝¹ : G.Impartial
inst✝ : H.Impartial
⊢ (G + H).grundyValue = G.grundyValue + H.grundyValue

Tactic:
rw [← (grundyValue G).toOrdinal_toNimber, ← (grundyValue H).toOrdinal_toNimber,
  ← grundyValue_nim_add_nim, grundyValue_eq_iff_equiv]

Result:
G H : PGame
inst✝¹ : G.Impartial
inst✝ : H.Impartial
⊢ G + H ≈ nim (toOrdinal G.grundyValue) + nim (toOrdinal H.grundyValue)
-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
lemma inf_orthogonal_self_le_ker_restrict {W : Submodule R M} (b₁ : B.IsRefl) :
    W ⊓ B.orthogonal W ≤ (LinearMap.ker <| B.restrict W).map W.subtype

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
W : Submodule R M
b₁ : B.IsRefl
⊢ W ⊓ B.orthogonal W ≤ Submodule.map W.subtype (ker (B.restrict W))

Tactic:
rintro v ⟨hv : v ∈ W, hv' : v ∈ B.orthogonal W⟩

Result:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
W : Submodule R M
b₁ : B.IsRefl
v : M
hv : v ∈ W
hv' : v ∈ B.orthogonal W
⊢ v ∈ Submodule.map W.subtype (ker (B.restrict W))

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
W : Submodule R M
b₁ : B.IsRefl
v : M
hv : v ∈ W
hv' : v ∈ B.orthogonal W
⊢ (B v).domRestrict W = 0 ∧ v ∈ W

Tactic:
refine ⟨?_, hv⟩

Result:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
W : Submodule R M
b₁ : B.IsRefl
v : M
hv : v ∈ W
hv' : v ∈ B.orthogonal W
⊢ (B v).domRestrict W = 0

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
W : Submodule R M
b₁ : B.IsRefl
v : M
hv : v ∈ W
hv' : v ∈ B.orthogonal W
⊢ (B v).domRestrict W = 0

Tactic:
ext ⟨w, hw⟩

Result:
case intro.h.mk
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
W : Submodule R M
b₁ : B.IsRefl
v : M
hv : v ∈ W
hv' : v ∈ B.orthogonal W
w : M
hw : w ∈ W
⊢ ((B v).domRestrict W) ⟨w, hw⟩ = 0 ⟨w, hw⟩

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
W : Submodule R M
b₁ : B.IsRefl
v : M
hv : v ∈ W
hv' : v ∈ B.orthogonal W
⊢ v ∈ Submodule.map W.subtype (ker (B.restrict W))

Tactic:
simp only [Submodule.mem_map, mem_ker, restrict_apply, Submodule.coe_subtype, Subtype.exists,
  exists_and_left, exists_prop, exists_eq_right_right]

Result:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
W : Submodule R M
b₁ : B.IsRefl
v : M
hv : v ∈ W
hv' : v ∈ B.orthogonal W
⊢ (B v).domRestrict W = 0 ∧ v ∈ W

Proof state:
case intro.h.mk
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
W : Submodule R M
b₁ : B.IsRefl
v : M
hv : v ∈ W
hv' : v ∈ B.orthogonal W
w : M
hw : w ∈ W
⊢ ((B v).domRestrict W) ⟨w, hw⟩ = 0 ⟨w, hw⟩

Tactic:
exact b₁ w v <| hv' w hw

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem tendsto_integral_approxOn_of_measurable_of_range_subset [MeasurableSpace E] [BorelSpace E]
    {f : α → E} (fmeas : Measurable f) (hf : Integrable f μ) (s : Set E) [SeparableSpace s]
    (hs : range f ∪ {0} ⊆ s) :
    Tendsto (fun n => (SimpleFunc.approxOn f fmeas s 0 (hs <| by simp) n).integral μ) atTop
      (𝓝 <| ∫ x, f x ∂μ)

Proof state:
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst✝ : SeparableSpace ↑s
hs : range f ∪ {0} ⊆ s
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ closure s

Tactic:
exact Eventually.of_forall fun x => subset_closure (hs (Set.mem_union_left _ (mem_range_self _)))

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
𝕜 : Type u_4
inst✝¹² : NormedAddCommGroup E
hE : CompleteSpace E
inst✝¹¹ : NontriviallyNormedField 𝕜
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : CompleteSpace F
G : Type u_5
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace ℝ G
inst✝⁵ : NormedSpace ℝ E
f✝ : α → E
m : MeasurableSpace α
μ : Measure α
X : Type u_6
inst✝⁴ : TopologicalSpace X
inst✝³ : FirstCountableTopology X
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst✝ : SeparableSpace ↑s
hs : range f ∪ {0} ⊆ s
n : ℕ
⊢ 0 ∈ range f ∪ {0}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst✝ : SeparableSpace ↑s
hs : range f ∪ {0} ⊆ s
⊢ Tendsto (fun n => SimpleFunc.integral μ (approxOn f fmeas s 0 ⋯ n)) atTop (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
apply tendsto_integral_approxOn_of_measurable hf fmeas _ _ (integrable_zero _ _ _)

Result:
α : Type u_1
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
hE : CompleteSpace E
inst✝³ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
f : α → E
fmeas : Measurable f
hf : Integrable f μ
s : Set E
inst✝ : SeparableSpace ↑s
hs : range f ∪ {0} ⊆ s
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ closure s
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma stieltjesOfMeasurableRat_ae_eq (hf : IsRatCondKernelCDF f κ ν) (a : α) (q : ℚ) :
    (fun b ↦ stieltjesOfMeasurableRat f hf.measurable (a, b) q) =ᵐ[ν a] fun b ↦ f (a, b) q

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a✝ : α
q : ℚ
a : β
ha : IsRatStieltjesPoint f (a✝, a)
⊢ ↑(stieltjesOfMeasurableRat f ⋯ (a✝, a)) ↑q = f (a✝, a) q

Tactic:
rw [stieltjesOfMeasurableRat_eq, toRatCDF_of_isRatStieltjesPoint ha]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
⊢ (fun b => ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q) =ᶠ[ae (ν a)] fun b => f (a, b) q

Tactic:
filter_upwards [hf.isRatStieltjesPoint_ae a] with a ha

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a✝ : α
q : ℚ
a : β
ha : IsRatStieltjesPoint f (a✝, a)
⊢ ↑(stieltjesOfMeasurableRat f ⋯ (a✝, a)) ↑q = f (a✝, a) q
-- Mathlib/LinearAlgebra/Ray.lean
theorem exists_pos_left_iff_sameRay_and_ne_zero (hx : x ≠ 0) :
    (∃ r : R, 0 < r ∧ r • x = y) ↔ SameRay R x y ∧ y ≠ 0

Proof state:
case mpr.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hxy : SameRay R x y
hy : y ≠ 0
⊢ ∃ r, 0 < r ∧ r • x = y

Tactic:
exact (exists_pos_left_iff_sameRay hx hy).2 hxy

Result:
no goals

Proof state:
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ (∃ r, 0 < r ∧ r • x = y) ↔ SameRay R x y ∧ y ≠ 0

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ (∃ r, 0 < r ∧ r • x = y) → SameRay R x y ∧ y ≠ 0

case mpr
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ SameRay R x y ∧ y ≠ 0 → ∃ r, 0 < r ∧ r • x = y

Proof state:
case mp.intro.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 < r
⊢ SameRay R x (r • x) ∧ r • x ≠ 0

Tactic:
simp [hx, hr.le, hr.ne']

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ (∃ r, 0 < r ∧ r • x = y) → SameRay R x y ∧ y ≠ 0

Tactic:
rintro ⟨r, hr, rfl⟩

Result:
case mp.intro.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x : M
hx : x ≠ 0
r : R
hr : 0 < r
⊢ SameRay R x (r • x) ∧ r • x ≠ 0

Proof state:
case mpr
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
⊢ SameRay R x y ∧ y ≠ 0 → ∃ r, 0 < r ∧ r • x = y

Tactic:
rintro ⟨hxy, hy⟩

Result:
case mpr.intro
R : Type u_1
inst✝² : LinearOrderedField R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
hx : x ≠ 0
hxy : SameRay R x y
hy : y ≠ 0
⊢ ∃ r, 0 < r ∧ r • x = y
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem contDiff_one_iff_deriv :
    ContDiff 𝕜 1 f₂ ↔ Differentiable 𝕜 f₂ ∧ Continuous (deriv f₂)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₂ : 𝕜 → F
⊢ Differentiable 𝕜 f₂ ∧ (0 = ω → AnalyticOn 𝕜 f₂ univ) ∧ ContDiff 𝕜 0 (deriv f₂) ↔
    Differentiable 𝕜 f₂ ∧ Continuous (deriv f₂)

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₂ : 𝕜 → F
⊢ ContDiff 𝕜 1 f₂ ↔ Differentiable 𝕜 f₂ ∧ Continuous (deriv f₂)

Tactic:
rw [show (1 : WithTop ℕ∞) = 0 + 1 from rfl, contDiff_succ_iff_deriv]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f₂ : 𝕜 → F
⊢ Differentiable 𝕜 f₂ ∧ (0 = ω → AnalyticOn 𝕜 f₂ univ) ∧ ContDiff 𝕜 0 (deriv f₂) ↔
    Differentiable 𝕜 f₂ ∧ Continuous (deriv f₂)
-- Mathlib/Order/Heyting/Basic.lean
theorem sdiff_sdiff_sdiff_le_sdiff : (a \ b) \ (a \ c) ≤ c \ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ (a \ b) \ (a \ c) ≤ c \ b

Tactic:
rw [sdiff_le_iff, sdiff_le_iff, sup_left_comm, sup_sdiff_self, sup_left_comm, sdiff_sup_self,
  sup_left_comm]

Result:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ a ⊔ (b ⊔ c)

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ≤ a ⊔ (b ⊔ c)

Tactic:
exact le_sup_left

Result:
no goals
-- Mathlib/RingTheory/Kaehler/CotangentComplex.lean
lemma cotangentSpaceBasis_apply (i) :
    P.cotangentSpaceBasis i = ((1 : S) ⊗ₜ[P.Ring] D R P.Ring (.X i) :)

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Generators R S
i : P.vars
⊢ P.cotangentSpaceBasis i = 1 ⊗ₜ[P.Ring] (D R P.Ring) (X i)

Tactic:
simp [cotangentSpaceBasis, toExtension]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem Prime.pow_dvd_iff_le_factorization {p k n : ℕ} (pp : Prime p) (hn : n ≠ 0) :
    p ^ k ∣ n ↔ k ≤ n.factorization p

Proof state:
p k n : ℕ
pp : Prime p
hn : n ≠ 0
⊢ p ^ k ∣ n ↔ k ≤ n.factorization p

Tactic:
rw [← factorization_le_iff_dvd (pow_pos pp.pos k).ne' hn, pp.factorization_pow, single_le_iff]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Tower.lean
theorem aeval_algebraMap_apply (x : σ → A) (p : MvPolynomial σ R) :
    aeval (algebraMap A B ∘ x) p = algebraMap A B (MvPolynomial.aeval x p)

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
⊢ (aeval (⇑(algebraMap A B) ∘ x)) p = (algebraMap A B) ((aeval x) p)

Tactic:
rw [aeval_def, aeval_def, ← coe_eval₂Hom, ← coe_eval₂Hom, map_eval₂Hom, ←
  IsScalarTower.algebraMap_eq]

Result:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
⊢ (eval₂Hom (algebraMap R B) (⇑(algebraMap A B) ∘ x)) p = (eval₂Hom (algebraMap R B) fun i => (algebraMap A B) (x i)) p

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
⊢ (eval₂Hom (algebraMap R B) (⇑(algebraMap A B) ∘ x)) p = (eval₂Hom (algebraMap R B) fun i => (algebraMap A B) (x i)) p

Tactic:
simp only [Function.comp_def]

Result:
no goals
-- Mathlib/CategoryTheory/NatIso.lean
theorem cancel_natIso_inv_right {X : D} {Y : C} (f f' : X ⟶ G.obj Y) :
    f ≫ α.inv.app Y = f' ≫ α.inv.app Y ↔ f = f'

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
α : F ≅ G
X : D
Y : C
f f' : X ⟶ G.obj Y
⊢ f ≫ α.inv.app Y = f' ≫ α.inv.app Y ↔ f = f'

Tactic:
simp only [cancel_mono, refl]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma IsReal.comap (f : k →+* K) {w : InfinitePlace K} (hφ : IsReal w) :
    IsReal (w.comap f)

Proof state:
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
hφ : w.IsReal
⊢ ComplexEmbedding.IsReal (w.embedding.comp f)

Tactic:
rw [← mk_embedding w, isReal_mk_iff] at hφ

Result:
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
hφ : ComplexEmbedding.IsReal w.embedding
⊢ ComplexEmbedding.IsReal (w.embedding.comp f)

Proof state:
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
hφ : ComplexEmbedding.IsReal w.embedding
⊢ ComplexEmbedding.IsReal (w.embedding.comp f)

Tactic:
exact hφ.comp f

Result:
no goals

Proof state:
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
hφ : w.IsReal
⊢ (w.comap f).IsReal

Tactic:
rw [← mk_embedding w, comap_mk, isReal_mk_iff]

Result:
k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
hφ : w.IsReal
⊢ ComplexEmbedding.IsReal (w.embedding.comp f)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Folds.lean
theorem iunfoldr_replace
    {f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α)
    (init : state 0 = a)
    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsbD i.val)) :
    iunfoldr f a = (state w, value)

Proof state:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
value : BitVec w
a : α
init : state 0 = a
step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value.getLsbD ↑i)
⊢ iunfoldr f a = (state w, value)

Tactic:
simp [iunfoldr.eq_test state value a init step]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem map_eq_bot_iff : I.map f = ⊥ ↔ I ≤ f.ker

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
⊢ map f I = ⊥ ↔ I ≤ f.ker

Tactic:
rw [← le_bot_iff]

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
⊢ map f I ≤ ⊥ ↔ I ≤ f.ker

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
⊢ map f I ≤ ⊥ ↔ I ≤ f.ker

Tactic:
exact LieIdeal.map_le_iff_le_comap

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Opposites.lean
/-- If `F : C ⥤ D` preserves finite coproducts, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite
    products. -/
lemma preservesFiniteProducts_op (F : C ⥤ D) [PreservesFiniteCoproducts F] :
    PreservesFiniteProducts F.op where
  preserves n

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesFiniteCoproducts F
n : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin n)) F.op

Tactic:
apply (config := { allowSynthFailures := true }) preservesLimitsOfShape_op

Result:
case inst
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesFiniteCoproducts F
n : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin n))ᵒᵖ F

Proof state:
case inst
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesFiniteCoproducts F
n : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin n))ᵒᵖ F

Tactic:
exact preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Result:
no goals
-- Mathlib/MeasureTheory/Group/Integral.lean
theorem integral_smul_eq_self {μ : Measure α} [SMulInvariantMeasure G α μ] (f : α → E) {g : G} :
    (∫ x, f (g • x) ∂μ) = ∫ x, f x ∂μ

Proof state:
α : Type u_3
G : Type u_4
E : Type u_5
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : Group G
inst✝³ : MeasurableSpace α
inst✝² : MulAction G α
inst✝¹ : MeasurableSMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
f : α → E
g : G
h : MeasurableEmbedding fun x => g • x
⊢ ∫ (x : α), f (g • x) ∂μ = ∫ (x : α), f x ∂μ

Tactic:
rw [← h.integral_map, map_smul]

Result:
no goals

Proof state:
α : Type u_3
G : Type u_4
E : Type u_5
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : Group G
inst✝³ : MeasurableSpace α
inst✝² : MulAction G α
inst✝¹ : MeasurableSMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
f : α → E
g : G
⊢ ∫ (x : α), f (g • x) ∂μ = ∫ (x : α), f x ∂μ

Tactic:
have h : MeasurableEmbedding fun x : α => g • x := (MeasurableEquiv.smul g).measurableEmbedding

Result:
α : Type u_3
G : Type u_4
E : Type u_5
inst✝⁷ : MeasurableSpace G
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : Group G
inst✝³ : MeasurableSpace α
inst✝² : MulAction G α
inst✝¹ : MeasurableSMul G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
f : α → E
g : G
h : MeasurableEmbedding fun x => g • x
⊢ ∫ (x : α), f (g • x) ∂μ = ∫ (x : α), f x ∂μ
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem mapsTo_extend (hs : s ⊆ f.source) :
    MapsTo (f.extend I) s ((f.extend I).symm ⁻¹' s ∩ range I)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
hs : s ⊆ f.source
⊢ MapsTo (↑(f.extend I)) s (↑(f.extend I).symm ⁻¹' s ∩ range ↑I)

Tactic:
rw [mapsTo', extend_coe, extend_coe_symm, preimage_comp, ← I.image_eq, image_comp,
  f.image_eq_target_inter_inv_preimage hs]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
hs : s ⊆ f.source
⊢ ↑I '' (f.target ∩ ↑f.symm ⁻¹' s) ⊆ ↑I '' (↑f.symm ⁻¹' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
s : Set M
hs : s ⊆ f.source
⊢ ↑I '' (f.target ∩ ↑f.symm ⁻¹' s) ⊆ ↑I '' (↑f.symm ⁻¹' s)

Tactic:
exact image_subset _ inter_subset_right

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_image_le (f : α → β) (s : Set α) : (f '' s).encard ≤ s.encard

Proof state:
case inr
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : Nonempty α
⊢ (f '' s).encard ≤ s.encard

Tactic:
rw [← (f.invFunOn_injOn_image s).encard_image]

Result:
case inr
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : Nonempty α
⊢ (Function.invFunOn f s '' (f '' s)).encard ≤ s.encard

Proof state:
case inl
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : IsEmpty α
⊢ (f '' s).encard ≤ s.encard

Tactic:
rw [s.eq_empty_of_isEmpty]

Result:
case inl
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : IsEmpty α
⊢ (f '' ∅).encard ≤ ∅.encard

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ (f '' s).encard ≤ s.encard

Tactic:
obtain (h | h) := isEmpty_or_nonempty α

Result:
case inl
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : IsEmpty α
⊢ (f '' s).encard ≤ s.encard

case inr
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : Nonempty α
⊢ (f '' s).encard ≤ s.encard

Proof state:
case inr.h
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : Nonempty α
⊢ Function.invFunOn f s '' (f '' s) ⊆ s

Tactic:
exact f.invFunOn_image_image_subset s

Result:
no goals

Proof state:
case inl
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : IsEmpty α
⊢ (f '' ∅).encard ≤ ∅.encard

Tactic:
simp

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : Nonempty α
⊢ (Function.invFunOn f s '' (f '' s)).encard ≤ s.encard

Tactic:
apply encard_le_encard

Result:
case inr.h
α : Type u_1
β : Type u_2
f : α → β
s : Set α
h : Nonempty α
⊢ Function.invFunOn f s '' (f '' s) ⊆ s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Folds.lean
theorem iunfoldr_replace_snd
  {f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α)
    (init : state 0 = a)
    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsbD i.val)) :
    (iunfoldr f a).snd = value

Proof state:
w : Nat
α : Type u_1
f : Fin w → α → α × Bool
state : Nat → α
value : BitVec w
a : α
init : state 0 = a
step : ∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value.getLsbD ↑i)
⊢ (iunfoldr f a).snd = value

Tactic:
simp [iunfoldr.eq_test state value a init step]

Result:
no goals