harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem mem_pmap {p : α → Prop} {f : ∀ a, p a → β} {l : Vector α n} {H b} :
    b ∈ pmap f l H ↔ ∃ (a : _) (h : a ∈ l), f a (H a h) = b

Proof state:
α : Type u_1
β : Type u_2
n : Nat
p : α → Prop
f : (a : α) → p a → β
l : Vector α n
H : ∀ (a : α), a ∈ l → p a
b : β
⊢ b ∈ pmap f l H ↔ ∃ a h, f a ⋯ = b

Tactic:
simp only [pmap_eq_map_attach, mem_map, mem_attach, true_and, Subtype.exists, eq_comm]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
lemma Reachable.exists_path_of_dist (hr : G.Reachable u v) :
    ∃ (p : G.Walk u v), p.IsPath ∧ p.length = G.dist u v

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
hr : G.Reachable u v
⊢ ∃ p, p.IsPath ∧ p.length = G.dist u v

Tactic:
obtain ⟨p, h⟩ := hr.exists_walk_length_eq_dist

Result:
case intro
V : Type u_1
G : SimpleGraph V
u v : V
hr : G.Reachable u v
p : G.Walk u v
h : p.length = G.dist u v
⊢ ∃ p, p.IsPath ∧ p.length = G.dist u v

Proof state:
case intro
V : Type u_1
G : SimpleGraph V
u v : V
hr : G.Reachable u v
p : G.Walk u v
h : p.length = G.dist u v
⊢ ∃ p, p.IsPath ∧ p.length = G.dist u v

Tactic:
exact ⟨p, p.isPath_of_length_eq_dist h, h⟩

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean
lemma quasiIsoAt_shift_iff {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n i j : ℤ) (h : n + i = j) :
    QuasiIsoAt (φ⟦n⟧') i ↔ QuasiIsoAt φ j

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : CochainComplex C ℤ
φ : K ⟶ L
n i j : ℤ
h : n + i = j
⊢ IsIso (homologyMap ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).map φ) i) ↔ IsIso (homologyMap φ j)

Tactic:
exact (NatIso.isIso_map_iff
  ((homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n i j h) φ)

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : CochainComplex C ℤ
φ : K ⟶ L
n i j : ℤ
h : n + i = j
⊢ QuasiIsoAt ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).map φ) i ↔ QuasiIsoAt φ j

Tactic:
simp only [quasiIsoAt_iff_isIso_homologyMap]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : CochainComplex C ℤ
φ : K ⟶ L
n i j : ℤ
h : n + i = j
⊢ IsIso (homologyMap ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).map φ) i) ↔ IsIso (homologyMap φ j)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_insertIfNew [LawfulBEq α] (h : m.WF) {k a : α} {v : β k} :
    (m.insertIfNew k v).get? a =
      if h : k == a ∧ ¬k ∈ m then some (cast (congrArg β (eq_of_beq h.1)) v)
      else m.get? a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k a : α
v : β k
⊢ (m.insertIfNew k v).get? a = if h : (k == a) = true ∧ ¬k ∈ m then some (cast ⋯ v) else m.get? a

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k a : α
v : β k
⊢ (m.insertIfNew k v).get? a = if h : (k == a) = true ∧ m.contains k = false then some (cast ⋯ v) else m.get? a

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
k a : α
v : β k
⊢ (m.insertIfNew k v).get? a = if h : (k == a) = true ∧ m.contains k = false then some (cast ⋯ v) else m.get? a

Tactic:
simp_to_raw using Raw₀.get?_insertIfNew ⟨m, _⟩

Result:
no goals
-- Mathlib/CategoryTheory/Localization/FiniteProducts.lean
lemma adj_counit_app (F : Discrete J ⥤ C) :
    (adj L hW).counit.app (F ⋙ L) =
      (Functor.const (Discrete J)).map ((compLimitFunctorIso L hW).hom.app F) ≫
        (Functor.compConstIso (Discrete J) L).hom.app (lim.obj F) ≫
        whiskerRight (constLimAdj.counit.app F) L

