harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Constructible.lean
lemma IsRetrocompact_iff_isSpectralMap_subtypeVal :
    IsRetrocompact s ↔ IsSpectralMap (Subtype.val : s → X)

Proof state:
case refine_1
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsRetrocompact s
t : Set X
htopen : IsOpen t
htcomp : IsCompact t
⊢ IsCompact (Subtype.val ⁻¹' t)

Tactic:
rw [IsEmbedding.subtypeVal.isCompact_iff, image_preimage_eq_inter_range,
  Subtype.range_coe_subtype, setOf_mem_eq, inter_comm]

Result:
case refine_1
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsRetrocompact s
t : Set X
htopen : IsOpen t
htcomp : IsCompact t
⊢ IsCompact (s ∩ t)

Proof state:
case refine_2
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsSpectralMap Subtype.val
t : Set X
htcomp : IsCompact t
htopen : IsOpen t
⊢ IsCompact (s ∩ t)

Tactic:
simpa using (hs.isCompact_preimage_of_isOpen htopen htcomp).image continuous_subtype_val

Result:
no goals

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ IsRetrocompact s ↔ IsSpectralMap Subtype.val

Tactic:
refine ⟨fun hs ↦ ⟨continuous_subtype_val, fun t htopen htcomp ↦ ?_⟩, fun hs t htcomp htopen ↦ ?_⟩

Result:
case refine_1
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsRetrocompact s
t : Set X
htopen : IsOpen t
htcomp : IsCompact t
⊢ IsCompact (Subtype.val ⁻¹' t)

case refine_2
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsSpectralMap Subtype.val
t : Set X
htcomp : IsCompact t
htopen : IsOpen t
⊢ IsCompact (s ∩ t)

Proof state:
case refine_1
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
hs : IsRetrocompact s
t : Set X
htopen : IsOpen t
htcomp : IsCompact t
⊢ IsCompact (s ∩ t)

Tactic:
exact hs htcomp htopen

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem span_singleton_mul_eq_span_singleton_mul {x y : R} (I J : Ideal R) :
    span {x} * I = span {y} * J ↔
      (∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ) ∧ ∀ zJ ∈ J, ∃ zI ∈ I, x * zI = y * zJ

Proof state:
R : Type u
inst✝ : CommSemiring R
x y : R
I J : Ideal R
⊢ span {x} * I = span {y} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zI = y * zJ) ∧ ∀ zJ ∈ J, ∃ zI ∈ I, x * zI = y * zJ

Tactic:
simp only [le_antisymm_iff, span_singleton_mul_le_span_singleton_mul, eq_comm]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem copy_nil {u u'} (hu : u = u') : (Walk.nil : G.Walk u u).copy hu hu = Walk.nil

Proof state:
V : Type u
G : SimpleGraph V
u u' : V
hu : u = u'
⊢ nil.copy hu hu = nil

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
u' : V
⊢ nil.copy ⋯ ⋯ = nil

Proof state:
V : Type u
G : SimpleGraph V
u' : V
⊢ nil.copy ⋯ ⋯ = nil

Tactic:
rfl

Result:
no goals
-- Mathlib/GroupTheory/Torsion.lean
theorem IsTorsion.of_surjective {f : G →* H} (hf : Function.Surjective f) (tG : IsTorsion G) :
    IsTorsion H := fun h => by
  obtain ⟨g, hg⟩ := hf h
  rw [← hg]
  exact f.isOfFinOrder (tG g)

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
tG : IsTorsion G
h : H
⊢ IsOfFinOrder h

Tactic:
obtain ⟨g, hg⟩ := hf h

Result:
case intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
tG : IsTorsion G
h : H
g : G
hg : f g = h
⊢ IsOfFinOrder h

Proof state:
case intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
tG : IsTorsion G
h : H
g : G
hg : f g = h
⊢ IsOfFinOrder h

Tactic:
rw [← hg]

Result:
case intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
tG : IsTorsion G
h : H
g : G
hg : f g = h
⊢ IsOfFinOrder (f g)

Proof state:
case intro
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
f : G →* H
hf : Function.Surjective ⇑f
tG : IsTorsion G
h : H
g : G
hg : f g = h
⊢ IsOfFinOrder (f g)

Tactic:
exact f.isOfFinOrder (tG g)

Result:
no goals
-- Mathlib/Order/SuccPred/LinearLocallyFinite.lean
theorem iterate_pred_toZ (i : ι) (hi : i < i0) : pred^[(-toZ i0 i).toNat] i0 = i

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ pred^[(-toZ i0 i).toNat] i0 = i

Tactic:
rw [toZ_of_lt hi, neg_neg, Int.toNat_natCast]

Result:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ pred^[Nat.find ⋯] i0 = i

Proof state:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ pred^[Nat.find ⋯] i0 = i

Tactic:
exact Nat.find_spec (exists_pred_iterate_of_le hi.le)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem epi_of_target_iso_zero {X Y : C} (f : X ⟶ Y) (i : Y ≅ 0) : Epi f :=
  ⟨fun {Z} g h _ => by rw [zero_of_source_iso_zero g i, zero_of_source_iso_zero h i]⟩

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : Y ≅ 0
Z : C
g h : Y ⟶ Z
x✝ : f ≫ g = f ≫ h
⊢ g = h

Tactic:
rw [zero_of_source_iso_zero g i, zero_of_source_iso_zero h i]

Result:
no goals
-- Mathlib/Topology/Order/ScottTopology.lean
lemma monotone_of_continuous [IsScott α D] (hf : Continuous f) : Monotone f := fun _ b hab ↦ by
  by_contra h
  simpa only [mem_compl_iff, mem_preimage, mem_Iic, le_refl, not_true]
    using isUpperSet_of_isOpen (D := D) ((isOpen_compl_iff.2 isClosed_Iic).preimage hf) hab h

Proof state:
α : Type u_1
β : Type u_2
D : Set (Set α)
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
inst✝ : IsScott α D
hf : Continuous f
x✝ b : α
hab : x✝ ≤ b
h : ¬f x✝ ≤ f b
⊢ False

Tactic:
simpa only [mem_compl_iff, mem_preimage, mem_Iic, le_refl, not_true]
  using isUpperSet_of_isOpen (D := D) ((isOpen_compl_iff.2 isClosed_Iic).preimage hf) hab h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
D : Set (Set α)
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
inst✝ : IsScott α D
hf : Continuous f
x✝ b : α
hab : x✝ ≤ b
⊢ f x✝ ≤ f b

Tactic:
by_contra h

Result:
α : Type u_1
β : Type u_2
D : Set (Set α)
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
inst✝ : IsScott α D
hf : Continuous f
x✝ b : α
hab : x✝ ≤ b
h : ¬f x✝ ≤ f b
⊢ False
-- Mathlib/CategoryTheory/Skeletal.lean
theorem skeleton_skeletal : Skeletal (Skeleton C)

Proof state:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Skeleton C
h : X ≅ Y
⊢ X = Y

Tactic:
have : X.out ≈ Y.out := ⟨(fromSkeleton C).mapIso h⟩

Result:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Skeleton C
h : X ≅ Y
this : Quotient.out X ≈ Quotient.out Y
⊢ X = Y

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ Skeletal (Skeleton C)

Tactic:
rintro X Y ⟨h⟩

Result:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Skeleton C
h : X ≅ Y
⊢ X = Y

Proof state:
case intro
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Skeleton C
h : X ≅ Y
this : Quotient.out X ≈ Quotient.out Y
⊢ X = Y

Tactic:
simpa using Quotient.sound this

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem inv_mul_cancel {x : tsze R M} (hx : fst x ≠ 0) : x⁻¹ * x = 1

Proof state:
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹ * x = 1

Tactic:
convert mul_left_eq_one _ _ (_root_.inv_mul_cancel₀ hx) using 2

Result:
case h.e'_2.h.e'_5
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹ = inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))

