harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
@[simp]
lemma coeff_preΨ (n : ℤ) : (W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) =
    if Even n then n / 2 else n

Proof state:
case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = ↑(if Even ↑n then ↑n / 2 else ↑n)
n : ℕ
⊢ -(W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = ↑(if Even ↑n then -↑n / 2 else -↑n)

Tactic:
rcases ih n, n.even_or_odd' with ⟨ih, ⟨n, rfl | rfl⟩⟩ <;>
  push_cast [even_two_mul, Int.not_even_two_mul_add_one, Int.neg_ediv_of_dvd ⟨n, rfl⟩] at * <;>
  rw [ih]

Result:
no goals

Proof state:
case nat
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = ↑(if Even ↑n then ↑n / 2 else ↑n)

Tactic:
exact_mod_cast W.preΨ_ofNat n ▸ W.coeff_preΨ' n

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = ↑(if Even ↑n then ↑n / 2 else ↑n)
n : ℕ
⊢ (W.preΨ (-↑n)).coeff (((-↑n).natAbs ^ 2 - if Even (-↑n) then 4 else 1) / 2) = ↑(if Even (-↑n) then -↑n / 2 else -↑n)

Tactic:
simp only [preΨ_neg, coeff_neg, Int.natAbs_neg, even_neg]

Result:
case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), (W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = ↑(if Even ↑n then ↑n / 2 else ↑n)
n : ℕ
⊢ -(W.preΨ ↑n).coeff (((↑n).natAbs ^ 2 - if Even ↑n then 4 else 1) / 2) = ↑(if Even ↑n then -↑n / 2 else -↑n)

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) = ↑(if Even n then n / 2 else n)

Tactic:
induction n using Int.negInduction with
| nat n => exact_mod_cast W.preΨ_ofNat n ▸ W.coeff_preΨ' n
| neg ih n =>
  simp only [preΨ_neg, coeff_neg, Int.natAbs_neg, even_neg]
  rcases ih n, n.even_or_odd' with ⟨ih, ⟨n, rfl | rfl⟩⟩ <;>
    push_cast [even_two_mul, Int.not_even_two_mul_add_one, Int.neg_ediv_of_dvd ⟨n, rfl⟩] at * <;>
    rw [ih]

Result:
no goals
-- Mathlib/Algebra/CharP/Quotient.lean
theorem quotient' {R : Type*} [CommRing R] (p : ℕ) [CharP R p] (I : Ideal R)
    (h : ∀ x : ℕ, (x : R) ∈ I → (x : R) = 0) : CharP (R ⧸ I) p :=
  ⟨fun x => by
    rw [← cast_eq_zero_iff R p x, ← map_natCast (Ideal.Quotient.mk I)]
    refine Ideal.Quotient.eq.trans (?_ : ↑x - 0 ∈ I ↔ _)
    rw [sub_zero]
    exact ⟨h x, fun h' => h'.symm ▸ I.zero_mem⟩⟩

Proof state:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ (Ideal.Quotient.mk I) ↑x = 0 ↔ ↑x = 0

Tactic:
refine Ideal.Quotient.eq.trans (?_ : ↑x - 0 ∈ I ↔ _)

Result:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑x - 0 ∈ I ↔ ↑x = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑x ∈ I ↔ ↑x = 0

Tactic:
exact ⟨h x, fun h' => h'.symm ▸ I.zero_mem⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑x - 0 ∈ I ↔ ↑x = 0

Tactic:
rw [sub_zero]

Result:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑x ∈ I ↔ ↑x = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ ↑x = 0 ↔ p ∣ x

Tactic:
rw [← cast_eq_zero_iff R p x, ← map_natCast (Ideal.Quotient.mk I)]

