harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem continuous_integral_integral :
    Continuous fun f : α × β →₁[μ.prod ν] E => ∫ x, ∫ y, f (x, y) ∂ν ∂μ

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ ↥(Lp E 1 (μ.prod ν)) → ℝ≥0∞

Tactic:
exact fun i => ∫⁻ x, ∫⁻ y, ‖i (x, y) - g (x, y)‖ₑ ∂ν ∂μ

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ Tendsto (fun i => ∫⁻ (x : α), ∫⁻ (y : β), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂ν ∂μ) (𝓝 g) (𝓝 0)

Tactic:
have this (i : α × β →₁[μ.prod ν] E) : Measurable fun z => ‖i z - g z‖ₑ :=
  ((Lp.stronglyMeasurable i).sub (Lp.stronglyMeasurable g)).enorm

Result:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
this : ∀ (i : ↥(Lp E 1 (μ.prod ν))), Measurable fun z => ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i => ∫⁻ (x : α), ∫⁻ (y : β), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂ν ∂μ) (𝓝 g) (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
this : ∀ (i : ↥(Lp E 1 (μ.prod ν))), Measurable fun z => ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i => ‖i - g‖) (𝓝 g) (𝓝 0)

Tactic:
rw [← tendsto_iff_norm_sub_tendsto_zero]

Result:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
this : ∀ (i : ↥(Lp E 1 (μ.prod ν))), Measurable fun z => ‖↑↑i z - ↑↑g z‖ₑ
⊢ Tendsto (fun i => i) (𝓝 g) (𝓝 g)

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ Tendsto (fun i => ∫⁻ (x : α), ‖∫ (y : β), ↑↑i (x, y) ∂ν - ∫ (y : β), ↑↑g (x, y) ∂ν‖ₑ ∂μ) (𝓝 g) (𝓝 0)

Tactic:
simp_rw [← lintegral_fn_integral_sub _ (L1.integrable_coeFn _) (L1.integrable_coeFn g)]

Result:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝³ : NormedAddCommGroup E
inst✝² : SFinite ν
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : ↥(Lp E 1 (μ.prod ν))
⊢ Tendsto (fun i => ∫⁻ (x : α), ‖∫ (y : β), ↑↑i (x, y) - ↑↑g (x, y) ∂ν‖ₑ ∂μ) (𝓝 g) (𝓝 0)
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem eq_of_prod_eq_prod [Nontrivial α] {a b : FactorSet α} (h : a.prod = b.prod) : a = b

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a b : FactorSet α
h : a.prod = b.prod
this : a.prod.factors = b.prod.factors
⊢ a = b

Tactic:
rwa [prod_factors, prod_factors] at this

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a b : FactorSet α
h : a.prod = b.prod
⊢ a = b

Tactic:
have : a.prod.factors = b.prod.factors := by rw [h]

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a b : FactorSet α
h : a.prod = b.prod
this : a.prod.factors = b.prod.factors
⊢ a = b

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a b : FactorSet α
h : a.prod = b.prod
⊢ a.prod.factors = b.prod.factors

Tactic:
rw [h]

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem id_mem_of_nonempty_isotropy (c : C) : c ∈ objs S → 𝟙 c ∈ S.arrows c c

Proof state:
case h.e'_5
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c : C
γ : c ⟶ c
hγ : γ ∈ S.arrows c c
⊢ 𝟙 c = γ ≫ Groupoid.inv γ

Tactic:
simp only [inv_eq_inv, IsIso.hom_inv_id]

Result:
no goals

Proof state:
case intro
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c : C
γ : c ⟶ c
hγ : γ ∈ S.arrows c c
⊢ 𝟙 c ∈ S.arrows c c

Tactic:
convert S.mul hγ (S.inv hγ)

Result:
case h.e'_5
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c : C
γ : c ⟶ c
hγ : γ ∈ S.arrows c c
⊢ 𝟙 c = γ ≫ Groupoid.inv γ

Proof state:
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c : C
⊢ c ∈ S.objs → 𝟙 c ∈ S.arrows c c

Tactic:
rintro ⟨γ, hγ⟩

