harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Algebra/Operations.lean
theorem le_self_mul_one_div {I : Submodule R A} (hI : I ≤ 1) : I ≤ I * (1 / I)

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
hI : I ≤ 1
⊢ I * 1 ≤ I * (1 / I)

Tactic:
apply mul_le_mul_right (one_le_one_div.mpr hI)

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
hI : I ≤ 1
⊢ I ≤ I * (1 / I)

Tactic:
refine (mul_one I).symm.trans_le ?_

Result:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
I : Submodule R A
hI : I ≤ 1
⊢ I * 1 ≤ I * (1 / I)
-- Mathlib/Analysis/Analytic/Basic.lean
lemma HasFPowerSeriesOnBall.hasFPowerSeriesWithinOnBall (hf : HasFPowerSeriesOnBall f p x r) :
    HasFPowerSeriesWithinOnBall f p s x r

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesWithinOnBall f p s x r

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
⊢ HasFPowerSeriesWithinOnBall f p s x r

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
⊢ HasFPowerSeriesWithinOnBall f p s x r

Tactic:
exact hf.mono (subset_univ _)

Result:
no goals
-- Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean
lemma eq_compactlyGenerated [t : TopologicalSpace X] [UCompactlyGeneratedSpace.{u} X] :
    t = compactlyGenerated.{u} X

Proof state:
case a
X : Type w
t : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
⊢ t ≤ compactlyGenerated X

Tactic:
exact UCompactlyGeneratedSpace.le_compactlyGenerated

Result:
no goals

Proof state:
X : Type w
t : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
⊢ t = compactlyGenerated X

Tactic:
apply le_antisymm

Result:
case a
X : Type w
t : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
⊢ t ≤ compactlyGenerated X

case a
X : Type w
t : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
⊢ compactlyGenerated X ≤ t

Proof state:
case a
X : Type w
t : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
⊢ compactlyGenerated X ≤ t

Tactic:
simp only [compactlyGenerated, ← continuous_iff_coinduced_le, continuous_sigma_iff,
  Sigma.forall]

Result:
case a
X : Type w
t : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
⊢ ∀ (a : CompHaus) (b : C(↑a.toTop, X)), Continuous fun a_1 => b a_1

Proof state:
case a
X : Type w
t : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
⊢ ∀ (a : CompHaus) (b : C(↑a.toTop, X)), Continuous fun a_1 => b a_1

Tactic:
exact fun S f ↦ f.2

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
theorem isIso_ι_of_isTerminal {j : J} (I : IsTerminal j) (F : J ⥤ C) [HasColimit F] :
    IsIso (colimit.ι F j) :=
  ⟨⟨colimit.desc _ (coconeOfDiagramTerminal I F), ⟨by simp, by ext; simp⟩⟩⟩

Proof state:
case w
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝ : HasColimit F
j✝ : J
⊢ colimit.ι F j✝ ≫ colimit.desc F (coconeOfDiagramTerminal I F) ≫ colimit.ι F j = colimit.ι F j✝ ≫ 𝟙 (colimit F)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝ : HasColimit F
⊢ colimit.desc F (coconeOfDiagramTerminal I F) ≫ colimit.ι F j = 𝟙 (colimit F)

Tactic:
ext

Result:
case w
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝ : HasColimit F
j✝ : J
⊢ colimit.ι F j✝ ≫ colimit.desc F (coconeOfDiagramTerminal I F) ≫ colimit.ι F j = colimit.ι F j✝ ≫ 𝟙 (colimit F)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝ : HasColimit F
⊢ colimit.ι F j ≫ colimit.desc F (coconeOfDiagramTerminal I F) = 𝟙 (F.obj j)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem dimH_def (s : Set X) : dimH s = ⨆ (d : ℝ≥0) (_ : μH[d] s = ∞), (d : ℝ≥0∞)

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
⊢ dimH s = ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d

Tactic:
borelize X