Proof state:
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₂, u₂} D
L : C ⥤ D
W : MorphismProperty C
inst✝³ : L.IsLocalization W
J : Type
inst✝² : HasProductsOfShape J C
hW : W.IsStableUnderProductsOfShape J
inst✝¹ : W.ContainsIdentities
inst✝ : Finite J
F : Discrete J ⥤ C
⊢ (adj L hW).counit.app (F ⋙ L) =
    (Functor.const (Discrete J)).map ((compLimitFunctorIso L hW).hom.app F) ≫
      (Functor.compConstIso (Discrete J) L).hom.app (lim.obj F) ≫ whiskerRight (constLimAdj.counit.app F) L

Tactic:
apply constLimAdj.localization_counit_app

Result:
no goals
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem iterate_verschiebung_mul_left (x y : 𝕎 R) (i : ℕ) :
    verschiebung^[i] x * y = verschiebung^[i] (x * frobenius^[i] y)

Proof state:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
ih : ∀ (y : 𝕎 R), (⇑verschiebung)^[i] x * y = (⇑verschiebung)^[i] (x * (⇑frobenius)^[i] y)
y : 𝕎 R
⊢ verschiebung ((⇑verschiebung)^[i] (x * (⇑frobenius)^[i] (frobenius y))) =
    verschiebung ((⇑verschiebung)^[i] (x * (⇑frobenius)^[i + 1] y))

Tactic:
rfl

Result:
no goals

Proof state:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
ih : ∀ (y : 𝕎 R), (⇑verschiebung)^[i] x * y = (⇑verschiebung)^[i] (x * (⇑frobenius)^[i] y)
y : 𝕎 R
⊢ (⇑verschiebung)^[i + 1] x * y = (⇑verschiebung)^[i + 1] (x * (⇑frobenius)^[i + 1] y)

Tactic:
rw [iterate_succ_apply', ← verschiebung_mul_frobenius, ih, iterate_succ_apply']

Result:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
ih : ∀ (y : 𝕎 R), (⇑verschiebung)^[i] x * y = (⇑verschiebung)^[i] (x * (⇑frobenius)^[i] y)
y : 𝕎 R
⊢ verschiebung ((⇑verschiebung)^[i] (x * (⇑frobenius)^[i] (frobenius y))) =
    verschiebung ((⇑verschiebung)^[i] (x * (⇑frobenius)^[i + 1] y))

Proof state:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
⊢ (⇑verschiebung)^[0] x * y = (⇑verschiebung)^[0] (x * (⇑frobenius)^[0] y)

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
i : ℕ
⊢ (⇑verschiebung)^[i] x * y = (⇑verschiebung)^[i] (x * (⇑frobenius)^[i] y)

Tactic:
induction' i with i ih generalizing y

Result:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x y : 𝕎 R
⊢ (⇑verschiebung)^[0] x * y = (⇑verschiebung)^[0] (x * (⇑frobenius)^[0] y)

case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
ih : ∀ (y : 𝕎 R), (⇑verschiebung)^[i] x * y = (⇑verschiebung)^[i] (x * (⇑frobenius)^[i] y)
y : 𝕎 R
⊢ (⇑verschiebung)^[i + 1] x * y = (⇑verschiebung)^[i + 1] (x * (⇑frobenius)^[i + 1] y)
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_le_logb (h : 0 < x) (h₁ : 0 < y) : logb b x ≤ logb b y ↔ x ≤ y

Proof state:
b x y : ℝ
hb : 1 < b
h : 0 < x
h₁ : 0 < y
⊢ logb b x ≤ logb b y ↔ x ≤ y

Tactic:
rw [logb, logb, div_le_div_iff_of_pos_right (log_pos hb), log_le_log_iff h h₁]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
lemma AnalyticAt.analyticWithinAt (hf : AnalyticAt 𝕜 f x) : AnalyticWithinAt 𝕜 f s x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
hf : AnalyticAt 𝕜 f x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
rw [← analyticWithinAt_univ] at hf

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f univ x
⊢ AnalyticWithinAt 𝕜 f s x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f univ x
⊢ AnalyticWithinAt 𝕜 f s x

Tactic:
apply hf.mono (subset_univ _)