Result:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : CharP R p
I : Ideal R
h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0
x : ℕ
⊢ (Ideal.Quotient.mk I) ↑x = 0 ↔ ↑x = 0
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[reassoc]
lemma map_μ_comp_counit_app_tensor (X Y : D) :
    F.map (μ G X Y) ≫ adj.counit.app (X ⊗ Y) =
      δ F _ _ ≫ (adj.counit.app X ⊗ adj.counit.app Y)

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.OplaxMonoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : D
⊢ F.map (adj.unit.app (G.obj X ⊗ G.obj Y) ≫ G.map (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ adj.counit.app Y))) ≫
      adj.counit.app (X ⊗ Y) =
    δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ adj.counit.app Y)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.OplaxMonoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : D
⊢ F.map (μ G X Y) ≫ adj.counit.app (X ⊗ Y) = δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ adj.counit.app Y)

Tactic:
rw [IsMonoidal.leftAdjoint_μ (adj := adj), homEquiv_unit]

Result:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : MonoidalCategory C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : MonoidalCategory D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : F.OplaxMonoidal
inst✝¹ : G.LaxMonoidal
inst✝ : adj.IsMonoidal
X Y : D
⊢ F.map (adj.unit.app (G.obj X ⊗ G.obj Y) ≫ G.map (δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ adj.counit.app Y))) ≫
      adj.counit.app (X ⊗ Y) =
    δ F (G.obj X) (G.obj Y) ≫ (adj.counit.app X ⊗ adj.counit.app Y)