Result:
X : Type u_2
inst✝¹ : EMetricSpace X
s : Set X
inst✝ : BorelSpace X
this✝ : MeasurableSpace X := borel X
⊢ dimH s = ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d

Proof state:
X : Type u_2
inst✝¹ : EMetricSpace X
s : Set X
inst✝ : BorelSpace X
this✝ : MeasurableSpace X := borel X
⊢ dimH s = ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d

Tactic:
rw [dimH]

Result:
no goals
-- Mathlib/RingTheory/SimpleRing/Basic.lean
lemma injective_ringHom_or_subsingleton_codomain
    {R S : Type*} [NonAssocRing R] [IsSimpleRing R] [NonAssocSemiring S]
    (f : R →+* S) : Function.Injective f ∨ Subsingleton S :=
  simple.eq_bot_or_eq_top (TwoSidedIdeal.ker f) |>.imp (TwoSidedIdeal.ker_eq_bot _ |>.1)
    (fun h => subsingleton_iff_zero_eq_one.1 <| by
      have mem : 1 ∈ TwoSidedIdeal.ker f := h.symm ▸ TwoSidedIdeal.mem_top _
      rwa [TwoSidedIdeal.mem_ker, map_one, eq_comm] at mem)

Proof state:
R : Type u_2
S : Type u_3
inst✝² : NonAssocRing R
inst✝¹ : IsSimpleRing R
inst✝ : NonAssocSemiring S
f : R →+* S
h : TwoSidedIdeal.ker f = ⊤
⊢ 0 = 1

Tactic:
have mem : 1 ∈ TwoSidedIdeal.ker f := h.symm ▸ TwoSidedIdeal.mem_top _

Result:
R : Type u_2
S : Type u_3
inst✝² : NonAssocRing R
inst✝¹ : IsSimpleRing R
inst✝ : NonAssocSemiring S
f : R →+* S
h : TwoSidedIdeal.ker f = ⊤
mem : 1 ∈ TwoSidedIdeal.ker f
⊢ 0 = 1

Proof state:
R : Type u_2
S : Type u_3
inst✝² : NonAssocRing R
inst✝¹ : IsSimpleRing R
inst✝ : NonAssocSemiring S
f : R →+* S
h : TwoSidedIdeal.ker f = ⊤
mem : 1 ∈ TwoSidedIdeal.ker f
⊢ 0 = 1

Tactic:
rwa [TwoSidedIdeal.mem_ker, map_one, eq_comm] at mem

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem small_iff_lift_mk_lt_univ {α : Type u} :
    Small.{v} α ↔ Cardinal.lift.{v+1,_} #α < univ.{v, max u (v + 1)}

Proof state:
case mp.mk.intro
α : Type u
β : Type v
e : Nonempty (α ≃ β)
⊢ ∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'

Tactic:
exact ⟨#β, lift_mk_eq.{u, _, v + 1}.2 e⟩

Result:
no goals

Proof state:
case mpr.intro
α : Type u
c : Cardinal.{v}
hc : lift.{v + 1, u} #α = lift.{max u (v + 1), v} c
⊢ Small.{v, u} α

Tactic:
exact ⟨⟨c.out, lift_mk_eq.{u, _, v + 1}.1 (hc.trans (congr rfl c.mk_out.symm))⟩⟩

Result:
no goals

Proof state:
α : Type u
⊢ Small.{v, u} α ↔ ∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'

Tactic:
constructor

Result:
case mp
α : Type u
⊢ Small.{v, u} α → ∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'

