harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem getElem?_take {l : List α} {n m : Nat} :
    (l.take n)[m]? = if m < n then l[m]? else none

Proof state:
case isFalse
α : Type u_1
l : List α
n m : Nat
h✝ : ¬m < n
⊢ (take n l)[m]? = none

Tactic:
next h => exact getElem?_take_eq_none (Nat.le_of_not_lt h)

Result:
no goals

Proof state:
α : Type u_1
l : List α
n m : Nat
h : m < n
⊢ (take n l)[m]? = l[m]?

Tactic:
exact getElem?_take_of_lt h

Result:
no goals

Proof state:
case isTrue
α : Type u_1
l : List α
n m : Nat
h✝ : m < n
⊢ (take n l)[m]? = l[m]?

Tactic:
next h => exact getElem?_take_of_lt h

Result:
no goals

Proof state:
α : Type u_1
l : List α
n m : Nat
⊢ (take n l)[m]? = if m < n then l[m]? else none

Tactic:
split

Result:
case isTrue
α : Type u_1
l : List α
n m : Nat
h✝ : m < n
⊢ (take n l)[m]? = l[m]?

case isFalse
α : Type u_1
l : List α
n m : Nat
h✝ : ¬m < n
⊢ (take n l)[m]? = none

Proof state:
α : Type u_1
l : List α
n m : Nat
h : ¬m < n
⊢ (take n l)[m]? = none

Tactic:
exact getElem?_take_eq_none (Nat.le_of_not_lt h)

Result:
no goals
-- Mathlib/AlgebraicGeometry/Spec.lean
theorem Spec.sheafedSpaceMap_comp {R S T : CommRingCat.{u}} (f : R ⟶ S) (g : S ⟶ T) :
    Spec.sheafedSpaceMap (f ≫ g) = Spec.sheafedSpaceMap g ≫ Spec.sheafedSpaceMap f :=
  AlgebraicGeometry.PresheafedSpace.Hom.ext _ _ (Spec.topMap_comp f g) <| by
    ext
    -- Porting note: was one liner
    -- `dsimp, rw category_theory.functor.map_id, rw category.comp_id, erw comap_comp f g, refl`
    rw [NatTrans.comp_app, sheafedSpaceMap_c_app, whiskerRight_app, eqToHom_refl]
    erw [(sheafedSpaceObj T).presheaf.map_id]
    dsimp only [CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply]
    rw [comap_comp]
    rfl

Proof state:
case w.hf.a
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (comap (CommRingCat.Hom.hom (f ≫ g)) (unop (op U✝))
              ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj (unop (op U✝))) ⋯) ≫
          (sheafedSpaceObj T).presheaf.map
            ((𝟙 (TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).base).op).app (op U✝))))
      x✝ =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).c.app (op U✝))) x✝

Tactic:
erw [(sheafedSpaceObj T).presheaf.map_id]

Result:
case w.hf.a
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (comap (CommRingCat.Hom.hom (f ≫ g)) (unop (op U✝))
              ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj (unop (op U✝))) ⋯) ≫
          𝟙
            ((sheafedSpaceObj T).presheaf.obj
              ((TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).base).op.obj (op U✝)))))
      x✝ =
    (CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).c.app (op U✝))) x✝
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycleFactorsFinset_eq_list_toFinset {σ : Perm α} {l : List (Perm α)} (hn : l.Nodup) :
    σ.cycleFactorsFinset = l.toFinset ↔
      (∀ f : Perm α, f ∈ l → f.IsCycle) ∧ l.Pairwise Disjoint ∧ l.prod = σ

Proof state:
case intro.mk.intro.intro.mpr.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
hc : ∀ f ∈ l, f.IsCycle
hd : List.Pairwise Disjoint l
hp : l.prod = σ
⊢ l' ~ l

Tactic:
refine list_cycles_perm_list_cycles ?_ hc' hc hd' hd