Result:
no goals
-- Mathlib/Topology/Bornology/Basic.lean
theorem isBounded_sUnion {S : Set (Set α)} (hs : S.Finite) :
    IsBounded (⋃₀ S) ↔ ∀ s ∈ S, IsBounded s

Proof state:
α : Type u_2
inst✝ : Bornology α
S : Set (Set α)
hs : S.Finite
⊢ IsBounded (⋃₀ S) ↔ ∀ s ∈ S, IsBounded s

Tactic:
rw [sUnion_eq_biUnion, isBounded_biUnion hs]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem sup_limZero {f g : CauSeq α abs} (hf : LimZero f) (hg : LimZero g) : LimZero (f ⊔ g)
  | ε, ε0 =>
    (exists_forall_ge_and (hf _ ε0) (hg _ ε0)).imp fun _ H j ij => by
      let ⟨H₁, H₂⟩ := H _ ij
      rw [abs_lt] at H₁ H₂ ⊢
      exact ⟨lt_sup_iff.mpr (Or.inl H₁.1), sup_lt_iff.mpr ⟨H₁.2, H₂.2⟩⟩

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x✝ : ℕ
H : ∀ j ≥ x✝, |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ x✝
H₁ : -ε < ↑f j ∧ ↑f j < ε
H₂ : -ε < ↑g j ∧ ↑g j < ε
⊢ -ε < ↑(f ⊔ g) j ∧ ↑(f ⊔ g) j < ε

Tactic:
exact ⟨lt_sup_iff.mpr (Or.inl H₁.1), sup_lt_iff.mpr ⟨H₁.2, H₂.2⟩⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x✝ : ℕ
H : ∀ j ≥ x✝, |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ x✝
H₁ : |↑f j| < ε
H₂ : |↑g j| < ε
⊢ |↑(f ⊔ g) j| < ε

Tactic:
rw [abs_lt] at H₁ H₂ ⊢

Result:
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x✝ : ℕ
H : ∀ j ≥ x✝, |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ x✝
H₁ : -ε < ↑f j ∧ ↑f j < ε
H₂ : -ε < ↑g j ∧ ↑g j < ε
⊢ -ε < ↑(f ⊔ g) j ∧ ↑(f ⊔ g) j < ε

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x✝ : ℕ
H : ∀ j ≥ x✝, |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ x✝
⊢ |↑(f ⊔ g) j| < ε

Tactic:
let ⟨H₁, H₂⟩ := H _ ij

Result:
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x✝ : ℕ
H : ∀ j ≥ x✝, |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ x✝
H₁ : |↑f j| < ε
H₂ : |↑g j| < ε
⊢ |↑(f ⊔ g) j| < ε
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem buckets_size_withComputedSize {self : Array (AssocList α β)} :
    (withComputedSize self).2.size = self.size

Proof state:
α : Type u
β : α → Type v
self : Array (AssocList α β)
⊢ (withComputedSize self).buckets.size = self.size

