harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem inl_of_isLimit {X Y : C} {t : BinaryBicone X Y} (ht : IsLimit t.toCone) :
    t.inl = ht.lift (BinaryFan.mk (𝟙 X) 0)

Proof state:
case x
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ ∀ (j : Discrete WalkingPair), t.inl ≫ t.toCone.π.app j = (BinaryFan.mk (𝟙 X) 0).π.app j

Tactic:
rintro ⟨⟨⟩⟩ <;> dsimp <;> simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ t.inl = ht.lift (BinaryFan.mk (𝟙 X) 0)

Tactic:
apply ht.uniq (BinaryFan.mk (𝟙 X) 0)

Result:
case x
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
t : BinaryBicone X Y
ht : IsLimit t.toCone
⊢ ∀ (j : Discrete WalkingPair), t.inl ≫ t.toCone.π.app j = (BinaryFan.mk (𝟙 X) 0).π.app j
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem sin_oangle_sub_right_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    Real.Angle.sin (o.oangle y (y - x)) = ‖x‖ / ‖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 x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ (o.oangle y (y - x)).sin = ‖x‖ / ‖y - x‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.sin_coe,
  InnerProductGeometry.sin_angle_sub_of_inner_eq_zero
    (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inl (o.right_ne_zero_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 y (y - x)).sign = 1

Tactic:
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

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 y (y - x)).sin = ‖x‖ / ‖y - x‖

Tactic:
have hs : (o.oangle y (y - x)).sign = 1 := by
  rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

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 x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ (o.oangle y (y - x)).sin = ‖x‖ / ‖y - x‖
-- Mathlib/Data/Matrix/Block.lean
theorem ext_iff_blocks {A B : Matrix (n ⊕ o) (l ⊕ m) α} :
    A = B ↔
      A.toBlocks₁₁ = B.toBlocks₁₁ ∧
        A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂ :=
  ⟨fun h => h ▸ ⟨rfl, rfl, rfl, rfl⟩, fun ⟨h₁₁, h₁₂, h₂₁, h₂₂⟩ => by
    rw [← fromBlocks_toBlocks A, ← fromBlocks_toBlocks B, h₁₁, h₁₂, h₂₁, h₂₂]⟩

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A B : Matrix (n ⊕ o) (l ⊕ m) α
x✝ :
  A.toBlocks₁₁ = B.toBlocks₁₁ ∧ A.toBlocks₁₂ = B.toBlocks₁₂ ∧ A.toBlocks₂₁ = B.toBlocks₂₁ ∧ A.toBlocks₂₂ = B.toBlocks₂₂
h₁₁ : A.toBlocks₁₁ = B.toBlocks₁₁
h₁₂ : A.toBlocks₁₂ = B.toBlocks₁₂
h₂₁ : A.toBlocks₂₁ = B.toBlocks₂₁
h₂₂ : A.toBlocks₂₂ = B.toBlocks₂₂
⊢ A = B

Tactic:
rw [← fromBlocks_toBlocks A, ← fromBlocks_toBlocks B, h₁₁, h₁₂, h₂₁, h₂₂]

Result:
no goals
-- Mathlib/NumberTheory/Modular.lean
theorem normSq_S_smul_lt_one (h : 1 < normSq z) : normSq ↑(S • z) < 1

Proof state:
z : ℍ
h : 1 < normSq ↑z
⊢ normSq ↑(S • z) < 1

Tactic:
simpa [coe_S, num, denom] using (inv_lt_inv₀ z.normSq_pos zero_lt_one).mpr h

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup_eq_bot_of_isEmpty [IsEmpty β] (f : β → α) (S : Finset β) : S.sup f = ⊥

Proof state:
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : IsEmpty β
f : β → α
S : Finset β
⊢ S.sup f = ⊥

Tactic:
rw [Finset.sup_eq_bot_iff]

Result:
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : IsEmpty β
f : β → α
S : Finset β
⊢ ∀ s ∈ S, f s = ⊥

Proof state:
α : Type u_2
β : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : IsEmpty β
f : β → α
S : Finset β
⊢ ∀ s ∈ S, f s = ⊥

