harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/LocallyFullyFaithful.lean
@[simp]
lemma Sieve.equalizer_self {U V : C} (f : U ⟶ V) : equalizer f f = ⊤

Proof state:
C : Type uC
inst✝ : Category.{vC, uC} C
U V : C
f : U ⟶ V
⊢ equalizer f f = ⊤

Tactic:
ext

Result:
case h
C : Type uC
inst✝ : Category.{vC, uC} C
U V : C
f : U ⟶ V
Y✝ : C
f✝ : Y✝ ⟶ U
⊢ (equalizer f f).arrows f✝ ↔ ⊤.arrows f✝

Proof state:
case h
C : Type uC
inst✝ : Category.{vC, uC} C
U V : C
f : U ⟶ V
Y✝ : C
f✝ : Y✝ ⟶ U
⊢ (equalizer f f).arrows f✝ ↔ ⊤.arrows f✝

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sheafification.lean
theorem HasSheafify.mk' {F : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A} (adj : F ⊣ sheafToPresheaf J A)
    [PreservesFiniteLimits F] : HasSheafify J A where
  isRightAdjoint := ⟨F, ⟨adj⟩⟩
  isLeftExact := ⟨by
    have : (sheafToPresheaf J A).IsRightAdjoint := ⟨_, ⟨adj⟩⟩
    exact fun _ _ _ ↦ preservesLimitsOfShape_of_natIso
      (adj.leftAdjointUniq (Adjunction.ofIsRightAdjoint (sheafToPresheaf J A)))⟩

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
F : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : F ⊣ sheafToPresheaf J A
inst✝ : PreservesFiniteLimits F
this : (sheafToPresheaf J A).IsRightAdjoint
⊢ ∀ (J_1 : Type) [inst : SmallCategory J_1] [inst_1 : FinCategory J_1],
    PreservesLimitsOfShape J_1 (sheafToPresheaf J A).leftAdjoint

Tactic:
exact fun _ _ _ ↦ preservesLimitsOfShape_of_natIso
  (adj.leftAdjointUniq (Adjunction.ofIsRightAdjoint (sheafToPresheaf J A)))

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
F : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : F ⊣ sheafToPresheaf J A
inst✝ : PreservesFiniteLimits F
⊢ ∀ (J_1 : Type) [inst : SmallCategory J_1] [inst_1 : FinCategory J_1],
    PreservesLimitsOfShape J_1 (sheafToPresheaf J A).leftAdjoint

Tactic:
have : (sheafToPresheaf J A).IsRightAdjoint := ⟨_, ⟨adj⟩⟩

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
F : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A
adj : F ⊣ sheafToPresheaf J A
inst✝ : PreservesFiniteLimits F
this : (sheafToPresheaf J A).IsRightAdjoint
⊢ ∀ (J_1 : Type) [inst : SmallCategory J_1] [inst_1 : FinCategory J_1],
    PreservesLimitsOfShape J_1 (sheafToPresheaf J A).leftAdjoint
-- Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean
theorem mdifferentiableWithinAt_iff_differentiableWithinAt :
    MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x ↔ DifferentiableWithinAt 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