Result:
case intro.mk.intro.intro.mpr.intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
hc : ∀ f ∈ l, f.IsCycle
hd : List.Pairwise Disjoint l
hp : l.prod = σ
⊢ l'.prod = l.prod
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_eq_iSup_sum' {ι : Type*} (s : ι → Finset α) (hs : ∀ t, ∃ i, t ⊆ s i) :
    ∑' a, f a = ⨆ i, ∑ a ∈ s i, f a

Proof state:
α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ ⨆ i, (fun t => ∑ a ∈ t, f a) (s i) = ⨆ s, ∑ a ∈ s, f a

Tactic:
exact (Finset.sum_mono_set f).iSup_comp_eq hs

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ ∑' (a : α), f a = ⨆ i, ∑ a ∈ s i, f a

Tactic:
rw [ENNReal.tsum_eq_iSup_sum]

Result:
α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ ⨆ s, ∑ a ∈ s, f a = ⨆ i, ∑ a ∈ s i, f a

Proof state:
α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ ⨆ i, ∑ a ∈ s i, f a = ⨆ s, ∑ a ∈ s, f a

Tactic:
change ⨆ i : ι, (fun t : Finset α => ∑ a ∈ t, f a) (s i) = ⨆ s : Finset α, ∑ a ∈ s, f a

Result:
α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ ⨆ i, (fun t => ∑ a ∈ t, f a) (s i) = ⨆ s, ∑ a ∈ s, f a

Proof state:
α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ ⨆ s, ∑ a ∈ s, f a = ⨆ i, ∑ a ∈ s i, f a

Tactic:
symm

Result:
α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ i, t ⊆ s i
⊢ ⨆ i, ∑ a ∈ s i, f a = ⨆ s, ∑ a ∈ s, f a
-- Mathlib/Analysis/MeanInequalities.lean
theorem geom_mean_le_arith_mean4_weighted (w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ≥0) :
    w₁ + w₂ + w₃ + w₄ = 1 →
      p₁ ^ (w₁ : ℝ) * p₂ ^ (w₂ : ℝ) * p₃ ^ (w₃ : ℝ) * p₄ ^ (w₄ : ℝ) ≤
        w₁ * p₁ + w₂ * p₂ + w₃ * p₃ + w₄ * p₄

Proof state:
w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ≥0
⊢ w₁ + w₂ + w₃ + w₄ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ * p₃ ^ ↑w₃ * p₄ ^ ↑w₄ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃ + w₄ * p₄

Tactic:
simpa only [Fin.prod_univ_succ, Fin.sum_univ_succ, Finset.prod_empty, Finset.sum_empty,
  Finset.univ_eq_empty, Fin.cons_succ, Fin.cons_zero, add_zero, mul_one, ← add_assoc,
  mul_assoc] using geom_mean_le_arith_mean_weighted univ ![w₁, w₂, w₃, w₄] ![p₁, p₂, p₃, p₄]

Result:
no goals
-- Mathlib/Data/ENat/Lattice.lean
lemma iSup_add_iSup_le [Nonempty ι] [Nonempty κ] {g : κ → ℕ∞} (h : ∀ i j, f i + g j ≤ a) :
    iSup f + iSup g ≤ a

Proof state:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ iSup f + iSup g ≤ a

Tactic:
simp_rw [iSup_add, add_iSup]

Result:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ ⨆ i, ⨆ i_1, f i + g i_1 ≤ a

Proof state:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ ⨆ i, ⨆ i_1, f i + g i_1 ≤ a

Tactic:
exact iSup₂_le h

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma map₂_snd {Y : C} (f : X ⟶ Y) (p : YonedaCollection F Y) :
    (YonedaCollection.map₂ F f p).snd = F.map ((CostructuredArrow.mkPrecomp p.fst f).op ≫
      eqToHom (by rw [YonedaCollection.map₂_fst f])) p.snd

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ op (CostructuredArrow.mk (yoneda.map f ≫ p.fst)) = op (CostructuredArrow.mk (map₂ F f p).fst)

