harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/SuccPred/Basic.lean
theorem pred_le_pred_of_le : a ≤ b → pred a ≤ pred b

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
a✝ : a ≤ b
⊢ pred a ≤ pred b

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
⊢ a ≤ b → pred a ≤ pred b

Tactic:
intro

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : PredOrder α
a b : α
inst✝ : NoMinOrder α
a✝ : a ≤ b
⊢ pred a ≤ pred b
-- Mathlib/Topology/Order/ScottTopology.lean
@[simp] lemma dirSupInaccOn_univ : DirSupInaccOn univ s ↔ DirSupInacc s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ DirSupInaccOn univ s ↔ DirSupInacc s

Tactic:
simp [DirSupInaccOn, DirSupInacc]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Rayleigh.lean
theorem iInf_rayleigh_eq_iInf_rayleigh_sphere {r : ℝ} (hr : 0 < r) :
    ⨅ x : { x : E // x ≠ 0 }, rayleighQuotient T x =
      ⨅ x : sphere (0 : E) r, rayleighQuotient T x :=
  show ⨅ x : ({0}ᶜ : Set E), rayleighQuotient T x = _ by
    simp only [← @sInf_image' _ _ _ _ (rayleighQuotient T),
      T.image_rayleigh_eq_image_rayleigh_sphere hr]

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
r : ℝ
hr : 0 < r
⊢ ⨅ x, T.rayleighQuotient ↑x = ⨅ x, T.rayleighQuotient ↑x

Tactic:
simp only [← @sInf_image' _ _ _ _ (rayleighQuotient T),
  T.image_rayleigh_eq_image_rayleigh_sphere hr]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem unzip_fst : (unzip l).fst = l.map Prod.fst

Proof state:
α✝ : Type u_1
β✝ : Type u_2
l : List (α✝ × β✝)
⊢ l.unzip.fst = map Prod.fst l

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem map_add_left (f₁ f₂ : M →ₗ[R] P) (g : N →ₗ[R] Q) :
    map (f₁ + f₂) g = map f₁ g + map f₂ g

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f₁ f₂ : M →ₗ[R] P
g : N →ₗ[R] Q
⊢ map (f₁ + f₂) g = map f₁ g + map f₂ g

Tactic:
ext

Result:
case H.h.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f₁ f₂ : M →ₗ[R] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (((mk R M N).compr₂ (map (f₁ + f₂) g)) x✝¹) x✝ = (((mk R M N).compr₂ (map f₁ g + map f₂ g)) x✝¹) x✝

Proof state:
case H.h.h
R : Type u_1
inst✝⁸ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R Q
inst✝ : Module R P
f₁ f₂ : M →ₗ[R] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ (((mk R M N).compr₂ (map (f₁ + f₂) g)) x✝¹) x✝ = (((mk R M N).compr₂ (map f₁ g + map f₂ g)) x✝¹) x✝

Tactic:
simp only [add_tmul, compr₂_apply, mk_apply, map_tmul, add_apply]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem characteristic_iff_map_eq : H.Characteristic ↔ ∀ ϕ : G ≃* G, H.map ϕ.toMonoidHom = H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.symm.toMonoidHom H = H

Tactic:
exact characteristic_iff_comap_eq.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), map ϕ.toMonoidHom H = H