-- Mathlib/CategoryTheory/Shift/Adjunction.lean
/-- Given an adjunction `adj : F ⊣ G`, `a` in `A` and commutation isomorphisms
`e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a` and
`e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a`, if `e₁` and `e₂` are compatible with the
unit of the adjunction `adj`, then we get a formula for `e₂.inv` in terms of `e₁`.
-/
lemma compatibilityUnit_right (h : CompatibilityUnit adj e₁ e₂) (Y : D) :
    e₂.inv.app Y = adj.unit.app _ ≫ G.map (e₁.hom.app _) ≫ G.map ((adj.counit.app _)⟦a⟧')

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y))
⊢ e₂.inv.app Y =
    (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫
      e₂.inv.app (F.obj (G.obj Y)) ≫ G.map ((shiftFunctor D a).map (adj.counit.app Y))

Tactic:
erw [← e₂.inv.naturality]

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫ e₂.inv.app (F.obj (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y))
⊢ e₂.inv.app Y =
    (shiftFunctor C a).map (adj.unit.app (G.obj Y)) ≫
      (G ⋙ shiftFunctor C a).map (adj.counit.app Y) ≫ e₂.inv.app ((𝟭 D).obj Y)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
⊢ e₂.inv.app Y =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map (e₁.hom.app (G.obj Y)) ≫ G.map ((shiftFunctor D a).map (adj.counit.app Y))

Tactic:
have := h (G.obj Y)

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
Y : D
this :
  (shiftFunctor C a).map (adj.unit.app (G.obj Y)) =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫ G.map (e₁.hom.app (G.obj Y)) ≫ e₂.hom.app (F.obj (G.obj Y))
⊢ e₂.inv.app Y =
    adj.unit.app ((shiftFunctor C a).obj (G.obj Y)) ≫
      G.map (e₁.hom.app (G.obj Y)) ≫ G.map ((shiftFunctor D a).map (adj.counit.app Y))
-- Mathlib/Topology/Order/ScottTopology.lean
lemma IsScott.scottHausdorff_le [IsScott α univ] :
    scottHausdorff α univ ≤ ‹TopologicalSpace α›

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ scottHausdorff α univ ≤ upperSet α ⊔ scottHausdorff α univ

Tactic:
exact le_sup_right

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ scottHausdorff α univ ≤ inst✝¹

Tactic:
rw [IsScott.topology_eq α univ, scott]

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ scottHausdorff α univ ≤ upperSet α ⊔ scottHausdorff α univ
-- Mathlib/FieldTheory/Relrank.lean
theorem relrank_eq_rank_of_le (h : A ≤ B) : relrank A B = Module.rank A (extendScalars h)

Proof state:
E : Type v
inst✝ : Field E
A B : Subfield E
h : A ≤ B
⊢ Module.rank ↥(A ⊓ B) ↥(extendScalars ⋯) = Module.rank ↥A ↥(extendScalars h)

Tactic:
have := inf_of_le_left h

Result:
E : Type v
inst✝ : Field E
A B : Subfield E
h : A ≤ B
this : A ⊓ B = A
⊢ Module.rank ↥(A ⊓ B) ↥(extendScalars ⋯) = Module.rank ↥A ↥(extendScalars h)

Proof state:
E : Type v
inst✝ : Field E
A B : Subfield E
h : A ≤ B
⊢ A.relrank B = Module.rank ↥A ↥(extendScalars h)

Tactic:
rw [relrank]

Result:
E : Type v
inst✝ : Field E
A B : Subfield E
h : A ≤ B
⊢ Module.rank ↥(A ⊓ B) ↥(extendScalars ⋯) = Module.rank ↥A ↥(extendScalars h)

Proof state:
E : Type v
inst✝ : Field E
A B : Subfield E
h : A ≤ B
this : A ⊓ B = A
⊢ Module.rank ↥(A ⊓ B) ↥(extendScalars ⋯) = Module.rank ↥A ↥(extendScalars h)

Tactic:
congr!

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem head_attach {xs : List α} (h) :
    xs.attach.head h = ⟨xs.head (by simpa using h), head_mem (by simpa using h)⟩

Proof state:
α : Type u_1
xs : List α
h : xs.attach ≠ []
⊢ xs.attach.head h = ⟨xs.head ⋯, ⋯⟩

Tactic:
cases xs with
| nil => simp at h
| cons x xs => simp [head_attach, h]

Result:
no goals

Proof state:
α : Type ?u.48444
xs : List α
h : xs.attach ≠ []
⊢ xs ≠ []

Tactic:
simpa using h

Result:
no goals

Proof state:
case cons
α : Type u_1
x : α
xs : List α
h : (x :: xs).attach ≠ []
⊢ (x :: xs).attach.head h = ⟨(x :: xs).head ⋯, ⋯⟩

Tactic:
simp [head_attach, h]

Result:
no goals

Proof state:
case nil
α : Type u_1
h : [].attach ≠ []
⊢ [].attach.head h = ⟨[].head ⋯, ⋯⟩

Tactic:
simp at h

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
theorem finrank_span_singleton {v : V} (hv : v ≠ 0) : finrank K (K ∙ v) = 1

Proof state:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ finrank K ↥(span K {v}) ≤ 1

Tactic:
exact finrank_span_le_card ({v} : Set V)

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ finrank K ↥(span K {v}) = 1

Tactic:
apply le_antisymm

Result:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ finrank K ↥(span K {v}) ≤ 1

case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ 1 ≤ finrank K ↥(span K {v})

Proof state:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ Nontrivial ↥(span K {v})

Tactic:
use ⟨v, mem_span_singleton_self v⟩, 0

Result:
case h
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ ⟨v, ⋯⟩ ≠ 0

Proof state:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ 1 ≤ finrank K ↥(span K {v})

Tactic:
rw [Nat.succ_le_iff, finrank_pos_iff]

Result:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ Nontrivial ↥(span K {v})

Proof state:
case h
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ ⟨v, ⋯⟩ ≠ 0

Tactic:
apply Subtype.coe_ne_coe.mp

Result:
case h
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ ↑⟨v, ⋯⟩ ≠ ↑0

Proof state:
case h
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : V
hv : v ≠ 0
⊢ ↑⟨v, ⋯⟩ ≠ ↑0

Tactic:
simp [hv]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean
lemma lt_largerSubobject (A : Subobject X) (hA : A ≠ ⊤) :
    A < largerSubobject hG A

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : A ≠ ⊤
⊢ A < largerSubobject hG A

Tactic:
dsimp only [largerSubobject]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : A ≠ ⊤
⊢ A < if hA : A = ⊤ then ⊤ else ⋯.choose

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : A ≠ ⊤
⊢ A < if hA : A = ⊤ then ⊤ else ⋯.choose

Tactic:
rw [dif_neg hA]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : A ≠ ⊤
⊢ A < ⋯.choose

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
G : C
inst✝ : Abelian C
hG : IsSeparator G
X : C
A : Subobject X
hA : A ≠ ⊤
⊢ A < ⋯.choose

Tactic:
exact (exists_larger_subobject hG A hA).choose_spec.choose

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem le_mul_inv_iff_le : 1 ≤ a * b⁻¹ ↔ b ≤ a

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b : α
⊢ 1 ≤ a * b⁻¹ ↔ b ≤ a

Tactic:
rw [← mul_le_mul_iff_right b, one_mul, inv_mul_cancel_right]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem comp_right_differentiable_iff {f : F → G} :
    Differentiable 𝕜 (f ∘ iso) ↔ Differentiable 𝕜 f

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : F → G
⊢ Differentiable 𝕜 (f ∘ ⇑iso) ↔ Differentiable 𝕜 f

Tactic:
simp only [← differentiableOn_univ, ← iso.comp_right_differentiableOn_iff, preimage_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_insertMany_empty_list_of_contains_eq_false [LawfulBEq α]
    {l : List (α × β)} {k : α} {fallback : β}
    (contains_eq_false : (l.map Prod.fst).contains k = false) :
    getD (insertMany (empty : Raw₀ α (fun _ => β)) l) k fallback = fallback

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
inst✝ : LawfulBEq α
l : List (α × β)
k : α
fallback : β
contains_eq_false : (List.map Prod.fst l).contains k = false
⊢ getD empty k fallback = fallback

Tactic:
apply getD_empty

Result:
no goals

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
inst✝ : LawfulBEq α
l : List (α × β)
k : α
fallback : β
contains_eq_false : (List.map Prod.fst l).contains k = false
⊢ getD (insertMany empty l).val k fallback = fallback

Tactic:
rw [getD_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ contains_eq_false]

Result:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
inst✝ : LawfulBEq α
l : List (α × β)
k : α
fallback : β
contains_eq_false : (List.map Prod.fst l).contains k = false
⊢ getD empty k fallback = fallback
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pos_of_lt_mul_right {a b c : Nat} (h : a < b * c) : 0 < b

Proof state:
a b c : Nat
h : a < b * c
⊢ 0 < b * c

Tactic:
omega

Result:
no goals

Proof state:
a b c : Nat
h : a < b * c
⊢ 0 < b

Tactic:
replace h : 0 < b * c := by omega

Result:
a b c : Nat
h : 0 < b * c
⊢ 0 < b

Proof state:
a b c : Nat
h : 0 < b * c
⊢ 0 < b

Tactic:
exact Nat.pos_of_mul_pos_right h

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_union_Ico {a b c d : α} (h₁ : min a b ≤ max c d) (h₂ : min c d ≤ max a b) :
    Ico a b ∪ Ico c d = Ico (min a c) (max b d)

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h₁ : a ⊓ b ≤ c ⊔ d
h₂ : c ⊓ d ≤ a ⊔ b
⊢ Ico a b ∪ Ico c d = Ico (a ⊓ c) (b ⊔ d)

Tactic:
rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico h₁ h₂]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orientation.lean
theorem det_to_matrix_orthonormalBasis_of_same_orientation
    (h : e.toBasis.orientation = f.toBasis.orientation) : e.toBasis.det f = 1

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation = f.toBasis.orientation
⊢ 0 < e.toBasis.det ⇑f

Tactic:
rw [e.toBasis.orientation_eq_iff_det_pos] at h

Result:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : 0 < e.toBasis.det ⇑f.toBasis
⊢ 0 < e.toBasis.det ⇑f

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation = f.toBasis.orientation
this : 0 < e.toBasis.det ⇑f
⊢ ¬e.toBasis.det ⇑f = -1

Tactic:
linarith

Result:
no goals

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation = f.toBasis.orientation
⊢ ¬e.toBasis.det ⇑f = -1

Tactic:
have : 0 < e.toBasis.det f := by
  rw [e.toBasis.orientation_eq_iff_det_pos] at h
  simpa using h

Result:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation = f.toBasis.orientation
this : 0 < e.toBasis.det ⇑f
⊢ ¬e.toBasis.det ⇑f = -1

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : 0 < e.toBasis.det ⇑f.toBasis
⊢ 0 < e.toBasis.det ⇑f

Tactic:
simpa using h

Result:
no goals

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation = f.toBasis.orientation
⊢ e.toBasis.det ⇑f = 1

Tactic:
apply (e.det_to_matrix_orthonormalBasis_real f).resolve_right

Result:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation = f.toBasis.orientation
⊢ ¬e.toBasis.det ⇑f = -1
-- Mathlib/Analysis/Convex/Basic.lean
theorem convex_segment (x y : E) : Convex 𝕜 [x -[𝕜] y]

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * ap + b * aq) • x + (a * bp + b * bq) • y = a • (ap • x + bp • y) + b • (aq • x + bq • y)