Result:
case intro
C : Type u
inst✝ : Groupoid C
S : Subgroupoid C
c : C
γ : c ⟶ c
hγ : γ ∈ S.arrows c c
⊢ 𝟙 c ∈ S.arrows c c
-- Mathlib/Analysis/Analytic/CPolynomial.lean
theorem HasFiniteFPowerSeriesAt.add (hf : HasFiniteFPowerSeriesAt f pf x n)
    (hg : HasFiniteFPowerSeriesAt g pg x m) :
    HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (max n m)

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
n m : ℕ
hf : HasFiniteFPowerSeriesAt f pf x n
hg : HasFiniteFPowerSeriesAt g pg x m
r : ℝ≥0∞
hr : HasFiniteFPowerSeriesOnBall f pf x n r ∧ HasFiniteFPowerSeriesOnBall g pg x m r
⊢ HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (n ⊔ m)

Tactic:
exact ⟨r, hr.1.add hr.2⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
n m : ℕ
hf : HasFiniteFPowerSeriesAt f pf x n
hg : HasFiniteFPowerSeriesAt g pg x m
⊢ HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (n ⊔ m)

Tactic:
rcases (hf.eventually.and hg.eventually).exists with ⟨r, hr⟩

Result:
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
n m : ℕ
hf : HasFiniteFPowerSeriesAt f pf x n
hg : HasFiniteFPowerSeriesAt g pg x m
r : ℝ≥0∞
hr : HasFiniteFPowerSeriesOnBall f pf x n r ∧ HasFiniteFPowerSeriesOnBall g pg x m r
⊢ HasFiniteFPowerSeriesAt (f + g) (pf + pg) x (n ⊔ m)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem surjOn_tan : SurjOn tan (Ioo (-(π / 2)) (π / 2)) univ :=
  have := neg_lt_self pi_div_two_pos
  continuousOn_tan_Ioo.surjOn_of_tendsto (nonempty_Ioo.2 this)
    (by rw [tendsto_comp_coe_Ioo_atBot this]; exact tendsto_tan_neg_pi_div_two)
    (by rw [tendsto_comp_coe_Ioo_atTop this]; exact tendsto_tan_pi_div_two)

Proof state:
this : -(π / 2) < π / 2
⊢ Tendsto (fun x => tan ↑x) atBot atBot

Tactic:
rw [tendsto_comp_coe_Ioo_atBot this]

Result:
this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[>] (-(π / 2))) atBot

Proof state:
this : -(π / 2) < π / 2
⊢ Tendsto (fun x => tan ↑x) atTop atTop

Tactic:
rw [tendsto_comp_coe_Ioo_atTop this]

Result:
this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[<] (π / 2)) atTop

Proof state:
this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[>] (-(π / 2))) atBot

Tactic:
exact tendsto_tan_neg_pi_div_two

Result:
no goals

Proof state:
this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[<] (π / 2)) atTop

