harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Generator/Presheaf.lean
@[reassoc]
lemma freeYonedaHomEquiv_symm_comp {X : C} {M : A} {F G : Cᵒᵖ ⥤ A} (α : M ⟶ F.obj (op X))
    (f : F ⟶ G) :
    freeYonedaHomEquiv.symm α ≫ f = freeYonedaHomEquiv.symm (α ≫ f.app (op X))

Proof state:
case intro.a
C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
X : C
M : A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
β : freeYoneda X M ⟶ F
⊢ freeYonedaHomEquiv (freeYonedaHomEquiv.symm (freeYonedaHomEquiv β) ≫ f) =
    freeYonedaHomEquiv (freeYonedaHomEquiv.symm (freeYonedaHomEquiv β ≫ f.app (op X)))

Tactic:
simp only [Equiv.symm_apply_apply, freeYonedaHomEquiv_comp, Equiv.apply_symm_apply]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
X : C
M : A
F G : Cᵒᵖ ⥤ A
α : M ⟶ F.obj (op X)
f : F ⟶ G
⊢ freeYonedaHomEquiv.symm α ≫ f = freeYonedaHomEquiv.symm (α ≫ f.app (op X))

Tactic:
obtain ⟨β, rfl⟩ := freeYonedaHomEquiv.surjective α

Result:
case intro
C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
X : C
M : A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
β : freeYoneda X M ⟶ F
⊢ freeYonedaHomEquiv.symm (freeYonedaHomEquiv β) ≫ f = freeYonedaHomEquiv.symm (freeYonedaHomEquiv β ≫ f.app (op X))

Proof state:
case intro
C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
X : C
M : A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
β : freeYoneda X M ⟶ F
⊢ freeYonedaHomEquiv.symm (freeYonedaHomEquiv β) ≫ f = freeYonedaHomEquiv.symm (freeYonedaHomEquiv β ≫ f.app (op X))

Tactic:
apply freeYonedaHomEquiv.injective

Result:
case intro.a
C : Type u
inst✝² : Category.{v, u} C
A : Type u'
inst✝¹ : Category.{v', u'} A
inst✝ : HasCoproducts A
X : C
M : A
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
β : freeYoneda X M ⟶ F
⊢ freeYonedaHomEquiv (freeYonedaHomEquiv.symm (freeYonedaHomEquiv β) ≫ f) =
    freeYonedaHomEquiv (freeYonedaHomEquiv.symm (freeYonedaHomEquiv β ≫ f.app (op X)))
-- Mathlib/Geometry/Manifold/Instances/Real.lean
theorem interior_halfSpace {n : ℕ} (p : ℝ≥0∞) (a : ℝ) (i : Fin n) :
    interior { y : PiLp p (fun _ : Fin n ↦ ℝ) | a ≤ y i } = { y | a < y i }