Tactic:
rw [YonedaCollection.map₂_fst f]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ (map₂ F f p).snd = F.map ((CostructuredArrow.mkPrecomp p.fst f).op ≫ eqToHom ⋯) p.snd

Tactic:
simp [map₂]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_neg_neg (x y : V) : o.oangle (-x) (-y) = o.oangle x y

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle (-x) (-y) = o.oangle x y

Tactic:
simp [oangle]

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
lemma isIso_iff_coyoneda_map_bijective {X Y : C} (f : X ⟶ Y) :
    IsIso f ↔ (∀ (T : C), Function.Bijective (fun (x : Y ⟶ T) => f ≫ x))

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
this : IsIso (coyoneda.map f.op)
T : C
⊢ IsIso fun x => f ≫ x

Tactic:
exact inferInstanceAs (IsIso ((coyoneda.map f.op).app _))

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
⊢ ∀ (T : C), Function.Bijective fun x => f ≫ x

Tactic:
have : IsIso (coyoneda.map f.op) := inferInstance

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
this : IsIso (coyoneda.map f.op)
⊢ ∀ (T : C), Function.Bijective fun x => f ≫ x

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ IsIso f ↔ ∀ (T : C), Function.Bijective fun x => f ≫ x

Tactic:
refine ⟨fun _ ↦ ?_, fun hf ↦ isIso_of_coyoneda_map_bijective f hf⟩

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
⊢ ∀ (T : C), Function.Bijective fun x => f ≫ x

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
this : IsIso (coyoneda.map f.op)
⊢ ∀ (T : C), Function.Bijective fun x => f ≫ x

Tactic:
intro T

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
this : IsIso (coyoneda.map f.op)
T : C
⊢ Function.Bijective fun x => f ≫ x

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
this : IsIso (coyoneda.map f.op)
T : C
⊢ Function.Bijective fun x => f ≫ x

Tactic:
rw [← isIso_iff_bijective]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
x✝ : IsIso f
this : IsIso (coyoneda.map f.op)
T : C
⊢ IsIso fun x => f ≫ x
-- Mathlib/Order/SupClosed.lean
@[simp] lemma isGLB_infClosure : IsGLB (infClosure s) a ↔ IsGLB s a

Proof state:
α : Type u_3
inst✝ : SemilatticeInf α
s : Set α
a : α
⊢ IsGLB (infClosure s) a ↔ IsGLB s a

Tactic:
simp [IsGLB]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_map_erase [DecidableEq ι] {a : ι} (h : a ∈ m) :
    f a * ((m.erase a).map f).prod = (m.map f).prod

Proof state:
ι : Type u_2
α : Type u_3
inst✝¹ : CommMonoid α
m : Multiset ι
f : ι → α
inst✝ : DecidableEq ι
a : ι
h : a ∈ m
⊢ f a * (map f (m.erase a)).prod = (map f m).prod

Tactic:
rw [← m.coe_toList, coe_erase, map_coe, map_coe, prod_coe, prod_coe,
  List.prod_map_erase f (mem_toList.2 h)]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
theorem min_lt_of_mul_lt_sq {a b c : M} (h : a * b < c ^ 2) : min a b < c

Proof state:
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
a b c : M
h : a * b < c ^ 2
⊢ a ⊓ b < c

Tactic:
simpa using min_lt_max_of_mul_lt_mul (h.trans_eq <| pow_two _)

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem zero_dotProduct : 0 ⬝ᵥ v = 0

Proof state:
m : Type u_2
α : Type v
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
⊢ 0 ⬝ᵥ v = 0

Tactic:
simp [dotProduct]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
lemma eq_zero_or_isProbabilityMeasure : μ = 0 ∨ IsProbabilityMeasure μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
⊢ μ = 0 ∨ IsProbabilityMeasure μ

Tactic:
rcases IsZeroOrProbabilityMeasure.measure_univ (μ := μ) with h | h