Tactic:
exact fun x _ => False.elim <| IsEmpty.false x

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem finite_setOf_absNorm_eq [CharZero S] (n : ℕ) :
    {I : Ideal S | Ideal.absNorm I = n}.Finite

Proof state:
case inr
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
⊢ {I | absNorm I = n}.Finite

Tactic:
let f := fun I : Ideal S => Ideal.map (Ideal.Quotient.mk (@Ideal.span S _ {↑n})) I

Result:
case inr
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
⊢ {I | absNorm I = n}.Finite

Proof state:
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
this : Finite (S ⧸ span {↑n})
g : Ideal (S ⧸ span {↑n}) → Set (S ⧸ span {↑n}) := SetLike.coe
⊢ (g '' (f '' {I | absNorm I = n})).Finite

Tactic:
exact Set.Finite.subset Set.finite_univ (Set.subset_univ _)

Result:
no goals

Proof state:
case inr.refine_2
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Nontrivial S
inst✝³ : IsDedekindDomain S
inst✝² : Module.Free ℤ S
inst✝¹ : Module.Finite ℤ S
inst✝ : CharZero S
n : ℕ
hn : n > 0
f : Ideal S → Ideal (S ⧸ span {↑n}) := fun I => map (Quotient.mk (span {↑n})) I
I : Ideal S
hI : I ∈ {I | absNorm I = n}
J : Ideal S
hJ : J ∈ {I | absNorm I = n}
h : f I = f J
⊢ comap (Quotient.mk (span {↑n})) (map (Quotient.mk (span {↑n})) I) =
    comap (Quotient.mk (span {↑n})) (map (Quotient.mk (span {↑n})) J)

Tactic:
congr

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem getElem_mapIdx {l : List α} {f : Nat → α → β} {i : Nat} {h : i < (l.mapIdx f).length} :
    (l.mapIdx f)[i] = f i (l[i]'(by simpa using h))

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : i < (mapIdx f l).length
⊢ some (mapIdx f l)[i] = some (f i l[i])

Tactic:
rw [← getElem?_eq_getElem, getElem?_mapIdx, getElem?_eq_getElem (by simpa using h)]

Result:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : i < (mapIdx f l).length
⊢ Option.map (f i) (some l[i]) = some (f i l[i])

Proof state:
α : Type ?u.79582
β : Type ?u.79594
l : List α
f : Nat → α → β
i : Nat
h : i < (mapIdx f l).length
⊢ i < l.length

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : i < (mapIdx f l).length
⊢ Option.map (f i) (some l[i]) = some (f i l[i])

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : i < (mapIdx f l).length
⊢ (mapIdx f l)[i] = f i l[i]

Tactic:
apply Option.some_inj.mp

Result:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : i < (mapIdx f l).length
⊢ some (mapIdx f l)[i] = some (f i l[i])

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
i : Nat
h : i < (mapIdx f l).length
⊢ i < l.length

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem map_fst_nhdsWithin (x : X × Y) : map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x) = 𝓝 x.1

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X × Y
s : Set X
hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x)
⊢ s ∈ 𝓝 x.1

Tactic:
rcases x with ⟨x, y⟩

Result:
case mk
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
x : X
y : Y
hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {(x, y).2}] (x, y))
⊢ s ∈ 𝓝 (x, y).1

Proof state:
case mk
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
x : X
y : Y
hs : ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ {x_1 | x_1 ∈ Prod.snd ⁻¹' {(x, y).2} → x_1 ∈ Prod.fst ⁻¹' s}
⊢ s ∈ 𝓝 (x, y).1

Tactic:
rcases hs with ⟨u, hu, v, hv, H⟩

Result:
case mk.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
x : X
y : Y
u : Set X
hu : u ∈ 𝓝 x
v : Set Y
hv : v ∈ 𝓝 y
H : u ×ˢ v ⊆ {x_1 | x_1 ∈ Prod.snd ⁻¹' {(x, y).2} → x_1 ∈ Prod.fst ⁻¹' s}
⊢ s ∈ 𝓝 (x, y).1