Proof state:
case h.e'_2.h.e'_5
R : Type u
M : Type v
inst✝³ : DivisionSemiring R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
hx : x.fst ≠ 0
⊢ x⁻¹ = inl x.fst⁻¹ + inr (-(x.fst⁻¹ •> x.snd <• x.fst⁻¹))

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
private lemma exists_lt_mul_left_of_nonneg {a b c : α} (ha : 0 ≤ a) (hc : 0 ≤ c) (h : c < a * b) :
    ∃ a' ∈ Set.Ico 0 a, c < a' * b

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
⊢ ∃ a' ∈ Set.Ico 0 a, c < a' * b

Tactic:
have hb : 0 < b := pos_of_mul_pos_right (hc.trans_lt h) ha

Result:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
⊢ ∃ a' ∈ Set.Ico 0 a, c < a' * b

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
⊢ ∃ a' ∈ Set.Ico 0 a, c < a' * b

Tactic:
obtain ⟨a', ha', a_a'⟩ := exists_between ((div_lt_iff₀ hb).2 h)

Result:
case intro.intro
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
a' : α
ha' : c / b < a'
a_a' : a' < a
⊢ ∃ a' ∈ Set.Ico 0 a, c < a' * b

Proof state:
case intro.intro
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : c < a * b
hb : 0 < b
a' : α
ha' : c / b < a'
a_a' : a' < a
⊢ ∃ a' ∈ Set.Ico 0 a, c < a' * b

