harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem Integrable.of_smul {c : ℝ} (hf : Integrable I l (c • f) vol) (hc : c ≠ 0) :
    Integrable I l f vol

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
I : Box ι
inst✝ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
c : ℝ
hf : Integrable I l (c • f) vol
hc : c ≠ 0
⊢ Integrable I l f vol

Tactic:
simpa [inv_smul_smul₀ hc] using hf.smul c⁻¹

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem triangle_assoc_comp_right (f : a ⟶ b) (g : b ⟶ c) :
    (α_ f (𝟙 b) g).inv ≫ (ρ_ f).hom ▷ g = f ◁ (λ_ g).hom

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (α_ f (𝟙 b) g).inv ≫ (ρ_ f).hom ▷ g = f ◁ (λ_ g).hom

Tactic:
rw [← triangle, inv_hom_id_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/ProjectiveFamilyContent.lean
lemma projectiveFamilyFun_empty (hP : IsProjectiveMeasureFamily P) :
    projectiveFamilyFun P ∅ = 0

Proof state:
ι : Type u_1
α : ι → Type u_2
mα : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
hP : IsProjectiveMeasureFamily P
⊢ projectiveFamilyFun P ∅ = 0

Tactic:
rw [projectiveFamilyFun_congr hP (empty_mem_measurableCylinders α) (cylinder_empty ∅).symm
  MeasurableSet.empty, measure_empty]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem dom_denumerable {α β} [Denumerable α] [Primcodable β] {f : α → β} :
    Primrec f ↔ Nat.Primrec fun n => encode (f (ofNat α n)) :=
  ⟨fun h => (pred.comp h).of_eq fun n => by simp, fun h =>
    (Nat.Primrec.succ.comp h).of_eq fun n => by simp⟩

Proof state:
α : Type u_4
β : Type u_5
inst✝¹ : Denumerable α
inst✝ : Primcodable β
f : α → β
h : Primrec f
n : ℕ
⊢ (encode (Option.map f (decode n))).pred = encode (f (ofNat α n))

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
inst✝¹ : Denumerable α
inst✝ : Primcodable β
f : α → β
h : Nat.Primrec fun n => encode (f (ofNat α n))
n : ℕ
⊢ (encode (f (ofNat α n))).succ = encode (Option.map f (decode n))

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem basis_eq_prod_sub_inv_mul_nodal_div (hi : i ∈ s) :
    Lagrange.basis s v i = C (nodalWeight s v i) * (nodal s v / (X - C (v i)))

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hi : i ∈ s
⊢ Lagrange.basis s v i = C (nodalWeight s v i) * (nodal s v / (X - C (v i)))

Tactic:
simp_rw [Lagrange.basis, basisDivisor, nodalWeight, prod_mul_distrib, map_prod, ←
  nodal_erase_eq_nodal_div hi, nodal]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem EquicontinuousOn.closure' {A : Set Y} {u : Y → X → α} {S : Set X}
    (hA : EquicontinuousOn (u ∘ (↑) : A → X → α) S) (hu : Continuous (S.restrict ∘ u)) :
    EquicontinuousOn (u ∘ (↑) : closure A → X → α) S :=
  fun x hx ↦ (hA x hx).closure' hu <| by exact continuous_apply ⟨x, hx⟩ |>.comp hu

Proof state:
X : Type u_3
Y : Type u_5
α : Type u_6
tX : TopologicalSpace X
tY : TopologicalSpace Y
uα : UniformSpace α
A : Set Y
u : Y → X → α
S : Set X
hA : EquicontinuousOn (u ∘ Subtype.val) S
hu : Continuous (S.restrict ∘ u)
x : X
hx : x ∈ S
⊢ Continuous (eval x ∘ u)

Tactic:
exact continuous_apply ⟨x, hx⟩ |>.comp hu

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem cauchy_neg : ∀ a, (-a : ℝ).cauchy = -a.cauchy
  | ⟨a⟩ => show (neg _).cauchy = _ by rw [neg_def]

Proof state:
a : Cauchy abs
⊢ (Real.neg { cauchy := a }).cauchy = -{ cauchy := a }.cauchy

Tactic:
rw [neg_def]

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
theorem mul_left_apply_of_ne (i : l) (j : m) (a : l) (b : n) (h : a ≠ i) (M : Matrix m n α) :
    (stdBasisMatrix i j c * M) a b = 0

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
a : l
b : n
h : a ≠ i
M : Matrix m n α
⊢ (stdBasisMatrix i j c * M) a b = 0

Tactic:
simp [mul_apply, h.symm]

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma lt_inv_smul_iff_of_pos [PosSMulStrictMono α β] [PosSMulReflectLT α β] (ha : 0 < a) :
    b₁ < a⁻¹ • b₂ ↔ a • b₁ < b₂

Proof state:
α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁵ : GroupWithZero α
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : MulAction α β
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulReflectLT α β
ha : 0 < a
⊢ b₁ < a⁻¹ • b₂ ↔ a • b₁ < b₂

Tactic:
rw [← smul_lt_smul_iff_of_pos_left ha, smul_inv_smul₀ ha.ne']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem pmap_nil {P : α → Prop} (f : ∀ a, P a → β) : pmap f [] (by simp) = [] := rfl

Proof state:
α : Type ?u.2363
β : Type ?u.2362
P : α → Prop
f : (a : α) → P a → β
⊢ ∀ (a : α), a ∈ [] → P a

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem kernelIsoOfEq_inv_comp_ι {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) :
    (kernelIsoOfEq h).inv ≫ kernel.ι _ = kernel.ι _

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernel g
h : f = g
⊢ (kernelIsoOfEq h).inv ≫ kernel.ι f = kernel.ι g

Tactic:
cases h

Result:
case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ inst✝ : HasKernel f
⊢ (kernelIsoOfEq ⋯).inv ≫ kernel.ι f = kernel.ι f

Proof state:
case refl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ inst✝ : HasKernel f
⊢ (kernelIsoOfEq ⋯).inv ≫ kernel.ι f = kernel.ι f

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem update_le_self_iff : update x i a ≤ x ↔ a ≤ x i

Proof state:
ι : Type u_1
π : ι → Type u_4
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → Preorder (π i)
x : (i : ι) → π i
i : ι
a : π i
⊢ update x i a ≤ x ↔ a ≤ x i

Tactic:
simp [update_le_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem append_congr (lw rw : Nat) (lhs lhs' : BitVec lw) (rhs rhs' : BitVec rw) (h1 : lhs' = lhs)
    (h2 : rhs' = rhs) :
    lhs' ++ rhs' = lhs ++ rhs

Proof state:
lw rw : Nat
lhs lhs' : BitVec lw
rhs rhs' : BitVec rw
h1 : lhs' = lhs
h2 : rhs' = rhs
⊢ lhs' ++ rhs' = lhs ++ rhs

Tactic:
simp[*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem lt_asymm {x y : BitVec n} : x < y → ¬ y < x

Proof state:
n : Nat
x y : BitVec n
⊢ x < y → ¬y < x

Tactic:
simp only [lt_def]

Result:
n : Nat
x y : BitVec n
⊢ x.toNat < y.toNat → ¬y.toNat < x.toNat

Proof state:
n : Nat
x y : BitVec n
⊢ x.toNat < y.toNat → ¬y.toNat < x.toNat

Tactic:
apply Nat.lt_asymm

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
theorem natCast_le_cast {m : ℕ} {n : ℚ≥0} : (m : K) ≤ n ↔ (m : ℚ≥0) ≤ n

Proof state:
K : Type u_5
inst✝ : LinearOrderedSemifield K
m : ℕ
n : ℚ≥0
⊢ ↑m ≤ ↑n ↔ ↑m ≤ n

Tactic:
rw [← cast_le (K := K), cast_natCast]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
lemma MapsTo.insert (h : MapsTo f s t) (x : α) : MapsTo f (insert x s) (insert (f x) t)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
x : α
⊢ MapsTo f (Insert.insert x s) (Insert.insert (f x) t)

Tactic:
simpa [← singleton_union] using h.mono_right subset_union_right

Result:
no goals
-- Mathlib/Algebra/Category/Ring/Basic.lean
lemma comp_apply {R S T : RingCat} (f : R ⟶ S) (g : S ⟶ T) (r : R) :
    (f ≫ g) r = g (f r)

Proof state:
R S T : RingCat
f : R ⟶ S
g : S ⟶ T
r : ↑R
⊢ (ConcreteCategory.hom (f ≫ g)) r = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) r)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/RestrictScalars.lean
theorem HasFDerivWithinAt.of_restrictScalars {g' : E →L[𝕜] F} (h : HasFDerivWithinAt f g' s x)
    (H : f'.restrictScalars 𝕜 = g') : HasFDerivWithinAt f f' s x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
f' : E →L[𝕜'] F
s : Set E
x : E
g' : E →L[𝕜] F
h : HasFDerivWithinAt f g' s x
H : ContinuousLinearMap.restrictScalars 𝕜 f' = g'
⊢ HasFDerivWithinAt f f' s x

Tactic:
rw [← H] at h

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
f' : E →L[𝕜'] F
s : Set E
x : E
g' : E →L[𝕜] F
h : HasFDerivWithinAt f (ContinuousLinearMap.restrictScalars 𝕜 f') s x
H : ContinuousLinearMap.restrictScalars 𝕜 f' = g'
⊢ HasFDerivWithinAt f f' s x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst✝⁹ : NontriviallyNormedField 𝕜'
inst✝⁸ : NormedAlgebra 𝕜 𝕜'
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜' E
inst✝⁴ : IsScalarTower 𝕜 𝕜' E
F : Type u_4
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
f' : E →L[𝕜'] F
s : Set E
x : E
g' : E →L[𝕜] F
h : HasFDerivWithinAt f (ContinuousLinearMap.restrictScalars 𝕜 f') s x
H : ContinuousLinearMap.restrictScalars 𝕜 f' = g'
⊢ HasFDerivWithinAt f f' s x

Tactic:
exact .of_isLittleO h.isLittleO

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem cgf_const' [IsFiniteMeasure μ] (hμ : μ ≠ 0) (c : ℝ) :
    cgf (fun _ => c) μ t = log (μ Set.univ).toReal + t * c

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ ¬(μ = 0 ∨ μ Set.univ = ⊤)

Tactic:
simp only [hμ, measure_ne_top μ Set.univ, or_self_iff, not_false_iff]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ cgf (fun x => c) μ t = log (μ Set.univ).toReal + t * c

Tactic:
simp only [cgf, mgf_const']

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ log ((μ Set.univ).toReal * rexp (t * c)) = log (μ Set.univ).toReal + t * c

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ (μ Set.univ).toReal ≠ 0

Tactic:
rw [Ne, ENNReal.toReal_eq_zero_iff, Measure.measure_univ_eq_zero]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ ¬(μ = 0 ∨ μ Set.univ = ⊤)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ log (μ Set.univ).toReal + log (rexp (t * c)) = log (μ Set.univ).toReal + t * c

Tactic:
rw [log_exp _]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ log ((μ Set.univ).toReal * rexp (t * c)) = log (μ Set.univ).toReal + t * c

Tactic:
rw [log_mul _ (exp_pos _).ne']

Result:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ log (μ Set.univ).toReal + log (rexp (t * c)) = log (μ Set.univ).toReal + t * c

Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ (μ Set.univ).toReal ≠ 0
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
@[simp]
lemma DilationEquiv.smulTorsor_preimage_ball {c : P} {k : 𝕜} (hk : k ≠ 0) :
    smulTorsor c hk ⁻¹' (Metric.ball c ‖k‖) = Metric.ball (0 : E) 1

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedDivisionRing 𝕜
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : BoundedSMul 𝕜 E
P : Type u_3
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
k : 𝕜
hk : k ≠ 0
⊢ ⇑(smulTorsor c hk) ⁻¹' Metric.ball c ‖k‖ = Metric.ball 0 1

Tactic:
aesop (add simp norm_smul)

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Constructions.lean
lemma cross_mk {v w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0) :
    cross (mk F v hv) (mk F w hw) =
      if h : crossProduct v w = 0 then mk F v hv else mk F (crossProduct v w) h

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
⊢ Quotient.mk'' ((fun v w => if h : (crossProduct ↑v) ↑w = 0 then v else ⟨(crossProduct ↑v) ↑w, h⟩) ⟨v, hv⟩ ⟨w, hw⟩) =
    if h : (crossProduct v) w = 0 then mk F v hv else mk F ((crossProduct v) w) h

Tactic:
split_ifs with h <;> simp only [h] <;> rfl

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
⊢ (mk F v hv).cross (mk F w hw) = if h : (crossProduct v) w = 0 then mk F v hv else mk F ((crossProduct v) w) h

Tactic:
change Quotient.mk'' _ = _

Result:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
⊢ Quotient.mk'' ((fun v w => if h : (crossProduct ↑v) ↑w = 0 then v else ⟨(crossProduct ↑v) ↑w, h⟩) ⟨v, hv⟩ ⟨w, hw⟩) =
    if h : (crossProduct v) w = 0 then mk F v hv else mk F ((crossProduct v) w) h
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddResult.lean
theorem size_assignments_insertRatUnits {n : Nat} (f : DefaultFormula n)
    (units : CNF.Clause (PosFin n)) :
    (f.insertRatUnits units).1.assignments.size = f.assignments.size

Proof state:
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
⊢ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst.size = f.assignments.size

Tactic:
exact size_insertUnit_fold f.ratUnits f.assignments false

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
⊢ (f.insertRatUnits units).fst.assignments.size = f.assignments.size

Tactic:
simp only [insertRatUnits]

Result:
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
⊢ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst.size = f.assignments.size
-- Mathlib/Algebra/Star/Unitary.lean
lemma toUnits_comp_map : toUnits.comp (map f) = (Units.map f).comp toUnits

Proof state:
F : Type u_2
R : Type u_3
S : Type u_4
inst✝⁶ : Monoid R
inst✝⁵ : StarMul R
inst✝⁴ : Monoid S
inst✝³ : StarMul S
inst✝² : FunLike F R S
inst✝¹ : StarHomClass F R S
inst✝ : MonoidHomClass F R S
f : F
⊢ toUnits.comp (map f) = (Units.map ↑f).comp toUnits

Tactic:
ext

Result:
case h.a
F : Type u_2
R : Type u_3
S : Type u_4
inst✝⁶ : Monoid R
inst✝⁵ : StarMul R
inst✝⁴ : Monoid S
inst✝³ : StarMul S
inst✝² : FunLike F R S
inst✝¹ : StarHomClass F R S
inst✝ : MonoidHomClass F R S
f : F
x✝ : ↥(unitary R)
⊢ ↑((toUnits.comp (map f)) x✝) = ↑(((Units.map ↑f).comp toUnits) x✝)

Proof state:
case h.a
F : Type u_2
R : Type u_3
S : Type u_4
inst✝⁶ : Monoid R
inst✝⁵ : StarMul R
inst✝⁴ : Monoid S
inst✝³ : StarMul S
inst✝² : FunLike F R S
inst✝¹ : StarHomClass F R S
inst✝ : MonoidHomClass F R S
f : F
x✝ : ↥(unitary R)
⊢ ↑((toUnits.comp (map f)) x✝) = ↑(((Units.map ↑f).comp toUnits) x✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem eq_eq_of_isGE_of_isGE_swap {o : Ordering} : o.isGE → o.swap.isGE → o = .eq

Proof state:
o : Ordering
⊢ o.isGE = true → o.swap.isGE = true → o = eq

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Topology/Connected/Basic.lean
theorem mem_connectedComponentIn {x : α} {F : Set α} (hx : x ∈ F) :
    x ∈ connectedComponentIn F x

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
hx : x ∈ F
⊢ x ∈ connectedComponentIn F x

Tactic:
simp [connectedComponentIn_eq_image hx, mem_connectedComponent, hx]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean
theorem closedBall_rpow_sub_one_eq_empty_aux {r t : ℝ} (hr : 0 < r) (ht : 1 < t) :
    Metric.closedBall (0 : E) (t ^ (-r⁻¹) - 1) = ∅

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 1 < t
⊢ Metric.closedBall 0 (t ^ (-r⁻¹) - 1) = ∅

Tactic:
rw [Metric.closedBall_eq_empty, sub_neg]

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 1 < t
⊢ t ^ (-r⁻¹) < 1

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 1 < t
⊢ t ^ (-r⁻¹) < 1

Tactic:
exact Real.rpow_lt_one_of_one_lt_of_neg ht (by simp only [hr, Right.neg_neg_iff, inv_pos])

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 1 < t
⊢ -r⁻¹ < 0

Tactic:
simp only [hr, Right.neg_neg_iff, inv_pos]

Result:
no goals
-- Mathlib/Topology/Separation/SeparatedNhds.lean
theorem Set.hasSeparatingCover_empty_left (s : Set X) : HasSeparatingCover ∅ s :=
  ⟨fun _ ↦ ∅, empty_subset (⋃ _, ∅),
   fun _ ↦ ⟨isOpen_empty, by simp only [closure_empty, empty_disjoint]⟩⟩

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
x✝ : ℕ
⊢ Disjoint (closure ((fun x => ∅) x✝)) s

Tactic:
simp only [closure_empty, empty_disjoint]

Result:
no goals
-- Mathlib/LinearAlgebra/Projection.lean
theorem prodEquivOfIsCompl_symm_apply_right (h : IsCompl p q) (x : q) :
    (prodEquivOfIsCompl p q h).symm x = (0, x) :=
  (prodEquivOfIsCompl p q h).symm_apply_eq.2 <| by simp

Proof state:
R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : ↥q
⊢ ↑x = (p.prodEquivOfIsCompl q h) (0, x)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
theorem sheafifyMap_sheafifyLift {P Q R : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (γ : Q ⟶ R)
    (hR : Presheaf.IsSheaf J R) :
    J.sheafifyMap η ≫ J.sheafifyLift γ hR = J.sheafifyLift (η ≫ γ) hR

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ J.sheafifyMap η ≫ J.sheafifyLift γ hR = J.sheafifyLift (η ≫ γ) hR

Tactic:
apply J.sheafifyLift_unique

Result:
case a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ J.toSheafify P ≫ J.sheafifyMap η ≫ J.sheafifyLift γ hR = η ≫ γ

Proof state:
case a
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
hR : Presheaf.IsSheaf J R
⊢ J.toSheafify P ≫ J.sheafifyMap η ≫ J.sheafifyLift γ hR = η ≫ γ

Tactic:
rw [← Category.assoc, ← J.toSheafify_naturality, Category.assoc, toSheafify_sheafifyLift]

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
theorem toNNRat_lt_toNNRat_iff' : toNNRat q < toNNRat p ↔ q < p ∧ 0 < p

Proof state:
p q : ℚ
⊢ q.toNNRat < p.toNNRat ↔ q < p ∧ 0 < p

Tactic:
simp [← coe_lt_coe, toNNRat, lt_irrefl]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem nonempty_sUnion {S : Set (Set α)} : (⋃₀ S).Nonempty ↔ ∃ s ∈ S, Set.Nonempty s

Proof state:
α : Type u_1
S : Set (Set α)
⊢ (⋃₀ S).Nonempty ↔ ∃ s ∈ S, s.Nonempty

Tactic:
simp [nonempty_iff_ne_empty]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/UV.lean
theorem compress_of_disjoint_of_le' (hva : Disjoint v a) (hua : u ≤ a) :
    compress u v ((a ⊔ v) \ u) = a

Proof state:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
u v a : α
hva : Disjoint v a
hua : u ≤ a
⊢ compress u v ((a ⊔ v) \ u) = a

Tactic:
rw [compress_of_disjoint_of_le disjoint_sdiff_self_right
    (le_sdiff.2 ⟨(le_sup_right : v ≤ a ⊔ v), hva.mono_right hua⟩),
  sdiff_sup_cancel (le_sup_of_le_left hua), hva.symm.sup_sdiff_cancel_right]

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem natDegree_basisDivisor_self : (basisDivisor x x).natDegree = 0

Proof state:
F : Type u_1
inst✝ : Field F
x : F
⊢ (basisDivisor x x).natDegree = 0

Tactic:
rw [basisDivisor_self, natDegree_zero]

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem mem_singleton {a b : α} : b ∈ ({a} : Multiset α) ↔ b = a

Proof state:
α : Type u_1
a b : α
⊢ b ∈ {a} ↔ b = a

Tactic:
simp only [← cons_zero, mem_cons, iff_self, or_false, not_mem_zero]

Result:
no goals
-- Mathlib/Data/Finset/SMulAntidiagonal.lean
theorem IsWF.min_smul [LinearOrder G] [LinearOrder P] [SMul G P] [IsOrderedCancelSMul G P]
    {s : Set G} {t : Set P} (hs : s.IsWF) (ht : t.IsWF) (hsn : s.Nonempty) (htn : t.Nonempty) :
    (hs.smul ht).min (hsn.smul htn) = hs.min hsn • ht.min htn

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ ∀ b ∈ s • t, hs.min hsn • ht.min htn ≤ b

Tactic:
rintro _ ⟨x, hx, y, hy, rfl⟩

Result:
case intro.intro.intro.intro
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
x : G
hx : x ∈ s
y : P
hy : y ∈ t
⊢ hs.min hsn • ht.min htn ≤ (fun x1 x2 => x1 • x2) x y

Proof state:
case intro.intro.intro.intro
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
x : G
hx : x ∈ s
y : P
hy : y ∈ t
⊢ hs.min hsn • ht.min htn ≤ (fun x1 x2 => x1 • x2) x y

Tactic:
exact IsOrderedSMul.smul_le_smul (hs.min_le _ hx) (ht.min_le _ hy)

Result:
no goals

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ hs.min hsn • ht.min htn ≤ ⋯.min ⋯

Tactic:
rw [IsWF.le_min_iff]

Result:
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ ∀ b ∈ s • t, hs.min hsn • ht.min htn ≤ b

Proof state:
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ ⋯.min ⋯ = hs.min hsn • ht.min htn

Tactic:
refine le_antisymm (IsWF.min_le _ _ (mem_smul.2 ⟨_, hs.min_mem _, _, ht.min_mem _, rfl⟩)) ?_

Result:
G : Type u_1
P : Type u_2
inst✝³ : LinearOrder G
inst✝² : LinearOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
s : Set G
t : Set P
hs : s.IsWF
ht : t.IsWF
hsn : s.Nonempty
htn : t.Nonempty
⊢ hs.min hsn • ht.min htn ≤ ⋯.min ⋯
-- Mathlib/Algebra/Module/Submodule/Range.lean
@[simp]
lemma comap_subtype_le_iff {p q r : Submodule R M} :
    q.comap p.subtype ≤ r.comap p.subtype ↔ p ⊓ q ≤ p ⊓ r :=
  ⟨fun h ↦ by simpa using map_mono (f := p.subtype) h,
   fun h ↦ by simpa using comap_mono (f := p.subtype) h⟩

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q r : Submodule R M
h : p ⊓ q ≤ p ⊓ r
⊢ comap p.subtype q ≤ comap p.subtype r

Tactic:
simpa using comap_mono (f := p.subtype) h

Result:
no goals

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q r : Submodule R M
h : comap p.subtype q ≤ comap p.subtype r
⊢ p ⊓ q ≤ p ⊓ r

Tactic:
simpa using map_mono (f := p.subtype) h

Result:
no goals