harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Bounded.lean
theorem bounded_lt_inter_lt [LinearOrder α] [NoMaxOrder α] (a : α) :
    Bounded (· < ·) (s ∩ { b | a < b }) ↔ Bounded (· < ·) s

Proof state:
α : Type u_1
s : Set α
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Bounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | a < b}) ↔ Bounded (fun x1 x2 => x1 ≤ x2) s

Tactic:
exact bounded_le_inter_lt a

Result:
no goals

Proof state:
α : Type u_1
s : Set α
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Bounded (fun x1 x2 => x1 < x2) (s ∩ {b | a < b}) ↔ Bounded (fun x1 x2 => x1 < x2) s

Tactic:
rw [← bounded_le_iff_bounded_lt, ← bounded_le_iff_bounded_lt]

Result:
α : Type u_1
s : Set α
inst✝¹ : LinearOrder α
inst✝ : NoMaxOrder α
a : α
⊢ Bounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | a < b}) ↔ Bounded (fun x1 x2 => x1 ≤ x2) s
-- Mathlib/Data/Finset/Image.lean
theorem range_add_one' (n : ℕ) :
    range (n + 1) = insert 0 ((range n).map ⟨fun i => i + 1, fun i j => by simp⟩)

Proof state:
n : ℕ
⊢ range (n + 1) = insert 0 (map { toFun := fun i => i + 1, inj' := ⋯ } (range n))

Tactic:
ext (⟨⟩ | ⟨n⟩) <;> simp [Nat.zero_lt_succ n]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n i j : ℕ
⊢ (fun i => i + 1) i = (fun i => i + 1) j → i = j

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem row_vecMul [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : m → α) :
    Matrix.row ι (v ᵥ* M) = Matrix.row ι v * M

Proof state:
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
⊢ row ι (v ᵥ* M) = row ι v * M

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
i✝ : ι
j✝ : n
⊢ row ι (v ᵥ* M) i✝ j✝ = (row ι v * M) i✝ j✝

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
ι : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
M : Matrix m n α
v : m → α
i✝ : ι
j✝ : n
⊢ row ι (v ᵥ* M) i✝ j✝ = (row ι v * M) i✝ j✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Finite.lean
theorem card_bot : Nat.card (⊥ : Subgroup G) = 1

Proof state:
G : Type u_1
inst✝ : Group G
⊢ Nat.card ↥⊥ = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem finite_toSet_toFinset [DecidableEq α] (s : Multiset α) :
    s.finite_toSet.toFinset = s.toFinset

Proof state:
case h
α : Type u
inst✝ : DecidableEq α
s : Multiset α
x : α
⊢ x ∈ ⋯.toFinset ↔ x ∈ s.toFinset

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
s : Multiset α
⊢ ⋯.toFinset = s.toFinset

Tactic:
ext x

Result:
case h
α : Type u
inst✝ : DecidableEq α
s : Multiset α
x : α
⊢ x ∈ ⋯.toFinset ↔ x ∈ s.toFinset
-- Mathlib/Order/BooleanAlgebra.lean
theorem sdiff_sdiff_right' : x \ (y \ z) = x \ y ⊔ x ⊓ z :=
  calc
    x \ (y \ z) = x \ y ⊔ x ⊓ y ⊓ z := sdiff_sdiff_right
    _ = z ⊓ x ⊓ y ⊔ x \ y

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x \ y ⊔ x ⊓ y ⊓ z = z ⊓ x ⊓ y ⊔ x \ y

Tactic:
ac_rfl

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ z ⊓ x ⊓ y ⊔ x \ y = x \ y ⊔ x ⊓ z

Tactic:
rw [sup_inf_inf_sdiff, sup_comm, inf_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/QuasiMeasurePreserving.lean
theorem preimage_iterate_ae_eq {s : Set α} {f : α → α} (hf : QuasiMeasurePreserving f μ μ) (k : ℕ)
    (hs : f ⁻¹' s =ᵐ[μ] s) : f^[k] ⁻¹' s =ᵐ[μ] s

Proof state:
case succ
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
k : ℕ
ih : f^[k] ⁻¹' s =ᵐ[μ] s
⊢ f^[k + 1] ⁻¹' s =ᵐ[μ] s

Tactic:
rw [iterate_succ, preimage_comp]

Result:
case succ
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
k : ℕ
ih : f^[k] ⁻¹' s =ᵐ[μ] s
⊢ f ⁻¹' (f^[k] ⁻¹' s) =ᵐ[μ] s

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
k : ℕ
hs : f ⁻¹' s =ᵐ[μ] s
⊢ f^[k] ⁻¹' s =ᵐ[μ] s

Tactic:
induction' k with k ih

Result:
case zero
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
⊢ f^[0] ⁻¹' s =ᵐ[μ] s

case succ
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
k : ℕ
ih : f^[k] ⁻¹' s =ᵐ[μ] s
⊢ f^[k + 1] ⁻¹' s =ᵐ[μ] s

Proof state:
case succ
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
k : ℕ
ih : f^[k] ⁻¹' s =ᵐ[μ] s
⊢ f ⁻¹' (f^[k] ⁻¹' s) =ᵐ[μ] s

Tactic:
exact EventuallyEq.trans (hf.preimage_ae_eq ih) hs

Result:
no goals

Proof state:
case zero
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s : Set α
f : α → α
hf : QuasiMeasurePreserving f μ μ
hs : f ⁻¹' s =ᵐ[μ] s
⊢ f^[0] ⁻¹' s =ᵐ[μ] s

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/Sort.lean
theorem sort_perm_toList (s : Finset α) : sort r s ~ s.toList

Proof state:
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Finset α
⊢ ↑(sort r s) = ↑s.toList

Tactic:
simp only [coe_toList, sort_eq]

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Finset α
⊢ sort r s ~ s.toList

Tactic:
rw [← Multiset.coe_eq_coe]

Result:
α : Type u_1
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : IsAntisymm α r
inst✝ : IsTotal α r
s : Finset α
⊢ ↑(sort r s) = ↑s.toList
-- Mathlib/Algebra/Ring/Parity.lean
lemma odd_neg_one : Odd (-1 : α)

Proof state:
α : Type u_2
inst✝ : Ring α
⊢ Odd (-1)

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurable_from_prod_countable [Countable β] [MeasurableSingletonClass β]
    {_ : MeasurableSpace γ} {f : α × β → γ} (hf : ∀ y, Measurable fun x => f (x, y)) :
    Measurable f :=
  measurable_from_prod_countable' hf (by simp +contextual)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
x✝ : MeasurableSpace γ
f : α × β → γ
hf : ∀ (y : β), Measurable fun x => f (x, y)
⊢ ∀ (y y' : β) (x : α), y' ∈ measurableAtom y → f (x, y') = f (x, y)

Tactic:
simp +contextual

Result:
no goals
-- Mathlib/Data/Finset/Fold.lean
theorem fold_image [DecidableEq α] {g : γ → α} {s : Finset γ}
    (H : ∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y) : (s.image g).fold op b f = s.fold op b (f ∘ g)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
op : β → β → β
hc : Std.Commutative op
ha : Std.Associative op
f : α → β
b : β
inst✝ : DecidableEq α
g : γ → α
s : Finset γ
H : ∀ x ∈ s, ∀ y ∈ s, g x = g y → x = y
⊢ fold op b f (image g s) = fold op b (f ∘ g) s

Tactic:
simp only [fold, image_val_of_injOn H, Multiset.map_map]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Internal.lean
theorem coe_mul_of_apply (r : ⨁ i, A i) {i : ι} (r' : A i) (n : ι) [Decidable (i ≤ n)] :
    ((r * of (fun i => A i) i r') n : R) = if i ≤ n then (r (n - i) : R) * r' else 0

Proof state:
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : SetLike σ R
inst✝⁸ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
⊢ ↑((r * (of (fun i => ↥(A i)) i) r') n) = if i ≤ n then ↑(r (n - i)) * ↑r' else 0

Tactic:
split_ifs with h

Result:
case pos
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : SetLike σ R
inst✝⁸ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
h : i ≤ n
⊢ ↑((r * (of (fun i => ↥(A i)) i) r') n) = ↑(r (n - i)) * ↑r'

case neg
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : SetLike σ R
inst✝⁸ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
h : ¬i ≤ n
⊢ ↑((r * (of (fun i => ↥(A i)) i) r') n) = 0

Proof state:
case pos
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : SetLike σ R
inst✝⁸ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
h : i ≤ n
⊢ ↑((r * (of (fun i => ↥(A i)) i) r') n) = ↑(r (n - i)) * ↑r'

case neg
ι : Type u_1
σ : Type u_2
R : Type u_4
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : Semiring R
inst✝⁹ : SetLike σ R
inst✝⁸ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁷ : AddCommMonoid ι
inst✝⁶ : PartialOrder ι
inst✝⁵ : CanonicallyOrderedAdd ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
r : ⨁ (i : ι), ↥(A i)
i : ι
r' : ↥(A i)
n : ι
inst✝ : Decidable (i ≤ n)
h : ¬i ≤ n
⊢ ↑((r * (of (fun i => ↥(A i)) i) r') n) = 0

Tactic:
exacts [coe_mul_of_apply_of_le _ _ _ n h, coe_mul_of_apply_of_not_le _ _ _ n h]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk'_eq_iff_eq' {x₁ x₂} {y₁ y₂ : S} :
    f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f.toMap (x₁ * y₂) = f.toMap (x₂ * y₁)

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y₁ y₂ : ↥S
⊢ f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f.toMap (x₁ * ↑y₂) = f.toMap (x₂ * ↑y₁)

Tactic:
simp only [f.mk'_eq_iff_eq, mul_comm]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Lifts.lean
theorem lifts_iff_liftsRing (p : S[X]) : p ∈ lifts f ↔ p ∈ liftsRing f

Proof state:
R : Type u
inst✝¹ : Ring R
S : Type v
inst✝ : Ring S
f : R →+* S
p : S[X]
⊢ p ∈ lifts f ↔ p ∈ liftsRing f

Tactic:
simp only [lifts, liftsRing, RingHom.mem_range, RingHom.mem_rangeS]

Result:
no goals
-- Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean
theorem support_nsmul (k : ℕ) (h : k ≠ 0) (a : FreeAbelianGroup X) :
    support (k • a) = support a

Proof state:
X : Type u_1
k : ℕ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ (k • a).support = a.support

Tactic:
apply support_zsmul k _ a

Result:
X : Type u_1
k : ℕ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ ↑k ≠ 0

Proof state:
X : Type u_1
k : ℕ
h : k ≠ 0
a : FreeAbelianGroup X
⊢ ↑k ≠ 0

Tactic:
exact mod_cast h

Result:
no goals
-- Mathlib/Topology/Sheaves/SheafCondition/PairwiseIntersections.lean
theorem isSheaf_iff_isSheafPairwiseIntersections : F.IsSheaf ↔ F.IsSheafPairwiseIntersections

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : TopCat
F : Presheaf C X
⊢ F.IsSheaf ↔ F.IsSheafPairwiseIntersections

Tactic:
rw [isSheaf_iff_isSheafOpensLeCover,
  isSheafOpensLeCover_iff_isSheafPairwiseIntersections]

Result:
no goals
-- Mathlib/Order/InitialSeg.lean
theorem transPrincipal_apply [IsWellOrder β s] [IsTrans γ t] (f : r ≼i s) (g : s ≺i t) (a : α) :
    f.transPrincipal g a = g (f a)

Proof state:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≃r s
⊢ (match Sum.inr f' with
        | Sum.inl f' => f'.trans g
        | Sum.inr f' => PrincipalSeg.relIsoTrans f' g).toRelEmbedding
      a =
    g.toRelEmbedding (f a)

Tactic:
rw [PrincipalSeg.relIsoTrans_apply, f.eq_relIso]

Result:
no goals

Proof state:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≺i s
⊢ (match Sum.inl f' with
        | Sum.inl f' => f'.trans g
        | Sum.inr f' => PrincipalSeg.relIsoTrans f' g).toRelEmbedding
      a =
    g.toRelEmbedding (f a)

Tactic:
rw [PrincipalSeg.trans_apply, f.eq_principalSeg]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
⊢ (match f.principalSumRelIso with
        | Sum.inl f' => f'.trans g
        | Sum.inr f' => PrincipalSeg.relIsoTrans f' g).toRelEmbedding
      a =
    g.toRelEmbedding (f a)

Tactic:
obtain f' | f' := f.principalSumRelIso

Result:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≺i s
⊢ (match Sum.inl f' with
        | Sum.inl f' => f'.trans g
        | Sum.inr f' => PrincipalSeg.relIsoTrans f' g).toRelEmbedding
      a =
    g.toRelEmbedding (f a)

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
f' : r ≃r s
⊢ (match Sum.inr f' with
        | Sum.inl f' => f'.trans g
        | Sum.inr f' => PrincipalSeg.relIsoTrans f' g).toRelEmbedding
      a =
    g.toRelEmbedding (f a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
⊢ (f.transPrincipal g).toRelEmbedding a = g.toRelEmbedding (f a)

Tactic:
rw [InitialSeg.transPrincipal]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝¹ : IsWellOrder β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
⊢ (match f.principalSumRelIso with
        | Sum.inl f' => f'.trans g
        | Sum.inr f' => PrincipalSeg.relIsoTrans f' g).toRelEmbedding
      a =
    g.toRelEmbedding (f a)
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
@[to_additive existing]
lemma cast_mulConst (A B : Finset G) : (σₘ[A, B] : 𝕜) = #(A * B) / #A

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑σₘ[A, B] = ↑(#(A * B)) / ↑(#A)

Tactic:
simp [mulConst]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_univ : ∫ x in univ, f x ∂μ = ∫ x, f x ∂μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
⊢ ∫ (x : X) in univ, f x ∂μ = ∫ (x : X), f x ∂μ

Tactic:
rw [Measure.restrict_univ]

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem closedBall_sup (p : Seminorm 𝕜 E) (q : Seminorm 𝕜 E) (e : E) (r : ℝ) :
    closedBall (p ⊔ q) e r = closedBall p e r ∩ closedBall q e r

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p q : Seminorm 𝕜 E
e : E
r : ℝ
⊢ (p ⊔ q).closedBall e r = p.closedBall e r ∩ q.closedBall e r

Tactic:
simp_rw [closedBall, ← Set.setOf_and, coe_sup, Pi.sup_apply, sup_le_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Filtered.lean
/-- A functor reflecting larger cofiltered limits also reflects smaller cofiltered limits. -/
lemma reflectsCofilteredLimitsOfSize_of_univLE (F : C ⥤ D) [UnivLE.{w, w'}]
    [UnivLE.{w₂, w₂'}] [ReflectsCofilteredLimitsOfSize.{w', w₂'} F] :
      ReflectsCofilteredLimitsOfSize.{w, w₂} F where
  reflects_cofiltered_limits J _ _

Proof state:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : ReflectsCofilteredLimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsCofiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
⊢ ReflectsLimitsOfShape J F

Tactic:
haveI := IsCofiltered.of_equivalence e.symm

Result:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : ReflectsCofilteredLimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsCofiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
this : IsCofiltered (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
⊢ ReflectsLimitsOfShape J F

Proof state:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : ReflectsCofilteredLimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsCofiltered J
⊢ ReflectsLimitsOfShape J F

Tactic:
let e := ((ShrinkHoms.equivalence J).trans <| Shrink.equivalence _).symm

Result:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : ReflectsCofilteredLimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsCofiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
⊢ ReflectsLimitsOfShape J F

Proof state:
C : Type u₁
inst✝⁴ : Category.{v, u₁} C
D : Type u₂
inst✝³ : Category.{v, u₂} D
F : C ⥤ D
inst✝² : UnivLE.{w, w'}
inst✝¹ : UnivLE.{w₂, w₂'}
inst✝ : ReflectsCofilteredLimitsOfSize.{w', w₂', v, u₁, u₂} F
J : Type w₂
x✝¹ : Category.{w, w₂} J
x✝ : IsCofiltered J
e : Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J) ≌ J :=
  ((ShrinkHoms.equivalence J).trans (Shrink.equivalence (ShrinkHoms.{w₂} J))).symm
this : IsCofiltered (Shrink.{w₂', w₂} (ShrinkHoms.{w₂} J))
⊢ ReflectsLimitsOfShape J F

Tactic:
exact reflectsLimitsOfShape_of_equiv e F

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finrank.lean
theorem one_lt_rank_of_one_lt_finrank (h : 1 < finrank R M) : 1 < Module.rank R M

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : 1 < finrank R M
⊢ 1 < Module.rank R M

Tactic:
simpa using lt_rank_of_lt_finrank h

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma div_lt_div_of_lt_of_dvd {a b d : ℕ} (hdb : d ∣ b) (h : a < b) : a / d < b / d

Proof state:
a b d : ℕ
hdb : d ∣ b
h : a < b
⊢ d * (a / d) < b

Tactic:
exact Nat.lt_of_le_of_lt (mul_div_le a d) h

Result:
no goals

Proof state:
a b d : ℕ
hdb : d ∣ b
h : a < b
⊢ a / d < b / d

Tactic:
rw [Nat.lt_div_iff_mul_lt' hdb]

Result:
a b d : ℕ
hdb : d ∣ b
h : a < b
⊢ d * (a / d) < b
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem natCoe_one [AddMonoidWithOne R] :
    ((1 : ArithmeticFunction ℕ) : ArithmeticFunction R) = 1

Proof state:
R : Type u_1
inst✝ : AddMonoidWithOne R
⊢ ↑1 = 1

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ ↑1 n = 1 n

Proof state:
case h
R : Type u_1
inst✝ : AddMonoidWithOne R
n : ℕ
⊢ ↑1 n = 1 n

Tactic:
simp [one_apply]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem norm_map_iff_adjoint_comp_self (u : H →L[𝕜] K) :
    (∀ x : H, ‖u x‖ = ‖x‖) ↔ adjoint u ∘L u = 1

Proof state:
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
H : Type u_5
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : InnerProductSpace 𝕜 H
inst✝³ : CompleteSpace H
K : Type u_6
inst✝² : NormedAddCommGroup K
inst✝¹ : InnerProductSpace 𝕜 K
inst✝ : CompleteSpace K
u : H →L[𝕜] K
⊢ (∀ (x : H), ‖u x‖ = ‖x‖) ↔ (adjoint u).comp u = 1

Tactic:
rw [LinearMap.norm_map_iff_inner_map_map u, u.inner_map_map_iff_adjoint_comp_self]

Result:
no goals
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem map_mod [Field k] (f : R →+* k) : (p % q).map f = p.map f % q.map f

Proof state:
case pos
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : q = 0
⊢ map f (p % q) = map f p % map f q

Tactic:
simp [hq0]

Result:
no goals

Proof state:
case neg
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ map f (p % q) = map f p % map f q

Tactic:
rw [mod_def, mod_def, leadingCoeff_map f, ← map_inv₀ f, ← map_C f, ← Polynomial.map_mul f,
  map_modByMonic f (monic_mul_leadingCoeff_inv hq0)]

Result:
no goals

Proof state:
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
⊢ map f (p % q) = map f p % map f q

Tactic:
by_cases hq0 : q = 0

Result:
case pos
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : q = 0
⊢ map f (p % q) = map f p % map f q

case neg
R : Type u
k : Type y
inst✝¹ : Field R
p q : R[X]
inst✝ : Field k
f : R →+* k
hq0 : ¬q = 0
⊢ map f (p % q) = map f p % map f q
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem basicOpen_pow (f : A) (n : ℕ) (hn : 0 < n) : basicOpen 𝒜 (f ^ n) = basicOpen 𝒜 f :=
  TopologicalSpace.Opens.ext <| by simpa using zeroLocus_singleton_pow 𝒜 f n hn

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
n : ℕ
hn : 0 < n
⊢ ↑(basicOpen 𝒜 (f ^ n)) = ↑(basicOpen 𝒜 f)

Tactic:
simpa using zeroLocus_singleton_pow 𝒜 f n hn

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem linearIndependent_iff_sum :
    LinearIndependent ℤ (eval C) ↔ LinearIndependent ℤ (SumEval C ho)

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ LinearIndependent ℤ (eval C) ↔ LinearIndependent ℤ (SumEval C ho)

Tactic:
rw [← linearIndependent_equiv (sum_equiv C hsC ho), SumEval,
  ← sum_equiv_comp_eval_eq_elim C hsC ho]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ LinearIndependent ℤ (eval C ∘ ⇑(sum_equiv C hsC ho)) ↔ LinearIndependent ℤ (eval C ∘ (sum_equiv C hsC ho).toFun)

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ LinearIndependent ℤ (eval C ∘ ⇑(sum_equiv C hsC ho)) ↔ LinearIndependent ℤ (eval C ∘ (sum_equiv C hsC ho).toFun)

Tactic:
exact Iff.rfl

Result:
no goals
-- Mathlib/Algebra/Order/Field/Defs.lean
/-- Equality holds when `b ≠ 0`. See `mul_inv_cancel_right`. -/
lemma le_mul_inv_right (ha : a ≤ 0) : a ≤ a * b * b⁻¹

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b : α
ha : a ≤ 0
⊢ a ≤ a * b * b⁻¹

Tactic:
obtain rfl | hb := eq_or_ne b 0 <;> simp [*]

Result:
no goals