Tactic:
exact ⟨a', ⟨(div_nonneg hc hb.le).trans ha'.le, a_a'⟩, (div_lt_iff₀ hb).1 ha'⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/Pullbacks.lean
theorem cocycle_snd_fst_snd (i j k : 𝒰.J) :
    t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j ≫ pullback.snd _ _ ≫ pullback.fst _ _ ≫
      pullback.snd _ _ = pullback.snd _ _ ≫ 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 k : 𝒰.J
⊢ t' 𝒰 f g i j k ≫
      t' 𝒰 f g j k i ≫
        t' 𝒰 f g k i j ≫
          pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
            pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) ≫ pullback.snd (𝒰.map i ≫ f) g =
    pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫
      pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) ≫ pullback.snd (𝒰.map i ≫ f) g

Tactic:
simp only [pullback.condition_assoc, t'_snd_fst_snd]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem normSq_add (a b : ℍ[R]) : normSq (a + b) = normSq a + normSq b + 2 * (a * star b).re :=
  calc
    normSq (a + b) = normSq a + (a * star b).re + ((b * star a).re + normSq b)

Proof state:
R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ normSq (a + b) = normSq a + (a * star b).re + ((b * star a).re + normSq b)

Tactic:
simp_rw [normSq_def, star_add, add_mul, mul_add, add_re]

Result:
no goals

Proof state:
R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ normSq a + normSq b + ((a * star b).re + (b * star a).re) = normSq a + normSq b + 2 * (a * star b).re

Tactic:
rw [← add_re, ← star_mul_star a b, self_add_star', coe_re]

Result:
no goals

Proof state:
R : Type u_3
inst✝ : CommRing R
a b : ℍ[R]
⊢ normSq a + (a * star b).re + ((b * star a).re + normSq b) = normSq a + normSq b + ((a * star b).re + (b * star a).re)

Tactic:
abel

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem coe_succ_lt_iff_lt {n : ℕ} {j k : Fin n} : (j : Fin <| n + 1) < k ↔ j < k

Proof state:
n : ℕ
j k : Fin n
⊢ ↑↑j < ↑↑k ↔ j < k

Tactic:
simp only [coe_eq_castSucc, castSucc_lt_castSucc_iff]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Quotient.lean
theorem card_orbit_mul_card_stabilizer_eq_card_group (b : β) [Fintype α] [Fintype <| orbit α b]
    [Fintype <| stabilizer α b] :
    Fintype.card (orbit α b) * Fintype.card (stabilizer α b) = Fintype.card α

Proof state:
α : Type u
β : Type v
inst✝⁴ : Group α
inst✝³ : MulAction α β
b : β
inst✝² : Fintype α
inst✝¹ : Fintype ↑(orbit α b)
inst✝ : Fintype ↥(stabilizer α b)
⊢ Fintype.card ↑(orbit α b) * Fintype.card ↥(stabilizer α b) = Fintype.card α

Tactic:
rw [← Fintype.card_prod, Fintype.card_congr (orbitProdStabilizerEquivGroup α b)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldlM_reverse [Monad m] (l : Vector α n) (f : β → α → m β) (b) :
    l.reverse.foldlM f b = l.foldrM (fun x y => f y x) b

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : β → α → m β
b : β
l : Array α
⊢ foldlM f b { toArray := l, size_toArray := ⋯ }.reverse =
    foldrM (fun x y => f y x) b { toArray := l, size_toArray := ⋯ }

Tactic:
simp [Array.foldlM_reverse]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝ : Monad m
l : Vector α n
f : β → α → m β
b : β
⊢ foldlM f b l.reverse = foldrM (fun x y => f y x) b l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : β → α → m β
b : β
l : Array α
⊢ foldlM f b { toArray := l, size_toArray := ⋯ }.reverse =
    foldrM (fun x y => f y x) b { toArray := l, size_toArray := ⋯ }
-- Mathlib/Data/Stream/Init.lean
theorem get_interleave_left : ∀ (n : ℕ) (s₁ s₂ : Stream' α),
    get (s₁ ⋈ s₂) (2 * n) = get s₁ n
  | 0, _, _ => rfl
  | n + 1, s₁, s₂ => by
    change get (s₁ ⋈ s₂) (succ (succ (2 * n))) = get s₁ (succ n)
    rw [get_succ, get_succ, interleave_eq, tail_cons, tail_cons]
    rw [get_interleave_left n (tail s₁) (tail s₂)]
    rfl

Proof state:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁.tail ⋈ s₂.tail).get (2 * n) = s₁.get n.succ

Tactic:
rw [get_interleave_left n (tail s₁) (tail s₂)]

Result:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ s₁.tail.get n = s₁.get n.succ

Proof state:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).get (2 * n).succ.succ = s₁.get n.succ

Tactic:
rw [get_succ, get_succ, interleave_eq, tail_cons, tail_cons]

Result:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁.tail ⋈ s₂.tail).get (2 * n) = s₁.get n.succ

Proof state:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).get (2 * (n + 1)) = s₁.get (n + 1)

