harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem mul_le_of_one_le_right [ExistsAddOfLE α] [PosMulMono α]
    [AddRightMono α] [AddRightReflectLE α]
    (ha : a ≤ 0) (h : 1 ≤ b) : a * b ≤ a

Proof state:
α : Type u
inst✝⁵ : Semiring α
inst✝⁴ : Preorder α
a b : α
inst✝³ : ExistsAddOfLE α
inst✝² : PosMulMono α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
ha : a ≤ 0
h : 1 ≤ b
⊢ a * b ≤ a

Tactic:
simpa only [mul_one] using mul_le_mul_of_nonpos_left h ha

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem wellFoundedOn_image {s : Set β} : (f '' s).WellFoundedOn r ↔ s.WellFoundedOn (r on f)

Proof state:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
s : Set β
⊢ (range fun x => f ↑x).WellFoundedOn r ↔ s.WellFoundedOn (r on f)

Tactic:
exact wellFoundedOn_range

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
s : Set β
⊢ (f '' s).WellFoundedOn r ↔ s.WellFoundedOn (r on f)

Tactic:
rw [image_eq_range]

Result:
α : Type u_2
β : Type u_3
r : α → α → Prop
f : β → α
s : Set β
⊢ (range fun x => f ↑x).WellFoundedOn r ↔ s.WellFoundedOn (r on f)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem containsThenInsert_fst_val [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} {b : β a} :
    (m.val.containsThenInsert a b).1 = (m.containsThenInsert a b).1

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
⊢ (m.val.containsThenInsert a b).fst = (m.containsThenInsert a b).fst

Tactic:
simp [Raw.containsThenInsert, m.2]

Result:
no goals
-- Mathlib/Order/Interval/Set/Pi.lean
theorem image_update_Ioo (f : ∀ i, α i) (i : ι) (a b : α i) :
    update f i '' Ioo a b = Ioo (update f i a) (update f i b)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Ioo a b = Ioo (update f i a) (update f i b)

Tactic:
rw [← Ico_diff_left, ← Ico_diff_left, image_diff (update_injective _ _), image_singleton,
  image_update_Ico]

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma coverEntropyEntourage_univ (T : X → X) {F : Set X} (h : F.Nonempty) :
    coverEntropyEntourage T F univ = 0

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
⊢ coverEntropyEntourage T F univ = 0

Tactic:
simp [coverEntropyEntourage, coverMincard_univ T h]

Result:
no goals
-- Mathlib/Data/Complex/Cardinality.lean
theorem mk_univ_complex : #(Set.univ : Set ℂ) = 𝔠

Proof state:
⊢ #↑Set.univ = 𝔠

Tactic:
rw [mk_univ, mk_complex]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem forall_coord_eq_zero_iff {x : M} : (∀ i, b.coord i x = 0) ↔ x = 0 :=
  Iff.trans (by simp only [b.coord_apply, DFunLike.ext_iff, Finsupp.zero_apply])
    b.repr.map_eq_zero_iff

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
x : M
⊢ (∀ (i : ι), (b.coord i) x = 0) ↔ b.repr x = 0

Tactic:
simp only [b.coord_apply, DFunLike.ext_iff, Finsupp.zero_apply]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem div_le_iff_le_mul : a / c ≤ b ↔ a ≤ b * c

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a b c : α
⊢ a / c ≤ b ↔ a ≤ b * c