case mpr
α : Type u
⊢ (∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c') → Small.{v, u} α

Proof state:
α : Type u
⊢ Small.{v, u} α ↔ lift.{v + 1, u} #α < univ.{v, max u (v + 1)}

Tactic:
rw [lt_univ']

Result:
α : Type u
⊢ Small.{v, u} α ↔ ∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'

Proof state:
case mp
α : Type u
⊢ Small.{v, u} α → ∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'

Tactic:
rintro ⟨β, e⟩

Result:
case mp.mk.intro
α : Type u
β : Type v
e : Nonempty (α ≃ β)
⊢ ∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c'

Proof state:
case mpr
α : Type u
⊢ (∃ c', lift.{v + 1, u} #α = lift.{max u (v + 1), v} c') → Small.{v, u} α

Tactic:
rintro ⟨c, hc⟩

Result:
case mpr.intro
α : Type u
c : Cardinal.{v}
hc : lift.{v + 1, u} #α = lift.{max u (v + 1), v} c
⊢ Small.{v, u} α
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem mem_uniformity_of_uniformContinuous_invariant [UniformSpace α] [UniformSpace β]
    {s : Set (β × β)} {f : α → α → β} (hf : UniformContinuous fun p : α × α => f p.1 p.2)
    (hs : s ∈ 𝓤 β) : ∃ u ∈ 𝓤 α, ∀ a b c, (a, b) ∈ u → (f a c, f b c) ∈ s

Proof state:
case intro.intro.intro.intro
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (β × β)
f : α → α → β
hf : Tendsto ((fun x => (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
hs : s ∈ 𝓤 β
u : Set (α × α)
hu : u ∈ 𝓤 α
v : Set (α × α)
hv : v ∈ 𝓤 α
huvt : u ×ˢ v ⊆ ((fun x => (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' s
⊢ ∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s

Tactic:
exact ⟨u, hu, fun a b c hab => @huvt ((_, _), (_, _)) ⟨hab, refl_mem_uniformity hv⟩⟩

Result:
no goals

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (β × β)
f : α → α → β
hf : Tendsto ((fun x => (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
hs : s ∈ 𝓤 β
⊢ ∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s

Tactic:
rcases mem_prod_iff.1 (mem_map.1 <| hf hs) with ⟨u, hu, v, hv, huvt⟩

Result:
case intro.intro.intro.intro
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (β × β)
f : α → α → β
hf : Tendsto ((fun x => (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
hs : s ∈ 𝓤 β
u : Set (α × α)
hu : u ∈ 𝓤 α
v : Set (α × α)
hv : v ∈ 𝓤 α
huvt : u ×ˢ v ⊆ ((fun x => (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' s
⊢ ∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (β × β)
f : α → α → β
hf : UniformContinuous fun p => f p.1 p.2
hs : s ∈ 𝓤 β
⊢ ∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s

Tactic:
rw [UniformContinuous, uniformity_prod_eq_prod, tendsto_map'_iff] at hf

Result:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (β × β)
f : α → α → β
hf : Tendsto ((fun x => (f x.1.1 x.1.2, f x.2.1 x.2.2)) ∘ fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 α) (𝓤 β)
hs : s ∈ 𝓤 β
⊢ ∃ u ∈ 𝓤 α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
-- Mathlib/Data/Finset/Fold.lean
theorem fold_union_inter [DecidableEq α] {s₁ s₂ : Finset α} {b₁ b₂ : β} :
    ((s₁ ∪ s₂).fold op b₁ f * (s₁ ∩ s₂).fold op b₂ f) = s₁.fold op b₂ f * s₂.fold op b₁ f

Proof state:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ op (Multiset.fold op b₁ (Multiset.map f (s₁ ∪ s₂).val)) (Multiset.fold op b₂ (Multiset.map f (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))

Tactic:
rw [← fold_add op, ← Multiset.map_add, union_val, inter_val, union_add_inter, Multiset.map_add,
  hc.comm, fold_add]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ op (fold op b₁ f (s₁ ∪ s₂)) (fold op b₂ f (s₁ ∩ s₂)) = op (fold op b₂ f s₁) (fold op b₁ f s₂)

Tactic:
unfold fold

Result:
α : Type u_1
β : Type u_2
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
b₁ b₂ : β
⊢ op (Multiset.fold op b₁ (Multiset.map f (s₁ ∪ s₂).val)) (Multiset.fold op b₂ (Multiset.map f (s₁ ∩ s₂).val)) =
    op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
-- Mathlib/Analysis/Complex/Basic.lean
theorem ofReal_tsum (f : α → ℝ) : (↑(∑' a, f a) : 𝕜) = ∑' a, (f a : 𝕜)

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
f : α → ℝ
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)

Tactic:
by_cases h : Summable f

Result:
case pos
α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
f : α → ℝ
h : Summable f
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)

case neg
α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
f : α → ℝ
h : ¬Summable f
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)

Proof state:
case pos
α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
f : α → ℝ
h : Summable f
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)

Tactic:
exact ContinuousLinearMap.map_tsum ofRealCLM h

Result:
no goals

Proof state:
case neg
α : Type u_1
𝕜 : Type u_2
inst✝ : RCLike 𝕜
f : α → ℝ
h : ¬Summable f
⊢ ↑(∑' (a : α), f a) = ∑' (a : α), ↑(f a)

Tactic:
rw [tsum_eq_zero_of_not_summable h,
  tsum_eq_zero_of_not_summable ((summable_ofReal _).not.mpr h), ofReal_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/VectorSpace.lean
theorem ofVectorSpaceIndex.linearIndependent :
    LinearIndependent K ((↑) : ofVectorSpaceIndex K V → V)

Proof state:
case h.e'_4
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ Subtype.val = ⇑(ofVectorSpace K V)

Tactic:
ext x

Result:
case h.e'_4.h
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : { x // x ∈ ofVectorSpaceIndex K V }
⊢ ↑x = (ofVectorSpace K V) x

Proof state:
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ LinearIndependent K Subtype.val

Tactic:
convert (ofVectorSpace K V).linearIndependent

Result:
case h.e'_4
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ Subtype.val = ⇑(ofVectorSpace K V)

Proof state:
case h.e'_4.h
K : Type u_3
V : Type u_4
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : { x // x ∈ ofVectorSpaceIndex K V }
⊢ ↑x = (ofVectorSpace K V) x

Tactic:
rw [ofVectorSpace_apply_self]

Result:
no goals
-- Mathlib/Order/Filter/FilterProduct.lean
theorem const_abs [LinearOrderedAddCommGroup β] (x : β) : (↑|x| : β*) = |↑x|

Proof state:
α : Type u
β : Type v
φ : Ultrafilter α
inst✝ : LinearOrderedAddCommGroup β
x : β
⊢ ↑|x| = |↑x|

Tactic:
rw [abs_def, map_const]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem degree_modByMonic_le_left : degree (p %ₘ q) ≤ degree p

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
⊢ (p %ₘ q).degree ≤ p.degree

Proof state:
case neg
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : ¬q.Monic
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
rw [modByMonic_eq_of_not_monic p hq]

Result:
no goals

Proof state:
case pos.inl
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : q.Monic
h✝ : p.degree < q.degree
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
rw [(modByMonic_eq_self_iff hq).mpr ‹_›]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
by_cases hq : q.Monic

Result:
case pos
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : q.Monic
⊢ (p %ₘ q).degree ≤ p.degree

case neg
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : ¬q.Monic
⊢ (p %ₘ q).degree ≤ p.degree

Proof state:
case pos.inr
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : q.Monic
h✝ : p.degree ≥ q.degree
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
exact (degree_modByMonic_le p hq).trans ‹_›

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : q.Monic
⊢ (p %ₘ q).degree ≤ p.degree

Tactic:
cases lt_or_ge (degree p) (degree q)

Result:
case pos.inl
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : q.Monic
h✝ : p.degree < q.degree
⊢ (p %ₘ q).degree ≤ p.degree

case pos.inr
R : Type u
inst✝ : Ring R
p q : R[X]
a✝ : Nontrivial R
hq : q.Monic
h✝ : p.degree ≥ q.degree
⊢ (p %ₘ q).degree ≤ p.degree
-- Mathlib/Data/Rel.lean
theorem preimage_inter_codom_eq (s : Set β) : r.preimage (s ∩ r.codom) = r.preimage s

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
s : Set β
⊢ r.preimage (s ∩ r.codom) = r.preimage s

Tactic:
rw [← dom_inv, preimage, preimage, image_inter_dom_eq]

Result:
no goals
-- Mathlib/GroupTheory/Commensurable.lean
theorem commensurable_inv (H : Subgroup G) (g : ConjAct G) :
    Commensurable (g • H) H ↔ Commensurable H (g⁻¹ • H)

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : ConjAct G
⊢ Commensurable (g • H) H ↔ Commensurable H (g⁻¹ • H)

Tactic:
rw [commensurable_conj, inv_smul_smul]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Hom.lean
@[simp]
lemma coweightMap_coweightEquiv_symm (e : RootPairing.Equiv P Q) (n : N) :
    e.toHom.coweightMap ((coweightEquiv P Q e).symm n) = n

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
e : P.Equiv Q
n : N
⊢ (coweightEquiv P Q e) ((coweightEquiv P Q e).symm n) = n

Tactic:
exact LinearEquiv.apply_symm_apply (coweightEquiv P Q e) n

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
e : P.Equiv Q
n : N
⊢ (↑e).coweightMap ((coweightEquiv P Q e).symm n) = n

Tactic:
rw [← coweightEquiv_apply]

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
ι₂ : Type u_5
M₂ : Type u_6
N₂ : Type u_7
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : AddCommGroup N₂
inst✝ : Module R N₂
P : RootPairing ι R M N
Q : RootPairing ι₂ R M₂ N₂
e : P.Equiv Q
n : N
⊢ (coweightEquiv P Q e) ((coweightEquiv P Q e).symm n) = n
-- Mathlib/Data/Ordmap/Ordset.lean
theorem dual_node4R (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :
    dual (node4R l x m y r) = node4L (dual r) y (dual m) x (dual l)

Proof state:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node4R x m y r).dual = r.dual.node4L y m.dual x l.dual

Tactic:
cases m <;> simp [node4L, node4R, node3L, dual_node3R, dual_node', add_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_finset_sum {ι} (s : Finset ι) {f : ι → α → G} (hf : ∀ i ∈ s, Integrable (f i) μ) :
    ∫ a, ∑ i ∈ s, f i a ∂μ = ∑ i ∈ s, ∫ a, f i a ∂μ

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
s : Finset ι
f : ι → α → G
hf : ∀ i ∈ s, Integrable (f i) μ
hG : ¬CompleteSpace G
⊢ ∫ (a : α), ∑ i ∈ s, f i a ∂μ = ∑ i ∈ s, ∫ (a : α), f i a ∂μ

Tactic:
simp [integral, hG]

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
s : Finset ι
f : ι → α → G
hf : ∀ i ∈ s, Integrable (f i) μ
⊢ ∫ (a : α), ∑ i ∈ s, f i a ∂μ = ∑ i ∈ s, ∫ (a : α), f i a ∂μ

Tactic:
by_cases hG : CompleteSpace G

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
s : Finset ι
f : ι → α → G
hf : ∀ i ∈ s, Integrable (f i) μ
hG : CompleteSpace G
⊢ ∫ (a : α), ∑ i ∈ s, f i a ∂μ = ∑ i ∈ s, ∫ (a : α), f i a ∂μ

case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
s : Finset ι
f : ι → α → G
hf : ∀ i ∈ s, Integrable (f i) μ
hG : ¬CompleteSpace G
⊢ ∫ (a : α), ∑ i ∈ s, f i a ∂μ = ∑ i ∈ s, ∫ (a : α), f i a ∂μ

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
s : Finset ι
f : ι → α → G
hf : ∀ i ∈ s, Integrable (f i) μ
hG : CompleteSpace G
⊢ ∫ (a : α), ∑ i ∈ s, f i a ∂μ = ∑ i ∈ s, ∫ (a : α), f i a ∂μ

Tactic:
simp only [integral, hG, L1.integral]

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
s : Finset ι
f : ι → α → G
hf : ∀ i ∈ s, Integrable (f i) μ
hG : CompleteSpace G
⊢ (if h : True then
      if hf : Integrable (fun a => ∑ i ∈ s, f i a) μ then L1.integralCLM (Integrable.toL1 (fun a => ∑ i ∈ s, f i a) hf)
      else 0
    else 0) =
    ∑ x ∈ s,
      if h : True then
        if hf : Integrable (fun a => f x a) μ then L1.integralCLM (Integrable.toL1 (fun a => f x a) hf) else 0
      else 0

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
s : Finset ι
f : ι → α → G
hf : ∀ i ∈ s, Integrable (f i) μ
hG : CompleteSpace G
⊢ (if h : True then
      if hf : Integrable (fun a => ∑ i ∈ s, f i a) μ then L1.integralCLM (Integrable.toL1 (fun a => ∑ i ∈ s, f i a) hf)
      else 0
    else 0) =
    ∑ x ∈ s,
      if h : True then
        if hf : Integrable (fun a => f x a) μ then L1.integralCLM (Integrable.toL1 (fun a => f x a) hf) else 0
      else 0

Tactic:
exact setToFun_finset_sum (dominatedFinMeasAdditive_weightedSMul _) s hf

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
lemma IsInducing.of_comp (hf : Continuous f) (hg : Continuous g) (hgf : IsInducing (g ∘ f)) :
    IsInducing f :=
  ⟨le_antisymm (by rwa [← continuous_iff_le_induced])
      (by
        rw [hgf.eq_induced, ← induced_compose]
        exact induced_mono hg.le_induced)⟩

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hf : Continuous f
hg : Continuous g
hgf : IsInducing (g ∘ f)
⊢ induced f inst✝² ≤ induced f (induced g inst✝)

Tactic:
exact induced_mono hg.le_induced

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hf : Continuous f
hg : Continuous g
hgf : IsInducing (g ∘ f)
⊢ induced f inst✝² ≤ inst✝¹

Tactic:
rw [hgf.eq_induced, ← induced_compose]

Result:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hf : Continuous f
hg : Continuous g
hgf : IsInducing (g ∘ f)
⊢ induced f inst✝² ≤ induced f (induced g inst✝)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hf : Continuous f
hg : Continuous g
hgf : IsInducing (g ∘ f)
⊢ inst✝¹ ≤ induced f inst✝²

Tactic:
rwa [← continuous_iff_le_induced]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean
lemma homogeneousLocalizationToStalk_stalkToFiberRingHom (x z) :
    homogeneousLocalizationToStalk 𝒜 x (stalkToFiberRingHom 𝒜 x z) = z

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
z : ↑((Proj.structureSheaf 𝒜).presheaf.stalk x)
⊢ homogeneousLocalizationToStalk 𝒜 x ((ConcreteCategory.hom (stalkToFiberRingHom 𝒜 x)) z) = z

Tactic:
obtain ⟨U, hxU, s, rfl⟩ := (Proj.structureSheaf 𝒜).presheaf.germ_exist x z

Result:
case intro.intro.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ↑(ProjectiveSpectrum.top 𝒜)
U : Opens ↑(ProjectiveSpectrum.top 𝒜)
hxU : x ∈ U
s : ToType ((Proj.structureSheaf 𝒜).presheaf.obj (op U))
⊢ homogeneousLocalizationToStalk 𝒜 x
      ((ConcreteCategory.hom (stalkToFiberRingHom 𝒜 x))
        ((ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ U x hxU)) s)) =
    (ConcreteCategory.hom ((Proj.structureSheaf 𝒜).presheaf.germ U x hxU)) s