Tactic:
simp_rw [map_equiv_eq_comap_symm']

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.symm.toMonoidHom H = H
-- Mathlib/Data/PFun.lean
theorem dom_comp (f : β →. γ) (g : α →. β) : (f.comp g).Dom = g.preimage f.Dom

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
⊢ (f.comp g).Dom = g.preimage f.Dom

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
x✝ : α
⊢ x✝ ∈ (f.comp g).Dom ↔ x✝ ∈ g.preimage f.Dom

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
x✝ : α
⊢ x✝ ∈ (f.comp g).Dom ↔ x✝ ∈ g.preimage f.Dom

Tactic:
simp_rw [mem_preimage, mem_dom, comp_apply, Part.mem_bind_iff, ← exists_and_right]

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
x✝ : α
⊢ (∃ y, ∃ a ∈ g x✝, y ∈ f a) ↔ ∃ y, ∃ x ∈ f y, y ∈ g x✝

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
x✝ : α
⊢ (∃ y, ∃ a ∈ g x✝, y ∈ f a) ↔ ∃ y, ∃ x ∈ f y, y ∈ g x✝

Tactic:
rw [exists_comm]

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
x✝ : α
⊢ (∃ b a, b ∈ g x✝ ∧ a ∈ f b) ↔ ∃ y, ∃ x ∈ f y, y ∈ g x✝

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
f : β →. γ
g : α →. β
x✝ : α
⊢ (∃ b a, b ∈ g x✝ ∧ a ∈ f b) ↔ ∃ y, ∃ x ∈ f y, y ∈ g x✝

Tactic:
simp_rw [and_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean
theorem map (h : μ ≪ ν) {f : α → β} (hf : Measurable f) : μ.map f ≪ ν.map f :=
  AbsolutelyContinuous.mk fun s hs => by simpa [hf, hs] using @h _

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ ν : Measure α
h : μ ≪ ν
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (map f ν) s = 0 → (map f μ) s = 0

Tactic:
simpa [hf, hs] using @h _

Result:
no goals
-- Mathlib/Algebra/Divisibility/Units.lean
theorem isRelPrime_mul_unit_right_right : IsRelPrime y (z * x) ↔ IsRelPrime y z

Proof state:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime y (z * x) ↔ IsRelPrime y z

Tactic:
rw [mul_comm, isRelPrime_mul_unit_left_right hu]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem natDegree_eq_of_degree_eq_some {p : R[X]} {n : ℕ} (h : degree p = n) : natDegree p = n

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.degree = ↑n
⊢ p.natDegree = n

Tactic:
rw [natDegree, h, Nat.cast_withBot, WithBot.unbotD_coe]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem card_pair_eq_one_or_two : #{a, b} = 1 ∨ #{a, b} = 2

Proof state:
α : Type u_1
a b : α
inst✝ : DecidableEq α
⊢ a = b ∨ ¬a = b

Tactic:
tauto

Result:
no goals

Proof state:
α : Type u_1
a b : α
inst✝ : DecidableEq α
⊢ #{a, b} = 1 ∨ #{a, b} = 2

Tactic:
simp [card_insert_eq_ite]

Result:
α : Type u_1
a b : α
inst✝ : DecidableEq α
⊢ a = b ∨ ¬a = b
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_div_coe_angle {x y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) :
    (arg (x / y) : Real.Angle) = arg x - arg y

Proof state:
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(x / y).arg = ↑x.arg - ↑y.arg

Tactic:
rw [div_eq_mul_inv, arg_mul_coe_angle hx (inv_ne_zero hy), arg_inv_coe_angle, sub_eq_add_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ofFin_eq_ofNat : @BitVec.ofFin w (Fin.mk x lt) = BitVec.ofNat w x

Proof state:
w x : Nat
lt : x < 2 ^ w
⊢ { toFin := ⟨x, lt⟩ } = BitVec.ofNat w x

Tactic:
simp only [BitVec.ofNat, Fin.ofNat', lt, Nat.mod_eq_of_lt]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem WithSeminorms.hasBasis (hp : WithSeminorms p) :
    (𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ p.basisSets) id

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
⊢ (𝓝 0).HasBasis (fun s => s ∈ p.basisSets) id

Tactic:
exact AddGroupFilterBasis.nhds_zero_hasBasis _

Result:
no goals
-- Mathlib/Topology/Sets/Closeds.lean
@[simp]
lemma coe_sSup {S : Set (Closeds α)} : ((sSup S : Closeds α) : Set α) =
    closure (⋃₀ ((↑) '' S))

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
S : Set (Closeds α)
⊢ ↑(sSup S) = closure (⋃₀ (SetLike.coe '' S))

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem next_of_valid' (cs cs' : List Char) :
    next ⟨cs ++ cs'⟩ ⟨utf8Len cs⟩ = ⟨utf8Len cs + (cs'.headD default).utf8Size⟩

Proof state:
cs cs' : List Char
⊢ { byteIdx := utf8Len cs } + cs'.headD default = { byteIdx := utf8Len cs + (cs'.headD default).utf8Size }