Tactic:
rw [← mul_le_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Basic.lean
theorem isUniformEmbedding_iff' [MetricSpace β] {f : γ → β} :
    IsUniformEmbedding f ↔
      (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
        ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ

Proof state:
β : Type v
γ : Type w
inst✝¹ : MetricSpace γ
inst✝ : MetricSpace β
f : γ → β
⊢ IsUniformEmbedding f ↔
    (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧
      ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ

Tactic:
rw [isUniformEmbedding_iff_isUniformInducing, isUniformInducing_iff, uniformContinuous_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findSome?_mkArray_of_isNone (h : (f a).isNone) :
    findSome? f (mkArray n a) = none

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
n : Nat
a : α✝¹
h : (f a).isNone = true
⊢ findSome? f (mkArray n a) = none

Tactic:
rw [Option.isNone_iff_eq_none] at h

Result:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
n : Nat
a : α✝¹
h : f a = none
⊢ findSome? f (mkArray n a) = none

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
n : Nat
a : α✝¹
h : f a = none
⊢ findSome? f (mkArray n a) = none

Tactic:
simp [findSome?_mkArray, h]

Result:
no goals
-- Mathlib/Data/Finsupp/NeLocus.lean
theorem neLocus_zero_right : f.neLocus 0 = f.support

Proof state:
case h
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f : α →₀ N
a✝ : α
⊢ a✝ ∈ f.neLocus 0 ↔ a✝ ∈ f.support

Tactic:
rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]

Result:
no goals

Proof state:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f : α →₀ N
⊢ f.neLocus 0 = f.support

Tactic:
ext

Result:
case h
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f : α →₀ N
a✝ : α
⊢ a✝ ∈ f.neLocus 0 ↔ a✝ ∈ f.support
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem equicontinuousOn_iff_continuousOn {F : ι → X → α} {S : Set X} :
    EquicontinuousOn F S ↔ ContinuousOn (ofFun ∘ Function.swap F : X → ι →ᵤ α) S

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
⊢ EquicontinuousOn F S ↔ ContinuousOn (⇑ofFun ∘ swap F) S

Tactic:
simp_rw [EquicontinuousOn, ContinuousOn, equicontinuousWithinAt_iff_continuousWithinAt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_eq_getD_default [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.1.WF) {a : α} :
    get! m a = getD m a default

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h : m.val.WF
a : α
⊢ get! m a = getD m a default

Tactic:
simp_to_model using List.getValue!_eq_getValueD_default

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem star_coe : star (x : ℍ[R,c₁,c₂,c₃]) = x

Proof state:
R : Type u_3
c₁ c₂ c₃ x : R
inst✝ : CommRing R
⊢ star ↑x = ↑x

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem idxOf_cons_self [BEq α] [ReflBEq α] {l : List α} : (a :: l).idxOf a = 0

Proof state:
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : ReflBEq α
l : List α
⊢ idxOf a (a :: l) = 0

Tactic:
simp [idxOf_cons]

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Basic.lean
@[to_additive]
lemma comp_apply {X Y T : CommGrp} (f : X ⟶ Y) (g : Y ⟶ T) (x : X) :
    (f ≫ g) x = g (f x)

Proof state:
X Y T : CommGrp
f : X ⟶ Y
g : Y ⟶ T
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Pointwise/Finset.lean
lemma smul_univ₀ [Fintype β] {s : Finset α} (hs : ¬s ⊆ 0) : s • (univ : Finset β) = univ :=
  coe_injective <| by
    rw [← coe_subset] at hs
    push_cast at hs ⊢
    exact Set.smul_univ₀ hs

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : ¬s ⊆ 0
⊢ ↑(s • univ) = ↑univ

Tactic:
rw [← coe_subset] at hs

Result:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : ¬↑s ⊆ ↑0
⊢ ↑(s • univ) = ↑univ

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : ¬↑s ⊆ 0
⊢ ↑s • Set.univ = Set.univ

Tactic:
exact Set.smul_univ₀ hs

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : ¬↑s ⊆ ↑0
⊢ ↑(s • univ) = ↑univ

Tactic:
push_cast at hs ⊢

Result:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq β
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : Fintype β
s : Finset α
hs : ¬↑s ⊆ 0
⊢ ↑s • Set.univ = Set.univ
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_map_of_injective (hf : Injective f) : (map f p).vars = p.vars

Proof state:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
hf : Injective ⇑f
⊢ ((map f) p).vars = p.vars

Tactic:
simp [vars, degrees_map_of_injective _ hf]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
lemma le_mul_of_forall_lt {a b c : ℝ≥0∞} (h₁ : a ≠ 0 ∨ b ≠ ∞) (h₂ : a ≠ ∞ ∨ b ≠ 0)
    (h : ∀ a' > a, ∀ b' > b, c ≤ a' * b') : c ≤ a * b

Proof state:
a b c : ℝ≥0∞
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ 0
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ a⁻¹ * b⁻¹ ≤ c⁻¹

Tactic:
exact mul_le_of_forall_lt fun a' ha' b' hb' ↦ ENNReal.le_inv_iff_le_inv.1 <|
  (h _ (ENNReal.lt_inv_iff_lt_inv.1 ha') _ (ENNReal.lt_inv_iff_lt_inv.1 hb')).trans_eq
  (ENNReal.mul_inv (Or.inr hb'.ne_top) (Or.inl ha'.ne_top)).symm

Result:
no goals

Proof state:
a b c : ℝ≥0∞
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ 0
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ c ≤ a * b

Tactic:
rw [← ENNReal.inv_le_inv, ENNReal.mul_inv h₁ h₂]

Result:
a b c : ℝ≥0∞
h₁ : a ≠ 0 ∨ b ≠ ⊤
h₂ : a ≠ ⊤ ∨ b ≠ 0
h : ∀ a' > a, ∀ b' > b, c ≤ a' * b'
⊢ a⁻¹ * b⁻¹ ≤ c⁻¹
-- Mathlib/Order/Heyting/Basic.lean
theorem compl_bot : (⊥ : α)ᶜ = ⊤

Proof state:
α : Type u_2
inst✝ : HeytingAlgebra α
⊢ ⊥ᶜ = ⊤

Tactic:
rw [← himp_bot, himp_self]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma ediv_dvd_ediv : ∀ {a b c : ℤ}, a ∣ b → b ∣ c → b / a ∣ c / a
  | a, _, _, ⟨b, rfl⟩, ⟨c, rfl⟩ =>
    if az : a = 0 then by simp [az]
    else by
      rw [Int.mul_ediv_cancel_left _ az, Int.mul_assoc, Int.mul_ediv_cancel_left _ az]
      apply Int.dvd_mul_right

Proof state:
a b c : ℤ
az : ¬a = 0
⊢ b ∣ b * c

Tactic:
apply Int.dvd_mul_right

Result:
no goals

Proof state:
a b c : ℤ
az : a = 0
⊢ a * b / a ∣ a * b * c / a

Tactic:
simp [az]

Result:
no goals

Proof state:
a b c : ℤ
az : ¬a = 0
⊢ a * b / a ∣ a * b * c / a

Tactic:
rw [Int.mul_ediv_cancel_left _ az, Int.mul_assoc, Int.mul_ediv_cancel_left _ az]

Result:
a b c : ℤ
az : ¬a = 0
⊢ b ∣ b * c
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem colimit.pre_map' [HasColimitsOfShape K C] (F : J ⥤ C) {E₁ E₂ : K ⥤ J} (α : E₁ ⟶ E₂) :
    colimit.pre F E₁ = colim.map (whiskerRight α F) ≫ colimit.pre F E₂

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
⊢ pre F E₁ = colim.map (whiskerRight α F) ≫ pre F E₂

Tactic:
ext1

Result:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
j✝ : K
⊢ ι (E₁ ⋙ F) j✝ ≫ pre F E₁ = ι (E₁ ⋙ F) j✝ ≫ colim.map (whiskerRight α F) ≫ pre F E₂

Proof state:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
j✝ : K
⊢ ι (E₁ ⋙ F) j✝ ≫ pre F E₁ = ι (E₁ ⋙ F) j✝ ≫ colim.map (whiskerRight α F) ≫ pre F E₂

Tactic:
simp [← assoc, assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem zeroIsoIsTerminal_hom {X : C} (t : IsTerminal X) : (zeroIsoIsTerminal t).hom = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
t : IsTerminal X
⊢ (zeroIsoIsTerminal t).hom = 0

Tactic:
ext

Result:
no goals
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem map_bot (f : A →ₐ[R] B) : (⊥ : Subalgebra R A).map f = ⊥ :=
  Subalgebra.toSubmodule_injective <| by
    simpa only [Subalgebra.map_toSubmodule, toSubmodule_bot] using Submodule.map_one _

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ Subalgebra.toSubmodule (Subalgebra.map f ⊥) = Subalgebra.toSubmodule ⊥

Tactic:
simpa only [Subalgebra.map_toSubmodule, toSubmodule_bot] using Submodule.map_one _

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
@[simp]
lemma ofTensorProduct_tmul (r : AdicCompletion I R) (x : M) :
    ofTensorProduct I M (r ⊗ₜ x) = r • of I M x

Proof state:
R : Type u_1
inst✝² : CommRing R
I : Ideal R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r : AdicCompletion I R
x : M
⊢ (ofTensorProduct I M) (r ⊗ₜ[R] x) = r • (of I M) x

Tactic:
simp [ofTensorProduct]

Result:
no goals
-- Mathlib/Data/Vector/Defs.lean
theorem toList_cons (a : α) (v : Vector α n) : toList (cons a v) = a :: toList v

Proof state:
case mk
α : Type u_1
n : ℕ
a : α
val✝ : List α
property✝ : val✝.length = n
⊢ (cons a ⟨val✝, property✝⟩).toList = a :: toList ⟨val✝, property✝⟩

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
a : α
v : Vector α n
⊢ (cons a v).toList = a :: v.toList

Tactic:
cases v

Result:
case mk
α : Type u_1
n : ℕ
a : α
val✝ : List α
property✝ : val✝.length = n
⊢ (cons a ⟨val✝, property✝⟩).toList = a :: toList ⟨val✝, property✝⟩
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem pullbackP1Iso_hom_fst (i : 𝒰.J) :
    (pullbackP1Iso 𝒰 f g i).hom ≫ pullback.fst _ _ = pullback.snd _ _

Proof state:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g
i : 𝒰.J
⊢ (pullbackP1Iso 𝒰 f g i).hom ≫ pullback.fst (𝒰.map i ≫ f) g = pullback.snd (p1 𝒰 f g) (𝒰.map i)

Tactic:
simp_rw [pullbackP1Iso, pullback.lift_fst]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem blimsup_eq_iInf_biSup {f : Filter β} {p : β → Prop} {u : β → α} :
    blimsup u f p = ⨅ s ∈ f, ⨆ (b) (_ : p b ∧ b ∈ s), u b

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ blimsup u f p = ⨅ s ∈ f, ⨆ b, ⨆ (_ : p b ∧ b ∈ s), u b

Tactic:
simp only [f.basis_sets.blimsup_eq_iInf_iSup, iSup_and', id, and_comm]

Result:
no goals
-- Mathlib/Computability/TMToPartrec.lean
theorem supports_biUnion {K : Option Γ' → Finset Λ'} {S} :
    Supports (Finset.univ.biUnion K) S ↔ ∀ a, Supports (K a) S

Proof state:
K : Option Γ' → Finset Λ'
S : Finset Λ'
⊢ Supports (Finset.univ.biUnion K) S ↔ ∀ (a : Option Γ'), Supports (K a) S

Tactic:
simpa [Supports] using forall_swap

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma eigenspace_def {f : End R M} {μ : R} :
    f.eigenspace μ = LinearMap.ker (f - μ • 1)

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ f.eigenspace μ = LinearMap.ker (f - μ • 1)

Tactic:
rw [eigenspace, genEigenspace_one]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
/-- `eq_nil_or_concat` in simp normal form -/
lemma eq_nil_or_concat' (l : List α) : l = [] ∨ ∃ L b, l = L ++ [b]

Proof state:
α : Type u
l : List α
⊢ l = [] ∨ ∃ L b, l = L ++ [b]

Tactic:
simpa using l.eq_nil_or_concat

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem inv_cthickening : (cthickening δ s)⁻¹ = cthickening δ s⁻¹

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ (cthickening δ s)⁻¹ = cthickening δ s⁻¹

Tactic:
simp_rw [cthickening, ← infEdist_inv]

Result:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ {x | EMetric.infEdist x s ≤ ENNReal.ofReal δ}⁻¹ = {x | EMetric.infEdist x⁻¹ s ≤ ENNReal.ofReal δ}

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ {x | EMetric.infEdist x s ≤ ENNReal.ofReal δ}⁻¹ = {x | EMetric.infEdist x⁻¹ s ≤ ENNReal.ofReal δ}

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_le_neg_one_iff : ⌊a⌋ ≤ -1 ↔ a < 0

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a : α
⊢ ⌊a⌋ ≤ -1 ↔ a < 0

Tactic:
rw [← zero_sub (1 : ℤ), floor_le_sub_one_iff, cast_zero]

Result:
no goals
-- Mathlib/RingTheory/HopkinsLevitzki.lean
theorem isNoetherian_iff_isArtinian : IsNoetherian R M ↔ IsArtinian R M :=
  IsSemiprimaryRing.induction R R M (P := fun M ↦ IsNoetherian R M ↔ IsArtinian R M)
    (fun M _ _ _ _ _ _ ↦ IsSemisimpleModule.finite_tfae.out 1 2)
    fun M _ _ _ _ h h' ↦ let N : Submodule R M := Ring.jacobson R • ⊤; by
      simp_rw [isNoetherian_iff_submodule_quotient N, isArtinian_iff_submodule_quotient N, N, h, h']

Proof state:
R : Type u_2
M✝ : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M✝
inst✝¹ : Module R M✝
inst✝ : IsSemiprimaryRing R
M : Type u
x✝³ : AddCommGroup M
x✝² x✝¹ : Module R M
x✝ : IsScalarTower R R M
h : (fun M [AddCommGroup M] [Module R M] [Module R M] => IsNoetherian R M ↔ IsArtinian R M) ↥(Ring.jacobson R • ⊤)
h' : (fun M [AddCommGroup M] [Module R M] [Module R M] => IsNoetherian R M ↔ IsArtinian R M) (M ⧸ Ring.jacobson R • ⊤)
N : Submodule R M := Ring.jacobson R • ⊤
⊢ (fun M [AddCommGroup M] [Module R M] [Module R M] => IsNoetherian R M ↔ IsArtinian R M) M

Tactic:
simp_rw [isNoetherian_iff_submodule_quotient N, isArtinian_iff_submodule_quotient N, N, h, h']

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma CompleteOrthogonalIdempotents.prod_one_sub
    (he : CompleteOrthogonalIdempotents e) :
    ∏ i, (1 - e i) = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ ∏ i : I, (1 - e i) = 0

Tactic:
rw [he.1.prod_one_sub, he.complete, sub_self]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem count_span_normalizedFactors_eq_of_normUnit {r X : R}
    (hr : r ≠ 0) (hX₁ : normUnit X = 1) (hX : Prime X) :
      Multiset.count (Ideal.span {X} : Ideal R) (normalizedFactors (Ideal.span {r})) =
        Multiset.count X (normalizedFactors r)

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : NormalizationMonoid R
inst✝¹ : DecidableEq R
inst✝ : DecidableEq (Ideal R)
r X : R
hr : r ≠ 0
hX₁ : normUnit X = 1
hX : Prime X
⊢ Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count X (normalizedFactors r)

Tactic:
simpa [hX₁, normalize_apply] using count_span_normalizedFactors_eq hr hX

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Killing.lean
@[simp]
lemma corootSpace_eq_bot_iff {α : Weight K H L} :
    corootSpace α = ⊥ ↔ α.IsZero

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : CharZero K
α : Weight K (↥H) L
⊢ corootSpace ⇑α = ⊥ ↔ α.IsZero

Tactic:
simp [← LieSubmodule.toSubmodule_eq_bot, coe_corootSpace_eq_span_singleton α]

Result:
no goals
-- Mathlib/Algebra/Homology/ExactSequence.lean
lemma isComplex_of_iso {S₁ S₂ : ComposableArrows C n} (e : S₁ ≅ S₂) (h₁ : S₁.IsComplex) :
    S₂.IsComplex where
  zero i hi

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S₁ S₂ : ComposableArrows C n
e : S₁ ≅ S₂
h₁ : S₁.IsComplex
i : ℕ
hi : autoParam (i + 2 ≤ n) _auto✝
⊢ S₂.map' i (i + 1) ⋯ ⋯ ≫ S₂.map' (i + 1) (i + 2) ⋯ hi = 0

Tactic:
rw [← cancel_epi (ComposableArrows.app' e.hom i), comp_zero,
  ← NatTrans.naturality_assoc, ← NatTrans.naturality,
  reassoc_of% (h₁.zero i hi), zero_comp]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
lemma Icc_map_sectR : (Icc a b).map (.sectR c _) = Icc (c, a) (c, b)

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : PartialOrder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
c : α
a b : β
⊢ map (Embedding.sectR c β) (Icc a b) = Icc (c, a) (c, b)

Tactic:
aesop (add safe forward [le_antisymm])

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean
theorem Asymptotics.isEquivalent_nat_floor :
    (fun (x : R) ↦ ↑⌊x⌋₊) ~[atTop] (fun x ↦ x)

Proof state:
R : Type u_1
inst✝² : NormedLinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
⊢ (fun x => ↑⌊x⌋₊) ~[atTop] fun x => x

Tactic:
refine isEquivalent_of_tendsto_one ?_ tendsto_nat_floor_div_atTop

Result:
R : Type u_1
inst✝² : NormedLinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
⊢ ∀ᶠ (x : R) in atTop, x = 0 → ↑⌊x⌋₊ = 0

Proof state:
R : Type u_1
inst✝² : NormedLinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
⊢ ∀ᶠ (x : R) in atTop, x = 0 → ↑⌊x⌋₊ = 0

Tactic:
filter_upwards with x hx using by rw [hx, Nat.floor_zero, Nat.cast_eq_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : NormedLinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
x : R
hx : x = 0
⊢ ↑⌊x⌋₊ = 0

Tactic:
rw [hx, Nat.floor_zero, Nat.cast_eq_zero]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
@[simp]
lemma one_lt_star_iff {x : R} : 1 < star x ↔ 1 < x

Proof state:
R : Type u
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
⊢ 1 < star x ↔ 1 < x

Tactic:
simpa using star_lt_star_iff (x := 1) (y := x)

Result:
no goals
-- Mathlib/Topology/Algebra/Monoid.lean
theorem Filter.HasBasis.mul_self {p : ι → Prop} {s : ι → Set M} (h : (𝓝 1).HasBasis p s) :
    (𝓝 1).HasBasis p fun i => s i * s i

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulOneClass M
inst✝ : ContinuousMul M
p : ι → Prop
s : ι → Set M
h : (𝓝 1).HasBasis p s
⊢ (Filter.map (Function.uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1)).HasBasis p fun i => s i * s i

Tactic:
simpa only [← image_mul_prod] using h.prod_self.map _

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulOneClass M
inst✝ : ContinuousMul M
p : ι → Prop
s : ι → Set M
h : (𝓝 1).HasBasis p s
⊢ (𝓝 1).HasBasis p fun i => s i * s i

Tactic:
rw [← nhds_mul_nhds_one, ← map₂_mul, ← map_uncurry_prod]

Result:
ι : Type u_1
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulOneClass M
inst✝ : ContinuousMul M
p : ι → Prop
s : ι → Set M
h : (𝓝 1).HasBasis p s
⊢ (Filter.map (Function.uncurry fun x1 x2 => x1 * x2) (𝓝 1 ×ˢ 𝓝 1)).HasBasis p fun i => s i * s i
-- Mathlib/Combinatorics/SimpleGraph/Prod.lean
theorem boxProd_adj_right {a : α} {b₁ b₂ : β} : (G □ H).Adj (a, b₁) (a, b₂) ↔ H.Adj b₁ b₂

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
a : α
b₁ b₂ : β
⊢ (G □ H).Adj (a, b₁) (a, b₂) ↔ H.Adj b₁ b₂

Tactic:
simp only [boxProd_adj, SimpleGraph.irrefl, false_and, and_true, false_or]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem nonempty_of_union_eq_top_of_nonempty {ι : Type*} (t : Set ι) (s : ι → Set α)
    (H : Nonempty α) (w : ⋃ i ∈ t, s i = ⊤) : t.Nonempty

Proof state:
α : Type u_1
ι : Type u_12
t : Set ι
s : ι → Set α
H : Nonempty α
w : ⋃ i ∈ t, s i = ⊤
⊢ t.Nonempty

Tactic:
obtain ⟨x, m, -⟩ := exists_set_mem_of_union_eq_top t s w H.some

Result:
case intro.intro
α : Type u_1
ι : Type u_12
t : Set ι
s : ι → Set α
H : Nonempty α
w : ⋃ i ∈ t, s i = ⊤
x : ι
m : x ∈ t
⊢ t.Nonempty

Proof state:
case intro.intro
α : Type u_1
ι : Type u_12
t : Set ι
s : ι → Set α
H : Nonempty α
w : ⋃ i ∈ t, s i = ⊤
x : ι
m : x ∈ t
⊢ t.Nonempty

Tactic:
exact ⟨x, m⟩

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Real.lean
lemma dist_right_le_of_mem_uIcc {x y z : ℝ} (h : y ∈ uIcc x z) : dist y z ≤ dist x z

Proof state:
x y z : ℝ
h : y ∈ uIcc x z
⊢ dist y z ≤ dist x z

Tactic:
simpa only [dist_comm _ z] using abs_sub_right_of_mem_uIcc h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean
theorem iteratedDeriv_exp_const_mul (n : ℕ) (c : ℝ) :
    (iteratedDeriv n fun s => exp (c * s)) = fun s => c ^ n * exp (c * s)

Proof state:
n : ℕ
c : ℝ
⊢ (iteratedDeriv n fun s => rexp (c * s)) = fun s => c ^ n * rexp (c * s)

Tactic:
rw [iteratedDeriv_comp_const_mul contDiff_exp, iteratedDeriv_eq_iterate, iter_deriv_exp]

Result:
no goals