harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Heyting/Basic.lean
theorem sdiff_le_sdiff_of_sup_le_sup_right (h : a ⊔ c ≤ b ⊔ c) : a \ c ≤ b \ c

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
h : a ⊔ c ≤ b ⊔ c
⊢ a \ c ≤ b \ c

Tactic:
rw [← sup_sdiff_right_self, ← @sup_sdiff_right_self _ _ b]

Result:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
h : a ⊔ c ≤ b ⊔ c
⊢ (a ⊔ c) \ c ≤ (b ⊔ c) \ c

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
h : a ⊔ c ≤ b ⊔ c
⊢ (a ⊔ c) \ c ≤ (b ⊔ c) \ c

Tactic:
exact sdiff_le_sdiff_right h

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma one_lt_inv₀ (ha : 0 < a) : 1 < a⁻¹ ↔ a < 1

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
⊢ 1 < a⁻¹ ↔ a < 1

Tactic:
simpa using one_lt_inv_mul₀ ha (b := 1)

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean
theorem Pi.hasProd {f : ι → ∀ x, π x} {g : ∀ x, π x} :
    HasProd f g ↔ ∀ x, HasProd (fun i ↦ f i x) (g x)

Proof state:
α : Type u_1
ι : Type u_4
π : α → Type u_5
inst✝¹ : (x : α) → CommMonoid (π x)
inst✝ : (x : α) → TopologicalSpace (π x)
f : ι → (x : α) → π x
g : (x : α) → π x
⊢ HasProd f g ↔ ∀ (x : α), HasProd (fun i => f i x) (g x)