Tactic:
simp [withComputedSize]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivAt.comp_hasFDerivWithinAt_of_eq {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {s} (x)
    (hh : HasDerivAt h₂ h₂' y) (hf : HasFDerivWithinAt f f' s x) (hy : y = f x) :
    HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
s : Set E
x : E
hh : HasDerivAt h₂ h₂' (f x)
hf : HasFDerivWithinAt f f' s x
hy : y = f x
⊢ HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Tactic:
exact hh.comp_hasFDerivWithinAt x hf

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
s : Set E
x : E
hh : HasDerivAt h₂ h₂' y
hf : HasFDerivWithinAt f f' s x
hy : y = f x
⊢ HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x

Tactic:
rw [hy] at hh

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
s : Set E
x : E
hh : HasDerivAt h₂ h₂' (f x)
hf : HasFDerivWithinAt f f' s x
hy : y = f x
⊢ HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x
-- Mathlib/Topology/OmegaCompletePartialOrder.lean
theorem notBelow_isOpen : IsOpen (notBelow y)

Proof state:
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
⊢ ωScottContinuous fun x => x ∈ notBelow y

Tactic:
rw [ωScottContinuous_iff_monotone_map_ωSup]

Result:
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
⊢ ∃ (hf : Monotone fun x => x ∈ notBelow y),
    ∀ (c : Chain α), (ωSup c ∈ notBelow y) = ωSup (c.map { toFun := fun x => x ∈ notBelow y, monotone' := hf })

Proof state:
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
⊢ ∃ (hf : Monotone fun x => x ∈ notBelow y),
    ∀ (c : Chain α), (ωSup c ∈ notBelow y) = ωSup (c.map { toFun := fun x => x ∈ notBelow y, monotone' := hf })

Tactic:
refine ⟨h, fun c ↦ eq_of_forall_ge_iff fun z ↦ ?_⟩

Result:
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
c : Chain α
z : Prop
⊢ (ωSup c ∈ notBelow y) ≤ z ↔ ωSup (c.map { toFun := fun x => x ∈ notBelow y, monotone' := h }) ≤ z

Proof state:
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
⊢ IsOpen (notBelow y)

Tactic:
dsimp only [IsOpen, TopologicalSpace.IsOpen, Scott.IsOpen]

Result:
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
⊢ ωScottContinuous fun x => x ∈ notBelow y

Proof state:
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
c : Chain α
z : Prop
⊢ (ωSup c ∈ notBelow y) ≤ z ↔ ωSup (c.map { toFun := fun x => x ∈ notBelow y, monotone' := h }) ≤ z

Tactic:
simp only [ωSup_le_iff, notBelow, mem_setOf_eq, le_Prop_eq, OrderHom.coe_mk, Chain.map_coe,
  Function.comp_apply, exists_imp, not_forall]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
⊢ IsOpen (notBelow y)

Tactic:
have h : Monotone (notBelow y) := fun x z hle ↦ mt hle.trans

Result:
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
⊢ IsOpen (notBelow y)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem decide_true_eq  {b : Bool} [Decidable (true = b)]  : decide (true  = b) =  b

Proof state:
b : Bool
inst✝ : Decidable (true = b)
⊢ decide (true = b) = b

Tactic:
cases b <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem dvd_sub_of_emod_eq {a b c : Int} (h : a % b = c) : b ∣ a - c

Proof state:
a b c : Int
h : a % b = c
hx : (a - c) % b = 0
⊢ b ∣ a - c

Tactic:
exact dvd_of_emod_eq_zero hx

Result:
no goals

Proof state:
a b c : Int
h : a % b = c
⊢ a % b % b = c % b

Tactic:
rw [h]

Result:
no goals

Proof state:
a b c : Int
h : a % b = c
⊢ b ∣ a - c

Tactic:
have hx : (a % b) % b = c % b := by
  rw [h]

Result:
a b c : Int
h : a % b = c
hx : a % b % b = c % b
⊢ b ∣ a - c

Proof state:
a b c : Int
h : a % b = c
hx : a % b % b = c % b
⊢ b ∣ a - c

Tactic:
rw [Int.emod_emod, ← emod_sub_cancel_right c, Int.sub_self, zero_emod] at hx

Result:
a b c : Int
h : a % b = c
hx : (a - c) % b = 0
⊢ b ∣ a - c
-- Mathlib/Topology/MetricSpace/Lipschitz.lean
theorem of_dist_le' {K : ℝ} (h : ∀ x y, dist (f x) (f y) ≤ K * dist x y) :
    LipschitzWith (Real.toNNReal K) f :=
  of_dist_le_mul fun x y =>
    le_trans (h x y) <| by gcongr; apply Real.le_coe_toNNReal

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
K : ℝ
h : ∀ (x y : α), dist (f x) (f y) ≤ K * dist x y
x y : α
⊢ K * dist x y ≤ ↑K.toNNReal * dist x y

Tactic:
gcongr

Result:
case h
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
K : ℝ
h : ∀ (x y : α), dist (f x) (f y) ≤ K * dist x y
x y : α
⊢ K ≤ ↑K.toNNReal

Proof state:
case h
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
K : ℝ
h : ∀ (x y : α), dist (f x) (f y) ≤ K * dist x y
x y : α
⊢ K ≤ ↑K.toNNReal

Tactic:
apply Real.le_coe_toNNReal

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem map_map (γ : Path x y) {Z : Type*} [TopologicalSpace Z]
    {f : X → Y} (hf : Continuous f) {g : Y → Z} (hg : Continuous g) :
    (γ.map hf).map hg = γ.map (hg.comp hf)

Proof state:
case a.h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y : X
γ : Path x y
Z : Type u_4
inst✝ : TopologicalSpace Z
f : X → Y
hf : Continuous f
g : Y → Z
hg : Continuous g
x✝ : ↑I
⊢ ((γ.map hf).map hg) x✝ = (γ.map ⋯) x✝

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y : X
γ : Path x y
Z : Type u_4
inst✝ : TopologicalSpace Z
f : X → Y
hf : Continuous f
g : Y → Z
hg : Continuous g
⊢ (γ.map hf).map hg = γ.map ⋯

Tactic:
ext

Result:
case a.h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
x y : X
γ : Path x y
Z : Type u_4
inst✝ : TopologicalSpace Z
f : X → Y
hf : Continuous f
g : Y → Z
hg : Continuous g
x✝ : ↑I
⊢ ((γ.map hf).map hg) x✝ = (γ.map ⋯) x✝
-- Mathlib/Topology/Instances/Discrete.lean
theorem discreteTopology_iff_orderTopology_of_pred_succ [LinearOrder α] [PredOrder α]
    [SuccOrder α] : DiscreteTopology α ↔ OrderTopology α

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
⊢ DiscreteTopology α ↔ OrderTopology α

Tactic:
refine ⟨fun h ↦ ⟨?_⟩, fun h ↦ .of_predOrder_succOrder⟩

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
h : DiscreteTopology α
⊢ inst✝³ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : PredOrder α
inst✝ : SuccOrder α
h : DiscreteTopology α
⊢ inst✝³ = generateFrom {s | ∃ a, s = Ioi a ∨ s = Iio a}

Tactic:
rw [h.eq_bot, LinearOrder.bot_topologicalSpace_eq_generateFrom]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Logic.lean
theorem congr_eqRec {β : α → Sort _} (f : (x : α) → β x → γ) (h : x = x') (y : β x) :
  f x' (Eq.rec y h) = f x y

Proof state:
case refl
α : Sort u_1
γ : Sort u_2
x : α
β : α → Sort u_3
f : (x : α) → β x → γ
y : β x
⊢ f x (⋯ ▸ y) = f x y

Tactic:
rfl

Result:
no goals

Proof state:
α : Sort u_1
γ : Sort u_2
x x' : α
β : α → Sort u_3
f : (x : α) → β x → γ
h : x = x'
y : β x
⊢ f x' (h ▸ y) = f x y

Tactic:
cases h

Result:
case refl
α : Sort u_1
γ : Sort u_2
x : α
β : α → Sort u_3
f : (x : α) → β x → γ
y : β x
⊢ f x (⋯ ▸ y) = f x y
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem aleph0_le_mul_iff' {a b : Cardinal.{u}} : ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0

Proof state:
a b : Cardinal.{u}
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0

Tactic:
simp only [aleph0_le_mul_iff, and_or_left, and_iff_right_of_imp this, @and_left_comm (a ≠ 0)]

Result:
a b : Cardinal.{u}
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0
⊢ b ≠ 0 ∧ ℵ₀ ≤ a ∨ a ≠ 0 ∧ ℵ₀ ≤ b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0

Proof state:
a b : Cardinal.{u}
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0

Tactic:
have : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0 := fun a => ne_bot_of_le_ne_bot aleph0_ne_zero a

Result:
a b : Cardinal.{u}
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0

Proof state:
a b : Cardinal.{u}
this : ∀ {a : Cardinal.{u}}, ℵ₀ ≤ a → a ≠ 0
⊢ b ≠ 0 ∧ ℵ₀ ≤ a ∨ a ≠ 0 ∧ ℵ₀ ≤ b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0

Tactic:
simp only [and_comm, or_comm]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Order/Ring.lean
@[simp, norm_cast] lemma neg_cast_eq_cast : (-m : R) = n ↔ m = 0 ∧ n = 0

Proof state:
R : Type u_1
inst✝ : LinearOrderedRing R
m n : ℕ
⊢ -↑m = ↑n ↔ m = 0 ∧ n = 0

Tactic:
simp [neg_eq_iff_add_eq_zero, ← cast_add]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Basic.lean
theorem ext_nat'' [MonoidWithZeroHomClass F ℕ A] (f g : F) (h_pos : ∀ {n : ℕ}, 0 < n → f n = g n) :
    f = g

Proof state:
case h
A : Type u_3
F : Type u_4
inst✝² : MulZeroOneClass A
inst✝¹ : FunLike F ℕ A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → f n = g n
⊢ ∀ (x : ℕ), f x = g x

Tactic:
rintro (_ | n)

Result:
case h.zero
A : Type u_3
F : Type u_4
inst✝² : MulZeroOneClass A
inst✝¹ : FunLike F ℕ A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → f n = g n
⊢ f 0 = g 0

case h.succ
A : Type u_3
F : Type u_4
inst✝² : MulZeroOneClass A
inst✝¹ : FunLike F ℕ A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → f n = g n
n : ℕ
⊢ f (n + 1) = g (n + 1)

Proof state:
case h.succ
A : Type u_3
F : Type u_4
inst✝² : MulZeroOneClass A
inst✝¹ : FunLike F ℕ A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → f n = g n
n : ℕ
⊢ f (n + 1) = g (n + 1)

Tactic:
exact h_pos n.succ_pos

Result:
no goals

Proof state:
case h.zero
A : Type u_3
F : Type u_4
inst✝² : MulZeroOneClass A
inst✝¹ : FunLike F ℕ A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → f n = g n
⊢ f 0 = g 0

Tactic:
simp [map_zero f, map_zero g]

Result:
no goals

Proof state:
A : Type u_3
F : Type u_4
inst✝² : MulZeroOneClass A
inst✝¹ : FunLike F ℕ A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → f n = g n
⊢ f = g

Tactic:
apply DFunLike.ext

Result:
case h
A : Type u_3
F : Type u_4
inst✝² : MulZeroOneClass A
inst✝¹ : FunLike F ℕ A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → f n = g n
⊢ ∀ (x : ℕ), f x = g x
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc]
lemma π_homologyMap_ι [S₁.HasHomology] [S₂.HasHomology] (φ : S₁ ⟶ S₂) :
    S₁.homologyπ ≫ homologyMap φ ≫ S₂.homologyι = S₁.iCycles ≫ φ.τ₂ ≫ S₂.pOpcycles

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₂
⊢ S₁.homologyπ ≫ homologyMap φ ≫ S₂.homologyι = S₁.iCycles ≫ φ.τ₂ ≫ S₂.pOpcycles

Tactic:
simp only [homologyι_naturality, homology_π_ι_assoc, p_opcyclesMap]

Result:
no goals
-- Mathlib/Data/List/AList.lean
theorem extract_eq_lookup_erase (a : α) (s : AList β) : extract a s = (lookup a s, erase a s)

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ dlookup a s.entries = lookup a s ∧ { entries := kerase a s.entries, nodupKeys := ⋯ } = erase a s

Tactic:
constructor <;> rfl

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ extract a s = (lookup a s, erase a s)

Tactic:
simp [extract]

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
s : AList β
⊢ dlookup a s.entries = lookup a s ∧ { entries := kerase a s.entries, nodupKeys := ⋯ } = erase a s
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueD_insertEntry_self {β : Type v} [BEq α] [EquivBEq α] {l : List ((_ : α) × β)}
    {k : α} {fallback v : β} : getValueD k (insertEntry k v l) fallback = v

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
k : α
fallback v : β
⊢ getValueD k (insertEntry k v l) fallback = v

Tactic:
simp [getValueD_insertEntry, BEq.refl]

Result:
no goals
-- Mathlib/Algebra/Lie/Basic.lean
theorem lie_sub : ⁅x, m - n⁆ = ⁅x, m⁆ - ⁅x, n⁆

Proof state:
L : Type v
M : Type w
inst✝² : LieRing L
inst✝¹ : AddCommGroup M
inst✝ : LieRingModule L M
x : L
m n : M
⊢ ⁅x, m - n⁆ = ⁅x, m⁆ - ⁅x, n⁆

Tactic:
simp [sub_eq_add_neg]

Result:
no goals