Tactic:
rfl

Result:
no goals

Proof state:
cs cs' : List Char
⊢ { data := cs ++ cs' }.next { byteIdx := utf8Len cs } = { byteIdx := utf8Len cs + (cs'.headD default).utf8Size }

Tactic:
simp only [next, get_of_valid]

Result:
cs cs' : List Char
⊢ { byteIdx := utf8Len cs } + cs'.headD default = { byteIdx := utf8Len cs + (cs'.headD default).utf8Size }
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem map_id : p.map (RingHom.id _) = p

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ map (RingHom.id R) p = p

Tactic:
simp [Polynomial.ext_iff, coeff_map]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FinallySmall.lean
theorem finallySmall_of_small_weakly_terminal_set [IsFilteredOrEmpty J] (s : Set J) [Small.{v} s]
    (hs : ∀ i, ∃ j ∈ s, Nonempty (i ⟶ j)) : FinallySmall.{v} J

Proof state:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsFilteredOrEmpty J
s : Set J
inst✝ : Small.{v, u} ↑s
hs : ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)
i : J
⊢ ∃ c, Nonempty (i ⟶ (fullSubcategoryInclusion fun x => x ∈ s).obj c)

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := hs i

Result:
case intro.intro
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsFilteredOrEmpty J
s : Set J
inst✝ : Small.{v, u} ↑s
hs : ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)
i j : J
hj₁ : j ∈ s
hj₂ : Nonempty (i ⟶ j)
⊢ ∃ c, Nonempty (i ⟶ (fullSubcategoryInclusion fun x => x ∈ s).obj c)

Proof state:
case intro.intro
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsFilteredOrEmpty J
s : Set J
inst✝ : Small.{v, u} ↑s
hs : ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)
i j : J
hj₁ : j ∈ s
hj₂ : Nonempty (i ⟶ j)
⊢ ∃ c, Nonempty (i ⟶ (fullSubcategoryInclusion fun x => x ∈ s).obj c)

Tactic:
exact ⟨⟨j, hj₁⟩, hj₂⟩

Result:
no goals

Proof state:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsFilteredOrEmpty J
s : Set J
inst✝ : Small.{v, u} ↑s
hs : ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)
⊢ (fullSubcategoryInclusion fun x => x ∈ s).Final

Tactic:
refine Functor.final_of_exists_of_isFiltered_of_fullyFaithful _ (fun i => ?_)

Result:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsFilteredOrEmpty J
s : Set J
inst✝ : Small.{v, u} ↑s
hs : ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)
i : J
⊢ ∃ c, Nonempty (i ⟶ (fullSubcategoryInclusion fun x => x ∈ s).obj c)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_iff_getElem? {a} {l : List α} : a ∈ l ↔ ∃ i : Nat, l[i]? = some a

Proof state:
α : Type u_1
a : α
l : List α
⊢ a ∈ l ↔ ∃ i, l[i]? = some a

Tactic:
simp [getElem?_eq_some_iff, mem_iff_getElem]

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem image_monotone_setOf_minimal (hf : ∀ ⦃x y⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)) :
    f '' {x | Minimal P x} = {x | Minimal (∃ x₀, P x₀ ∧ f x₀ = ·) x}

Proof state:
case refine_1
α : Type u_1
P : α → Prop
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : β
⊢ x ∈ f '' {x | Minimal P x} → x ∈ {x | Minimal (fun x => ∃ x₀, P x₀ ∧ f x₀ = x) x}

Tactic:
rintro ⟨x, (hx : Minimal _ x), rfl⟩

Result:
case refine_1.intro.intro
α : Type u_1
P : α → Prop
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : α
hx : Minimal P x
⊢ f x ∈ {x | Minimal (fun x => ∃ x₀, P x₀ ∧ f x₀ = x) x}