Tactic:
exact tendsto_tan_pi_div_two

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem blimsup_mono (h : ∀ x, p x → q x) : blimsup u f p ≤ blimsup u f q :=
  sInf_le_sInf fun a ha => ha.mono <| by tauto

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ (x : β), p x → q x
a : α
ha : a ∈ {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
⊢ ∀ (x : β), (q x → u x ≤ a) → p x → u x ≤ a

Tactic:
tauto

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma HasUnifEigenvalue.mem_spectrum {f : End R M} {μ : R} (hμ : HasUnifEigenvalue f μ 1) :
    μ ∈ spectrum R f

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
hμ : f.HasUnifEigenvalue μ 1
h_unit : IsUnit ((algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
⊢ False

Tactic:
rcases hμ.exists_hasUnifEigenvector with ⟨v, hv⟩

Result:
case intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
hμ : f.HasUnifEigenvalue μ 1
h_unit : IsUnit ((algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
v : M
hv : f.HasUnifEigenvector μ 1 v
⊢ False

Proof state:
case intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
hμ : f.HasUnifEigenvalue μ 1
h_unit : IsUnit ((algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
v : M
hv : f.HasUnifEigenvector μ 1 v
⊢ μ • v - f v = 0

Tactic:
rw [hv.apply_eq_smul, sub_self]

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
hμ : f.HasUnifEigenvalue μ 1
⊢ μ ∈ spectrum R f

Tactic:
refine spectrum.mem_iff.mpr fun h_unit ↦ ?_

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
hμ : f.HasUnifEigenvalue μ 1
h_unit : IsUnit ((algebraMap R (End R M)) μ - f)
⊢ False

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
hμ : f.HasUnifEigenvalue μ 1
h_unit : IsUnit ((algebraMap R (End R M)) μ - f)
⊢ False

Tactic:
set f' := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
hμ : f.HasUnifEigenvalue μ 1
h_unit : IsUnit ((algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
⊢ False

Proof state:
case intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
hμ : f.HasUnifEigenvalue μ 1
h_unit : IsUnit ((algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
v : M
hv : f.HasUnifEigenvector μ 1 v
⊢ False

Tactic:
refine hv.2 ((LinearMap.ker_eq_bot'.mp f'.ker) v (?_ : μ • v - f v = 0))

Result:
case intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
hμ : f.HasUnifEigenvalue μ 1
h_unit : IsUnit ((algebraMap R (End R M)) μ - f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
v : M
hv : f.HasUnifEigenvector μ 1 v
⊢ μ • v - f v = 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
theorem mkXorCached_le_size (aig : AIG α) {input : BinaryInput aig} :
    aig.decls.size ≤ (aig.mkXorCached input).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ (aig.mkXorCached input).aig.decls.size

Tactic:
simp only [mkXorCached]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤
    (((aig.mkGateCached (input.asGateInput false false)).aig.mkGateCached
                  ((input.asGateInput true true).cast ⋯)).aig.mkGateCached
            { lhs := { ref := (aig.mkGateCached (input.asGateInput false false)).ref.cast ⋯, inv := true },
              rhs :=
                {
                  ref :=
                    ((aig.mkGateCached (input.asGateInput false false)).aig.mkGateCached
                        ((input.asGateInput true true).cast ⋯)).ref,
                  inv := true } }).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤
    (((aig.mkGateCached (input.asGateInput false false)).aig.mkGateCached
                  ((input.asGateInput true true).cast ⋯)).aig.mkGateCached
            { lhs := { ref := (aig.mkGateCached (input.asGateInput false false)).ref.cast ⋯, inv := true },
              rhs :=
                {
                  ref :=
                    ((aig.mkGateCached (input.asGateInput false false)).aig.mkGateCached
                        ((input.asGateInput true true).cast ⋯)).ref,
                  inv := true } }).aig.decls.size

Tactic:
apply LawfulOperator.le_size_of_le_aig_size

Result:
case h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤
    ((aig.mkGateCached (input.asGateInput false false)).aig.mkGateCached
            ((input.asGateInput true true).cast ⋯)).aig.decls.size

Proof state:
case h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤
    ((aig.mkGateCached (input.asGateInput false false)).aig.mkGateCached
            ((input.asGateInput true true).cast ⋯)).aig.decls.size

Tactic:
apply LawfulOperator.le_size_of_le_aig_size

Result:
case h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ (aig.mkGateCached (input.asGateInput false false)).aig.decls.size

Proof state:
case h.h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ aig.decls.size

Tactic:
omega

Result:
no goals

Proof state:
case h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ (aig.mkGateCached (input.asGateInput false false)).aig.decls.size

Tactic:
apply LawfulOperator.le_size_of_le_aig_size

Result:
case h.h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ aig.decls.size
-- Mathlib/CategoryTheory/Monad/Basic.lean
lemma isSplitEpi_iff_isIso_counit (T : Comonad C) (X : C) [IsIso T.δ] :
    IsSplitEpi (T.ε.app X) ↔ IsIso (T.ε.app X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Comonad C
X : C
inst✝ : IsIso T.δ
x✝ : IsSplitEpi (T.ε.app X)
⊢ section_ (T.ε.app X) ≫ T.ε.app X = 𝟙 ((𝟭 C).obj X)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Comonad C
X : C
inst✝ : IsIso T.δ
x✝ : IsSplitEpi (T.ε.app X)
⊢ T.ε.app X ≫ section_ (T.ε.app X) = 𝟙 (T.obj X)

Tactic:
erw [← map_id, ← IsSplitEpi.id (T.ε.app X), map_comp, T.map_counit_app X, T.ε.naturality]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Comonad C
X : C
inst✝ : IsIso T.δ
x✝ : IsSplitEpi (T.ε.app X)
⊢ T.ε.app X ≫ section_ (T.ε.app X) = T.ε.app X ≫ (𝟭 C).map (section_ (T.ε.app X))

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Comonad C
X : C
inst✝ : IsIso T.δ
⊢ IsSplitEpi (T.ε.app X) ↔ IsIso (T.ε.app X)

Tactic:
refine ⟨fun _ ↦ ⟨section_ (T.ε.app X), ?_, by simp⟩, fun _ ↦ inferInstance⟩

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Comonad C
X : C
inst✝ : IsIso T.δ
x✝ : IsSplitEpi (T.ε.app X)
⊢ T.ε.app X ≫ section_ (T.ε.app X) = 𝟙 (T.obj X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Comonad C
X : C
inst✝ : IsIso T.δ
x✝ : IsSplitEpi (T.ε.app X)
⊢ T.ε.app X ≫ section_ (T.ε.app X) = T.ε.app X ≫ (𝟭 C).map (section_ (T.ε.app X))

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem cos_oangle_add_left_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    Real.Angle.cos (o.oangle (x + y) y) = ‖y‖ / ‖x + y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (x + y)).cos = ‖y‖ / ‖x + y‖

Tactic:
rw [add_comm]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (y + x)).cos = ‖y‖ / ‖y + x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (y + x)).cos = ‖y‖ / ‖y + x‖

Tactic:
exact (-o).cos_oangle_add_right_of_oangle_eq_pi_div_two h

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x + y) y).cos = ‖y‖ / ‖x + y‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ((-o).oangle y (x + y)).cos = ‖y‖ / ‖x + y‖
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem not_mem_compl : a ∉ sᶜ ↔ a ∈ s

Proof state:
α : Type u_1
s : Finset α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ a ∉ sᶜ ↔ a ∈ s

Tactic:
rw [mem_compl, not_not]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma toAffineLift_add (P Q : W.Point) :
    (P + Q).toAffineLift = P.toAffineLift + Q.toAffineLift

Proof state:
case mk.mk.mk.mk
F : Type u
inst✝ : Field F
W : Projective F
point✝¹ : PointClass F
a✝¹ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹)
point✝ : PointClass F
a✝ : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ (mk hP + mk hQ).toAffineLift = (mk hP).toAffineLift + (mk hQ).toAffineLift

Tactic:
exact toAffine_add hP hQ

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : W.Point
⊢ (P + Q).toAffineLift = P.toAffineLift + Q.toAffineLift

Tactic:
rcases P, Q with ⟨@⟨⟨_⟩, hP⟩, @⟨⟨_⟩, hQ⟩⟩

Result:
case mk.mk.mk.mk
F : Type u
inst✝ : Field F
W : Projective F
point✝¹ : PointClass F
a✝¹ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝¹)
point✝ : PointClass F
a✝ : Fin 3 → F
hQ : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ (mk hP + mk hQ).toAffineLift = (mk hP).toAffineLift + (mk hQ).toAffineLift
-- Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
lemma toPerfectPairing_apply_apply_Polarization (x y : M) :
    P.toPerfectPairing y (P.Polarization x) = P.RootForm x y

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
x y : M
⊢ (P.toPerfectPairing y) (P.Polarization x) = (P.RootForm x) y

Tactic:
simp [RootForm]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Maps.lean
theorem comap_map_eq (f : V ↪ W) (G : SimpleGraph V) : (G.map f).comap f = G

Proof state:
case Adj.h.h.a
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝¹ x✝ : V
⊢ (SimpleGraph.comap (⇑f) (SimpleGraph.map f G)).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝

Tactic:
simp

Result:
no goals

Proof state:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
⊢ SimpleGraph.comap (⇑f) (SimpleGraph.map f G) = G

Tactic:
ext

Result:
case Adj.h.h.a
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
x✝¹ x✝ : V
⊢ (SimpleGraph.comap (⇑f) (SimpleGraph.map f G)).Adj x✝¹ x✝ ↔ G.Adj x✝¹ x✝
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem tendsto_inv_nhdsGT {a : H} : Tendsto Inv.inv (𝓝[>] a) (𝓝[<] a⁻¹) :=
  (continuous_inv.tendsto a).inf <| by simp [tendsto_principal_principal]

Proof state:
H : Type x
inst✝² : TopologicalSpace H
inst✝¹ : OrderedCommGroup H
inst✝ : ContinuousInv H
a : H
⊢ Tendsto (fun a => a⁻¹) (𝓟 (Ioi a)) (𝓟 (Iio a⁻¹))

Tactic:
simp [tendsto_principal_principal]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.sub_int_mul_eq [Ring α] [Ring β] (h : Antiperiodic f c) (n : ℤ) :
    f (x - n * c) = (n.negOnePow : ℤ) * f x

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : Ring α
inst✝ : Ring β
h : Antiperiodic f c
n : ℤ
⊢ f (x - ↑n * c) = ↑↑n.negOnePow * f x

Tactic:
simpa only [zsmul_eq_mul] using h.sub_zsmul_eq n

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
lemma map_le_iff (P : MorphismProperty C) {F : C ⥤ D} (Q : MorphismProperty D)
    [RespectsIso Q] :
    P.map F ≤ Q ↔ P ≤ Q.inverseImage F

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
P : MorphismProperty C
F : C ⥤ D
Q : MorphismProperty D
inst✝ : Q.RespectsIso
h : P ≤ Q.inverseImage F
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk (F.map f') ≅ Arrow.mk f
⊢ Q f

Tactic:
exact (Q.arrow_mk_iso_iff e).1 (h _ hf')

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
P : MorphismProperty C
F : C ⥤ D
Q : MorphismProperty D
inst✝ : Q.RespectsIso
⊢ P.map F ≤ Q ↔ P ≤ Q.inverseImage F

Tactic:
constructor

Result:
case mp
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
P : MorphismProperty C
F : C ⥤ D
Q : MorphismProperty D
inst✝ : Q.RespectsIso
⊢ P.map F ≤ Q → P ≤ Q.inverseImage F

case mpr
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
P : MorphismProperty C
F : C ⥤ D
Q : MorphismProperty D
inst✝ : Q.RespectsIso
⊢ P ≤ Q.inverseImage F → P.map F ≤ Q

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
P : MorphismProperty C
F : C ⥤ D
Q : MorphismProperty D
inst✝ : Q.RespectsIso
⊢ P ≤ Q.inverseImage F → P.map F ≤ Q

Tactic:
intro h X Y f ⟨X', Y', f', hf', ⟨e⟩⟩

Result:
case mpr
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
P : MorphismProperty C
F : C ⥤ D
Q : MorphismProperty D
inst✝ : Q.RespectsIso
h : P ≤ Q.inverseImage F
X Y : D
f : X ⟶ Y
X' Y' : C
f' : X' ⟶ Y'
hf' : P f'
e : Arrow.mk (F.map f') ≅ Arrow.mk f
⊢ Q f

Proof state:
case mp
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
P : MorphismProperty C
F : C ⥤ D
Q : MorphismProperty D
inst✝ : Q.RespectsIso
⊢ P.map F ≤ Q → P ≤ Q.inverseImage F

Tactic:
intro h X Y f hf

Result:
case mp
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
P : MorphismProperty C
F : C ⥤ D
Q : MorphismProperty D
inst✝ : Q.RespectsIso
h : P.map F ≤ Q
X Y : C
f : X ⟶ Y
hf : P f
⊢ Q.inverseImage F f

Proof state:
case mp
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{u_2, u_1} D
P : MorphismProperty C
F : C ⥤ D
Q : MorphismProperty D
inst✝ : Q.RespectsIso
h : P.map F ≤ Q
X Y : C
f : X ⟶ Y
hf : P f
⊢ Q.inverseImage F f

Tactic:
exact h (F.map f) (map_mem_map P F f hf)

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Chain.lean
@[simp] lemma chainBot_neg : chainBot (-α) β = chainTop α β

Proof state:
case h
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
x✝ : L
⊢ (chainBot (-α) β) x✝ = (chainTop α β) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
⊢ chainBot (-α) β = chainTop α β

Tactic:
ext

Result:
case h
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
x✝ : L
⊢ (chainBot (-α) β) x✝ = (chainTop α β) x✝