Proof state:
case mk
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
x : X
y : Y
hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {(x, y).2}] (x, y))
⊢ s ∈ 𝓝 (x, y).1

Tactic:
rw [mem_map, nhdsWithin, mem_inf_principal, mem_nhds_prod_iff] at hs

Result:
case mk
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
x : X
y : Y
hs : ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ {x_1 | x_1 ∈ Prod.snd ⁻¹' {(x, y).2} → x_1 ∈ Prod.fst ⁻¹' s}
⊢ s ∈ 𝓝 (x, y).1

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X × Y
⊢ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x) = 𝓝 x.1

Tactic:
refine le_antisymm (continuousAt_fst.mono_left inf_le_left) fun s hs => ?_

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X × Y
s : Set X
hs : s ∈ map Prod.fst (𝓝[Prod.snd ⁻¹' {x.2}] x)
⊢ s ∈ 𝓝 x.1

Proof state:
case mk.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
x : X
y : Y
u : Set X
hu : u ∈ 𝓝 x
v : Set Y
hv : v ∈ 𝓝 y
H : ∀ x ∈ u, ∀ y_1 ∈ v, y_1 = y → x ∈ s
⊢ s ∈ 𝓝 (x, y).1

Tactic:
exact mem_of_superset hu fun z hz => H _ hz _ (mem_of_mem_nhds hv) rfl

Result:
no goals

Proof state:
case mk.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
x : X
y : Y
u : Set X
hu : u ∈ 𝓝 x
v : Set Y
hv : v ∈ 𝓝 y
H : u ×ˢ v ⊆ {x_1 | x_1 ∈ Prod.snd ⁻¹' {(x, y).2} → x_1 ∈ Prod.fst ⁻¹' s}
⊢ s ∈ 𝓝 (x, y).1

Tactic:
simp only [prod_subset_iff, mem_singleton_iff, mem_setOf_eq, mem_preimage] at H

Result:
case mk.intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
x : X
y : Y
u : Set X
hu : u ∈ 𝓝 x
v : Set Y
hv : v ∈ 𝓝 y
H : ∀ x ∈ u, ∀ y_1 ∈ v, y_1 = y → x ∈ s
⊢ s ∈ 𝓝 (x, y).1
-- Mathlib/Algebra/Order/Archimedean/Basic.lean
theorem existsUnique_zpow_near_of_one_lt {a : α} (ha : 1 < a) (g : α) :
    ∃! k : ℤ, a ^ k ≤ g ∧ g < a ^ (k + 1)

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedCommGroup α
inst✝ : MulArchimedean α
a : α
ha : 1 < a
g : α
⊢ ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)

Tactic:
let s : Set ℤ := { n : ℤ | a ^ n ≤ g }

Result:
α : Type u_1
inst✝¹ : LinearOrderedCommGroup α
inst✝ : MulArchimedean α
a : α
ha : 1 < a
g : α
s : Set ℤ := {n | a ^ n ≤ g}
⊢ ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)

Proof state:
case intro
α : Type u_1
inst✝¹ : LinearOrderedCommGroup α
inst✝ : MulArchimedean α
a : α
ha : 1 < a
g : α
s : Set ℤ := {n | a ^ n ≤ g}
k : ℕ
hk : g⁻¹ ≤ a ^ k
⊢ ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)

Tactic:
have h_ne : s.Nonempty := ⟨-k, by simpa [s] using inv_le_inv' hk⟩

Result:
case intro
α : Type u_1
inst✝¹ : LinearOrderedCommGroup α
inst✝ : MulArchimedean α
a : α
ha : 1 < a
g : α
s : Set ℤ := {n | a ^ n ≤ g}
k : ℕ
hk : g⁻¹ ≤ a ^ k
h_ne : s.Nonempty
⊢ ∃! k, a ^ k ≤ g ∧ g < a ^ (k + 1)

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : LinearOrderedCommGroup α
inst✝ : MulArchimedean α
a : α
ha : 1 < a
g : α
s : Set ℤ := {n | a ^ n ≤ g}
k✝ : ℕ
hk✝ : g⁻¹ ≤ a ^ k✝
h_ne : s.Nonempty
k : ℕ
hk : g ≤ a ^ k
h_bdd : ∀ n ∈ s, n ≤ ↑k
m : ℤ
hm : m ∈ s
hm' : ∀ z ∈ s, z ≤ m
hm'' : g < a ^ (m + 1)
n : ℤ
hn : (fun k => a ^ k ≤ g ∧ g < a ^ (k + 1)) n
⊢ a ^ m < a ^ (n + 1)