Tactic:
simp only [HasProd, tendsto_pi_nhds, prod_apply]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc]
lemma RightHomologyData.rightHomologyIso_hom_naturality
    (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
    h₁.homologyIso.hom ≫ rightHomologyMap' φ h₁ h₂ =
      homologyMap φ ≫ h₂.homologyIso.hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
⊢ h₁.homologyIso.hom ≫ rightHomologyMap' φ h₁ h₂ = homologyMap φ ≫ h₂.homologyIso.hom

Tactic:
rw [← cancel_epi h₁.homologyIso.inv, Iso.inv_hom_id_assoc,
  ← cancel_epi (leftRightHomologyComparison' S₁.leftHomologyData h₁),
  ← leftRightHomologyComparison'_naturality φ S₁.leftHomologyData h₁ S₂.leftHomologyData h₂,
  ← cancel_epi (S₁.leftHomologyData.homologyIso.hom),
  LeftHomologyData.leftHomologyIso_hom_naturality_assoc,
  leftRightHomologyComparison'_fac, leftRightHomologyComparison'_fac, assoc,
  Iso.hom_inv_id_assoc, Iso.hom_inv_id_assoc, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem smul_continuousOn [LocallyCompactSpace X] [T2Space X] {𝕜 : Type*} [NormedField 𝕜]
    [SecondCountableTopologyEither X E] [NormedSpace 𝕜 E] {f : X → 𝕜} {g : X → E} {s : Set X}
    (hs : IsLocallyClosed s) (hf : LocallyIntegrableOn f s μ) (hg : ContinuousOn g s) :
    LocallyIntegrableOn (fun x => f x • g x) s μ

Proof state:
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
μ : Measure X
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : LocallyCompactSpace X
inst✝³ : T2Space X
𝕜 : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : SecondCountableTopologyEither X E
inst✝ : NormedSpace 𝕜 E
f : X → 𝕜
g : X → E
s : Set X
hs : IsLocallyClosed s
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
⊢ LocallyIntegrableOn (fun x => f x • g x) s μ

Tactic:
rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢

Result:
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
μ : Measure X
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : LocallyCompactSpace X
inst✝³ : T2Space X
𝕜 : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : SecondCountableTopologyEither X E
inst✝ : NormedSpace 𝕜 E
f : X → 𝕜
g : X → E
s : Set X
hs : IsLocallyClosed s
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn (fun x => f x • g x) k μ

Proof state:
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
μ : Measure X
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : LocallyCompactSpace X
inst✝³ : T2Space X
𝕜 : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : SecondCountableTopologyEither X E
inst✝ : NormedSpace 𝕜 E
f : X → 𝕜
g : X → E
s : Set X
hs : IsLocallyClosed s
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn (fun x => f x • g x) k μ

Tactic:
exact fun k hk_sub hk_c => (hf k hk_sub hk_c).smul_continuousOn (hg.mono hk_sub) hk_c

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Int.lean
theorem isInteger_smul {a : R} {x : M'} (hx : IsInteger f x) : IsInteger f (a • x)

Proof state:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
a : R
x : M'
x' : M
hx : f x' = x
⊢ f (a • x') = a • x

Tactic:
rw [← hx, LinearMapClass.map_smul]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
a : R
x : M'
hx : IsInteger f x
⊢ IsInteger f (a • x)

Tactic:
rcases hx with ⟨x', hx⟩

Result:
case intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
a : R
x : M'
x' : M
hx : f x' = x
⊢ IsInteger f (a • x)

Proof state:
case intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
a : R
x : M'
x' : M
hx : f x' = x
⊢ IsInteger f (a • x)

Tactic:
use a • x'

Result:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_3
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
a : R
x : M'
x' : M
hx : f x' = x
⊢ f (a • x') = a • x
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem coprod.map_codiag {X Y : C} (f : X ⟶ Y) [HasBinaryCoproduct X X] [HasBinaryCoproduct Y Y] :
    coprod.map f f ≫ codiag Y = codiag X ≫ f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasBinaryCoproduct X X
inst✝ : HasBinaryCoproduct Y Y
⊢ map f f ≫ codiag Y = codiag X ≫ f

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix
    [Fintype κ'] [DecidableEq ι] [DecidableEq ι'] :
    c.toMatrix c' * LinearMap.toMatrix b' c' f * b'.toMatrix b = LinearMap.toMatrix b c f

Proof state:
case intro
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_9
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁵ : Fintype ι'
inst✝⁴ : Finite κ
inst✝³ : Fintype ι
inst✝² : Fintype κ'
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
val✝ : Fintype κ
⊢ c.toMatrix ⇑c' * (toMatrix b' c') f * b'.toMatrix ⇑b = (toMatrix b c) f

Tactic:
rw [basis_toMatrix_mul_linearMap_toMatrix, linearMap_toMatrix_mul_basis_toMatrix]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_9
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁵ : Fintype ι'
inst✝⁴ : Finite κ
inst✝³ : Fintype ι
inst✝² : Fintype κ'
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
⊢ c.toMatrix ⇑c' * (toMatrix b' c') f * b'.toMatrix ⇑b = (toMatrix b c) f

Tactic:
cases nonempty_fintype κ

Result:
case intro
ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Type u_9
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
b : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
inst✝⁵ : Fintype ι'
inst✝⁴ : Finite κ
inst✝³ : Fintype ι
inst✝² : Fintype κ'
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
val✝ : Fintype κ
⊢ c.toMatrix ⇑c' * (toMatrix b' c') f * b'.toMatrix ⇑b = (toMatrix b c) f
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem Step.not_rev {x b} : Step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)

Proof state:
α : Type u
L₁ L₂ : List (α × Bool)
x : α
b : Bool
⊢ Step (L₁ ++ (x, !b) :: (x, b) :: L₂) (L₁ ++ L₂)

Tactic:
cases b <;> exact Step.not

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem ne_zero_of_mem_rootSet {p : T[X]} [CommRing S] [IsDomain S] [Algebra T S] {a : S}
    (h : a ∈ p.rootSet S) : p ≠ 0 := fun hf => by rwa [hf, rootSet_zero] at h

Proof state:
S : Type v
T : Type w
inst✝³ : CommRing T
p : T[X]
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a : S
h : a ∈ p.rootSet S
hf : p = 0
⊢ False

Tactic:
rwa [hf, rootSet_zero] at h

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem Hom.ext_one_left {n : SimplexCategory} (f g : ⦋1⦌ ⟶ n)
    (h0 : f.toOrderHom 0 = g.toOrderHom 0

Proof state:
n : SimplexCategory
f g : ⦋1⦌ ⟶ n
h0 : autoParam ((toOrderHom f) 0 = (toOrderHom g) 0) _auto✝
h1 : autoParam ((toOrderHom f) 1 = (toOrderHom g) 1) _auto✝
⊢ f = g

Tactic:
ext i

Result:
case a.h.h.h
n : SimplexCategory
f g : ⦋1⦌ ⟶ n
h0 : autoParam ((toOrderHom f) 0 = (toOrderHom g) 0) _auto✝
h1 : autoParam ((toOrderHom f) 1 = (toOrderHom g) 1) _auto✝
i : Fin (⦋1⦌.len + 1)
⊢ ↑((toOrderHom f) i) = ↑((toOrderHom g) i)

Proof state:
case a.h.h.h
n : SimplexCategory
f g : ⦋1⦌ ⟶ n
h0 : autoParam ((toOrderHom f) 0 = (toOrderHom g) 0) _auto✝
h1 : autoParam ((toOrderHom f) 1 = (toOrderHom g) 1) _auto✝
i : Fin (⦋1⦌.len + 1)
⊢ ↑((toOrderHom f) i) = ↑((toOrderHom g) i)

Tactic:
match i with
| 0 => exact h0 ▸ rfl
| 1 => exact h1 ▸ rfl

Result:
no goals

Proof state:
n : SimplexCategory
f g : ⦋1⦌ ⟶ n
h0 : autoParam ((toOrderHom f) 0 = (toOrderHom g) 0) _auto✝
h1 : autoParam ((toOrderHom f) 1 = (toOrderHom g) 1) _auto✝
i : Fin (⦋1⦌.len + 1)
⊢ ↑((toOrderHom f) 0) = ↑((toOrderHom g) 0)

Tactic:
exact h0 ▸ rfl

Result:
no goals

Proof state:
n : SimplexCategory
f g : ⦋1⦌ ⟶ n
h0 : autoParam ((toOrderHom f) 0 = (toOrderHom g) 0) _auto✝
h1 : autoParam ((toOrderHom f) 1 = (toOrderHom g) 1) _auto✝
i : Fin (⦋1⦌.len + 1)
⊢ ↑((toOrderHom f) 1) = ↑((toOrderHom g) 1)

Tactic:
exact h1 ▸ rfl

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem mem_primeFactorsList_mul_right {p a b : ℕ} (hpb : p ∈ b.primeFactorsList) (ha : a ≠ 0) :
    p ∈ (a * b).primeFactorsList

Proof state:
p a b : ℕ
hpb : p ∈ b.primeFactorsList
ha : a ≠ 0
⊢ p ∈ (a * b).primeFactorsList

Tactic:
rw [mul_comm]

Result:
p a b : ℕ
hpb : p ∈ b.primeFactorsList
ha : a ≠ 0
⊢ p ∈ (b * a).primeFactorsList

Proof state:
p a b : ℕ
hpb : p ∈ b.primeFactorsList
ha : a ≠ 0
⊢ p ∈ (b * a).primeFactorsList

Tactic:
exact mem_primeFactorsList_mul_left hpb ha

Result:
no goals
-- Mathlib/Order/Directed.lean
/-- If `f` is monotone and antitone on a directed order, then `f` is constant. -/
lemma constant_of_monotone_antitone [IsDirected α (· ≤ ·)] (hf : Monotone f) (hf' : Antitone f)
    (a b : α) : f a = f b

Proof state:
α : Type u
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Preorder α
f : α → β
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
hf : Monotone f
hf' : Antitone f
a b : α
⊢ f a = f b

Tactic:
obtain ⟨c, hac, hbc⟩ := exists_ge_ge a b

Result:
case intro.intro
α : Type u
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Preorder α
f : α → β
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
hf : Monotone f
hf' : Antitone f
a b c : α
hac : a ≤ c
hbc : b ≤ c
⊢ f a = f b

Proof state:
case intro.intro
α : Type u
β : Type v
inst✝² : PartialOrder β
inst✝¹ : Preorder α
f : α → β
inst✝ : IsDirected α fun x1 x2 => x1 ≤ x2
hf : Monotone f
hf' : Antitone f
a b c : α
hac : a ≤ c
hbc : b ≤ c
⊢ f a = f b

Tactic:
exact le_antisymm ((hf hac).trans <| hf' hbc) ((hf hbc).trans <| hf' hac)

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
@[simp]
lemma blimsup_sup_not : blimsup u f p ⊔ blimsup u f (¬p ·) = limsup u f

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteDistribLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ (blimsup u f p ⊔ blimsup u f fun x => ¬p x) = limsup u f

Tactic:
simp_rw [← blimsup_or_eq_sup, or_not, blimsup_true]

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
lemma map_add_eq_map_add_linearDeriv_add [DecidableEq ι] [Fintype ι] (x h : (i : ι) → M₁ i) :
    f (x + h) = f x + f.linearDeriv x h + ∑ s with 2 ≤ #s, f (s.piecewise h x)

Proof state:
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommGroup (M₁ i)
inst✝⁴ : AddCommGroup M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x h : (i : ι) → M₁ i
⊢ ∑ x_1 ∈ filter (fun x => 2 ≤ #x) Finset.univ.powerset, f (x_1.piecewise h x) +
      ∑ x_1 ∈ filter (fun x => ¬2 ≤ #x) Finset.univ.powerset, f (x_1.piecewise h x) =
    f x + (f.linearDeriv x) h + ∑ s ∈ filter (fun s => 2 ≤ #s) Finset.univ.powerset, f (s.piecewise h x)

Tactic:
simp_rw [not_le, Nat.lt_succ, le_iff_lt_or_eq (b := 1), Nat.lt_one_iff, filter_or,
  ← powersetCard_eq_filter, sum_union (univ.pairwise_disjoint_powersetCard zero_ne_one),
  powersetCard_zero, powersetCard_one, sum_singleton, Finset.piecewise_empty, sum_map,
  Function.Embedding.coeFn_mk, Finset.piecewise_singleton, linearDeriv_apply, add_comm]

Result:
no goals
-- Mathlib/Topology/MetricSpace/ProperSpace/Lemmas.lean
theorem exists_lt_subset_ball (hs : IsClosed s) (h : s ⊆ ball x r) : ∃ r' < r, s ⊆ ball x r'

Proof state:
case inl
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
hr : r ≤ 0
⊢ ∃ r' < r, s ⊆ ball x r'

Tactic:
rw [ball_eq_empty.2 hr, subset_empty_iff] at h

Result:
case inl
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s = ∅
hr : r ≤ 0
⊢ ∃ r' < r, s ⊆ ball x r'

Proof state:
case inl
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
hr : r ≤ 0
hs : IsClosed ∅
⊢ ∃ r' < r, ∅ ⊆ ball x r'

Tactic:
exact (exists_lt r).imp fun r' hr' => ⟨hr', empty_subset _⟩

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s = ∅
hr : r ≤ 0
⊢ ∃ r' < r, s ⊆ ball x r'

Tactic:
subst s

Result:
case inl
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
hr : r ≤ 0
hs : IsClosed ∅
⊢ ∃ r' < r, ∅ ⊆ ball x r'

Proof state:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
⊢ ∃ r' < r, s ⊆ ball x r'

Tactic:
rcases le_or_lt r 0 with hr | hr

Result:
case inl
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
hr : r ≤ 0
⊢ ∃ r' < r, s ⊆ ball x r'

case inr
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
hr : 0 < r
⊢ ∃ r' < r, s ⊆ ball x r'

Proof state:
case inr
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : ProperSpace α
x : α
r : ℝ
s : Set α
hs : IsClosed s
h : s ⊆ ball x r
hr : 0 < r
⊢ ∃ r' < r, s ⊆ ball x r'

Tactic:
exact (exists_pos_lt_subset_ball hr hs h).imp fun r' hr' => ⟨hr'.1.2, hr'.2⟩

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_nhds_coe_iff {α : Type*} {l : Filter α} {x : ℝ≥0} {f : ℝ≥0∞ → α} :
    Tendsto f (𝓝 ↑x) l ↔ Tendsto (f ∘ (↑) : ℝ≥0 → α) (𝓝 x) l

Proof state:
α : Type u_4
l : Filter α
x : ℝ≥0
f : ℝ≥0∞ → α
⊢ Tendsto f (𝓝 ↑x) l ↔ Tendsto (f ∘ ofNNReal) (𝓝 x) l

Tactic:
rw [nhds_coe, tendsto_map'_iff]

Result:
no goals
-- Mathlib/Data/PFunctor/Multivariate/Basic.lean
theorem comp.get_map (f : α ⟹ β) (x : comp P Q α) :
    comp.get (f <$$> x) = (fun i (x : Q i α) => f <$$> x) <$$> comp.get x

Proof state:
n m : ℕ
P : MvPFunctor.{u} n
Q : Fin2 n → MvPFunctor.{u} m
α β : TypeVec.{u} m
f : α ⟹ β
x : ↑(P.comp Q) α
⊢ get (f <$$> x) = (fun i x => f <$$> x) <$$> get x

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem minimal_false : ¬ Minimal (fun _ ↦ False) x

Proof state:
α : Type u_1
x : α
inst✝ : LE α
⊢ ¬Minimal (fun x => False) x

Tactic:
simp [Minimal]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
/-- If `f x y` is continuous in `x` for all `y ∈ s`,
then the set of `x` such that `f x` maps `s` to `t` is closed. -/
lemma IsClosed.setOf_mapsTo {α : Type*} {f : X → α → Z} {s : Set α} {t : Set Z} (ht : IsClosed t)
    (hf : ∀ a ∈ s, Continuous (f · a)) : IsClosed {x | MapsTo (f x) s t}

Proof state:
X : Type u
Z : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
α : Type u_5
f : X → α → Z
s : Set α
t : Set Z
ht : IsClosed t
hf : ∀ a ∈ s, Continuous fun x => f x a
⊢ IsClosed {x | MapsTo (f x) s t}

Tactic:
simpa only [MapsTo, setOf_forall] using isClosed_biInter fun y hy ↦ ht.preimage (hf y hy)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem iff_self_and : ∀ {a b : Bool}, (a = (a && b)) ↔ (a → b)

Proof state:
⊢ ∀ {a b : Bool}, a = (a && b) ↔ a = true → b = true

Tactic:
decide

Result:
no goals
-- Mathlib/GroupTheory/Exponent.lean
@[to_additive AddMonoid.one_lt_exponent]
lemma one_lt_exponent [Nontrivial G] : 1 < Monoid.exponent G

Proof state:
G : Type u
inst✝² : LeftCancelMonoid G
inst✝¹ : Finite G
inst✝ : Nontrivial G
⊢ 1 < exponent G

Tactic:
rw [Nat.one_lt_iff_ne_zero_and_ne_one]

Result:
G : Type u
inst✝² : LeftCancelMonoid G
inst✝¹ : Finite G
inst✝ : Nontrivial G
⊢ exponent G ≠ 0 ∧ exponent G ≠ 1

Proof state:
G : Type u
inst✝² : LeftCancelMonoid G
inst✝¹ : Finite G
inst✝ : Nontrivial G
⊢ exponent G ≠ 0 ∧ exponent G ≠ 1

Tactic:
exact ⟨exponent_ne_zero_of_finite, mt exp_eq_one_iff.mp (not_subsingleton G)⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addZ_of_X_eq {P Q : Fin 3 → R} (hx : P x * Q z ^ 2 = Q x * P z ^ 2) : addZ P Q = 0

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ addZ P Q = 0

Tactic:
rw [addZ, hx, sub_self]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapIdx_eq_empty_iff {l : Array α} : mapIdx f l = #[] ↔ l = #[]

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : Array α
⊢ mapIdx f l = #[] ↔ l = #[]

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
⊢ mapIdx f { toList := l } = #[] ↔ { toList := l } = #[]

Proof state:
case mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
l : List α
⊢ mapIdx f { toList := l } = #[] ↔ { toList := l } = #[]

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Hydra.lean
theorem cutExpand_add_left {t u} (s) : CutExpand r (s + t) (s + u) ↔ CutExpand r t u :=
  exists₂_congr fun _ _ ↦ and_congr Iff.rfl <| by rw [add_assoc, add_assoc, add_left_cancel_iff]

Proof state:
α : Type u_1
r : α → α → Prop
t u s x✝¹ : Multiset α
x✝ : α
⊢ s + t + {x✝} = s + u + x✝¹ ↔ t + {x✝} = u + x✝¹

Tactic:
rw [add_assoc, add_assoc, add_left_cancel_iff]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem mkContinuousLinear_norm_le' (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') (C : ℝ)
    (H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) : ‖mkContinuousLinear f C H‖ ≤ max C 0

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
G' : Type wG'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
f : G →ₗ[𝕜] MultilinearMap 𝕜 E G'
C : ℝ
H : ∀ (x : G) (m : (i : ι) → E i), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖
⊢ ‖{ toFun := fun x => (f x).mkContinuous (C * ‖x‖) ⋯, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (C ⊔ 0) ⋯‖ ≤ C ⊔ 0

Tactic:
exact LinearMap.mkContinuous_norm_le _ (le_max_right _ _) _

Result:
no goals

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
G' : Type wG'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
f : G →ₗ[𝕜] MultilinearMap 𝕜 E G'
C : ℝ
H : ∀ (x : G) (m : (i : ι) → E i), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖
⊢ ‖mkContinuousLinear f C H‖ ≤ C ⊔ 0

Tactic:
dsimp only [mkContinuousLinear]

Result:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
G' : Type wG'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : NormedSpace 𝕜 G
inst✝² : SeminormedAddCommGroup G'
inst✝¹ : NormedSpace 𝕜 G'
inst✝ : Fintype ι
f : G →ₗ[𝕜] MultilinearMap 𝕜 E G'
C : ℝ
H : ∀ (x : G) (m : (i : ι) → E i), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i : ι, ‖m i‖
⊢ ‖{ toFun := fun x => (f x).mkContinuous (C * ‖x‖) ⋯, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (C ⊔ 0) ⋯‖ ≤ C ⊔ 0
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem prepartition_tag {ν : ι → ℤ} {B : Box ι} (hν : ν ∈ admissibleIndex n B) :
    (prepartition n B).tag (box n ν) = tag n ν

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
B : Box ι
hν : ν ∈ admissibleIndex n B
⊢ (prepartition n B).tag (box n ν) = tag n ν

Tactic:
dsimp only [prepartition]

Result:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
B : Box ι
hν : ν ∈ admissibleIndex n B
⊢ (if hI : ∃ ν_1 ∈ admissibleIndex n B, box n ν = box n ν_1 then tag n hI.choose else ⋯.choose) = tag n ν

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
B : Box ι
hν : ν ∈ admissibleIndex n B
h : ∃ ν' ∈ admissibleIndex n B, box n ν = box n ν'
⊢ (if hI : ∃ ν_1 ∈ admissibleIndex n B, box n ν = box n ν_1 then tag n hI.choose else ⋯.choose) = tag n ν

Tactic:
rw [dif_pos h, (tag_injective n).eq_iff, ← (box_injective n).eq_iff]

Result:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
B : Box ι
hν : ν ∈ admissibleIndex n B
h : ∃ ν' ∈ admissibleIndex n B, box n ν = box n ν'
⊢ box n h.choose = box n ν

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
B : Box ι
hν : ν ∈ admissibleIndex n B
⊢ (if hI : ∃ ν_1 ∈ admissibleIndex n B, box n ν = box n ν_1 then tag n hI.choose else ⋯.choose) = tag n ν

Tactic:
have h : ∃ ν' ∈ admissibleIndex n B, box n ν = box n ν' := ⟨ν, hν, rfl⟩

Result:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
B : Box ι
hν : ν ∈ admissibleIndex n B
h : ∃ ν' ∈ admissibleIndex n B, box n ν = box n ν'
⊢ (if hI : ∃ ν_1 ∈ admissibleIndex n B, box n ν = box n ν_1 then tag n hI.choose else ⋯.choose) = tag n ν

Proof state:
ι : Type u_1
n : ℕ
inst✝¹ : NeZero n
inst✝ : Fintype ι
ν : ι → ℤ
B : Box ι
hν : ν ∈ admissibleIndex n B
h : ∃ ν' ∈ admissibleIndex n B, box n ν = box n ν'
⊢ box n h.choose = box n ν

Tactic:
exact h.choose_spec.2.symm

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_add_nsmul [AddMonoid G] [AddMonoid H] [AddConstMapClass F G H a b]
    (f : F) (x : G) (n : ℕ) : f (x + n • a) = f x + n • b

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddMonoid G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
⊢ f (x + n • a) = f x + n • b

Tactic:
simpa using (AddConstMapClass.semiconj f).iterate_right n x

Result:
no goals
-- Mathlib/Data/PNat/Interval.lean
theorem card_fintype_Icc : Fintype.card (Set.Icc a b) = b + 1 - a

Proof state:
a b : ℕ+
⊢ Fintype.card ↑(Set.Icc a b) = ↑b + 1 - ↑a

Tactic:
rw [← card_Icc, Fintype.card_ofFinset]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem dot_smul_left (xs ys : IntList) (i : Int) : (i * xs).dot ys = i * xs.dot ys

Proof state:
xs ys : IntList
i : Int
⊢ (i * xs).dot ys = i * xs.dot ys

Tactic:
simp [dot]

Result:
no goals