harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Rat/Cast/Order.lean
theorem cast_strictMono : StrictMono ((↑) : ℚ≥0 → K) := fun p q h => by
  rwa [NNRat.cast_def, NNRat.cast_def, div_lt_div_iff₀, ← Nat.cast_mul, ← Nat.cast_mul,
    Nat.cast_lt (α := K), ← NNRat.lt_def]
  · simp
  · simp

Proof state:
K : Type u_5
inst✝ : LinearOrderedSemifield K
p q : ℚ≥0
h : p < q
⊢ ↑p < ↑q

Tactic:
rwa [NNRat.cast_def, NNRat.cast_def, div_lt_div_iff₀, ← Nat.cast_mul, ← Nat.cast_mul,
  Nat.cast_lt (α := K), ← NNRat.lt_def]

Result:
case hb
K : Type u_5
inst✝ : LinearOrderedSemifield K
p q : ℚ≥0
h : p < q
⊢ 0 < ↑p.den

case hd
K : Type u_5
inst✝ : LinearOrderedSemifield K
p q : ℚ≥0
h : p < q
⊢ 0 < ↑q.den

Proof state:
case hb
K : Type u_5
inst✝ : LinearOrderedSemifield K
p q : ℚ≥0
h : p < q
⊢ 0 < ↑p.den

Tactic:
simp

Result:
no goals

