harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Filter/Prod.lean
theorem coprod_eq_prod_top_sup_top_prod (f : Filter α) (g : Filter β) :
    Filter.coprod f g = f ×ˢ ⊤ ⊔ ⊤ ×ˢ g

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f.coprod g = comap Prod.fst f ⊔ comap Prod.snd g

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f.coprod g = f ×ˢ ⊤ ⊔ ⊤ ×ˢ g

Tactic:
rw [prod_top, top_prod]

Result:
α : Type u_1
β : Type u_2
f : Filter α
g : Filter β
⊢ f.coprod g = comap Prod.fst f ⊔ comap Prod.snd g
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem sum_ite_eq' {N : Type*} [AddCommMonoid N] [DecidableEq G] (f : SkewMonoidAlgebra k G)
    (a : G) (b : G → k → N) : (f.sum fun (x : G) (v : k) ↦ if x = a then b x v else 0) =
      if a ∈ f.support then b a (f.coeff a) else 0

Proof state:
k : Type u_1
G : Type u_2
inst✝² : AddCommMonoid k
N : Type u_3
inst✝¹ : AddCommMonoid N
inst✝ : DecidableEq G
f : SkewMonoidAlgebra k G
a : G
b : G → k → N
⊢ (f.sum fun x v => if x = a then b x v else 0) = if a ∈ f.support then b a (f.coeff a) else 0

Tactic:
simp only [sum_def', Finsupp.sum, f.toFinsupp.support.sum_ite_eq', support]

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
@[simp] lemma toLeft_map_sumComm : (u.map (Equiv.sumComm _ _).toEmbedding).toLeft = u.toRight

Proof state:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ (map (Equiv.sumComm α β).toEmbedding u).toLeft = u.toRight

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : β
⊢ x ∈ (map (Equiv.sumComm α β).toEmbedding u).toLeft ↔ x ∈ u.toRight

Proof state:
case h
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : β
⊢ x ∈ (map (Equiv.sumComm α β).toEmbedding u).toLeft ↔ x ∈ u.toRight

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem eq_liftOfRightInverse (hf : Function.RightInverse f_inv f) (g : A →+* C)
    (hg : RingHom.ker f ≤ RingHom.ker g) (h : B →+* C) (hh : h.comp f = g) :
    h = f.liftOfRightInverse f_inv hf ⟨g, hg⟩

Proof state:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
h : B →+* C
hh : h.comp f = g
⊢ h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩

Tactic:
simp_rw [← hh]

Result:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
h : B →+* C
hh : h.comp f = g
⊢ h = (f.liftOfRightInverse f_inv hf) ⟨h.comp f, ⋯⟩

Proof state:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
h : B →+* C
hh : h.comp f = g
⊢ h = (f.liftOfRightInverse f_inv hf) ⟨h.comp f, ⋯⟩

Tactic:
exact ((f.liftOfRightInverse f_inv hf).apply_symm_apply _).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_eq_get [LawfulBEq α] (h : m.WF) {a : α} {h} : get m a h = m.get a h

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝ : LawfulBEq α
h✝ : m.WF
a : α
h : a ∈ m
⊢ get m a h = m.get a h

Tactic:
simp_to_raw using Raw₀.Const.get_eq_get

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem writtenInExtChartAt_chartAt_symm_comp [ChartedSpace H H'] (x : M') {y}
    (hy : y ∈ letI := ChartedSpace.comp H H' M'; (extChartAt I x).target) :
    ( letI := ChartedSpace.comp H H' M'
      writtenInExtChartAt I I (chartAt H' x x) (chartAt H' x).symm y) = y

Proof state:
𝕜 : Type u_1
E : Type u_2
H : Type u_4
M' : Type u_6
H' : Type u_7
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H H'
x : M'
y : E
hy : y ∈ (extChartAt I x).target
this : ChartedSpace H M' := ChartedSpace.comp H H' M'
⊢ writtenInExtChartAt I I (↑(chartAt H' x) x) (↑(chartAt H' x).symm) y = y

Tactic:
simp_all only [mfld_simps, chartAt_comp]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
H : Type u_4
M' : Type u_6
H' : Type u_7
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H H'
x : M'
y : E
hy : y ∈ (extChartAt I x).target
⊢ writtenInExtChartAt I I (↑(chartAt H' x) x) (↑(chartAt H' x).symm) y = y