Proof state:
case refine_1.intro.intro
α : Type u_1
P : α → Prop
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : α
hx : Minimal P x
⊢ f x ∈ {x | Minimal (fun x => ∃ x₀, P x₀ ∧ f x₀ = x) x}

Tactic:
exact (minimal_mem_image_monotone_iff hx.prop hf).2 hx

Result:
no goals

Proof state:
case refine_2
α : Type u_1
P : α → Prop
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : β
h : x ∈ {x | Minimal (fun x => ∃ x₀, P x₀ ∧ f x₀ = x) x}
⊢ x ∈ f '' {x | Minimal P x}

Tactic:
obtain ⟨y, hy, rfl⟩ := (mem_setOf_eq ▸ h).prop

Result:
case refine_2.intro.intro
α : Type u_1
P : α → Prop
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
y : α
hy : P y
h : f y ∈ {x | Minimal (fun x => ∃ x₀, P x₀ ∧ f x₀ = x) x}
⊢ f y ∈ f '' {x | Minimal P x}

Proof state:
case refine_2.intro.intro
α : Type u_1
P : α → Prop
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
y : α
hy : P y
h : f y ∈ {x | Minimal (fun x => ∃ x₀, P x₀ ∧ f x₀ = x) x}
⊢ f y ∈ f '' {x | Minimal P x}

Tactic:
exact mem_image_of_mem _ <| (minimal_mem_image_monotone_iff (s := setOf P) hy hf).1 h

Result:
no goals

Proof state:
α : Type u_1
P : α → Prop
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
⊢ f '' {x | Minimal P x} = {x | Minimal (fun x => ∃ x₀, P x₀ ∧ f x₀ = x) x}

Tactic:
refine Set.ext fun x ↦ ⟨?_, fun h ↦ ?_⟩

Result:
case refine_1
α : Type u_1
P : α → Prop
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : β
⊢ x ∈ f '' {x | Minimal P x} → x ∈ {x | Minimal (fun x => ∃ x₀, P x₀ ∧ f x₀ = x) x}

case refine_2
α : Type u_1
P : α → Prop
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α → β
hf : ∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ x ≤ y)
x : β
h : x ∈ {x | Minimal (fun x => ∃ x₀, P x₀ ∧ f x₀ = x) x}
⊢ x ∈ f '' {x | Minimal P x}
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.get?_eq [BEq α] [Hashable α] {m : Raw α (fun _ => β)} (h : m.WF) {a : α} :
    Raw.Const.get? m a = Raw₀.Const.get? ⟨m, h.size_buckets_pos⟩ a

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α fun x => β
h : m.WF
a : α
⊢ Raw.Const.get? m a = Raw₀.Const.get? ⟨m, ⋯⟩ a