⊢ MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
simp only [mdifferentiableWithinAt_iff', mfld_simps]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
⊢ ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_3
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
s : Set E
x : E
⊢ ContinuousWithinAt f s x ∧ DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
exact ⟨fun H => H.2, fun H => ⟨H.continuousWithinAt, H⟩⟩

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem const_le {x y : α} : const x ≤ const y ↔ x ≤ y

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
x y : α
⊢ const x ≤ const y ↔ x < y ∨ x = y

Tactic:
exact or_congr const_lt const_equiv

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
x y : α
⊢ const x ≤ const y ↔ x ≤ y

Tactic:
rw [le_iff_lt_or_eq]

Result:
α : Type u_1
inst✝ : LinearOrderedField α
x y : α
⊢ const x ≤ const y ↔ x < y ∨ x = y
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem posDef_of_toMatrix' [DecidableEq n] {Q : QuadraticForm ℝ (n → ℝ)}
    (hQ : Q.toMatrix'.PosDef) : Q.PosDef

Proof state:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : (toMatrix' Q).PosDef
⊢ (LinearMap.BilinMap.toQuadraticMap
      ((LinearMap.toMatrix₂' ℝ).invFun ((↑(LinearMap.toMatrix₂' ℝ)).toFun ((associatedHom ℝ) Q)))).PosDef

Tactic:
exact hQ.toQuadraticForm'

Result:
no goals

Proof state:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : (toMatrix' Q).PosDef
⊢ PosDef Q

Tactic:
rw [← toQuadraticMap_associated ℝ Q,
  ← (LinearMap.toMatrix₂' ℝ).left_inv ((associatedHom (R := ℝ) ℝ) Q)]

Result:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Q : QuadraticForm ℝ (n → ℝ)
hQ : (toMatrix' Q).PosDef
⊢ (LinearMap.BilinMap.toQuadraticMap
      ((LinearMap.toMatrix₂' ℝ).invFun ((↑(LinearMap.toMatrix₂' ℝ)).toFun ((associatedHom ℝ) Q)))).PosDef
-- Mathlib/Algebra/Order/Floor.lean
theorem add_one_le_ceil_iff : n + 1 ≤ ⌈a⌉₊ ↔ (n : α) < a

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : FloorSemiring α
a : α
n : ℕ
⊢ n + 1 ≤ ⌈a⌉₊ ↔ ↑n < a

Tactic:
rw [← Nat.lt_ceil, Nat.add_one_le_iff]

Result:
no goals
-- Mathlib/Condensed/Discrete/Colimit.lean
@[simp]
lemma lanPresheafNatIso_hom_app (hF : ∀ S : Profinite, IsColimit <| F.mapCocone S.asLimitCone.op)
    (S : Profiniteᵒᵖ) : (lanPresheafNatIso hF).hom.app S =
      colimit.desc _ (Profinite.Extend.cocone _ _)

Proof state:
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : (S : Profinite) → IsColimit (F.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
⊢ (lanPresheafNatIso hF).hom.app S =
    colimit.desc (CostructuredArrow.proj toProfinite.op (Opposite.op (Opposite.unop S)) ⋙ toProfinite.op ⋙ F)
      (Profinite.Extend.cocone F (Opposite.unop S))

Tactic:
simp [lanPresheafNatIso]

Result:
no goals
-- Mathlib/Control/Functor.lean
theorem comp_map (g' : α → β) (h : β → γ) :
    ∀ x : Comp F G α, Comp.map (h ∘ g') x = Comp.map h (Comp.map g' x)
  | Comp.mk x => by simp [Comp.map, Comp.mk, Functor.map_comp_map, functor_norm, Function.comp_def]

Proof state:
F : Type u → Type w
G : Type v → Type u
inst✝³ : Functor F
inst✝² : Functor G
inst✝¹ : LawfulFunctor F
inst✝ : LawfulFunctor G
α β γ : Type v
g' : α → β
h : β → γ
x : F (G α)
⊢ Comp.map (h ∘ g') (mk x) = Comp.map h (Comp.map g' (mk x))

Tactic:
simp [Comp.map, Comp.mk, Functor.map_comp_map, functor_norm, Function.comp_def]

Result:
no goals
-- Mathlib/Data/ENNReal/Holder.lean
lemma inv_inv_add_inv : (p⁻¹ + q⁻¹)⁻¹ = r

Proof state:
p q r : ℝ≥0∞
inst✝ : p.HolderTriple q r
⊢ (p⁻¹ + q⁻¹)⁻¹ = r

Tactic:
simp [inv_add_inv_eq_inv p q r]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem op_inl {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) :
    c.op.inl = c.fst.op

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
c : PullbackCone f g
⊢ c.op.inl = c.fst.op

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/Sites/MorphismProperty.lean
lemma pretopology_le_pretopology (hPQ : P ≤ Q) :
    pretopology P ≤ pretopology Q

Proof state:
P : MorphismProperty Scheme
inst✝⁷ : P.IsMultiplicative
inst✝⁶ : P.RespectsIso
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : IsJointlySurjectivePreserving P
Q : MorphismProperty Scheme
inst✝³ : Q.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving Q
hPQ : P ≤ Q
⊢ pretopology P ≤ pretopology Q

Tactic:
rintro X - ⟨𝒰, rfl⟩

Result:
case intro
P : MorphismProperty Scheme
inst✝⁷ : P.IsMultiplicative
inst✝⁶ : P.RespectsIso
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : IsJointlySurjectivePreserving P
Q : MorphismProperty Scheme
inst✝³ : Q.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving Q
hPQ : P ≤ Q
X : Scheme
𝒰 : Cover P X
⊢ Presieve.ofArrows 𝒰.obj 𝒰.map ∈ (pretopology Q).coverings X

Proof state:
case intro
P : MorphismProperty Scheme
inst✝⁷ : P.IsMultiplicative
inst✝⁶ : P.RespectsIso
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : IsJointlySurjectivePreserving P
Q : MorphismProperty Scheme
inst✝³ : Q.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving Q
hPQ : P ≤ Q
X : Scheme
𝒰 : Cover P X
⊢ Presieve.ofArrows 𝒰.obj 𝒰.map ∈ (pretopology Q).coverings X

Tactic:
use 𝒰.changeProp Q (fun j ↦ hPQ _ (𝒰.map_prop j))

Result:
case h
P : MorphismProperty Scheme
inst✝⁷ : P.IsMultiplicative
inst✝⁶ : P.RespectsIso
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : IsJointlySurjectivePreserving P
Q : MorphismProperty Scheme
inst✝³ : Q.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving Q
hPQ : P ≤ Q
X : Scheme
𝒰 : Cover P X
⊢ Presieve.ofArrows 𝒰.obj 𝒰.map = Presieve.ofArrows (Cover.changeProp Q 𝒰 ⋯).obj (Cover.changeProp Q 𝒰 ⋯).map

Proof state:
case h
P : MorphismProperty Scheme
inst✝⁷ : P.IsMultiplicative
inst✝⁶ : P.RespectsIso
inst✝⁵ : P.IsStableUnderBaseChange
inst✝⁴ : IsJointlySurjectivePreserving P
Q : MorphismProperty Scheme
inst✝³ : Q.IsMultiplicative
inst✝² : Q.RespectsIso
inst✝¹ : Q.IsStableUnderBaseChange
inst✝ : IsJointlySurjectivePreserving Q
hPQ : P ≤ Q
X : Scheme
𝒰 : Cover P X
⊢ Presieve.ofArrows 𝒰.obj 𝒰.map = Presieve.ofArrows (Cover.changeProp Q 𝒰 ⋯).obj (Cover.changeProp Q 𝒰 ⋯).map

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem not_or_iff_left_iff_imp  : ∀ {a b : Bool}, ((!a || b) = a) ↔ a ∧ b

Proof state:
⊢ ∀ {a b : Bool}, (!a || b) = a ↔ a = true ∧ b = true

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem add_emod_emod (m n k : Int) : (m + n % k) % k = (m + n) % k

Proof state:
m n k : Int
⊢ (m + n % k) % k = (m + n) % k

Tactic:
rw [Int.add_comm, emod_add_emod, Int.add_comm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean
lemma isImmersion_eq_inf : @IsImmersion = (@IsPreimmersion ⊓
    topologically fun {_ _} _ _ f ↦ IsLocallyClosed (Set.range f) : MorphismProperty Scheme)

Proof state:
⊢ @IsImmersion = @IsPreimmersion ⊓ topologically fun {x x_1} x_2 x_3 f => IsLocallyClosed (Set.range f)

Tactic:
ext

Result:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsImmersion x✝ ↔ (@IsPreimmersion ⊓ topologically fun {x x_1} x_2 x_3 f => IsLocallyClosed (Set.range f)) x✝

Proof state:
case h.h.h.a
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsImmersion x✝ ↔ (@IsPreimmersion ⊓ topologically fun {x x_1} x_2 x_3 f => IsLocallyClosed (Set.range f)) x✝

Tactic:
exact isImmersion_iff _

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem get_odd : ∀ (n : ℕ) (s : Stream' α), get (odd s) n = get s (2 * n + 1) := fun n s => by
  rw [odd_eq, get_even]; rfl

Proof state:
α : Type u
n : ℕ
s : Stream' α
⊢ s.odd.get n = s.get (2 * n + 1)

Tactic:
rw [odd_eq, get_even]

Result:
α : Type u
n : ℕ
s : Stream' α
⊢ s.tail.get (2 * n) = s.get (2 * n + 1)

Proof state:
α : Type u
n : ℕ
s : Stream' α
⊢ s.tail.get (2 * n) = s.get (2 * n + 1)

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
lemma exists_pos {k : ℕ} (hζ : ζ ^ k = 1) (hk : k ≠ 0) :
    ∃ k' > 0, IsPrimitiveRoot ζ k' :=
  ⟨orderOf ζ, by
    rw [gt_iff_lt, orderOf_pos_iff, isOfFinOrder_iff_pow_eq_one]
    exact ⟨k, Nat.pos_iff_ne_zero.mpr hk, hζ⟩, .orderOf _⟩

Proof state:
M : Type u_1
inst✝ : CommMonoid M
ζ : M
k : ℕ
hζ : ζ ^ k = 1
hk : k ≠ 0
⊢ orderOf ζ > 0

Tactic:
rw [gt_iff_lt, orderOf_pos_iff, isOfFinOrder_iff_pow_eq_one]

Result:
M : Type u_1
inst✝ : CommMonoid M
ζ : M
k : ℕ
hζ : ζ ^ k = 1
hk : k ≠ 0
⊢ ∃ n, 0 < n ∧ ζ ^ n = 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
ζ : M
k : ℕ
hζ : ζ ^ k = 1
hk : k ≠ 0
⊢ ∃ n, 0 < n ∧ ζ ^ n = 1

Tactic:
exact ⟨k, Nat.pos_iff_ne_zero.mpr hk, hζ⟩

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean
theorem balancedHull_mono (hst : s ⊆ t) : balancedHull 𝕜 s ⊆ balancedHull 𝕜 t

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
hst : s ⊆ t
x : E
hx : x ∈ balancedHull 𝕜 s
⊢ x ∈ balancedHull 𝕜 t

Tactic:
rw [mem_balancedHull_iff] at *

Result:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
hst : s ⊆ t
x : E
hx : ∃ r, ‖r‖ ≤ 1 ∧ x ∈ r • s
⊢ ∃ r, ‖r‖ ≤ 1 ∧ x ∈ r • t

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
hst : s ⊆ t
x : E
hx : ∃ r, ‖r‖ ≤ 1 ∧ x ∈ r • s
⊢ ∃ r, ‖r‖ ≤ 1 ∧ x ∈ r • t

Tactic:
obtain ⟨r, hr₁, hr₂⟩ := hx

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
hst : s ⊆ t
x : E
r : 𝕜
hr₁ : ‖r‖ ≤ 1
hr₂ : x ∈ r • s
⊢ ∃ r, ‖r‖ ≤ 1 ∧ x ∈ r • t

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
hst : s ⊆ t
x : E
r : 𝕜
hr₁ : ‖r‖ ≤ 1
hr₂ : x ∈ r • s
⊢ ∃ r, ‖r‖ ≤ 1 ∧ x ∈ r • t

Tactic:
use r

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
hst : s ⊆ t
x : E
r : 𝕜
hr₁ : ‖r‖ ≤ 1
hr₂ : x ∈ r • s
⊢ ‖r‖ ≤ 1 ∧ x ∈ r • t

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
hst : s ⊆ t
x : E
r : 𝕜
hr₁ : ‖r‖ ≤ 1
hr₂ : x ∈ r • s
⊢ ‖r‖ ≤ 1 ∧ x ∈ r • t

Tactic:
exact ⟨hr₁, smul_set_mono hst hr₂⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
hst : s ⊆ t
⊢ balancedHull 𝕜 s ⊆ balancedHull 𝕜 t

Tactic:
intro x hx

Result:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
hst : s ⊆ t
x : E
hx : x ∈ balancedHull 𝕜 s
⊢ x ∈ balancedHull 𝕜 t
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_hom' (s : Multiset ι) {F : Type*} [FunLike F α β]
    [MonoidHomClass F α β] (f : F)
    (g : ι → α) : (s.map fun i => f <| g i).prod = f (s.map g).prod

Proof state:
case h.e'_2.h.e'_3
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Multiset ι
F : Type u_7
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
g : ι → α
⊢ map (fun i => f (g i)) s = map (⇑f) (map g s)

Tactic:
exact (map_map _ _ _).symm

Result:
no goals

Proof state:
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Multiset ι
F : Type u_7
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
g : ι → α
⊢ (map (fun i => f (g i)) s).prod = f (map g s).prod

Tactic:
convert (s.map g).prod_hom f

Result:
case h.e'_2.h.e'_3
ι : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Multiset ι
F : Type u_7
inst✝¹ : FunLike F α β
inst✝ : MonoidHomClass F α β
f : F
g : ι → α
⊢ map (fun i => f (g i)) s = map (⇑f) (map g s)
-- Mathlib/Topology/ContinuousMap/Ordered.lean
@[simp, norm_cast]
lemma coe_inf' {ι : Type*} {s : Finset ι} (H : s.Nonempty) (f : ι → C(α, β)) :
    ⇑(s.inf' H f) = s.inf' H fun i ↦ ⇑(f i)

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
x✝ : α
⊢ (s.inf' H f) x✝ = s.inf' H (fun i => ⇑(f i)) x✝

Tactic:
simp [inf'_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
⊢ ⇑(s.inf' H f) = s.inf' H fun i => ⇑(f i)

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
ι : Type u_3
s : Finset ι
H : s.Nonempty
f : ι → C(α, β)
x✝ : α
⊢ (s.inf' H f) x✝ = s.inf' H (fun i => ⇑(f i)) x✝
-- Mathlib/Order/Interval/Set/OrdConnected.lean
theorem ordConnected_dual {s : Set α} : OrdConnected (OrderDual.ofDual ⁻¹' s) ↔ OrdConnected s :=
  ⟨fun h => by simpa only [ordConnected_def] using h.dual, fun h => h.dual⟩

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
h : (⇑ofDual ⁻¹' s).OrdConnected
⊢ s.OrdConnected

Tactic:
simpa only [ordConnected_def] using h.dual

Result:
no goals
-- Mathlib/RingTheory/WittVector/Teichmuller.lean
theorem teichmuller_zero : teichmuller p (0 : R) = 0

Proof state:
case h.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n✝ : ℕ
⊢ ((teichmuller p) 0).coeff (n✝ + 1) = 0

Tactic:
rfl

Result:
no goals

Proof state:
case h.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n✝ : ℕ
⊢ ((teichmuller p) 0).coeff (n✝ + 1) = coeff 0 (n✝ + 1)

Tactic:
rw [zero_coeff]

Result:
case h.succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
n✝ : ℕ
⊢ ((teichmuller p) 0).coeff (n✝ + 1) = 0
-- Mathlib/FieldTheory/Minpoly/Basic.lean
theorem natDegree_eq_one_iff :
    (minpoly A x).natDegree = 1 ↔ x ∈ (algebraMap A B).range

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
⊢ (minpoly A x).natDegree = 1 ↔ x ∈ (algebraMap A B).range

Tactic:
rw [← Polynomial.degree_eq_iff_natDegree_eq_of_pos zero_lt_one]

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
⊢ (minpoly A x).degree = ↑1 ↔ x ∈ (algebraMap A B).range

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : Nontrivial B
⊢ (minpoly A x).degree = ↑1 ↔ x ∈ (algebraMap A B).range

Tactic:
exact degree_eq_one_iff

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorAdd'_zero_add_inv_app (a : A) (X : C) :
    (shiftFunctorAdd' C 0 a a (zero_add a)).inv.app X =
    ((shiftFunctorZero C A).hom.app X)⟦a⟧'

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctorAdd' C 0 a a ⋯).inv.app X = (shiftFunctor C a).map ((shiftFunctorZero C A).hom.app X)

Tactic:
simpa using NatTrans.congr_app (congr_arg Iso.inv (shiftFunctorAdd'_zero_add C a)) X

Result:
no goals
-- Mathlib/Order/OrdContinuous.lean
theorem map_iSup (hf : LeftOrdContinuous f) (g : ι → α) : f (⨆ i, g i) = ⨆ i, f (g i)

Proof state:
α : Type u
β : Type v
ι : Sort x
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
g : ι → α
⊢ sSup (range (f ∘ fun i => g i)) = sSup (range fun i => f (g i))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Sort x
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
g : ι → α
⊢ f (⨆ i, g i) = ⨆ i, f (g i)

Tactic:
simp only [iSup, hf.map_sSup', ← range_comp]

Result:
α : Type u
β : Type v
ι : Sort x
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
g : ι → α
⊢ sSup (range (f ∘ fun i => g i)) = sSup (range fun i => f (g i))
-- Mathlib/RingTheory/Polynomial/ScaleRoots.lean
theorem degree_scaleRoots (p : R[X]) {s : R} : degree (scaleRoots p s) = degree p

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
⊢ (p.scaleRoots s).degree = p.degree

Tactic:
haveI := Classical.propDecidable

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
⊢ (p.scaleRoots s).degree = p.degree

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ (p.scaleRoots s).coeff p.natDegree ≠ 0

Tactic:
rw [coeff_scaleRoots_natDegree]

Result:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ p.leadingCoeff ≠ 0

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
⊢ (p.scaleRoots s).degree = p.degree

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : p = 0
⊢ (p.scaleRoots s).degree = p.degree

case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ (p.scaleRoots s).degree = p.degree

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
h : p.leadingCoeff = 0
⊢ False

Tactic:
have := leadingCoeff_eq_zero.mp h

Result:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this✝ : (a : Prop) → Decidable a
hp : ¬p = 0
h : p.leadingCoeff = 0
this : p = 0
⊢ False

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : p = 0
⊢ (p.scaleRoots s).degree = p.degree

Tactic:
rw [hp, zero_scaleRoots]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ p.leadingCoeff ≠ 0

Tactic:
intro h

Result:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
h : p.leadingCoeff = 0
⊢ False

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ (p.scaleRoots s).degree = p.degree

Tactic:
refine le_antisymm (Finset.sup_mono (support_scaleRoots_le p s)) (degree_le_degree ?_)

Result:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ (p.scaleRoots s).coeff p.natDegree ≠ 0

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]
s : R
this✝ : (a : Prop) → Decidable a
hp : ¬p = 0
h : p.leadingCoeff = 0
this : p = 0
⊢ False

Tactic:
contradiction

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem normSq_sub (z w : ℂ) : normSq (z - w) = normSq z + normSq w - 2 * (z * conj w).re

Proof state:
z w : ℂ
⊢ normSq (z - w) = normSq z + normSq w - 2 * (z * (starRingEnd ℂ) w).re

Tactic:
rw [sub_eq_add_neg, normSq_add]

Result:
z w : ℂ
⊢ normSq z + normSq (-w) + 2 * (z * (starRingEnd ℂ) (-w)).re = normSq z + normSq w - 2 * (z * (starRingEnd ℂ) w).re

Proof state:
z w : ℂ
⊢ normSq z + normSq (-w) + 2 * (z * (starRingEnd ℂ) (-w)).re = normSq z + normSq w - 2 * (z * (starRingEnd ℂ) w).re

Tactic:
simp only [RingHom.map_neg, mul_neg, neg_re, normSq_neg]

Result:
z w : ℂ
⊢ normSq z + normSq w + -(2 * (z * (starRingEnd ℂ) w).re) = normSq z + normSq w - 2 * (z * (starRingEnd ℂ) w).re

Proof state:
z w : ℂ
⊢ normSq z + normSq w + -(2 * (z * (starRingEnd ℂ) w).re) = normSq z + normSq w - 2 * (z * (starRingEnd ℂ) w).re

Tactic:
ring

Result:
no goals