Tactic:
change get (s₁ ⋈ s₂) (succ (succ (2 * n))) = get s₁ (succ n)

Result:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ (s₁ ⋈ s₂).get (2 * n).succ.succ = s₁.get n.succ

Proof state:
α : Type u
n : ℕ
s₁ s₂ : Stream' α
⊢ s₁.tail.get n = s₁.get n.succ

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Intrinsic.lean
theorem intrinsicInterior_singleton (x : P) : intrinsicInterior 𝕜 ({x} : Set P) = {x}

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
x : P
⊢ intrinsicInterior 𝕜 {x} = {x}

Tactic:
simp only [intrinsicInterior, preimage_coe_affineSpan_singleton, interior_univ, image_univ,
  Subtype.range_coe_subtype, mem_affineSpan_singleton, setOf_eq_eq_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem count_cast (l : Vector α n) : (l.cast h).count a = l.count a

Proof state:
α : Type u_1
inst✝ : BEq α
n a✝ : Nat
h : n = a✝
a : α
l : Vector α n
⊢ count a (Vector.cast h l) = count a l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
inst✝ : BEq α
a✝ : Nat
a : α
l : Array α
h : l.size = a✝
⊢ count a (Vector.cast h { toArray := l, size_toArray := ⋯ }) = count a { toArray := l, size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
a✝ : Nat
a : α
l : Array α
h : l.size = a✝
⊢ count a (Vector.cast h { toArray := l, size_toArray := ⋯ }) = count a { toArray := l, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean
theorem le_rpow_one_add_norm_iff_norm_le {r t : ℝ} (hr : 0 < r) (ht : 0 < t) (x : E) :
    t ≤ (1 + ‖x‖) ^ (-r) ↔ ‖x‖ ≤ t ^ (-r⁻¹) - 1

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

Tactic:
exact (Real.le_rpow_inv_iff_of_neg (by positivity) ht (neg_lt_zero.mpr hr)).symm

Result:
no goals

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

Tactic:
rw [le_sub_iff_add_le', neg_inv]

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

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
r t : ℝ
hr : 0 < r
ht : 0 < t
x : E
⊢ 0 < 1 + ‖x‖

Tactic:
positivity

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range_add (a b : Nat) : range (a + b) = range a ++ (range b).map (a + ·)

Proof state:
a b : Nat
⊢ range (a + b) = range a ++ map (fun x => a + x) (range b)

Tactic:
rw [← range'_eq_map_range]

Result:
a b : Nat
⊢ range (a + b) = range a ++ range' a b

Proof state:
a b : Nat
⊢ range (a + b) = range a ++ range' a b

Tactic:
simpa [range_eq_range', Nat.add_comm] using (range'_append_1 0 a b).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem containsThenInsert_fst {k : α} {v : β k} : (m.containsThenInsert k v).1 = m.contains k

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

Tactic:
rw [containsThenInsert_eq_containsₘ, contains_eq_containsₘ]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem ext_fourfold' {φ ψ : (M ⊗[R] N) ⊗[R] P ⊗[R] Q →ₗ[R] S}
    (H : ∀ w x y z, φ (w ⊗ₜ x ⊗ₜ (y ⊗ₜ z)) = ψ (w ⊗ₜ x ⊗ₜ (y ⊗ₜ z))) : φ = ψ

Proof state:
case H.H.h.h.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
S : Type u_9
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : AddCommMonoid S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R Q
inst✝¹ : Module R S
inst✝ : Module R P
φ ψ : (M ⊗[R] N) ⊗[R] P ⊗[R] Q →ₗ[R] S
H : ∀ (w : M) (x : N) (y : P) (z : Q), φ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z) = ψ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z)
m : M
n : N
p : P
q : Q
⊢ (((mk R P Q).compr₂ ((((mk R M N).compr₂ ((mk R (M ⊗[R] N) (P ⊗[R] Q)).compr₂ φ)) m) n)) p) q =
    (((mk R P Q).compr₂ ((((mk R M N).compr₂ ((mk R (M ⊗[R] N) (P ⊗[R] Q)).compr₂ ψ)) m) n)) p) q

Tactic:
exact H m n p q

Result:
no goals

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
S : Type u_9
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : AddCommMonoid S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R Q
inst✝¹ : Module R S
inst✝ : Module R P
φ ψ : (M ⊗[R] N) ⊗[R] P ⊗[R] Q →ₗ[R] S
H : ∀ (w : M) (x : N) (y : P) (z : Q), φ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z) = ψ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z)
⊢ φ = ψ

Tactic:
ext m n p q

Result:
case H.H.h.h.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
S : Type u_9
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : AddCommMonoid S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R Q
inst✝¹ : Module R S
inst✝ : Module R P
φ ψ : (M ⊗[R] N) ⊗[R] P ⊗[R] Q →ₗ[R] S
H : ∀ (w : M) (x : N) (y : P) (z : Q), φ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z) = ψ ((w ⊗ₜ[R] x) ⊗ₜ[R] y ⊗ₜ[R] z)
m : M
n : N
p : P
q : Q
⊢ (((mk R P Q).compr₂ ((((mk R M N).compr₂ ((mk R (M ⊗[R] N) (P ⊗[R] Q)).compr₂ φ)) m) n)) p) q =
    (((mk R P Q).compr₂ ((((mk R M N).compr₂ ((mk R (M ⊗[R] N) (P ⊗[R] Q)).compr₂ ψ)) m) n)) p) q
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem _root_.Submodule.map_comap_eq_self [RingHomSurjective τ₁₂] {f : F} {q : Submodule R₂ M₂}
    (h : q ≤ range f) : map f (comap f q) = q

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
F : Type u_10
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F τ₁₂ M M₂
inst✝ : RingHomSurjective τ₁₂
f : F
q : Submodule R₂ M₂
h : q ≤ range f
⊢ map f (comap f q) = q