Tactic:
simp [Raw.Const.get?, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/CompleteLattice.lean
@[to_additive]
lemma csInf_inv (hs₀ : s.Nonempty) (hs₁ : BddAbove s) : sInf s⁻¹ = (sSup s)⁻¹

Proof state:
M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
⊢ sInf ((fun x => x⁻¹) '' s) = (sSup s)⁻¹

Tactic:
exact ((OrderIso.inv _).map_csSup' hs₀ hs₁).symm

Result:
no goals

Proof state:
M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
⊢ sInf s⁻¹ = (sSup s)⁻¹

Tactic:
rw [← image_inv_eq_inv]

Result:
M : Type u_1
inst✝³ : ConditionallyCompleteLattice M
inst✝² : Group M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
s : Set M
hs₀ : s.Nonempty
hs₁ : BddAbove s
⊢ sInf ((fun x => x⁻¹) '' s) = (sSup s)⁻¹
-- Mathlib/Data/Nat/ModEq.lean
theorem odd_of_mod_four_eq_three {n : ℕ} : n % 4 = 3 → n % 2 = 1

Proof state:
n : ℕ
⊢ n % 4 = 3 → n % 2 = 1

Tactic:
simpa [ModEq] using @ModEq.of_mul_left 2 n 3 2

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem map_Iic (f : α ≃o β) (a : α) : map f (Iic a) = Iic (f a)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
⊢ (map f) (Iic a) = Iic (f a)

Tactic:
ext

Result:
case a.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
x✝ : β
⊢ x✝ ∈ ↑((map f) (Iic a)) ↔ x✝ ∈ ↑(Iic (f a))

Proof state:
case a.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
a : α
x✝ : β
⊢ x✝ ∈ ↑((map f) (Iic a)) ↔ x✝ ∈ ↑(Iic (f a))

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_eq_true_iff_two_mul_ge {x : BitVec w} : x.msb = true ↔ 2 * x.toNat ≥ 2^w

Proof state:
w : Nat
x : BitVec w
⊢ x.msb = true ↔ 2 * x.toNat ≥ 2 ^ w

Tactic:
simp [← Bool.ne_false_iff, msb_eq_false_iff_two_mul_lt]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem kahler_comp_rightAngleRotation' (x y : E) :
    -(Complex.I * (Complex.I * o.kahler x y)) = o.kahler x y

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ -(Complex.I * (Complex.I * (o.kahler x) y)) = (o.kahler x) y

Tactic:
linear_combination -o.kahler x y * Complex.I_sq

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

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

Tactic:
rw [← floor_lt, le_sub_one_iff]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
lemma natDegree_minpolyDiv_succ [Nontrivial S] :
    natDegree (minpolyDiv R x) + 1 = natDegree (minpoly R x)

Proof state:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ (minpolyDiv R x).natDegree + 1 = (minpoly R x).natDegree

Tactic:
rw [← (minpoly.monic hx).natDegree_map (algebraMap R S), ← minpolyDiv_spec, natDegree_mul']

Result:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ (minpolyDiv R x).natDegree + 1 = (minpolyDiv R x).natDegree + (X - C x).natDegree

R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ (minpolyDiv R x).leadingCoeff * (X - C x).leadingCoeff ≠ 0

Proof state:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ (minpolyDiv R x).leadingCoeff * (X - C x).leadingCoeff ≠ 0

Tactic:
simpa using minpolyDiv_ne_zero hx

Result:
no goals

Proof state:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
hx : IsIntegral R x
inst✝ : Nontrivial S
⊢ (minpolyDiv R x).natDegree + 1 = (minpolyDiv R x).natDegree + (X - C x).natDegree

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem swap_apply_eq_iff {x y z w : α} : swap x y z = w ↔ z = swap x y w

Proof state:
α : Sort u_1
inst✝ : DecidableEq α
x y z w : α
⊢ (swap x y) z = w ↔ z = (swap x y) w

Tactic:
rw [apply_eq_iff_eq_symm_apply, symm_swap]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem areaForm_rightAngleRotation_left (x y : E) : ω (J x) y = -⟪x, y⟫

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.areaForm (o.rightAngleRotation x)) y = -inner x y

Tactic:
rw [← o.inner_comp_rightAngleRotation, o.inner_rightAngleRotation_right, neg_neg]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem rnDeriv_add (s t : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ]
    [t.HaveLebesgueDecomposition μ] [(s + t).HaveLebesgueDecomposition μ] :
    (s + t).rnDeriv μ =ᵐ[μ] s.rnDeriv μ + t.rnDeriv μ

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝² : s.HaveLebesgueDecomposition μ
inst✝¹ : t.HaveLebesgueDecomposition μ
inst✝ : (s + t).HaveLebesgueDecomposition μ
⊢ (s + t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ + t.rnDeriv μ

Tactic:
refine
  Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _)
    ((integrable_rnDeriv _ _).add (integrable_rnDeriv _ _)) ?_

Result:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝² : s.HaveLebesgueDecomposition μ
inst✝¹ : t.HaveLebesgueDecomposition μ
inst✝ : (s + t).HaveLebesgueDecomposition μ
⊢ μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst✝² : s.HaveLebesgueDecomposition μ
inst✝¹ : t.HaveLebesgueDecomposition μ
inst✝ : (s + t).HaveLebesgueDecomposition μ
⊢ μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)

Tactic:
rw [← add_right_inj ((s + t).singularPart μ), singularPart_add_withDensity_rnDeriv_eq,
  withDensityᵥ_add (integrable_rnDeriv _ _) (integrable_rnDeriv _ _), singularPart_add,
  add_assoc, add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
  singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
  singularPart_add_withDensity_rnDeriv_eq]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Defs.lean
theorem mul_self_eq_zero : a * a = 0 ↔ a = 0

Proof state:
M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a : M₀
⊢ a * a = 0 ↔ a = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem card_Ioi_eq_card_Ici_sub_one (a : α) : #(Ioi a) = #(Ici a) - 1

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrderTop α
a : α
⊢ #(Ioi a) = #(Ici a) - 1

Tactic:
rw [Ici_eq_cons_Ioi, card_cons, Nat.add_sub_cancel_right]

Result:
no goals
-- Mathlib/RingTheory/DividedPowers/Basic.lean
theorem dpow_mul_right {n : ℕ} (ha : a ∈ I) :
    hI.dpow n (a * b) = hI.dpow n a * b ^ n

Proof state:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
a b : A
hI : DividedPowers I
n : ℕ
ha : a ∈ I
⊢ hI.dpow n (a * b) = hI.dpow n a * b ^ n

Tactic:
rw [mul_comm, hI.dpow_mul ha, mul_comm]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem constantCoeff_inv (φ : MvPowerSeries σ k) :
    constantCoeff σ k φ⁻¹ = (constantCoeff σ k φ)⁻¹

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
⊢ (constantCoeff σ k) φ⁻¹ = ((constantCoeff σ k) φ)⁻¹

Tactic:
rw [← coeff_zero_eq_constantCoeff_apply, coeff_inv, if_pos rfl]

Result:
no goals

Proof state:
σ : Type u_1
k : Type u_3
inst✝ : Field k
φ : MvPowerSeries σ k
⊢ (constantCoeff σ k) φ⁻¹ = ((constantCoeff σ k) φ)⁻¹

Tactic:
classical
rw [← coeff_zero_eq_constantCoeff_apply, coeff_inv, if_pos rfl]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem lift_mk'_spec (x v) (y : S) : f.lift hg (f.mk' x y) = v ↔ g x = g y * v

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
v : P
y : ↥S
⊢ g x * ↑((IsUnit.liftRight (g.restrict S) hg) y)⁻¹ = v ↔ g x = g ↑y * v