Result:
case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
h : μ univ = 0
⊢ μ = 0 ∨ IsProbabilityMeasure μ

case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
h : μ univ = 1
⊢ μ = 0 ∨ IsProbabilityMeasure μ

Proof state:
case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
h : μ univ = 0
⊢ μ = 0 ∨ IsProbabilityMeasure μ

Tactic:
apply Or.inl (measure_univ_eq_zero.mp h)

Result:
no goals

Proof state:
case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsZeroOrProbabilityMeasure μ
h : μ univ = 1
⊢ μ = 0 ∨ IsProbabilityMeasure μ

Tactic:
exact Or.inr ⟨h⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_add_left {f : α → ℝ≥0∞} (hf : Measurable f) (g : α → ℝ≥0∞) :
    μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (f + g)) s = (μ.withDensity f + μ.withDensity g) s

Tactic:
rw [withDensity_apply _ hs, Measure.add_apply, withDensity_apply _ hs, withDensity_apply _ hs,
  ← lintegral_add_left hf]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (f + g) a ∂μ = ∫⁻ (a : α) in s, f a + g a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (a : α) in s, (f + g) a ∂μ = ∫⁻ (a : α) in s, f a + g a ∂μ

Tactic:
simp only [Pi.add_apply]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
⊢ μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g

Tactic:
refine Measure.ext fun s hs => ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (μ.withDensity (f + g)) s = (μ.withDensity f + μ.withDensity g) s
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem univ_sum_single_apply' [AddCommMonoid M] [Fintype α] (i : α) (m : M) :
    ∑ j : α, single j m i = m

Proof state:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ x : α, Pi.single x m i = m

Tactic:
rw [Finset.sum_pi_single]

Result:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m

Proof state:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ j : α, (single j m) i = m

Tactic:
simp_rw [single, coe_mk]

Result:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ x : α, Pi.single x m i = m

Proof state:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ ∑ x : α, Pi.single x m i = m

Tactic:
classical rw [Finset.sum_pi_single]

Result:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
inst✝ : Fintype α
i : α
m : M
⊢ (if i ∈ univ then m else 0) = m
-- Mathlib/Topology/MetricSpace/Contracting.lean
theorem efixedPoint_eq_of_edist_lt_top' (hf : ContractingWith K f) {s : Set α} (hsc : IsComplete s)
    (hsf : MapsTo f s s) (hfs : ContractingWith K <| hsf.restrict f s s) {x : α} (hxs : x ∈ s)
    (hx : edist x (f x) ≠ ∞) {t : Set α} (htc : IsComplete t) (htf : MapsTo f t t)
    (hft : ContractingWith K <| htf.restrict f t t) {y : α} (hyt : y ∈ t) (hy : edist y (f y) ≠ ∞)
    (hxy : edist x y ≠ ∞) :
    efixedPoint' f hsc hsf hfs x hxs hx = efixedPoint' f htc htf hft y hyt hy

Proof state:
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ edistLtTopSetoid x y

Tactic:
exact lt_top_iff_ne_top.2 hxy

Result:
no goals