Tactic:
exact lt_of_le_of_lt hm hn.2

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
@[deprecated negPart_eq_neg (since := "2024-11-18")]
lemma eq_negPart_iff (a : A) : a = -a⁻ ↔ a ≤ 0

Proof state:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
⊢ a = -a⁻ ↔ a ≤ 0

Tactic:
rw [← neg_inj, neg_neg, eq_comm, negPart_eq_neg]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean
@[reassoc (attr := simp)]
lemma add'_comp (f₁ f₂ : L.obj X ⟶ L.obj Y) (g : L.obj Y ⟶ L.obj Z) :
    add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)

Proof state:
case intro.intro.intro.intro.hφ₂
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.f ≫ γ.s = α.s ≫ γ.f
⊢ f₂ ≫ g = (LeftFraction₂.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.s ≫ γ.s) ⋯).snd.map L ⋯

Tactic:
rw [h₂, hβ]

Result:
case intro.intro.intro.intro.hφ₂
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.f ≫ γ.s = α.s ≫ γ.f
⊢ α.snd.map L ⋯ ≫ β.map L ⋯ = (LeftFraction₂.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.s ≫ γ.s) ⋯).snd.map L ⋯

Proof state:
case intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map L ⋯
⊢ add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)

Tactic:
obtain ⟨γ, hγ⟩ := (RightFraction.mk _ α.hs β.f).exists_leftFraction

Result:
case intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : (RightFraction.mk α.s ⋯ β.f).f ≫ γ.s = (RightFraction.mk α.s ⋯ β.f).s ≫ γ.f
⊢ add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)

Proof state:
case intro.intro.intro.intro.hφ₂
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.f ≫ γ.s = α.s ≫ γ.f
⊢ α.snd.map L ⋯ ≫ β.map L ⋯ = (LeftFraction₂.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.s ≫ γ.s) ⋯).snd.map L ⋯

Tactic:
exact LeftFraction.map_comp_map_eq_map _ _ _ hγ _