Tactic:
letI := ChartedSpace.comp H H' M'

Result:
𝕜 : Type u_1
E : Type u_2
H : Type u_4
M' : Type u_6
H' : Type u_7
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
inst✝³ : TopologicalSpace H'
inst✝² : TopologicalSpace M'
inst✝¹ : ChartedSpace H' M'
inst✝ : ChartedSpace H H'
x : M'
y : E
hy : y ∈ (extChartAt I x).target
this : ChartedSpace H M' := ChartedSpace.comp H H' M'
⊢ writtenInExtChartAt I I (↑(chartAt H' x) x) (↑(chartAt H' x).symm) y = y
-- Mathlib/MeasureTheory/PiSystem.lean
theorem IsPiSystem.singleton (S : Set α) : IsPiSystem ({S} : Set (Set α))

Proof state:
α : Type u_1
S s : Set α
h_s : s ∈ {S}
t : Set α
h_t : t ∈ {S}
a✝ : (s ∩ t).Nonempty
⊢ s ∩ t ∈ {S}

Tactic:
rw [Set.mem_singleton_iff.1 h_s, Set.mem_singleton_iff.1 h_t, Set.inter_self,
  Set.mem_singleton_iff]

Result:
no goals

Proof state:
α : Type u_1
S : Set α
⊢ IsPiSystem {S}

Tactic:
intro s h_s t h_t _

Result:
α : Type u_1
S s : Set α
h_s : s ∈ {S}
t : Set α
h_t : t ∈ {S}
a✝ : (s ∩ t).Nonempty
⊢ s ∩ t ∈ {S}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Extra.lean
theorem size_toUTF8 (s : String) : s.toUTF8.size = s.utf8ByteSize

Proof state:
s : String
⊢ (List.map (List.length ∘ utf8EncodeChar) s.data).sum = utf8ByteSize.go s.data

Tactic:
induction s.data <;> simp [List.map, List.flatten, utf8ByteSize.go, Nat.add_comm, *]

Result:
no goals

Proof state:
s : String
⊢ s.toUTF8.size = s.utf8ByteSize

Tactic:
simp [toUTF8, ByteArray.size, Array.size, utf8ByteSize, List.flatMap]

Result:
s : String
⊢ (List.map (List.length ∘ utf8EncodeChar) s.data).sum = utf8ByteSize.go s.data
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma setLIntegral_condKernel (hf : Measurable f) {s : Set β}
    (hs : MeasurableSet s) {t : Set Ω} (ht : MeasurableSet t) :
    ∫⁻ b in s, ∫⁻ ω in t, f (b, ω) ∂(ρ.condKernel b) ∂ρ.fst
      = ∫⁻ x in s ×ˢ t, f x ∂ρ

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel

Tactic:
rw [setLIntegral_compProd hf hs ht]

Result:
no goals

Proof state:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst = ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ

Tactic:
conv_rhs => rw [← ρ.disintegrate ρ.condKernel]

Result:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β) in s, ∫⁻ (ω : Ω) in t, f (b, ω) ∂ρ.condKernel b ∂ρ.fst =
    ∫⁻ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_singleton_left : image₂ f {a} t = t.image fun b => f a b :=
  ext fun x => by simp

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
t : Finset β
a : α
x : γ
⊢ x ∈ image₂ f {a} t ↔ x ∈ image (fun b => f a b) t

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem image_coe_Icc : (some : α → WithTop α) '' Icc a b = Icc (a : WithTop α) b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some '' Icc a b = Icc ↑a ↑b

