harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/SmallObject/TransfiniteCompositionLifting.lean
lemma transfiniteCompositions_pushouts_coproducts_le_llp_rlp :
    (transfiniteCompositions.{w} (coproducts.{w} W).pushouts) ≤ W.rlp.llp

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
⊢ transfiniteCompositions.{w, v, u} (coproducts.{w, v, u} W).pushouts ≤ W.rlp.llp

Tactic:
simpa using transfiniteCompositions_le_llp_rlp (coproducts.{w} W).pushouts

Result:
no goals
-- Mathlib/Topology/Algebra/Module/LocallyConvex.lean
theorem locallyConvexSpace_sInf {ts : Set (TopologicalSpace E)}
    (h : ∀ t ∈ ts, @LocallyConvexSpace 𝕜 E _ _ _ t) : @LocallyConvexSpace 𝕜 E _ _ _ (sInf ts)

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
ts : Set (TopologicalSpace E)
h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
⊢ LocallyConvexSpace 𝕜 E

Tactic:
refine
  LocallyConvexSpace.ofBases 𝕜 E (fun _ => fun If : Set ts × (ts → Set E) => ⋂ i ∈ If.1, If.2 i)
    (fun x => fun If : Set ts × (ts → Set E) =>
      If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ @nhds _ (↑i) x ∧ Convex 𝕜 (If.2 i))
    (fun x => ?_) fun x If hif => convex_iInter fun i => convex_iInter fun hi => (hif.2 i hi).2

Result:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
ts : Set (TopologicalSpace E)
h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
x : E
⊢ (𝓝 x).HasBasis ((fun x If => If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 x ∧ Convex 𝕜 (If.2 i)) x)
    ((fun x If => ⋂ i ∈ If.1, If.2 i) x)

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
ts : Set (TopologicalSpace E)
h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
x : E
⊢ (𝓝 x).HasBasis ((fun x If => If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 x ∧ Convex 𝕜 (If.2 i)) x)
    ((fun x If => ⋂ i ∈ If.1, If.2 i) x)

Tactic:
rw [nhds_sInf, ← iInf_subtype'']

Result:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
ts : Set (TopologicalSpace E)
h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
x : E
⊢ (⨅ i, 𝓝 x).HasBasis ((fun x If => If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 x ∧ Convex 𝕜 (If.2 i)) x)
    ((fun x If => ⋂ i ∈ If.1, If.2 i) x)

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
ts : Set (TopologicalSpace E)
h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
x : E
⊢ (⨅ i, 𝓝 x).HasBasis ((fun x If => If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ 𝓝 x ∧ Convex 𝕜 (If.2 i)) x)
    ((fun x If => ⋂ i ∈ If.1, If.2 i) x)

Tactic:
exact hasBasis_iInf' fun i : ts => (@locallyConvexSpace_iff 𝕜 E _ _ _ ↑i).mp (h (↑i) i.2) x

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
ts : Set (TopologicalSpace E)
h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E

Tactic:
letI : TopologicalSpace E := sInf ts

Result:
𝕜 : Type u_2
E : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
ts : Set (TopologicalSpace E)
h : ∀ t ∈ ts, LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
⊢ LocallyConvexSpace 𝕜 E
-- Mathlib/Data/Fintype/Powerset.lean
@[simp] lemma powerset_eq_univ : s.powerset = univ ↔ s = univ

Proof state:
α : Type u_1
inst✝ : Fintype α
s : Finset α
⊢ s.powerset = univ ↔ s = univ

Tactic:
rw [← Finset.powerset_univ, powerset_inj]

Result:
no goals
-- Mathlib/Topology/Compactness/Compact.lean
theorem compl_mem_coclosedCompact : sᶜ ∈ coclosedCompact X ↔ IsCompact (closure s)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ sᶜ ∈ coclosedCompact X ↔ IsCompact (closure s)