Tactic:
match_scalars <;> noncomm_ring

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * ap + b * aq + (a * bp + b * bq) = 1

Tactic:
rw [add_add_add_comm, ← mul_add, ← mul_add, habp, habq, mul_one, mul_one, hab]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (ap • x + bp • y) + b • (aq • x + bq • y) ∈ [x-[𝕜]y]

Tactic:
refine
  ⟨a * ap + b * aq, a * bp + b * bq, add_nonneg (mul_nonneg ha hap) (mul_nonneg hb haq),
    add_nonneg (mul_nonneg ha hbp) (mul_nonneg hb hbq), ?_, ?_⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * ap + b * aq + (a * bp + b * bq) = 1

case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * ap + b * aq) • x + (a * bp + b * bq) • y = a • (ap • x + bp • y) + b • (aq • x + bq • y)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y : E
⊢ Convex 𝕜 [x-[𝕜]y]

Tactic:
rintro p ⟨ap, bp, hap, hbp, habp, rfl⟩ q ⟨aq, bq, haq, hbq, habq, rfl⟩ a b ha hb hab

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x y : E
ap bp : 𝕜
hap : 0 ≤ ap
hbp : 0 ≤ bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 ≤ aq
hbq : 0 ≤ bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (ap • x + bp • y) + b • (aq • x + bq • y) ∈ [x-[𝕜]y]
-- Mathlib/Data/Nat/Size.lean
theorem shiftLeft'_tt_eq_mul_pow (m) : ∀ n, shiftLeft' true m n + 1 = (m + 1) * 2 ^ n
  | 0 => by simp [shiftLeft', pow_zero, Nat.one_mul]
  | k + 1 => by
    rw [shiftLeft', bit_val, Bool.toNat_true, add_assoc, ← Nat.mul_add_one,
      shiftLeft'_tt_eq_mul_pow m k, mul_left_comm, mul_comm 2, pow_succ]

Proof state:
m k : ℕ
⊢ shiftLeft' true m (k + 1) + 1 = (m + 1) * 2 ^ (k + 1)

Tactic:
rw [shiftLeft', bit_val, Bool.toNat_true, add_assoc, ← Nat.mul_add_one,
  shiftLeft'_tt_eq_mul_pow m k, mul_left_comm, mul_comm 2, pow_succ]

Result:
no goals

Proof state:
m : ℕ
⊢ shiftLeft' true m 0 + 1 = (m + 1) * 2 ^ 0

Tactic:
simp [shiftLeft', pow_zero, Nat.one_mul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem DifferentiableWithinAt.rpow (hf : DifferentiableWithinAt ℝ f s x)
    (hg : DifferentiableWithinAt ℝ g s x) (h : f x ≠ 0) :
    DifferentiableWithinAt ℝ (fun x => f x ^ g x) s x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : E → ℝ
x : E
s : Set E
hf : DifferentiableWithinAt ℝ f s x
hg : DifferentiableWithinAt ℝ g s x
h : f x ≠ 0
⊢ DifferentiableWithinAt ℝ (fun x => f x ^ g x) s x

Tactic:
exact (differentiableAt_rpow_of_ne (f x, g x) h).comp_differentiableWithinAt x (hf.prod hg)

Result:
no goals