Tactic:
rw [← preimage_coe_Icc, image_preimage_eq_inter_range, range_coe,
  inter_eq_self_of_subset_left
    (Subset.trans Icc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem eval_monoidalComp
    {η η' : f ⟶ g} {α : g ≅ h} {θ θ' : h ⟶ i} {αθ : g ⟶ i} {ηαθ : f ⟶ i}
    (e_η : η = η') (e_θ : θ = θ') (e_αθ : α.hom ≫ θ' = αθ) (e_ηαθ : η' ≫ αθ = ηαθ) :
    η ≫ α.hom ≫ θ = ηαθ

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g h i : a ⟶ b
η η' : f ⟶ g
α : g ≅ h
θ θ' : h ⟶ i
αθ : g ⟶ i
ηαθ : f ⟶ i
e_η : η = η'
e_θ : θ = θ'
e_αθ : α.hom ≫ θ' = αθ
e_ηαθ : η' ≫ αθ = ηαθ
⊢ η ≫ α.hom ≫ θ = ηαθ

Tactic:
simp [e_η, e_θ, e_αθ, e_ηαθ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem divRec_succ' (m : Nat) (args : DivModArgs w) (qr : DivModState w) :
    divRec (m+1) args qr =
    let wn := qr.wn - 1
    let wr := qr.wr + 1
    let r' := shiftConcat qr.r (args.n.getLsbD wn)
    let input : DivModState _ :=
      if r' < args.d then {
        q := qr.q.shiftConcat false,
        r := r'
        wn, wr
      } else {
        q := qr.q.shiftConcat true,
        r := r' - args.d
        wn, wr
      }
    divRec m args input

Proof state:
w m : Nat
args : DivModArgs w
qr : DivModState w
⊢ divRec (m + 1) args qr =
    let wn := qr.wn - 1;
    let wr := qr.wr + 1;
    let r' := qr.r.shiftConcat (args.n.getLsbD wn);
    let input :=
      if r' < args.d then { wn := wn, wr := wr, q := qr.q.shiftConcat false, r := r' }
      else { wn := wn, wr := wr, q := qr.q.shiftConcat true, r := r' - args.d };
    divRec m args input

Tactic:
simp [divRec_succ, divSubtractShift]

Result:
no goals
-- Mathlib/Probability/Density.lean
theorem integral_pdf_smul [IsFiniteMeasure ℙ] {X : Ω → E} [HasPDF X ℙ μ] {f : E → F}
    (hf : AEStronglyMeasurable f μ) : ∫ x, (pdf X ℙ μ x).toReal • f x ∂μ = ∫ x, f (X x) ∂ℙ

Proof state:
Ω : Type u_1
E : Type u_2
inst✝⁴ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : IsFiniteMeasure ℙ
X : Ω → E
inst✝ : HasPDF X ℙ μ
f : E → F
hf : AEStronglyMeasurable f μ
⊢ ∫ (x : E), (pdf X ℙ μ x).toReal • f x ∂μ = ∫ (x : Ω), f (X x) ∂ℙ

Tactic:
rw [← integral_map (HasPDF.aemeasurable X ℙ μ) (hf.mono_ac HasPDF.absolutelyContinuous),
  map_eq_withDensity_pdf X ℙ μ, pdf_def, integral_rnDeriv_smul HasPDF.absolutelyContinuous,
  withDensity_rnDeriv_eq _ _ HasPDF.absolutelyContinuous]

Result:
no goals
-- Mathlib/Order/Sublattice.lean
lemma top_prod (L : Sublattice β) : (⊤ : Sublattice α).prod L = L.comap LatticeHom.snd :=
  ext fun a ↦ by simp [mem_prod, LatticeHom.coe_snd]

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L : Sublattice β
a : α × β
⊢ a ∈ ⊤.prod L ↔ a ∈ comap LatticeHom.snd L

Tactic:
simp [mem_prod, LatticeHom.coe_snd]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem enorm_eq_ofReal (hr : 0 ≤ r) : ‖r‖ₑ = .ofReal r

Proof state:
r : ℝ
hr : 0 ≤ r
⊢ ‖r‖ₑ = ENNReal.ofReal r

Tactic:
rw [← ofReal_norm_eq_enorm, norm_of_nonneg hr]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_cons [CommMonoid β] {n : ℕ} (x : β) (f : Fin n → β) :
    (∏ i : Fin n.succ, (cons x f : Fin n.succ → β) i) = x * ∏ i : Fin n, f i

Proof state:
β : Type u_2
inst✝ : CommMonoid β
n : ℕ
x : β
f : Fin n → β
⊢ ∏ i : Fin n.succ, cons x f i = x * ∏ i : Fin n, f i

Tactic:
simp_rw [prod_univ_succ, cons_zero, cons_succ]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem lt_one_of_mul_lt_left [MulRightReflectLT α] {a b : α}
    (h : a * b < b) :
    a < 1 :=
  lt_of_mul_lt_mul_right' (a := b) <| by simpa only [one_mul]

Proof state:
α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : MulRightReflectLT α
a b : α
h : a * b < b
⊢ a * b < 1 * b

Tactic:
simpa only [one_mul]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extChartAt_image_nhd_mem_nhds_of_mem_interior_range {x y} (hx : y ∈ (extChartAt I x).source)
    (h'x : extChartAt I x y ∈ interior (range I)) {s : Set M} (h : s ∈ 𝓝 y) :
    (extChartAt I x) '' s ∈ 𝓝 (extChartAt I x y)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x y : M
hx : y ∈ (extChartAt I x).source
h'x : ↑(extChartAt I x) y ∈ interior (range ↑I)
s : Set M
h : s ∈ 𝓝 y
⊢ y ∈ (chartAt H x).source

Tactic:
simpa using hx

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x y : M
hx : y ∈ (extChartAt I x).source
h'x : ↑(extChartAt I x) y ∈ interior (range ↑I)
s : Set M
h : s ∈ 𝓝 y
⊢ ↑((chartAt H x).extend I) '' s ∈ 𝓝 (↑((chartAt H x).extend I) y)

Tactic:
exact extend_image_nhd_mem_nhds_of_mem_interior_range _ (by simpa using hx) h'x h

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x y : M
hx : y ∈ (extChartAt I x).source
h'x : ↑(extChartAt I x) y ∈ interior (range ↑I)
s : Set M
h : s ∈ 𝓝 y
⊢ ↑(extChartAt I x) '' s ∈ 𝓝 (↑(extChartAt I x) y)

Tactic:
rw [extChartAt]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x y : M
hx : y ∈ (extChartAt I x).source
h'x : ↑(extChartAt I x) y ∈ interior (range ↑I)
s : Set M
h : s ∈ 𝓝 y
⊢ ↑((chartAt H x).extend I) '' s ∈ 𝓝 (↑((chartAt H x).extend I) y)
-- Mathlib/Topology/Constructions.lean
lemma IsOpenEmbedding.sumElim {f : X → Z} {g : Y → Z}
    (hf : IsOpenEmbedding f) (hg : IsOpenEmbedding g) (h : Injective (Sum.elim f g)) :
    IsOpenEmbedding (Sum.elim f g)

Proof state:
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : Continuous f ∧ Injective f ∧ IsOpenMap f
hg : Continuous g ∧ Injective g ∧ IsOpenMap g
h : Injective (Sum.elim f g)
⊢ Continuous (Sum.elim f g) ∧ Injective (Sum.elim f g) ∧ IsOpenMap (Sum.elim f g)

Tactic:
exact ⟨hf.1.sumElim hg.1, h, hf.2.2.sumElim hg.2.2⟩

Result:
no goals

Proof state:
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsOpenEmbedding f
hg : IsOpenEmbedding g
h : Injective (Sum.elim f g)
⊢ IsOpenEmbedding (Sum.elim f g)

Tactic:
rw [isOpenEmbedding_iff_continuous_injective_isOpenMap] at hf hg ⊢

Result:
X : Type u
Y : Type v
Z : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : Continuous f ∧ Injective f ∧ IsOpenMap f
hg : Continuous g ∧ Injective g ∧ IsOpenMap g
h : Injective (Sum.elim f g)
⊢ Continuous (Sum.elim f g) ∧ Injective (Sum.elim f g) ∧ IsOpenMap (Sum.elim f g)
-- Mathlib/Tactic/LinearCombination/Lemmas.lean
theorem le_of_le [OrderedCancelAddCommMonoid α] (p : (a:α) ≤ b) (H : a' + b ≤ b' + a) :
    a' ≤ b'

Proof state:
α : Type u_1
a a' b b' : α
inst✝ : OrderedCancelAddCommMonoid α
p : a ≤ b
H : a' + b ≤ b' + a
⊢ b' + a ≤ b' + b

Tactic:
apply add_le_add_left p

Result:
no goals

Proof state:
α : Type u_1
a a' b b' : α
inst✝ : OrderedCancelAddCommMonoid α
p : a ≤ b
H : a' + b ≤ b' + a
⊢ a' + b ≤ b' + b

Tactic:
apply H.trans

Result:
α : Type u_1
a a' b b' : α
inst✝ : OrderedCancelAddCommMonoid α
p : a ≤ b
H : a' + b ≤ b' + a
⊢ b' + a ≤ b' + b

Proof state:
α : Type u_1
a a' b b' : α
inst✝ : OrderedCancelAddCommMonoid α
p : a ≤ b
H : a' + b ≤ b' + a
⊢ a' ≤ b'

Tactic:
rw [← add_le_add_iff_right b]

Result:
α : Type u_1
a a' b b' : α
inst✝ : OrderedCancelAddCommMonoid α
p : a ≤ b
H : a' + b ≤ b' + a
⊢ a' + b ≤ b' + b
-- Mathlib/Data/Complex/Basic.lean
@[simp] lemma div_ofReal_re (z : ℂ) (x : ℝ) : (z / x).re = z.re / x

Proof state:
z : ℂ
x : ℝ
⊢ (z / ↑x).re = z.re / x

Tactic:
rw [div_ofReal]

Result:
no goals
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem eval_unique (φ : R[X] →ₐ[R] A) (p) : φ p = eval₂ (algebraMap R A) (φ X) p

Proof state:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
φ : R[X] →ₐ[R] A
p : R[X]
⊢ φ p = eval₂ (algebraMap R A) (φ X) p

Tactic:
rw [← aeval_def, aeval_algHom, aeval_X_left, AlgHom.comp_id]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean
theorem isLocalHom_stalkMap_congr {X Y : RingedSpace} (f g : X ⟶ Y) (H : f = g) (x)
    (h : IsLocalHom (f.stalkMap x).hom) :
    IsLocalHom (g.stalkMap x).hom

Proof state:
X Y : RingedSpace
f g : X ⟶ Y
H : f = g
x : ↑↑X.toPresheafedSpace
h : IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f x))
⊢ IsLocalHom (CommRingCat.Hom.hom (eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap f x))

Tactic:
infer_instance

Result:
no goals

Proof state:
X Y : RingedSpace
f g : X ⟶ Y
H : f = g
x : ↑↑X.toPresheafedSpace
h : IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f x))
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap g x))