Proof state:
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ edistLtTopSetoid x (efixedPoint' f htc htf hft y hyt hy)

Tactic:
trans y

Result:
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ edistLtTopSetoid x y

α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hfs : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
t : Set α
htc : IsComplete t
htf : MapsTo f t t
hft : ContractingWith K (MapsTo.restrict f t t htf)
y : α
hyt : y ∈ t
hy : edist y (f y) ≠ ⊤
hxy : edist x y ≠ ⊤
h' : edist (efixedPoint' f hsc hsf hfs x hxs hx) (efixedPoint' f htc htf hft y hyt hy) = ⊤
⊢ edistLtTopSetoid y (efixedPoint' f htc htf hft y hyt hy)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β k} :
    (m.insertIfNew k v).contains a = (k == a || m.contains a)

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
v : β k
⊢ (m.insertIfNew k v).contains a = (k == a || m.contains a)

Tactic:
simp_to_model [insertIfNew] using List.containsKey_insertEntryIfNew

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem coeff_C_mul_X_pow (x : R) (k n : ℕ) :
    coeff R n (C R x * X ^ k : R⟦X⟧) = if n = k then x else 0

Proof state:
R : Type u_1
inst✝ : Semiring R
x : R
k n : ℕ
⊢ (coeff R n) ((C R) x * X ^ k) = if n = k then x else 0

Tactic:
simp [X_pow_eq, coeff_monomial]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_negDblY (P : Fin 3 → A) : (W'.baseChange B).toProjective.negDblY (f ∘ P) =
    f ((W'.baseChange A).toProjective.negDblY P)

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P : Fin 3 → A
⊢ (baseChange W' B).toProjective.negDblY (⇑f ∘ P) = f ((baseChange W' A).toProjective.negDblY P)

Tactic:
rw [← RingHom.coe_coe, ← map_negDblY, map_baseChange]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
/-- Binary **rearrangement inequality**. -/
lemma smul_add_smul_le_smul_add_smul (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) :
    a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : StrictOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ ≤ b₂
a : α
ha₀ : 0 ≤ a
ha : a₁ ≤ a₁ + a
⊢ a₁ • b₁ + (a₁ • b₂ + a • b₁) ≤ a₁ • b₁ + (a₁ • b₂ + a • b₂)

Tactic:
gcongr

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : StrictOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ ≤ b₂
a : α
ha₀ : 0 ≤ a
ha : a₁ ≤ a₁ + a
⊢ a₁ • b₂ + (a₁ + a) • b₁ ≤ a₁ • b₁ + (a₁ + a) • b₂

Tactic:
rw [add_smul, add_smul, add_left_comm]

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : StrictOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ ≤ b₂
a : α
ha₀ : 0 ≤ a
ha : a₁ ≤ a₁ + a
⊢ a₁ • b₁ + (a₁ • b₂ + a • b₁) ≤ a₁ • b₁ + (a₁ • b₂ + a • b₂)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : StrictOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂

Tactic:
obtain ⟨a, ha₀, rfl⟩ := exists_nonneg_add_of_le ha

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁴ : StrictOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ : α
b₁ b₂ : β
hb : b₁ ≤ b₂
a : α
ha₀ : 0 ≤ a
ha : a₁ ≤ a₁ + a
⊢ a₁ • b₂ + (a₁ + a) • b₁ ≤ a₁ • b₁ + (a₁ + a) • b₂
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_subset_ge_of_subset_image (f : α → β) {s : Set α} {t : Set β} (h : t ⊆ f '' s) :
    #t ≤ #({ x ∈ s | f x ∈ t } : Set α)

Proof state:
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ #↑t ≤ #↑{x | x ∈ s ∧ f x ∈ t}

Tactic:
convert mk_preimage_of_subset_range _ _ h using 1

Result:
case h.e'_4
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ #↑{x | x ∈ s ∧ f x ∈ t} = #↑((fun x => f ↑x) ⁻¹' t)

Proof state:
case h.e'_4
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ #↑{x | x ∈ s ∧ f x ∈ t} = #↑((fun x => f ↑x) ⁻¹' t)

Tactic:
rw [mk_sep]

Result:
case h.e'_4
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ #↑{x | f ↑x ∈ t} = #↑((fun x => f ↑x) ⁻¹' t)

Proof state:
case h.e'_4
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ #↑{x | f ↑x ∈ t} = #↑((fun x => f ↑x) ⁻¹' t)

Tactic:
rfl

Result:
no goals

Proof state:
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
⊢ #↑t ≤ #↑{x | x ∈ s ∧ f x ∈ t}

Tactic:
rw [image_eq_range] at h

Result:
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ #↑t ≤ #↑{x | x ∈ s ∧ f x ∈ t}