Result:
no goals
-- Mathlib/Analysis/Calculus/Taylor.lean
theorem taylor_within_zero_eval (f : ℝ → E) (s : Set ℝ) (x₀ x : ℝ) :
    taylorWithinEval f 0 s x₀ x = f x₀

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ (PolynomialModule.eval x)
      (∑ k ∈ Finset.range (0 + 1),
        (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
          ((PolynomialModule.single ℝ k) ((↑k !)⁻¹ • iteratedDerivWithin k f s x₀))) =
    f x₀

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ (PolynomialModule.eval x) (taylorWithin f 0 s x₀) = f x₀

Tactic:
dsimp only [taylorWithin]

Result:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ (PolynomialModule.eval x)
      (∑ k ∈ Finset.range (0 + 1),
        (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
          ((PolynomialModule.single ℝ k) (taylorCoeffWithin f k s x₀))) =
    f x₀

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ (PolynomialModule.eval x)
      (∑ k ∈ Finset.range (0 + 1),
        (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
          ((PolynomialModule.single ℝ k) (taylorCoeffWithin f k s x₀))) =
    f x₀

Tactic:
dsimp only [taylorCoeffWithin]

Result:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ (PolynomialModule.eval x)
      (∑ k ∈ Finset.range (0 + 1),
        (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀))
          ((PolynomialModule.single ℝ k) ((↑k !)⁻¹ • iteratedDerivWithin k f s x₀))) =
    f x₀

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ taylorWithinEval f 0 s x₀ x = f x₀

Tactic:
dsimp only [taylorWithinEval]

Result:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ x : ℝ
⊢ (PolynomialModule.eval x) (taylorWithin f 0 s x₀) = f x₀
-- Mathlib/RingTheory/Trace/Basic.lean
theorem PowerBasis.trace_gen_eq_sum_roots [Nontrivial S] (pb : PowerBasis K S)
    (hf : (minpoly K pb.gen).Splits (algebraMap K F)) :
    algebraMap K F (trace K S pb.gen) = ((minpoly K pb.gen).aroots F).sum

Proof state:
S : Type u_2
inst✝⁵ : CommRing S
K : Type u_4
inst✝⁴ : Field K
F : Type u_6
inst✝³ : Field F
inst✝² : Algebra K S
inst✝¹ : Algebra K F
inst✝ : Nontrivial S
pb : PowerBasis K S
hf : Splits (algebraMap K F) (minpoly K pb.gen)
⊢ (algebraMap K F) ((Algebra.trace K S) pb.gen) = ((minpoly K pb.gen).aroots F).sum

Tactic:
rw [PowerBasis.trace_gen_eq_nextCoeff_minpoly, RingHom.map_neg, ←
  nextCoeff_map (algebraMap K F).injective,
  sum_roots_eq_nextCoeff_of_monic_of_split ((minpoly.monic (PowerBasis.isIntegral_gen _)).map _)
    ((splits_id_iff_splits _).2 hf),
  neg_neg]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_add_right_eq_arcsin_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    o.oangle x (x + y) = Real.arcsin (‖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 x y = ↑(π / 2)
⊢ o.oangle x (x + y) = ↑(Real.arcsin (‖y‖ / ‖x + y‖))

Tactic:
have hs : (o.oangle x (x + y)).sign = 1 := by
  rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

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 x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ o.oangle x (x + y) = ↑(Real.arcsin (‖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 x y = ↑(π / 2)
hs : (o.oangle x (x + y)).sign = 1
⊢ o.oangle x (x + y) = ↑(Real.arcsin (‖y‖ / ‖x + y‖))

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs,
  InnerProductGeometry.angle_add_eq_arcsin_of_inner_eq_zero
    (o.inner_eq_zero_of_oangle_eq_pi_div_two h)
    (Or.inl (o.left_ne_zero_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 (x + y)).sign = 1

Tactic:
rw [oangle_sign_add_right, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem ker_eq_bot_iff_eq_zero : ker f = ⊥ ↔ ∀ x, f x = 0 → x = 0

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
⊢ ker f = ⊥ ↔ ∀ (x : R), f x = 0 → x = 0

Tactic:
rw [← injective_iff_map_eq_zero f, injective_iff_ker_eq_bot]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
@[simp]
lemma map_c₆ : (W.map φ).c₆ = φ W.c₆

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ (W.map φ).c₆ = φ W.c₆

Tactic:
simp only [c₆, map_b₂, map_b₄, map_b₆]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ -φ W.b₂ ^ 3 + 36 * φ W.b₂ * φ W.b₄ - 216 * φ W.b₆ = φ (-W.b₂ ^ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆)

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ -φ W.b₂ ^ 3 + 36 * φ W.b₂ * φ W.b₄ - 216 * φ W.b₆ = φ (-W.b₂ ^ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆)

Tactic:
map_simp

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem liftRel_cons (R : α → β → Prop) (a b s t) :
    LiftRel R (cons a s) (cons b t) ↔ R a b ∧ LiftRel R s t

Proof state:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
s : WSeq α
t : WSeq β
⊢ LiftRel R (cons a s) (cons b t) ↔ R a b ∧ LiftRel R s t

Tactic:
rw [liftRel_destruct_iff]

Result:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
s : WSeq α
t : WSeq β
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (cons a s).destruct (cons b t).destruct ↔ R a b ∧ LiftRel R s t

Proof state:
α : Type u
β : Type v
R : α → β → Prop
a : α
b : β
s : WSeq α
t : WSeq β
⊢ Computation.LiftRel (LiftRelO R (LiftRel R)) (cons a s).destruct (cons b t).destruct ↔ R a b ∧ LiftRel R s t

Tactic:
simp [-liftRel_pure_left, -liftRel_pure_right]

Result:
no goals