Tactic:
rw [PresheafedSpace.stalkMap.congr_hom _ _ H.symm x]

Result:
X Y : RingedSpace
f g : X ⟶ Y
H : f = g
x : ↑↑X.toPresheafedSpace
h : IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap f x))
⊢ IsLocalHom (CommRingCat.Hom.hom (eqToHom ⋯ ≫ PresheafedSpace.Hom.stalkMap f x))
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[simp]
lemma homologyMap_add : homologyMap (φ + ψ) i = homologyMap φ i + homologyMap ψ i

Proof state:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ homologyMap (φ + ψ) i = homologyMap φ i + homologyMap ψ i

Tactic:
dsimp [homologyMap]

Result:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ + ψ)) =
    ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ) +
      ShortComplex.homologyMap ((shortComplexFunctor C c i).map ψ)

Proof state:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ + ψ)) =
    ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ) +
      ShortComplex.homologyMap ((shortComplexFunctor C c i).map ψ)

Tactic:
rw [← ShortComplex.homologyMap_add]

Result:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ + ψ)) =
    ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ + (shortComplexFunctor C c i).map ψ)

Proof state:
C : Type u_1
ι : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
φ ψ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.homologyMap ((shortComplexFunctor C c i).map (φ + ψ)) =
    ShortComplex.homologyMap ((shortComplexFunctor C c i).map φ + (shortComplexFunctor C c i).map ψ)

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
lemma limsSup_principal_eq_csSup (h : BddAbove s) (hs : s.Nonempty) : limsSup (𝓟 s) = sSup s

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : s.Nonempty
⊢ sInf {a | ∀ x ∈ s, x ≤ a} = sSup s