Tactic:
rw [mem_coclosedCompact_iff, compl_compl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Convert.lean
theorem CNF.convertLRAT_readyForRupAdd (cnf : CNF Nat) :
    DefaultFormula.ReadyForRupAdd (CNF.convertLRAT cnf)

Proof state:
cnf : CNF Nat
⊢ (let lifted := lift cnf;
    let lratCnf := convertLRAT' lifted;
    DefaultFormula.ofArray (none :: lratCnf).toArray).ReadyForRupAdd

Tactic:
apply DefaultFormula.readyForRupAdd_ofArray

Result:
no goals

Proof state:
cnf : CNF Nat
⊢ (convertLRAT cnf).ReadyForRupAdd

Tactic:
unfold CNF.convertLRAT

Result:
cnf : CNF Nat
⊢ (let lifted := lift cnf;
    let lratCnf := convertLRAT' lifted;
    DefaultFormula.ofArray (none :: lratCnf).toArray).ReadyForRupAdd
-- Mathlib/Topology/Ultrafilter.lean
theorem isClosed_iff_ultrafilter : IsClosed s ↔
    ∀ x, ∀ u : Ultrafilter X, ↑u ≤ 𝓝 x → s ∈ u → x ∈ s

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ IsClosed s ↔ ∀ (x : X) (u : Ultrafilter X), ↑u ≤ 𝓝 x → s ∈ u → x ∈ s

Tactic:
simp [isClosed_iff_clusterPt, ClusterPt, ← exists_ultrafilter_iff]

Result:
no goals
-- Mathlib/FieldTheory/Normal/Closure.lean
theorem normalClosure_le_iff_of_normal {K₁ K₂ : IntermediateField F L} [Normal F K₂] :
    normalClosure F K₁ L ≤ K₂ ↔ K₁ ≤ K₂

Proof state:
F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
⊢ normalClosure F (↥K₁) L ≤ K₂ ↔ K₁ ≤ K₂

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
h : normalClosure F (↥K₁) L ≤ K₂
⊢ K₁ ≤ K₂

case refine_2
F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
h : K₁ ≤ K₂
⊢ normalClosure F (↥K₁) L ≤ K₂

Proof state:
case refine_1
F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
h : ∀ (f : ↥K₁ →ₐ[F] L), f.fieldRange ≤ K₂
⊢ K₁ ≤ K₂

Tactic:
simpa only [fieldRange_val] using h K₁.val

Result:
no goals

Proof state:
case refine_2
F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
h : K₁ ≤ K₂
⊢ normalClosure F (↥K₁) L ≤ K₂

Tactic:
rw [← normalClosure_of_normal K₂]

Result:
case refine_2
F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
h : K₁ ≤ K₂
⊢ normalClosure F (↥K₁) L ≤ normalClosure F (↥K₂) L

Proof state:
case refine_1
F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
h : normalClosure F (↥K₁) L ≤ K₂
⊢ K₁ ≤ K₂

Tactic:
rw [normalClosure_le_iff] at h

Result:
case refine_1
F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
h : ∀ (f : ↥K₁ →ₐ[F] L), f.fieldRange ≤ K₂
⊢ K₁ ≤ K₂

Proof state:
case refine_2
F : Type u_1
L : Type u_3
inst✝⁴ : Field F
inst✝³ : Field L
inst✝² : Algebra F L
inst✝¹ : Normal F L
K₁ K₂ : IntermediateField F L
inst✝ : Normal F ↥K₂
h : K₁ ≤ K₂
⊢ normalClosure F (↥K₁) L ≤ normalClosure F (↥K₂) L

Tactic:
exact normalClosure_mono K₁ K₂ h

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem Ico_eq_locus_Ioc_eq_iUnion_Ioo :
    { b | toIcoMod hp a b = toIocMod hp a b } = ⋃ z : ℤ, Set.Ioo (a + z • p) (a + p + z • p)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a : α
⊢ {b | toIcoMod hp a b = toIocMod hp a b} = ⋃ z, Set.Ioo (a + z • p) (a + p + z • p)

Tactic:
ext1

Result:
case h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a x✝ : α
⊢ x✝ ∈ {b | toIcoMod hp a b = toIocMod hp a b} ↔ x✝ ∈ ⋃ z, Set.Ioo (a + z • p) (a + p + z • p)

Proof state:
case h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a x✝ : α
⊢ x✝ ∈ {b | toIcoMod hp a b = toIocMod hp a b} ↔ x✝ ∈ ⋃ z, Set.Ioo (a + z • p) (a + p + z • p)

Tactic:
simp_rw [Set.mem_setOf, Set.mem_iUnion, ← Set.sub_mem_Ioo_iff_left, ←
  not_modEq_iff_toIcoMod_eq_toIocMod, modEq_iff_not_forall_mem_Ioo_mod hp, not_forall,
  Classical.not_not]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_lt_logb_of_base_lt_one (hx : 0 < x) (hxy : x < y) : logb b y < logb b x

Proof state:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hxy : x < y
⊢ logb b y < logb b x

Tactic:
rw [logb, logb, div_lt_div_right_of_neg (log_neg b_pos b_lt_one)]

Result:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hxy : x < y
⊢ log x < log y

Proof state:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hxy : x < y
⊢ log x < log y

Tactic:
exact log_lt_log hx hxy

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Basic.lean
lemma term_pos {a : ℕ → ℂ} {n : ℕ} (hn : n ≠ 0) (h : 0 < a n) (x : ℝ) : 0 < term a x n

Proof state:
a : ℕ → ℂ
n : ℕ
hn : n ≠ 0
h : 0 < a n
x : ℝ
⊢ 0 < term a (↑x) n

Tactic:
simpa only [term_of_ne_zero hn] using mul_pos h <| inv_natCast_cpow_ofReal_pos hn x

Result:
no goals
-- Mathlib/Algebra/Homology/BifunctorAssociator.lean
@[reassoc (attr := simp)]
lemma ι_mapBifunctor₂₃Desc (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃)
    (h : ComplexShape.r c₁ c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) :
    ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h ≫ mapBifunctor₂₃Desc c₁₂ f =
      f i₁ i₂ i₃ h

Proof state:
C₁ : Type u_1
C₂ : Type u_2
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝²³ : Category.{u_15, u_1} C₁
inst✝²² : Category.{u_17, u_2} C₂
inst✝²¹ : Category.{u_16, u_5} C₃
inst✝²⁰ : Category.{u_13, u_6} C₄
inst✝¹⁹ : Category.{u_14, u_4} C₂₃
inst✝¹⁸ : HasZeroMorphisms C₁
inst✝¹⁷ : HasZeroMorphisms C₂
inst✝¹⁶ : HasZeroMorphisms C₃
inst✝¹⁵ : Preadditive C₂₃
inst✝¹⁴ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹³ : G₂₃.PreservesZeroMorphisms
inst✝¹² : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹¹ : F.PreservesZeroMorphisms
inst✝¹⁰ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁹ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁸ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁷ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁶ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁵ : TotalComplexShape c₁ c₂₃ c₄
inst✝⁴ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝³ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝² : DecidableEq ι₂₃
inst✝¹ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j : ι₄
A : C₄
f :
  (i₁ : ι₁) →
    (i₂ : ι₂) →
      (i₃ : ι₃) → c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j → ((F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶ A)
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
⊢ ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h ≫ mapBifunctor₂₃Desc c₁₂ f = f i₁ i₂ i₃ h

Tactic:
apply GradedObject.ι_mapBifunctorBifunctor₂₃Desc

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem length_insertIdx_of_le_length (h : n ≤ length as) : length (insertIdx n a as) = length as + 1

Proof state:
α : Type u
a : α
n : Nat
as : List α
h : n ≤ as.length
⊢ (insertIdx n a as).length = as.length + 1

Tactic:
simp [length_insertIdx, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem sub_nonpos_of_le {a b : Int} (h : a ≤ b) : a - b ≤ 0

Proof state:
a b : Int
h : a ≤ b
⊢ a - b ≤ 0

Tactic:
have h := Int.add_le_add_right h (-b)

Result:
a b : Int
h✝ : a ≤ b
h : a + -b ≤ b + -b
⊢ a - b ≤ 0

Proof state:
a b : Int
h✝ : a ≤ b
h : a + -b ≤ b + -b
⊢ a - b ≤ 0

Tactic:
rwa [Int.add_right_neg] at h

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem length_rotate (l : List α) (n : ℕ) : (l.rotate n).length = l.length

Proof state:
α : Type u
l : List α
n : ℕ
⊢ (l.rotate n).length = l.length

Tactic:
rw [rotate_eq_rotate', length_rotate']

Result:
no goals
-- Mathlib/AlgebraicGeometry/Stalk.lean
lemma stalkClosedPointTo_comp (g : X ⟶ Y) :
    stalkClosedPointTo (f ≫ g) = g.stalkMap _ ≫ stalkClosedPointTo f

Proof state:
X Y : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
g : X ⟶ Y
⊢ (Hom.stalkMap g ((ConcreteCategory.hom f.base) (closedPoint ↑R)) ≫ Hom.stalkMap f (closedPoint ↑R)) ≫
      (stalkClosedPointIso R).hom =
    Hom.stalkMap g ((ConcreteCategory.hom f.base) (closedPoint ↑R)) ≫ stalkClosedPointTo f

Tactic:
exact Category.assoc _ _ _

Result:
no goals

Proof state:
X Y : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
g : X ⟶ Y
⊢ stalkClosedPointTo (f ≫ g) = Hom.stalkMap g ((ConcreteCategory.hom f.base) (closedPoint ↑R)) ≫ stalkClosedPointTo f

Tactic:
rw [stalkClosedPointTo, Scheme.stalkMap_comp]

Result:
X Y : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
g : X ⟶ Y
⊢ (Hom.stalkMap g ((ConcreteCategory.hom f.base) (closedPoint ↑R)) ≫ Hom.stalkMap f (closedPoint ↑R)) ≫
      (stalkClosedPointIso R).hom =
    Hom.stalkMap g ((ConcreteCategory.hom f.base) (closedPoint ↑R)) ≫ stalkClosedPointTo f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem boole_getElem_le_count (a : α) (l : Vector α n) (i : Nat) (h : i < n) :
    (if l[i] == a then 1 else 0) ≤ l.count a

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a : α
i : Nat
l : Array α
h : i < l.size
⊢ (if ({ toArray := l, size_toArray := ⋯ }[i] == a) = true then 1 else 0) ≤ count a { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.boole_getElem_le_count, h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
n : Nat
a : α
l : Vector α n
i : Nat
h : i < n
⊢ (if (l[i] == a) = true then 1 else 0) ≤ count a l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
a : α
i : Nat
l : Array α
h : i < l.size
⊢ (if ({ toArray := l, size_toArray := ⋯ }[i] == a) = true then 1 else 0) ≤ count a { toArray := l, size_toArray := ⋯ }
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem mem_sSup {s : Set (Submodule R M)} {m : M} :
    (m ∈ sSup s) ↔ ∀ N, (∀ p ∈ s, p ≤ N) → m ∈ N

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
m : M
⊢ m ∈ sSup s ↔ ∀ (N : Submodule R M), (∀ p ∈ s, p ≤ N) → m ∈ N

Tactic:
simp_rw [sSup_eq_iSup, Submodule.mem_iSup, iSup_le_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem Bool.not_eq_of_eq_false {a : Bool} (h : a = false) : (!a) = true

Proof state:
a : Bool
h : a = false
⊢ (!a) = true

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem toReal_le_toReal {x y : EReal} (h : x ≤ y) (hx : x ≠ ⊥) (hy : y ≠ ⊤) :
    x.toReal ≤ y.toReal

Proof state:
x y : EReal
h : x ≤ y
hx : x ≠ ⊥
hy : y ≠ ⊤
⊢ x.toReal ≤ y.toReal

Tactic:
lift x to ℝ using ⟨ne_top_of_le_ne_top hy h, hx⟩

Result:
case intro
y : EReal
hy : y ≠ ⊤
x : ℝ
h : ↑x ≤ y
hx : ↑x ≠ ⊥
⊢ (↑x).toReal ≤ y.toReal

Proof state:
case intro.intro
x : ℝ
hx : ↑x ≠ ⊥
y : ℝ
hy : ↑y ≠ ⊤
h : ↑x ≤ ↑y
⊢ (↑x).toReal ≤ (↑y).toReal

Tactic:
simpa using h

Result:
no goals

Proof state:
case intro
y : EReal
hy : y ≠ ⊤
x : ℝ
h : ↑x ≤ y
hx : ↑x ≠ ⊥
⊢ (↑x).toReal ≤ y.toReal

Tactic:
lift y to ℝ using ⟨hy, ne_bot_of_le_ne_bot hx h⟩

Result:
case intro.intro
x : ℝ
hx : ↑x ≠ ⊥
y : ℝ
hy : ↑y ≠ ⊤
h : ↑x ≤ ↑y
⊢ (↑x).toReal ≤ (↑y).toReal
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem exists_associated_pow_of_associated_pow_mul {a b c : R} (hab : IsCoprime a b) {k : ℕ}
    (h : Associated (c ^ k) (a * b)) : ∃ d : R, Associated (d ^ k) a

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
a b c : R
hab : IsCoprime a b
k : ℕ
h : Associated (c ^ k) (a * b)
⊢ ∃ d, Associated (d ^ k) a

Tactic:
obtain ⟨u, hu⟩ := h.symm

Result:
case intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
a b c : R
hab : IsCoprime a b
k : ℕ
h : Associated (c ^ k) (a * b)
u : Rˣ
hu : a * b * ↑u = c ^ k
⊢ ∃ d, Associated (d ^ k) a

Proof state:
case intro
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
a b c : R
hab : IsCoprime a b
k : ℕ
h : Associated (c ^ k) (a * b)
u : Rˣ
hu : a * b * ↑u = c ^ k
⊢ ∃ d, Associated (d ^ k) a

Tactic:
exact exists_associated_pow_of_mul_eq_pow'
  ((isCoprime_mul_unit_right_right u.isUnit a b).mpr hab) <| mul_assoc a _ _ ▸ hu

Result:
no goals
-- Mathlib/Analysis/Convex/Segment.lean
theorem segment_same (x : E) : [x -[𝕜] x] = {x} :=
  Set.ext fun z =>
    ⟨fun ⟨a, b, _, _, hab, hz⟩ => by
      simpa only [(add_smul _ _ _).symm, mem_singleton_iff, hab, one_smul, eq_comm] using hz,
      fun h => mem_singleton_iff.1 h ▸ left_mem_segment 𝕜 z z⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
x z : E
x✝ : z ∈ [x-[𝕜]x]
a b : 𝕜
left✝¹ : 0 ≤ a
left✝ : 0 ≤ b
hab : a + b = 1
hz : a • x + b • x = z
⊢ z ∈ {x}

Tactic:
simpa only [(add_smul _ _ _).symm, mem_singleton_iff, hab, one_smul, eq_comm] using hz

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem eta (f : R[X]) : Polynomial.ofFinsupp f.toFinsupp = f

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
toFinsupp✝ : R[ℕ]
⊢ { toFinsupp := { toFinsupp := toFinsupp✝ }.toFinsupp } = { toFinsupp := toFinsupp✝ }

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
⊢ { toFinsupp := f.toFinsupp } = f

Tactic:
cases f

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
toFinsupp✝ : R[ℕ]
⊢ { toFinsupp := { toFinsupp := toFinsupp✝ }.toFinsupp } = { toFinsupp := toFinsupp✝ }
-- Mathlib/Analysis/RCLike/Basic.lean
theorem smul_im (r : ℝ) (z : K) : im (r • z) = r * im z

Proof state:
K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ im (r • z) = r * im z

Tactic:
rw [real_smul_eq_coe_mul, im_ofReal_mul]

Result:
no goals
-- Mathlib/Data/Nat/Find.lean
lemma findGreatest_spec (hmb : m ≤ n) (hm : P m) : P (Nat.findGreatest P n)

Proof state:
case pos
m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : findGreatest P n = 0
⊢ P (findGreatest P n)

Tactic:
cases m

Result:
case pos.zero
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : findGreatest P n = 0
hmb : 0 ≤ n
hm : P 0
⊢ P (findGreatest P n)

case pos.succ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : findGreatest P n = 0
n✝ : ℕ
hmb : n✝ + 1 ≤ n
hm : P (n✝ + 1)
⊢ P (findGreatest P n)

Proof state:
case neg
m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : ¬findGreatest P n = 0
⊢ P (findGreatest P n)

Tactic:
exact (findGreatest_eq_iff.1 rfl).2.1 h

Result:
no goals

Proof state:
m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
⊢ P (findGreatest P n)

Tactic:
by_cases h : Nat.findGreatest P n = 0

Result:
case pos
m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : findGreatest P n = 0
⊢ P (findGreatest P n)

case neg
m : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : ¬findGreatest P n = 0
⊢ P (findGreatest P n)

Proof state:
case pos.zero
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : findGreatest P n = 0
hmb : 0 ≤ n
hm : P 0
⊢ P (findGreatest P n)

Tactic:
rwa [h]

Result:
no goals

Proof state:
case pos.succ
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : findGreatest P n = 0
n✝ : ℕ
hmb : n✝ + 1 ≤ n
hm : P (n✝ + 1)
⊢ P (findGreatest P n)

Tactic:
exact ((findGreatest_eq_zero_iff.1 h) (zero_lt_succ _) hmb hm).elim

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem if_ctx_congr (h_c : P ↔ Q) (h_t : Q → x = u) (h_e : ¬Q → y = v) : ite P x y = ite Q u v :=
  match ‹Decidable P›, ‹Decidable Q› with
  | isFalse _,  isFalse h₂ => by simp_all
  | isTrue _,   isTrue h₂  => by simp_all
  | isFalse h₁, isTrue h₂  => absurd h₂ (Iff.mp (not_congr h_c) h₁)
  | isTrue h₁,  isFalse h₂ => absurd h₁ (Iff.mpr (not_congr h_c) h₂)

Proof state:
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
x y u v : α
h_c : P ↔ Q
h_t : Q → x = u
h_e : ¬Q → y = v
h✝ : ¬P
h₂ : ¬Q
⊢ (if P then x else y) = if Q then u else v

Tactic:
simp_all

Result:
no goals

Proof state:
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
inst✝ : Decidable Q
x y u v : α
h_c : P ↔ Q
h_t : Q → x = u
h_e : ¬Q → y = v
h✝ : P
h₂ : Q
⊢ (if P then x else y) = if Q then u else v

Tactic:
simp_all

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.im (hf : Integrable f μ) : Integrable (fun x => RCLike.im (f x)) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f 1 μ
⊢ MemLp (fun x => RCLike.im (f x)) 1 μ

Tactic:
exact hf.im

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : Integrable f μ
⊢ Integrable (fun x => RCLike.im (f x)) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
𝕜 : Type u_6
inst✝ : RCLike 𝕜
f : α → 𝕜
hf : MemLp f 1 μ
⊢ MemLp (fun x => RCLike.im (f x)) 1 μ
-- Mathlib/Algebra/Ring/Defs.lean
theorem mul_one_add [LeftDistribClass α] (a b : α) : a * (1 + b) = a + a * b

Proof state:
α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : LeftDistribClass α
a b : α
⊢ a * (1 + b) = a + a * b

Tactic:
rw [mul_add, mul_one]

Result:
no goals
-- Mathlib/Analysis/Analytic/IsolatedZeros.lean
theorem iterate_dslope_fslope_ne_zero (hp : HasFPowerSeriesAt f p z₀) (h : p ≠ 0) :
    (swap dslope z₀)^[p.order] f z₀ ≠ 0

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ (swap dslope z₀)^[p.order] f z₀ ≠ 0

Tactic:
rw [← coeff_zero (has_fpower_series_iterate_dslope_fslope p.order hp) 1]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ (fslope^[p.order] p 0) 1 ≠ 0

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hp : HasFPowerSeriesAt f p z₀
h : p ≠ 0
⊢ (fslope^[p.order] p 0) 1 ≠ 0

Tactic:
simpa [coeff_eq_zero] using apply_order_ne_zero h

Result:
no goals
-- Mathlib/Algebra/Lie/Abelian.lean
theorem toLinearMap_maxTrivLinearMapEquivLieModuleHom (f : maxTrivSubmodule R L (M →ₗ[R] N)) :
    (maxTrivLinearMapEquivLieModuleHom (M := M) (N := N) f : M →ₗ[R] N) = (f : M →ₗ[R] N)

Proof state:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
⊢ ↑(maxTrivLinearMapEquivLieModuleHom f) = ↑f

Tactic:
ext

Result:
case h
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
x✝ : M
⊢ ↑(maxTrivLinearMapEquivLieModuleHom f) x✝ = ↑f x✝

Proof state:
case h
R : Type u
L : Type v
M : Type w
N : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : LieRingModule L N
inst✝ : LieModule R L N
f : ↥(maxTrivSubmodule R L (M →ₗ[R] N))
x✝ : M
⊢ ↑(maxTrivLinearMapEquivLieModuleHom f) x✝ = ↑f x✝

Tactic:
rfl

Result:
no goals