Proof state:
case hsurj
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (Fin n → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
⊢ Surjective ⇑f

Tactic:
apply Function.surjective_eval

Result:
no goals

Proof state:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (Fin n → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
⊢ interior (⇑f ⁻¹' Ici a) = ⇑f ⁻¹' Ioi a

Tactic:
rw [f.interior_preimage, interior_Ici]

Result:
case hsurj
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (Fin n → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
⊢ Surjective ⇑f

Proof state:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (Fin n → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
⊢ interior {y | a ≤ y i} = {y | a < y i}

Tactic:
change interior (f ⁻¹' Ici a) = f ⁻¹' Ioi a

Result:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (Fin n → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
⊢ interior (⇑f ⁻¹' Ici a) = ⇑f ⁻¹' Ioi a

Proof state:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
⊢ interior {y | a ≤ y i} = {y | a < y i}

Tactic:
let f : (Π _ : Fin n, ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i

Result:
n : ℕ
p : ℝ≥0∞
a : ℝ
i : Fin n
f : (Fin n → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj i
⊢ interior {y | a ≤ y i} = {y | a < y i}
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
/-- Given `u : α → β` a uniform inducing map, a family `𝓕 : ι → X → α` is equicontinuous at a point
`x₀ : X` within a subset `S : Set X` iff the family `𝓕'`, obtained by composing each function
of `𝓕` by `u`, is equicontinuous at `x₀` within `S`. -/
lemma IsUniformInducing.equicontinuousWithinAt_iff {F : ι → X → α} {S : Set X} {x₀ : X} {u : α → β}
    (hu : IsUniformInducing u) : EquicontinuousWithinAt F S x₀ ↔
      EquicontinuousWithinAt ((u ∘ ·) ∘ F) S x₀

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
x₀ : X
u : α → β
hu : IsUniformInducing u
this : IsInducing (⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)
⊢ ContinuousWithinAt ((⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun) ∘ ⇑ofFun ∘ swap F) S x₀ ↔
    ContinuousWithinAt (⇑ofFun ∘ swap ((fun x => u ∘ x) ∘ F)) S x₀

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
x₀ : X
u : α → β
hu : IsUniformInducing u
this : IsInducing (⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)
⊢ EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt ((fun x => u ∘ x) ∘ F) S x₀

Tactic:
simp only [equicontinuousWithinAt_iff_continuousWithinAt, this.continuousWithinAt_iff]

Result:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
x₀ : X
u : α → β
hu : IsUniformInducing u
this : IsInducing (⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)
⊢ ContinuousWithinAt ((⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun) ∘ ⇑ofFun ∘ swap F) S x₀ ↔
    ContinuousWithinAt (⇑ofFun ∘ swap ((fun x => u ∘ x) ∘ F)) S x₀

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
x₀ : X
u : α → β
hu : IsUniformInducing u
⊢ EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt ((fun x => u ∘ x) ∘ F) S x₀

Tactic:
have := (UniformFun.postcomp_isUniformInducing (α := ι) hu).isInducing

Result:
ι : Type u_1
X : Type u_3
α : Type u_6
β : Type u_8
tX : TopologicalSpace X
uα : UniformSpace α
uβ : UniformSpace β
F : ι → X → α
S : Set X
x₀ : X
u : α → β
hu : IsUniformInducing u
this : IsInducing (⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)
⊢ EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt ((fun x => u ∘ x) ∘ F) S x₀
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_of_zero_length (h : w = 0) (x : BitVec w) : x.toNat = 0

Proof state:
x : BitVec 0
⊢ x.toNat = 0

Tactic:
simp [toNat_zero_length]

Result:
no goals

Proof state:
w : Nat
h : w = 0
x : BitVec w
⊢ x.toNat = 0

Tactic:
subst h

Result:
x : BitVec 0
⊢ x.toNat = 0
-- Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean
lemma AbsolutelyContinuous.compProd_left [SFinite ν] (hμν : μ ≪ ν) (κ : Kernel α β) :
    μ ⊗ₘ κ ≪ ν ⊗ₘ κ

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
this : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (ν ⊗ₘ κ) s = 0
⊢ (μ ⊗ₘ κ) s = 0

Tactic:
rw [Measure.compProd_apply hs, lintegral_eq_zero_iff (Kernel.measurable_kernel_prod_mk_left hs)]
  at hs_zero ⊢

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
this : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (fun a => (κ a) (Prod.mk a ⁻¹' s)) =ᶠ[ae ν] 0
⊢ (fun a => (κ a) (Prod.mk a ⁻¹' s)) =ᶠ[ae μ] 0

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
this : SFinite μ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ κ

Tactic:
refine Measure.AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
this : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (ν ⊗ₘ κ) s = 0
⊢ (μ ⊗ₘ κ) s = 0

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ κ

Tactic:
simp [compProd_of_not_isSFiniteKernel _ _ hκ]

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
this : SFinite μ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (fun a => (κ a) (Prod.mk a ⁻¹' s)) =ᶠ[ae ν] 0
⊢ (fun a => (κ a) (Prod.mk a ⁻¹' s)) =ᶠ[ae μ] 0

Tactic:
exact hμν.ae_eq hs_zero

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ κ

Tactic:
by_cases hκ : IsSFiniteKernel κ

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ κ

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : ¬IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ κ

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ κ

Tactic:
have : SFinite μ := sFinite_of_absolutelyContinuous hμν

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
κ : Kernel α β
hκ : IsSFiniteKernel κ
this : SFinite μ
⊢ μ ⊗ₘ κ ≪ ν ⊗ₘ κ
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma map_baseChange [Algebra F K] [IsScalarTower R F K] [Algebra F L] [IsScalarTower R F L]
    (f : K →ₐ[F] L) (P : W'⟮F⟯) : map f (baseChange F K P) = baseChange F L P

Proof state:
R : Type r
F : Type u
K : Type v
L : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Field L
W' : Affine R
inst✝⁶ : Algebra R F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : Algebra F K
inst✝² : IsScalarTower R F K
inst✝¹ : Algebra F L
inst✝ : IsScalarTower R F L
f : K →ₐ[F] L
P : W'⟮F⟯
⊢ (map f) ((baseChange F K) P) = (baseChange F L) P

Tactic:
have : Subsingleton (F →ₐ[F] L) := inferInstance

Result:
R : Type r
F : Type u
K : Type v
L : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Field L
W' : Affine R
inst✝⁶ : Algebra R F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : Algebra F K
inst✝² : IsScalarTower R F K
inst✝¹ : Algebra F L
inst✝ : IsScalarTower R F L
f : K →ₐ[F] L
P : W'⟮F⟯
this : Subsingleton (F →ₐ[F] L)
⊢ (map f) ((baseChange F K) P) = (baseChange F L) P

Proof state:
R : Type r
F : Type u
K : Type v
L : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : Field F
inst✝⁸ : Field K
inst✝⁷ : Field L
W' : Affine R
inst✝⁶ : Algebra R F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : Algebra F K
inst✝² : IsScalarTower R F K
inst✝¹ : Algebra F L
inst✝ : IsScalarTower R F L
f : K →ₐ[F] L
P : W'⟮F⟯
this : Subsingleton (F →ₐ[F] L)
⊢ (map f) ((baseChange F K) P) = (baseChange F L) P

Tactic:
convert map_map (Algebra.ofId F K) f P

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem Matrix.mulVecLin_one [DecidableEq n] :
    Matrix.mulVecLin (1 : Matrix n n R) = LinearMap.id

Proof state:
case h.h.h
R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i✝ x✝ : n
⊢ (mulVecLin 1 ∘ₗ single R (fun i => R) i✝) 1 x✝ = (LinearMap.id ∘ₗ single R (fun i => R) i✝) 1 x✝

Tactic:
simp [Matrix.one_apply, Pi.single_apply, eq_comm]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ mulVecLin 1 = LinearMap.id

Tactic:
ext

Result:
case h.h.h
R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
i✝ x✝ : n
⊢ (mulVecLin 1 ∘ₗ single R (fun i => R) i✝) 1 x✝ = (LinearMap.id ∘ₗ single R (fun i => R) i✝) 1 x✝
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_functions_apply₂ {f : L.Functions 2} {t₁ t₂ : L.Term α} {v : α → M} :
    (f.apply₂ t₁ t₂).realize v = funMap f ![t₁.realize v, t₂.realize v]

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ realize v (f.apply₂ t₁ t₂) = funMap f ![realize v t₁, realize v t₂]

Tactic:
rw [Functions.apply₂, Term.realize]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ (funMap f fun i => realize v (![t₁, t₂] i)) = funMap f ![realize v t₁, realize v t₂]

Proof state:
case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ ∀ (i : Fin 1), realize v (![t₁, t₂] i.succ) = ![realize v t₁, realize v t₂] i.succ

Tactic:
simp only [Matrix.cons_val_succ, Matrix.cons_val_fin_one, forall_const]

Result:
no goals

Proof state:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ realize v (![t₁, t₂] 0) = ![realize v t₁, realize v t₂] 0

Tactic:
simp only [Matrix.cons_val_zero]

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ (funMap f fun i => realize v (![t₁, t₂] i)) = funMap f ![realize v t₁, realize v t₂]

Tactic:
refine congr rfl (funext (Fin.cases ?_ ?_))

Result:
case refine_1
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ realize v (![t₁, t₂] 0) = ![realize v t₁, realize v t₂] 0

case refine_2
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
f : L.Functions 2
t₁ t₂ : L.Term α
v : α → M
⊢ ∀ (i : Fin 1), realize v (![t₁, t₂] i.succ) = ![realize v t₁, realize v t₂] i.succ
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
lemma ediam_eq_top_of_not_preconnected (h : ¬G.Preconnected) : G.ediam = ⊤

Proof state:
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
⊢ G.ediam = ⊤

Tactic:
cases isEmpty_or_nonempty α

Result:
case inl
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : IsEmpty α
⊢ G.ediam = ⊤

case inr
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : Nonempty α
⊢ G.ediam = ⊤

Proof state:
case inr
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : Nonempty α
⊢ G.ediam = ⊤

Tactic:
apply ediam_eq_top_of_not_connected

Result:
case inr.h
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : Nonempty α
⊢ ¬G.Connected

Proof state:
case inl
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : IsEmpty α
⊢ False

Tactic:
exact h <| IsEmpty.forall_iff.mpr trivial

Result:
no goals

Proof state:
case inl
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : IsEmpty α
⊢ G.ediam = ⊤

Tactic:
exfalso

Result:
case inl
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : IsEmpty α
⊢ False

Proof state:
case inr.h
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : Nonempty α
⊢ ¬(G.Preconnected ∧ Nonempty α)

Tactic:
tauto

Result:
no goals

Proof state:
case inr.h
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : Nonempty α
⊢ ¬G.Connected

Tactic:
rw [connected_iff]

Result:
case inr.h
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : Nonempty α
⊢ ¬(G.Preconnected ∧ Nonempty α)
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem norm_div_cos_angle_add_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) (h0 : x ≠ 0 ∨ y = 0) :
    ‖x‖ / Real.cos (angle x (x + y)) = ‖x + y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y = 0
⊢ ‖x‖ / Real.cos (angle x (x + y)) = ‖x + y‖

Tactic:
rw [cos_angle_add_of_inner_eq_zero h]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y = 0
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖

Proof state:
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : y = 0
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖

Tactic:
simp [h0]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y = 0
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖

Tactic:
rcases h0 with (h0 | h0)

Result:
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖

case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : y = 0
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖

Proof state:
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖

Tactic:
rw [div_div_eq_mul_div, mul_comm, div_eq_mul_inv, mul_inv_cancel_right₀ (norm_ne_zero_iff.2 h0)]

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem map_comp : map (fun (i : ι) ↦ g i ∘ₗ f i) = map g ∘ₗ map f

Proof state:
case H.H
ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
g : (i : ι) → t i →ₗ[R] t' i
f : (i : ι) → s i →ₗ[R] t i
x✝ : (i : ι) → s i
⊢ ((map fun i => g i ∘ₗ f i).compMultilinearMap (tprod R)) x✝ = ((map g ∘ₗ map f).compMultilinearMap (tprod R)) x✝

Tactic:
simp only [LinearMap.compMultilinearMap_apply, map_tprod, LinearMap.coe_comp, Function.comp_apply]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
g : (i : ι) → t i →ₗ[R] t' i
f : (i : ι) → s i →ₗ[R] t i
⊢ (map fun i => g i ∘ₗ f i) = map g ∘ₗ map f

Tactic:
ext

Result:
case H.H
ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
g : (i : ι) → t i →ₗ[R] t' i
f : (i : ι) → s i →ₗ[R] t i
x✝ : (i : ι) → s i
⊢ ((map fun i => g i ∘ₗ f i).compMultilinearMap (tprod R)) x✝ = ((map g ∘ₗ map f).compMultilinearMap (tprod R)) x✝
-- Mathlib/Topology/Semicontinuous.lean
theorem IsClosed.lowerSemicontinuous_indicator (hs : IsClosed s) (hy : y ≤ 0) :
    LowerSemicontinuous (indicator s fun _x => y)

Proof state:
case pos
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
x' : α
⊢ z < s.indicator (fun _x => y) x'

Tactic:
by_cases h' : x' ∈ s <;> simp [h', hz, hz.trans_le hy]

Result:
no goals

Proof state:
case h
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
h : x ∉ s
hz : z < 0
⊢ ∀ a ∈ sᶜ, z < s.indicator (fun _x => y) a

Tactic:
simp +contextual [hz]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
⊢ LowerSemicontinuous (s.indicator fun _x => y)

Tactic:
intro x z hz

Result:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
hz : z < s.indicator (fun _x => y) x
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < s.indicator (fun _x => y) x'

Proof state:
case neg
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
h : x ∉ s
hz : z < 0
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < s.indicator (fun _x => y) x'

Tactic:
filter_upwards [hs.isOpen_compl.mem_nhds h]

Result:
case h
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
h : x ∉ s
hz : z < 0
⊢ ∀ a ∈ sᶜ, z < s.indicator (fun _x => y) a

Proof state:
case pos
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < s.indicator (fun _x => y) x'

Tactic:
refine Filter.Eventually.of_forall fun x' => ?_

Result:
case pos
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
x' : α
⊢ z < s.indicator (fun _x => y) x'

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
hz : z < s.indicator (fun _x => y) x
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < s.indicator (fun _x => y) x'

Tactic:
by_cases h : x ∈ s <;> simp [h] at hz

Result:
case pos
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
h : x ∈ s
hz : z < y
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < s.indicator (fun _x => y) x'

case neg
α : Type u_1
inst✝² : TopologicalSpace α
β : Type u_2
inst✝¹ : Preorder β
s : Set α
y : β
inst✝ : Zero β
hs : IsClosed s
hy : y ≤ 0
x : α
z : β
h : x ∉ s
hz : z < 0
⊢ ∀ᶠ (x' : α) in 𝓝 x, z < s.indicator (fun _x => y) x'
-- Mathlib/Analysis/Calculus/LHopital.lean
theorem lhopital_zero_nhds' (hdf : ∀ᶠ x in 𝓝[≠] a, DifferentiableAt ℝ f x)
    (hg' : ∀ᶠ x in 𝓝[≠] a, deriv g x ≠ 0) (hfa : Tendsto f (𝓝[≠] a) (𝓝 0))
    (hga : Tendsto g (𝓝[≠] a) (𝓝 0))
    (hdiv : Tendsto (fun x => (deriv f) x / (deriv g) x) (𝓝[≠] a) l) :
    Tendsto (fun x => f x / g x) (𝓝[≠] a) l

Proof state:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : ∀ᶠ (x : ℝ) in 𝓝[≠] a, DifferentiableAt ℝ f x
hg' : ∀ᶠ (x : ℝ) in 𝓝[≠] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[≠] a) (𝓝 0)
hga : Tendsto g (𝓝[≠] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[≠] a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[≠] a) l

Tactic:
simp only [← Iio_union_Ioi, nhdsWithin_union, tendsto_sup, eventually_sup] at *

Result:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : (∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ f x) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, DifferentiableAt ℝ f x
hg' : (∀ᶠ (x : ℝ) in 𝓝[<] a, deriv g x ≠ 0) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0) ∧ Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0) ∧ Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] a) l ∧ Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[<] a) l ∧ Tendsto (fun x => f x / g x) (𝓝[>] a) l

Proof state:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : (∀ᶠ (x : ℝ) in 𝓝[<] a, DifferentiableAt ℝ f x) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, DifferentiableAt ℝ f x
hg' : (∀ᶠ (x : ℝ) in 𝓝[<] a, deriv g x ≠ 0) ∧ ∀ᶠ (x : ℝ) in 𝓝[>] a, deriv g x ≠ 0
hfa : Tendsto f (𝓝[<] a) (𝓝 0) ∧ Tendsto f (𝓝[>] a) (𝓝 0)
hga : Tendsto g (𝓝[<] a) (𝓝 0) ∧ Tendsto g (𝓝[>] a) (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) (𝓝[<] a) l ∧ Tendsto (fun x => deriv f x / deriv g x) (𝓝[>] a) l
⊢ Tendsto (fun x => f x / g x) (𝓝[<] a) l ∧ Tendsto (fun x => f x / g x) (𝓝[>] a) l

Tactic:
exact ⟨lhopital_zero_nhds_left hdf.1 hg'.1 hfa.1 hga.1 hdiv.1,
  lhopital_zero_nhds_right hdf.2 hg'.2 hfa.2 hga.2 hdiv.2⟩

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_add_right (a b : α) : toIcoMod hp a (b + p) = toIcoMod hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a (b + p) = toIcoMod hp a b

Tactic:
simpa only [one_zsmul] using toIcoMod_add_zsmul hp a b 1

Result:
no goals