Tactic:
exact csInf_upperBounds_eq_csSup h hs

Result:
no goals

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : s.Nonempty
⊢ (𝓟 s).limsSup = sSup s

Tactic:
simp only [limsSup, eventually_principal]

Result:
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : s.Nonempty
⊢ sInf {a | ∀ x ∈ s, x ≤ a} = sSup s
-- Mathlib/Analysis/Complex/AbsMax.lean
theorem eventually_eq_of_isLocalMax_norm {f : E → F} {c : E}
    (hd : ∀ᶠ z in 𝓝 c, DifferentiableAt ℂ f z) (hc : IsLocalMax (norm ∘ f) c) :
    ∀ᶠ y in 𝓝 c, f y = f c

Proof state:
case intro.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → F
c : E
hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMax (norm ∘ f) c
r : ℝ
hr₀ : 0 < r
hr : ∀ ⦃x : E⦄, x ∈ closedBall c r → DifferentiableAt ℂ f x ∧ (norm ∘ f) x ≤ (norm ∘ f) c
⊢ ∀ᶠ (y : E) in 𝓝 c, f y = f c

Tactic:
exact nhds_basis_closedBall.eventually_iff.2
  ⟨r, hr₀, eqOn_closedBall_of_isMaxOn_norm (DifferentiableOn.diffContOnCl fun x hx =>
      (hr <| closure_ball_subset_closedBall hx).1.differentiableWithinAt) fun x hx =>
    (hr <| ball_subset_closedBall hx).2⟩