Proof state:
case hd
K : Type u_5
inst✝ : LinearOrderedSemifield K
p q : ℚ≥0
h : p < q
⊢ 0 < ↑q.den

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem derivWithin.scomp (hg : DifferentiableWithinAt 𝕜' g₁ t' (h x))
    (hh : DifferentiableWithinAt 𝕜 h s x) (hs : MapsTo h s t') :
    derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

case inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Proof state:
case inl
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Tactic:
exact (HasDerivWithinAt.scomp x hg.hasDerivWithinAt hh.hasDerivWithinAt hs).derivWithin hxs

Result:
no goals

Proof state:
case inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
t' : Set 𝕜'
h : 𝕜 → 𝕜'
g₁ : 𝕜' → F
hg : DifferentiableWithinAt 𝕜' g₁ t' (h x)
hh : DifferentiableWithinAt 𝕜 h s x
hs : MapsTo h s t'
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Antilipschitz.lean
theorem to_rightInvOn' {s : Set α} (hf : AntilipschitzWith K (s.restrict f)) {g : β → α}
    {t : Set β} (g_maps : MapsTo g t s) (g_inv : RightInvOn g f t) :
    LipschitzWith K (t.restrict g) := fun x y => by
  simpa only [restrict_apply, g_inv x.mem, g_inv y.mem, Subtype.edist_mk_mk]
    using hf ⟨g x, g_maps x.mem⟩ ⟨g y, g_maps y.mem⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
s : Set α
hf : AntilipschitzWith K (s.restrict f)
g : β → α
t : Set β
g_maps : MapsTo g t s
g_inv : RightInvOn g f t
x y : ↑t
⊢ edist (t.restrict g x) (t.restrict g y) ≤ ↑K * edist x y

Tactic:
simpa only [restrict_apply, g_inv x.mem, g_inv y.mem, Subtype.edist_mk_mk]
  using hf ⟨g x, g_maps x.mem⟩ ⟨g y, g_maps y.mem⟩

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma LeftHomologyData.exact_iff [S.HasHomology]
    (h : S.LeftHomologyData) :
    S.Exact ↔ IsZero h.H

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ S.Exact ↔ IsZero h.H

Tactic:
rw [S.exact_iff_isZero_homology]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ IsZero S.homology ↔ IsZero h.H

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
h : S.LeftHomologyData
⊢ IsZero S.homology ↔ IsZero h.H

Tactic:
exact Iso.isZero_iff h.homologyIso

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem integrable_comp_iff ⦃f : γ → E⦄ (hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)) :
    Integrable f ((η ∘ₖ κ) a) ↔
    (∀ᵐ y ∂κ a, Integrable f (η y)) ∧ Integrable (fun y ↦ ∫ z, ‖f z‖ ∂η y) (κ a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
f : γ → E
hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ Integrable f ((η ∘ₖ κ) a) ↔ (∀ᵐ (y : β) ∂κ a, Integrable f (η y)) ∧ Integrable (fun y => ∫ (z : γ), ‖f z‖ ∂η y) (κ a)

Tactic:
simp only [Integrable, hf, hasFiniteIntegral_comp_iff' hf, true_and, eventually_and, hf.comp,
  hf.norm.integral_kernel_comp]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Basic.lean
theorem measure_iUnion_null_iff {ι : Sort*} [Countable ι] {s : ι → Set α} :
    μ (⋃ i, s i) = 0 ↔ ∀ i, μ (s i) = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
μ : F
ι : Sort u_4
inst✝ : Countable ι
s : ι → Set α
⊢ μ (⋃ i, s i) = 0 ↔ ∀ (i : ι), μ (s i) = 0

Tactic:
rw [← sUnion_range, measure_sUnion_null_iff (countable_range s), forall_mem_range]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
lemma ker_equiv_comp (f : R →+* S) (e : S ≃+* T) :
    ker (e.toRingHom.comp f) = RingHom.ker f

Proof state:
R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
e : S ≃+* T
⊢ ker (e.toRingHom.comp f) = ker f

Tactic:
rw [← RingHom.comap_ker, RingEquiv.toRingHom_eq_coe, RingHom.ker_coe_equiv, RingHom.ker]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem image_ball (h : α ≃ᵢ β) (x : α) (r : ℝ) : h '' Metric.ball x r = Metric.ball (h x) r

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ
⊢ ⇑h '' Metric.ball x r = Metric.ball (h x) r

Tactic:
rw [← h.preimage_symm, h.symm.preimage_ball, symm_symm]

Result:
no goals
-- Mathlib/Algebra/Algebra/Tower.lean
theorem algebraMap_smul [SMul R M] [IsScalarTower R A M] (r : R) (x : M) :
    algebraMap R A r • x = r • x

Proof state:
R : Type u
A : Type w
M : Type v₁
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : MulAction A M
inst✝¹ : SMul R M
inst✝ : IsScalarTower R A M
r : R
x : M
⊢ (algebraMap R A) r • x = r • x

Tactic:
rw [Algebra.algebraMap_eq_smul_one, smul_assoc, one_smul]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
theorem map_ratCast [DivisionRing α] [DivisionRing β] [RingHomClass F α β] (f : F) (q : ℚ) :
    f q = q

Proof state:
F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : FunLike F α β
inst✝² : DivisionRing α
inst✝¹ : DivisionRing β
inst✝ : RingHomClass F α β
f : F
q : ℚ
⊢ f ↑q = ↑q

Tactic:
rw [cast_def, map_div₀, map_intCast, map_natCast, cast_def]

Result:
no goals
-- Mathlib/Computability/TMToPartrec.lean
theorem codeSupp_cons (f fs k) :
    codeSupp (Code.cons f fs) k =
      trStmts₁ (trNormal (Code.cons f fs) k) ∪ codeSupp f (Cont'.cons₁ fs k)

Proof state:
f fs : Code
k : Cont'
⊢ codeSupp (f.cons fs) k = trStmts₁ (trNormal (f.cons fs) k) ∪ codeSupp f (Cont'.cons₁ fs k)

Tactic:
simp [codeSupp, codeSupp', contSupp, Finset.union_assoc]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/MStructure.lean
theorem distrib_lattice_lemma [FaithfulSMul M X] {P Q R : { P : M // IsLprojection X P }} :
    ((↑P : M) + ↑Pᶜ * R) * (↑P + ↑Q * ↑R * ↑Pᶜ) = ↑P + ↑Q * ↑R * ↑Pᶜ

Proof state:
X : Type u_1
inst✝³ : NormedAddCommGroup X
M : Type u_2
inst✝² : Ring M
inst✝¹ : Module M X
inst✝ : FaithfulSMul M X
P Q R : { P // IsLprojection X P }
⊢ (↑P + ↑Pᶜ * ↑R) * (↑P + ↑Q * ↑R * ↑Pᶜ) = ↑P + ↑Q * ↑R * ↑Pᶜ

Tactic:
rw [add_mul, mul_add, mul_add, (mul_assoc _ (R : M) (↑Q * ↑R * ↑Pᶜ)),
  ← mul_assoc (R : M) (↑Q * ↑R) _, ← coe_inf Q, (Pᶜ.prop.commute R.prop).eq,
  ((Q ⊓ R).prop.commute Pᶜ.prop).eq, (R.prop.commute (Q ⊓ R).prop).eq, coe_inf Q,
  mul_assoc (Q : M), ← mul_assoc, mul_assoc (R : M), (Pᶜ.prop.commute P.prop).eq, mul_compl_self,
  zero_mul, mul_zero, zero_add, add_zero, ← mul_assoc, P.prop.proj.eq,
  R.prop.proj.eq, ← coe_inf Q, mul_assoc, ((Q ⊓ R).prop.commute Pᶜ.prop).eq, ← mul_assoc,
  Pᶜ.prop.proj.eq]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Normalize.lean
theorem evalWhiskerLeft_comp
    {f : a ⟶ b} {g : b ⟶ c} {h i : c ⟶ d}
    {η : h ⟶ i} {η₁ : g ≫ h ⟶ g ≫ i} {η₂ : f ≫ g ≫ h ⟶ f ≫ g ≫ i}
    {η₃ : f ≫ g ≫ h ⟶ (f ≫ g) ≫ i} {η₄ : (f ≫ g) ≫ h ⟶ (f ≫ g) ≫ i}
    (e_η₁ : g ◁ η = η₁) (e_η₂ : f ◁ η₁ = η₂)
    (e_η₃ : η₂ ≫ (α_ _ _ _).inv = η₃) (e_η₄ : (α_ _ _ _).hom ≫ η₃ = η₄) :
    (f ≫ g) ◁ η = η₄

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h i : c ⟶ d
η : h ⟶ i
η₁ : g ≫ h ⟶ g ≫ i
η₂ : f ≫ g ≫ h ⟶ f ≫ g ≫ i
η₃ : f ≫ g ≫ h ⟶ (f ≫ g) ≫ i
η₄ : (f ≫ g) ≫ h ⟶ (f ≫ g) ≫ i
e_η₁ : g ◁ η = η₁
e_η₂ : f ◁ η₁ = η₂
e_η₃ : η₂ ≫ (α_ f g i).inv = η₃
e_η₄ : (α_ f g h).hom ≫ η₃ = η₄
⊢ (f ≫ g) ◁ η = η₄

Tactic:
simp [e_η₁, e_η₂, e_η₃, e_η₄]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem _root_.stronglyMeasurable_iff_measurable_separable {m : MeasurableSpace α}
    [TopologicalSpace β] [PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] :
    StronglyMeasurable f ↔ Measurable f ∧ IsSeparable (range f)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
x✝ : Measurable f ∧ IsSeparable (range f)
Hm : Measurable f
Hsep : IsSeparable (range f)
⊢ StronglyMeasurable f

Tactic:
have := Hsep.secondCountableTopology

Result:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
x✝ : Measurable f ∧ IsSeparable (range f)
Hm : Measurable f
Hsep : IsSeparable (range f)
this : SecondCountableTopology ↑(range f)
⊢ StronglyMeasurable f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
x✝ : Measurable f ∧ IsSeparable (range f)
Hm : Measurable f
Hsep : IsSeparable (range f)
this : SecondCountableTopology ↑(range f)
⊢ StronglyMeasurable f

Tactic:
have Hm' : StronglyMeasurable (rangeFactorization f) := Hm.subtype_mk.stronglyMeasurable

Result:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
x✝ : Measurable f ∧ IsSeparable (range f)
Hm : Measurable f
Hsep : IsSeparable (range f)
this : SecondCountableTopology ↑(range f)
Hm' : StronglyMeasurable (rangeFactorization f)
⊢ StronglyMeasurable f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
⊢ StronglyMeasurable f ↔ Measurable f ∧ IsSeparable (range f)

Tactic:
refine ⟨fun H ↦ ⟨H.measurable, H.isSeparable_range⟩, fun ⟨Hm, Hsep⟩  ↦ ?_⟩

Result:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
x✝ : Measurable f ∧ IsSeparable (range f)
Hm : Measurable f
Hsep : IsSeparable (range f)
⊢ StronglyMeasurable f

Proof state:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝³ : TopologicalSpace β
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
x✝ : Measurable f ∧ IsSeparable (range f)
Hm : Measurable f
Hsep : IsSeparable (range f)
this : SecondCountableTopology ↑(range f)
Hm' : StronglyMeasurable (rangeFactorization f)
⊢ StronglyMeasurable f

Tactic:
exact continuous_subtype_val.comp_stronglyMeasurable Hm'

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffDist_zero_iff_closure_eq_closure (fin : hausdorffEdist s t ≠ ⊤) :
    hausdorffDist s t = 0 ↔ closure s = closure t

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
fin : hausdorffEdist s t ≠ ⊤
⊢ hausdorffDist s t = 0 ↔ closure s = closure t

Tactic:
simp [← hausdorffEdist_zero_iff_closure_eq_closure, hausdorffDist,
  ENNReal.toReal_eq_zero_iff, fin]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_C_lt_degree_C_mul_X (ha : a ≠ 0) : degree (C b) < degree (C a * X)

Proof state:
R : Type u
a b : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C b).degree < (C a * X).degree

Tactic:
simpa only [degree_C_mul_X ha] using degree_C_lt

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_finset [MeasurableSingletonClass α] (s : Finset α) (f : α → ℝ≥0∞) :
    ∫⁻ x in s, f x ∂μ = ∑ x ∈ s, f x * μ {x}

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst✝ : MeasurableSingletonClass α
s : Finset α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in ↑s, f x ∂μ = ∑ x ∈ s, f x * μ {x}

Tactic:
simp only [lintegral_countable _ s.countable_toSet, ← Finset.tsum_subtype']

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem disjoint_nhds_nhds_iff_not_inseparable : Disjoint (𝓝 x) (𝓝 y) ↔ ¬Inseparable x y

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
x y : X
⊢ Disjoint (𝓝 x) (𝓝 y) ↔ ¬Inseparable x y

Tactic:
rw [disjoint_nhds_nhds_iff_not_specializes, specializes_iff_inseparable]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
@[simp] lemma closure_union_closure_left_eq (M : Matroid α) (X Y : Set α) :
    M.closure (M.closure X ∪ Y) = M.closure (X ∪ Y)

Proof state:
α : Type u_2
M : Matroid α
X Y : Set α
⊢ M.closure (M.closure X ∪ Y) = M.closure (X ∪ Y)

Tactic:
rw [← closure_closure_union_closure_eq_closure_union, closure_closure,
  closure_closure_union_closure_eq_closure_union]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
theorem inv_eq_of_mul (h : a * b = 1) : a⁻¹ = b

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b : G₀
h : a * b = 1
⊢ a⁻¹ = b

Tactic:
rw [← inv_mul_cancel_left₀ (left_ne_zero_of_mul_eq_one h) b, h, mul_one]

Result:
no goals
-- Mathlib/Order/Category/HeytAlg.lean
lemma id_apply (X : HeytAlg) (x : X) :
    (𝟙 X : X ⟶ X) x = x

Proof state:
X : HeytAlg
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem diag_injective : Function.Injective (Sym2.diag : α → Sym2 α) := fun x y h => by
  cases Sym2.exact h <;> rfl

Proof state:
α : Type u_1
x y : α
h : diag x = diag y
⊢ x = y

Tactic:
cases Sym2.exact h <;> rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem contDiff_iff_iteratedDeriv {n : ℕ∞} : ContDiff 𝕜 n f ↔
    (∀ m : ℕ, (m : ℕ∞) ≤ n → Continuous (iteratedDeriv m f)) ∧
      ∀ m : ℕ, (m : ℕ∞) < n → Differentiable 𝕜 (iteratedDeriv m f)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
n : ℕ∞
⊢ ContDiff 𝕜 (↑n) f ↔
    (∀ (m : ℕ), ↑m ≤ n → Continuous (iteratedDeriv m f)) ∧ ∀ (m : ℕ), ↑m < n → Differentiable 𝕜 (iteratedDeriv m f)

Tactic:
simp only [contDiff_iff_continuous_differentiable, iteratedFDeriv_eq_equiv_comp,
  LinearIsometryEquiv.comp_continuous_iff, LinearIsometryEquiv.comp_differentiable_iff]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigO_iff : f =O[l] g ↔ ∃ c : ℝ, ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
⊢ f =O[l] g ↔ ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖

Tactic:
simp only [IsBigO_def, IsBigOWith_def]

Result:
no goals
-- Mathlib/Order/Filter/Pointwise.lean
theorem pure_mul_pure : (pure a : Filter α) * pure b = pure (a * b)

Proof state:
α : Type u_2
inst✝ : Mul α
a b : α
⊢ pure a * pure b = pure (a * b)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem leadingCoeff_X_pow_sub_C {n : ℕ} (hn : 0 < n) {r : R} :
    (X ^ n - C r).leadingCoeff = 1

Proof state:
R : Type u
inst✝ : Ring R
n : ℕ
hn : 0 < n
r : R
⊢ (X ^ n - C r).leadingCoeff = 1

Tactic:
rw [sub_eq_add_neg, ← map_neg C r, leadingCoeff_X_pow_add_C hn]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem IsProbabilityMeasure.ne_zero (μ : Measure α) [IsProbabilityMeasure μ] : μ ≠ 0 :=
  mt measure_univ_eq_zero.2 <| by simp [measure_univ]

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

Tactic:
simp [measure_univ]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/Over/Connected.lean
theorem raised_cone_lowers_to_original [IsConnected J] {B : C} {F : J ⥤ Over B}
    (c : Cone (F ⋙ forget B)) :
    (forget B).mapCone (raiseCone c) = c

Proof state:
J : Type u'
inst✝² : Category.{v', u'} J
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsConnected J
B : C
F : J ⥤ Over B
c : Cone (F ⋙ forget B)
⊢ (forget B).mapCone (raiseCone c) = c

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem Function.true_comp {f : α → β} : ((fun _ => true) ∘ f) = fun _ => true

Proof state:
α : Sort u_1
β : Sort u_2
f : α → β
⊢ (fun x => true) ∘ f = fun x => true

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Dual.lean
theorem inclusionInDoubleDual_norm_le : ‖inclusionInDoubleDual 𝕜 E‖ ≤ 1

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ ‖ContinuousLinearMap.id 𝕜 (Dual 𝕜 E)‖ ≤ 1

Tactic:
exact ContinuousLinearMap.norm_id_le

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ ‖inclusionInDoubleDual 𝕜 E‖ ≤ 1

Tactic:
rw [inclusionInDoubleDual_norm_eq]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
⊢ ‖ContinuousLinearMap.id 𝕜 (Dual 𝕜 E)‖ ≤ 1
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_le_div (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
hb : 0 < b
⊢ 1 ≤ a / b ↔ b ≤ a

Tactic:
rw [le_div_iff₀ hb, one_mul]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
lemma krullDim_nonpos_iff_forall_isMin : krullDim α ≤ 0 ↔ ∀ x : α, IsMin x

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ (∀ (x : α) ⦃b : α⦄, x ≤ b → b ≤ x) ↔ ∀ (x : α) ⦃b : α⦄, b ≤ x → x ≤ b

Tactic:
exact forall_swap

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ krullDim α ≤ 0 ↔ ∀ (x : α), IsMin x

Tactic:
simp only [krullDim_nonpos_iff_forall_isMax, IsMax, IsMin]

Result:
α : Type u_1
inst✝ : Preorder α
⊢ (∀ (x : α) ⦃b : α⦄, x ≤ b → b ≤ x) ↔ ∀ (x : α) ⦃b : α⦄, b ≤ x → x ≤ b
-- Mathlib/Order/UpperLower/Basic.lean
theorem prod_le_prod_iff : s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₁ = ⊥ ∨ t₁ = ⊥ :=
  prod_subset_prod_iff.trans <| by simp

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s₁ s₂ : LowerSet α
t₁ t₂ : LowerSet β
⊢ ↑s₁ ⊆ ↑s₂ ∧ ↑t₁ ⊆ ↑t₂ ∨ ↑s₁ = ∅ ∨ ↑t₁ = ∅ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₁ = ⊥ ∨ t₁ = ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem gcd_image [DecidableEq β] {g : γ → β} (s : Finset γ) :
    (s.image g).gcd f = s.gcd (f ∘ g)

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
s : Finset γ
⊢ (image g s).gcd f = s.gcd (f ∘ g)

Tactic:
induction s using Finset.induction <;> simp [*]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
f : β → α
inst✝ : DecidableEq β
g : γ → β
s : Finset γ
⊢ (image g s).gcd f = s.gcd (f ∘ g)

Tactic:
classical induction s using Finset.induction <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem sinh_neg_iff : sinh x < 0 ↔ x < 0

Proof state:
x : ℝ
⊢ sinh x < 0 ↔ x < 0

Tactic:
simpa only [sinh_zero] using @sinh_lt_sinh x 0

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
theorem ind {β : G.ComponentCompl K → Prop}
    (f : ∀ ⦃v⦄ (hv : v ∉ K), β (G.componentComplMk hv)) : ∀ C : G.ComponentCompl K, β C

Proof state:
V : Type u
G : SimpleGraph V
K : Set V
β : G.ComponentCompl K → Prop
f : ∀ ⦃v : V⦄ (hv : v ∉ K), β (G.componentComplMk hv)
⊢ ∀ (C : G.ComponentCompl K), β C

Tactic:
apply ConnectedComponent.ind

Result:
case h
V : Type u
G : SimpleGraph V
K : Set V
β : G.ComponentCompl K → Prop
f : ∀ ⦃v : V⦄ (hv : v ∉ K), β (G.componentComplMk hv)
⊢ ∀ (v : ↑Kᶜ), β ((induce Kᶜ G).connectedComponentMk v)

Proof state:
case h
V : Type u
G : SimpleGraph V
K : Set V
β : G.ComponentCompl K → Prop
f : ∀ ⦃v : V⦄ (hv : v ∉ K), β (G.componentComplMk hv)
⊢ ∀ (v : ↑Kᶜ), β ((induce Kᶜ G).connectedComponentMk v)

Tactic:
exact fun ⟨v, vnK⟩ => f vnK

Result:
no goals
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp.lean
lemma id_apply (M : SemiNormedGrp) (r : M) :
    (𝟙 M : M ⟶ M) r = r

Proof state:
M : SemiNormedGrp
r : M.carrier
⊢ (ConcreteCategory.hom (𝟙 M)) r = r

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monad/Basic.lean
lemma map_unit_app (T : Monad C) (X : C) [IsIso T.μ] :
    T.map (T.η.app X) = T.η.app (T.obj X)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
X : C
inst✝ : IsIso T.μ
⊢ T.map (T.η.app X) = T.η.app (T.obj X)

Tactic:
simp [← cancel_mono (T.μ.app _)]

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Defs.lean
theorem mod_add_div' (m k : R) : m % k + m / k * k = m

Proof state:
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m % k + m / k * k = m

Tactic:
rw [mul_comm]

Result:
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m % k + k * (m / k) = m

Proof state:
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m % k + k * (m / k) = m

Tactic:
exact mod_add_div _ _

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
@[simp] lemma truncatedSup_empty (a : α) : truncatedSup ∅ a = ⊤ := truncatedSup_of_not_mem (by simp)

Proof state:
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : OrderTop α
a : α
⊢ a ∉ lowerClosure ↑∅

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
/-- See `ENNReal.mul_inv_cancel_right'` for a stronger version. -/
protected lemma mul_inv_cancel_right (hb₀ : b ≠ 0) (hb : b ≠ ∞) : a * b * b⁻¹ = a :=
  ENNReal.mul_inv_cancel_right' (by simp [hb₀]) (by simp [hb])

Proof state:
a b : ℝ≥0∞
hb₀ : b ≠ 0
hb : b ≠ ⊤
⊢ b = 0 → a = 0

Tactic:
simp [hb₀]

Result:
no goals

Proof state:
a b : ℝ≥0∞
hb₀ : b ≠ 0
hb : b ≠ ⊤
⊢ b = ⊤ → a = 0

Tactic:
simp [hb]

Result:
no goals