Tactic:
rwa [Submodule.map_comap_eq, inf_eq_right]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Images.lean
theorem hom_comp_map_image_ι {X Y : A} (f : X ⟶ Y) :
    (iso L f).hom ≫ L.map (image.ι f) = image.ι (L.map f)

Proof state:
A : Type u₁
B : Type u₂
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Category.{v₂, u₂} B
inst✝⁵ : HasEqualizers A
inst✝⁴ : HasImages A
inst✝³ : StrongEpiCategory B
inst✝² : HasImages B
L : A ⥤ B
inst✝¹ : ∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) L
inst✝ : ∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), PreservesColimit (span f g) L
X Y : A
f : X ⟶ Y
⊢ (iso L f).hom ≫ L.map (image.ι f) = image.ι (L.map f)

Tactic:
rw [iso_hom, image.lift_fac]

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem Fintype.card_subtype [Fintype α] (p : α → Prop) [DecidablePred p] :
    Fintype.card { x // p x } = #{x | p x}

Proof state:
α : Type u_1
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ ∀ (x : α), x ∈ filter (fun x => p x) univ ↔ p x

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ card { x // p x } = #(filter (fun x => p x) univ)

Tactic:
refine Fintype.card_of_subtype _ ?_

Result:
α : Type u_1
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
⊢ ∀ (x : α), x ∈ filter (fun x => p x) univ ↔ p x
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem prev_eq (f : Hom C₁ C₂) {i j : ι} (w : c.Rel i j) :
    f.prev j = (C₁.xPrevIso w).hom ≫ f.f i ≫ (C₂.xPrevIso w).inv

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
f : C₁.Hom C₂
j : ι
w : c.Rel (c.prev j) j
⊢ f.prev j = (C₁.xPrevIso w).hom ≫ f.f (c.prev j) ≫ (C₂.xPrevIso w).inv

Tactic:
simp only [xPrevIso, eqToIso_refl, Iso.refl_hom, Iso.refl_inv, comp_id, id_comp]

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
f : C₁.Hom C₂
i j : ι
w : c.Rel i j
⊢ f.prev j = (C₁.xPrevIso w).hom ≫ f.f i ≫ (C₂.xPrevIso w).inv

Tactic:
obtain rfl := c.prev_eq' w

Result:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex V c
f : C₁.Hom C₂
j : ι
w : c.Rel (c.prev j) j
⊢ f.prev j = (C₁.xPrevIso w).hom ≫ f.f (c.prev j) ≫ (C₂.xPrevIso w).inv
-- Mathlib/Topology/ContinuousOn.lean
theorem continuous_prod_of_discrete_left [DiscreteTopology α] {f : α × β → γ} :
    Continuous f ↔ ∀ a, Continuous (f ⟨a, ·⟩)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ Continuous f ↔ ∀ (a : α), Continuous fun x => f (a, x)

Tactic:
simp_rw [continuous_iff_continuousOn_univ]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ ContinuousOn f univ ↔ ∀ (a : α), ContinuousOn (fun x => f (a, x)) univ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ ContinuousOn f univ ↔ ∀ (a : α), ContinuousOn (fun x => f (a, x)) univ

Tactic:
exact continuousOn_prod_of_discrete_left

Result:
no goals
-- Mathlib/Order/PiLex.lean
theorem toLex_update_le_self_iff : toLex (update x i a) ≤ toLex x ↔ a ≤ x i

Proof state:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
x : (i : ι) → β i
i : ι
a : β i
⊢ toLex (update x i a) ≤ toLex x ↔ a ≤ x i

Tactic:
simp_rw [le_iff_lt_or_eq, toLex_update_lt_self_iff, toLex_inj, update_eq_self_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Conj.lean
theorem conjAut_apply (f : Aut X) : α.conjAut f = α.symm ≪≫ f ≪≫ α

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
f : Aut X
⊢ α.conjAut f = α.symm ≪≫ f ≪≫ α

Tactic:
aesop_cat

Result:
no goals