Result:
no goals

Proof state:
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → F
c : E
hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMax (norm ∘ f) c
⊢ ∀ᶠ (y : E) in 𝓝 c, f y = f c

Tactic:
rcases nhds_basis_closedBall.eventually_iff.1 (hd.and hc) with ⟨r, hr₀, hr⟩

Result:
case intro.intro
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℂ E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : StrictConvexSpace ℝ F
f : E → F
c : E
hd : ∀ᶠ (z : E) in 𝓝 c, DifferentiableAt ℂ f z
hc : IsLocalMax (norm ∘ f) c
r : ℝ
hr₀ : 0 < r
hr : ∀ ⦃x : E⦄, x ∈ closedBall c r → DifferentiableAt ℂ f x ∧ (norm ∘ f) x ≤ (norm ∘ f) c
⊢ ∀ᶠ (y : E) in 𝓝 c, f y = f c
-- Mathlib/Data/Nat/Count.lean
theorem count_le {n : ℕ} : count p n ≤ n

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ #(filter (fun x => p x) (range n)) ≤ n

Tactic:
exact (card_filter_le _ _).trans_eq (card_range _)

Result:
no goals

Proof state:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n ≤ n

Tactic:
rw [count_eq_card_filter_range]

Result:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ #(filter (fun x => p x) (range n)) ≤ n
-- Mathlib/NumberTheory/Modular.lean
lemma exists_one_half_le_im_smul (τ : ℍ) : ∃ γ : SL(2, ℤ), 1 / 2 ≤ im (γ • τ)

Proof state:
case intro
τ : ℍ
γ : SL(2, ℤ)
hγ : γ • τ ∈ fd
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im

Tactic:
use γ

Result:
case h
τ : ℍ
γ : SL(2, ℤ)
hγ : γ • τ ∈ fd
⊢ 1 / 2 ≤ (γ • τ).im

Proof state:
τ : ℍ
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im

Tactic:
obtain ⟨γ, hγ⟩ := exists_smul_mem_fd τ

Result:
case intro
τ : ℍ
γ : SL(2, ℤ)
hγ : γ • τ ∈ fd
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im

Proof state:
case h
τ : ℍ
γ : SL(2, ℤ)
hγ : γ • τ ∈ fd
⊢ 1 / 2 ≤ (γ • τ).im

Tactic:
nlinarith [three_le_four_mul_im_sq_of_mem_fd hγ, im_pos (γ • τ)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem shiftLeftRec_zero {x : BitVec w₁} {y : BitVec w₂} :
    shiftLeftRec x y 0 = x <<< (y &&& twoPow w₂ 0)

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
⊢ x.shiftLeftRec y 0 = x <<< (y &&& twoPow w₂ 0)

Tactic:
simp [shiftLeftRec]

Result:
no goals