Tactic:
exact mul_inv_left hg _ _ _

Result:
no goals

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
v : P
y : ↥S
⊢ (f.lift hg) (f.mk' x y) = v ↔ g x = g ↑y * v

Tactic:
rw [f.lift_mk' hg]

Result:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x : M
v : P
y : ↥S
⊢ g x * ↑((IsUnit.liftRight (g.restrict S) hg) y)⁻¹ = v ↔ g x = g ↑y * v
-- Mathlib/Topology/Basic.lean
theorem Set.MapsTo.closure {t : Set Y} (h : MapsTo f s t)
    (hc : Continuous f) : MapsTo f (closure s) (closure t)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
t : Set Y
h : MapsTo f s t
hc : Continuous f
⊢ MapsTo f (closure s) (closure t)

Tactic:
simp only [MapsTo, mem_closure_iff_clusterPt]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
t : Set Y
h : MapsTo f s t
hc : Continuous f
⊢ ∀ ⦃x : X⦄, ClusterPt x (𝓟 s) → ClusterPt (f x) (𝓟 t)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
t : Set Y
h : MapsTo f s t
hc : Continuous f
⊢ ∀ ⦃x : X⦄, ClusterPt x (𝓟 s) → ClusterPt (f x) (𝓟 t)

Tactic:
exact fun x hx => hx.map hc.continuousAt (tendsto_principal_principal.2 h)

Result:
no goals