harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/SmallObject/WellOrderInductionData.lean
lemma val_injective {j : J} {e e' : d.Extension val₀ j} (h : e.val = e'.val) : e = e'

Proof state:
case mk
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
e' : d.Extension val₀ j
val✝ : F.obj (op j)
map_zero✝ : F.map (homOfLE ⋯).op val✝ = val₀
map_succ✝ : ∀ (i : J) (hi : i < j), F.map (homOfLE ⋯).op val✝ = d.succ i ⋯ (F.map (homOfLE ⋯).op val✝)
map_limit✝ :
  ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
    F.map (homOfLE hij).op val✝ =
      d.lift i hi
        ⟨fun x =>
          match x with
          | op ⟨k, hk⟩ => F.map (homOfLE ⋯).op val✝,
          ⋯⟩
h : { val := val✝, map_zero := map_zero✝, map_succ := map_succ✝, map_limit := map_limit✝ }.val = e'.val
⊢ { val := val✝, map_zero := map_zero✝, map_succ := map_succ✝, map_limit := map_limit✝ } = e'

Tactic:
cases e'

Result:
case mk.mk
J : Type u
inst✝² : LinearOrder J
inst✝¹ : SuccOrder J
F : Jᵒᵖ ⥤ Type v
d : F.WellOrderInductionData
inst✝ : OrderBot J
val₀ : F.obj (op ⊥)
j : J
val✝¹ : F.obj (op j)
map_zero✝¹ : F.map (homOfLE ⋯).op val✝¹ = val₀
map_succ✝¹ : ∀ (i : J) (hi : i < j), F.map (homOfLE ⋯).op val✝¹ = d.succ i ⋯ (F.map (homOfLE ⋯).op val✝¹)
map_limit✝¹ :
  ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
    F.map (homOfLE hij).op val✝¹ =
      d.lift i hi
        ⟨fun x =>
          match x with
          | op ⟨k, hk⟩ => F.map (homOfLE ⋯).op val✝¹,
          ⋯⟩
val✝ : F.obj (op j)
map_zero✝ : F.map (homOfLE ⋯).op val✝ = val₀
map_succ✝ : ∀ (i : J) (hi : i < j), F.map (homOfLE ⋯).op val✝ = d.succ i ⋯ (F.map (homOfLE ⋯).op val✝)
map_limit✝ :
  ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
    F.map (homOfLE hij).op val✝ =
      d.lift i hi
        ⟨fun x =>
          match x with
          | op ⟨k, hk⟩ => F.map (homOfLE ⋯).op val✝,
          ⋯⟩
h :
  { val := val✝¹, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ }.val =
    { val := val✝, map_zero := map_zero✝, map_succ := map_succ✝, map_limit := map_limit✝ }.val
⊢ { val := val✝¹, map_zero := map_zero✝¹, map_succ := map_succ✝¹, map_limit := map_limit✝¹ } =
    { val := val✝, map_zero := map_zero✝, map_succ := map_succ✝, map_limit := map_limit✝ }
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem mem_closedBall_self (h : 0 ≤ ε) : x ∈ closedBall x ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
h : 0 ≤ ε
⊢ x ∈ closedBall x ε

Tactic:
rwa [mem_closedBall, dist_self]

Result:
no goals
-- Mathlib/ModelTheory/Order.lean
theorem isFraisse_finite_linear_order :
    IsFraisse {M : CategoryTheory.Bundled.{0} Language.order.Structure |
      Finite M ∧ M ⊨ Language.order.linearOrderTheory}

Proof state:
this : Language.order.Structure ℚ := orderStructure ℚ
⊢ IsFraisse {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}

Tactic:
exact (isFraisseLimit_of_countable_nonempty_dlo ℚ).isFraisse

Result:
no goals

Proof state:
⊢ IsFraisse {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}

Tactic:
letI : Language.order.Structure ℚ := orderStructure _

Result:
this : Language.order.Structure ℚ := orderStructure ℚ
⊢ IsFraisse {M | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem lt_ciSup_iff [Nonempty ι] {f : ι → α} (hb : BddAbove (range f)) :
    a < iSup f ↔ ∃ i, a < f i

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrder α
a : α
inst✝ : Nonempty ι
f : ι → α
hb : BddAbove (range f)
⊢ a < iSup f ↔ ∃ i, a < f i

Tactic:
simpa only [mem_range, exists_exists_eq_and] using lt_csSup_iff hb (range_nonempty _)

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
lemma comapOn_isBase_iff_of_bijOn (h : BijOn f E N.E) :
    (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ B ⊆ E

Proof state:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : BijOn f E N.E
⊢ B ⊆ E → ((N.comapOn E f).IsBase B ↔ N.IsBase (f '' B))

Tactic:
suffices h' : B ⊆ E → InjOn f B from fun hB ↦
  by simp [hB, comapOn_isBase_iff_of_surjOn h.surjOn, h']

Result:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : BijOn f E N.E
⊢ B ⊆ E → InjOn f B

Proof state:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : BijOn f E N.E
h' : B ⊆ E → InjOn f B
hB : B ⊆ E
⊢ (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B)

Tactic:
simp [hB, comapOn_isBase_iff_of_surjOn h.surjOn, h']

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : BijOn f E N.E
⊢ (N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ B ⊆ E

Tactic:
rw [← and_iff_left_of_imp (IsBase.subset_ground (M := N.comapOn E f) (B := B)),
  comapOn_ground_eq, and_congr_left_iff]

Result:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : BijOn f E N.E
⊢ B ⊆ E → ((N.comapOn E f).IsBase B ↔ N.IsBase (f '' B))

Proof state:
α : Type u_1
β : Type u_2
f : α → β
N : Matroid β
E B : Set α
h : BijOn f E N.E
⊢ B ⊆ E → InjOn f B

Tactic:
exact fun hBE ↦ h.injOn.mono hBE

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLintegral_pos_iff {f : α → ℝ≥0∞} (hf : Measurable f) {s : Set α} :
    0 < ∫⁻ a in s, f a ∂μ ↔ 0 < μ (Function.support f ∩ s)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
⊢ 0 < ∫⁻ (a : α) in s, f a ∂μ ↔ 0 < μ (support f ∩ s)

Tactic:
rw [lintegral_pos_iff_support hf, Measure.restrict_apply (measurableSet_support hf)]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Limits/Basic.lean
theorem colimit_isOpen_iff (F : J ⥤ TopCat.{u}) [HasColimit F]
    (U : Set ((colimit F : _) : Type u)) :
    IsOpen U ↔ ∀ j, IsOpen (colimit.ι F j ⁻¹' U)

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ TopCat
inst✝ : HasColimit F
U : Set ↑(colimit F)
⊢ IsOpen U ↔ ∀ (j : J), IsOpen (⇑(ConcreteCategory.hom (colimit.ι F j)) ⁻¹' U)

Tactic:
apply isOpen_iff_of_isColimit _ (colimit.isColimit _)

Result:
no goals
-- Mathlib/RingTheory/Generators.lean
@[simp]
lemma Hom.comp_id [Algebra R S'] [IsScalarTower R R' S'] [IsScalarTower R S S'] (f : Hom P P') :
    f.comp (Hom.id P) = f

Proof state:
case val.h.a
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Generators R S
R' : Type u_2
S' : Type u_1
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Generators R' S'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
x✝ : P.vars
m✝ : P'.vars →₀ ℕ
⊢ coeff m✝ ((f.comp (Hom.id P)).val x✝) = coeff m✝ (f.val x✝)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Generators R S
R' : Type u_2
S' : Type u_1
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Generators R' S'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
⊢ f.comp (Hom.id P) = f

Tactic:
ext

Result:
case val.h.a
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Generators R S
R' : Type u_2
S' : Type u_1
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Generators R' S'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f : P.Hom P'
x✝ : P.vars
m✝ : P'.vars →₀ ℕ
⊢ coeff m✝ ((f.comp (Hom.id P)).val x✝) = coeff m✝ (f.val x✝)
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma eventually_deriv_one_sub_smoothingFn :
    deriv (fun x => 1 - ε x) =ᶠ[atTop] fun x => x⁻¹ / (log x ^ 2) := calc
  deriv (fun x => 1 - ε x) =ᶠ[atTop] -(deriv ε)

Proof state:
case h
x : ℝ
hx : 1 < x
⊢ (-deriv ε) x = x⁻¹ / log x ^ 2

Tactic:
simp [deriv_smoothingFn hx, neg_div]

Result:
no goals

Proof state:
case h
x : ℝ
hx : 1 < x
⊢ deriv (fun x => 1 - ε x) x = (-deriv ε) x

Tactic:
rw [deriv_sub] <;> aesop

Result:
no goals

Proof state:
⊢ (deriv fun x => 1 - ε x) =ᶠ[atTop] -deriv ε

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Result:
case h
x : ℝ
hx : 1 < x
⊢ deriv (fun x => 1 - ε x) x = (-deriv ε) x

Proof state:
⊢ -deriv ε =ᶠ[atTop] fun x => x⁻¹ / log x ^ 2

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Result:
case h
x : ℝ
hx : 1 < x
⊢ (-deriv ε) x = x⁻¹ / log x ^ 2
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem PosSemidef.dotProduct_mulVec_zero_iff
    {A : Matrix n n 𝕜} (hA : PosSemidef A) (x : n → 𝕜) :
    star x ⬝ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0

Proof state:
case mp.intro
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
x : n → 𝕜
B : Matrix n n 𝕜
hA : (Bᴴ * B).PosSemidef
⊢ star x ⬝ᵥ (Bᴴ * B) *ᵥ x = 0 → (Bᴴ * B) *ᵥ x = 0

Tactic:
rw [← Matrix.mulVec_mulVec, dotProduct_mulVec,
  vecMul_conjTranspose, star_star, dotProduct_star_self_eq_zero]

Result:
case mp.intro
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
x : n → 𝕜
B : Matrix n n 𝕜
hA : (Bᴴ * B).PosSemidef
⊢ B *ᵥ x = 0 → Bᴴ *ᵥ B *ᵥ x = 0

Proof state:
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
⊢ star x ⬝ᵥ A *ᵥ x = 0 ↔ A *ᵥ x = 0

Tactic:
constructor

Result:
case mp
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
⊢ star x ⬝ᵥ A *ᵥ x = 0 → A *ᵥ x = 0

case mpr
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
⊢ A *ᵥ x = 0 → star x ⬝ᵥ A *ᵥ x = 0

Proof state:
case mp.intro
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
x : n → 𝕜
B : Matrix n n 𝕜
hA : (Bᴴ * B).PosSemidef
h0 : B *ᵥ x = 0
⊢ Bᴴ *ᵥ B *ᵥ x = 0

Tactic:
rw [h0, mulVec_zero]

Result:
no goals

Proof state:
case mpr
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
h0 : A *ᵥ x = 0
⊢ star x ⬝ᵥ A *ᵥ x = 0

Tactic:
rw [h0, dotProduct_zero]

Result:
no goals

Proof state:
case mp
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
⊢ star x ⬝ᵥ A *ᵥ x = 0 → A *ᵥ x = 0

Tactic:
obtain ⟨B, rfl⟩ := posSemidef_iff_eq_transpose_mul_self.mp hA

Result:
case mp.intro
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
x : n → 𝕜
B : Matrix n n 𝕜
hA : (Bᴴ * B).PosSemidef
⊢ star x ⬝ᵥ (Bᴴ * B) *ᵥ x = 0 → (Bᴴ * B) *ᵥ x = 0

Proof state:
case mp.intro
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
x : n → 𝕜
B : Matrix n n 𝕜
hA : (Bᴴ * B).PosSemidef
⊢ B *ᵥ x = 0 → Bᴴ *ᵥ B *ᵥ x = 0

Tactic:
intro h0

Result:
case mp.intro
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
x : n → 𝕜
B : Matrix n n 𝕜
hA : (Bᴴ * B).PosSemidef
h0 : B *ᵥ x = 0
⊢ Bᴴ *ᵥ B *ᵥ x = 0

Proof state:
case mpr
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
⊢ A *ᵥ x = 0 → star x ⬝ᵥ A *ᵥ x = 0

Tactic:
intro h0

Result:
case mpr
n : Type u_2
𝕜 : Type u_4
inst✝¹ : Fintype n
inst✝ : RCLike 𝕜
A : Matrix n n 𝕜
hA : A.PosSemidef
x : n → 𝕜
h0 : A *ᵥ x = 0
⊢ star x ⬝ᵥ A *ᵥ x = 0
-- Mathlib/Data/Real/ConjExponents.lean
@[simp, norm_cast] lemma isConjExponent_coe : (p : ℝ).IsConjExponent q ↔ p.IsConjExponent q

Proof state:
p q : ℝ≥0
⊢ 1 < p → ((↑p)⁻¹ + (↑q)⁻¹ = 1 ↔ p⁻¹ + q⁻¹ = 1)

Tactic:
norm_cast

Result:
p q : ℝ≥0
⊢ 1 < p → (p⁻¹ + q⁻¹ = 1 ↔ p⁻¹ + q⁻¹ = 1)

Proof state:
p q : ℝ≥0
⊢ 1 < p → (p⁻¹ + q⁻¹ = 1 ↔ p⁻¹ + q⁻¹ = 1)

Tactic:
simp

Result:
no goals

Proof state:
p q : ℝ≥0
⊢ (↑p).IsConjExponent ↑q ↔ p.IsConjExponent q

Tactic:
simp [Real.isConjExponent_iff, isConjExponent_iff]

Result:
p q : ℝ≥0
⊢ 1 < p → ((↑p)⁻¹ + (↑q)⁻¹ = 1 ↔ p⁻¹ + q⁻¹ = 1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseIdx_append_of_lt_size {l : Array α} {k : Nat} (hk : k < l.size) (l' : Array α) (h) :
    eraseIdx (l ++ l') k = eraseIdx l k ++ l'

Proof state:
case mk
α : Type u_1
k : Nat
l' : Array α
l : List α
hk : k < { toList := l }.size
h : k < ({ toList := l } ++ l').size
⊢ ({ toList := l } ++ l').eraseIdx k h = { toList := l }.eraseIdx k hk ++ l'

Tactic:
rcases l' with ⟨l'⟩

Result:
case mk.mk
α : Type u_1
k : Nat
l : List α
hk : k < { toList := l }.size
l' : List α
h : k < ({ toList := l } ++ { toList := l' }).size
⊢ ({ toList := l } ++ { toList := l' }).eraseIdx k h = { toList := l }.eraseIdx k hk ++ { toList := l' }

Proof state:
case mk.mk
α : Type u_1
k : Nat
l : List α
hk : k < { toList := l }.size
l' : List α
h : k < ({ toList := l } ++ { toList := l' }).size
⊢ ({ toList := l } ++ { toList := l' }).eraseIdx k h = { toList := l }.eraseIdx k hk ++ { toList := l' }

Tactic:
simp at hk

Result:
case mk.mk
α : Type u_1
k : Nat
l : List α
hk✝ : k < { toList := l }.size
l' : List α
h : k < ({ toList := l } ++ { toList := l' }).size
hk : k < l.length
⊢ ({ toList := l } ++ { toList := l' }).eraseIdx k h = { toList := l }.eraseIdx k hk✝ ++ { toList := l' }

Proof state:
α : Type u_1
l : Array α
k : Nat
hk : k < l.size
l' : Array α
h : k < (l ++ l').size
⊢ (l ++ l').eraseIdx k h = l.eraseIdx k hk ++ l'

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
k : Nat
l' : Array α
l : List α
hk : k < { toList := l }.size
h : k < ({ toList := l } ++ l').size
⊢ ({ toList := l } ++ l').eraseIdx k h = { toList := l }.eraseIdx k hk ++ l'

Proof state:
case mk.mk
α : Type u_1
k : Nat
l : List α
hk✝ : k < { toList := l }.size
l' : List α
h : k < ({ toList := l } ++ { toList := l' }).size
hk : k < l.length
⊢ ({ toList := l } ++ { toList := l' }).eraseIdx k h = { toList := l }.eraseIdx k hk✝ ++ { toList := l' }

Tactic:
simp [List.eraseIdx_append_of_lt_length, *]

Result:
no goals
-- Mathlib/Algebra/Ring/Units.lean
theorem sub_divp (a b : α) (u : αˣ) : a - b /ₚ u = (a * u - b) /ₚ u

Proof state:
α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ a - b /ₚ u = (a * ↑u - b) /ₚ u

Tactic:
simp only [divp, sub_mul, Units.mul_inv_cancel_right]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_addXYZ (P Q : Fin 3 → A) : (W'.baseChange B).toProjective.addXYZ (f ∘ P) (f ∘ Q) =
    f ∘ (W'.baseChange A).toProjective.addXYZ P Q

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Projective R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
P Q : Fin 3 → A
⊢ (baseChange W' B).toProjective.addXYZ (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ (baseChange W' A).toProjective.addXYZ P Q

Tactic:
rw [← RingHom.coe_coe, ← map_addXYZ, map_baseChange]

Result:
no goals
-- Mathlib/Order/Cofinal.lean
theorem GaloisConnection.map_cofinal [Preorder β] {f : β → α} {g : α → β}
    (h : GaloisConnection f g) {s : Set α} (hs : IsCofinal s) : IsCofinal (g '' s)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
g : α → β
h : GaloisConnection f g
s : Set α
hs : IsCofinal s
a : β
b : α
hb : b ∈ s
hb' : f a ≤ b
⊢ ∃ y ∈ g '' s, a ≤ y

Tactic:
exact ⟨g b, Set.mem_image_of_mem _ hb, h.le_iff_le.1 hb'⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
g : α → β
h : GaloisConnection f g
s : Set α
hs : IsCofinal s
a : β
⊢ ∃ y ∈ g '' s, a ≤ y

Tactic:
obtain ⟨b, hb, hb'⟩ := hs (f a)

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
g : α → β
h : GaloisConnection f g
s : Set α
hs : IsCofinal s
a : β
b : α
hb : b ∈ s
hb' : f a ≤ b
⊢ ∃ y ∈ g '' s, a ≤ y

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
g : α → β
h : GaloisConnection f g
s : Set α
hs : IsCofinal s
⊢ IsCofinal (g '' s)

Tactic:
intro a

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
g : α → β
h : GaloisConnection f g
s : Set α
hs : IsCofinal s
a : β
⊢ ∃ y ∈ g '' s, a ≤ y
-- Mathlib/Data/Multiset/AddSub.lean
protected lemma add_sub_cancel_right : s + t - t = s

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ count a (s + t - t) = count a s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s + t - t = s

Tactic:
ext a

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ count a (s + t - t) = count a s
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma eval_polynomialY (P : Fin 3 → R) :
    eval P W'.polynomialY = 2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P) W'.polynomialY = 2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3

Tactic:
rw [polynomialY_eq]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P) (C 2 * X y + C W'.a₁ * X x * X z + C W'.a₃ * X z ^ 3) = 2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ (eval P) (C 2 * X y + C W'.a₁ * X x * X z + C W'.a₃ * X z ^ 3) = 2 * P y + W'.a₁ * P x * P z + W'.a₃ * P z ^ 3

Tactic:
eval_simp

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem iterate_mod_apply (h : IsPeriodicPt f n x) (m : ℕ) : f^[m % n] x = f^[m] x

Proof state:
α : Type u_1
f : α → α
x : α
n : ℕ
h : IsPeriodicPt f n x
m : ℕ
⊢ f^[m % n] x = f^[m] x

Tactic:
conv_rhs => rw [← Nat.mod_add_div m n, iterate_add_apply, (h.mul_const _).eq]

Result:
no goals
-- Mathlib/Order/Closure.lean
theorem closureOperator_gi_self [PartialOrder α] (c : ClosureOperator α) :
    c.gi.gc.closureOperator = c

Proof state:
case a
α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
x : α
⊢ ⋯.closureOperator x = c x

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
⊢ ⋯.closureOperator = c

Tactic:
ext x

Result:
case a
α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
x : α
⊢ ⋯.closureOperator x = c x
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem tendsto_iff_forall_testAgainstNN_tendsto {γ : Type*} {F : Filter γ}
    {μs : γ → FiniteMeasure Ω} {μ : FiniteMeasure Ω} :
    Tendsto μs F (𝓝 μ) ↔
      ∀ f : Ω →ᵇ ℝ≥0, Tendsto (fun i ↦ (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Tactic:
rw [FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto]

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ (∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).toWeakDualBCNN f) F (𝓝 (μ.toWeakDualBCNN f))) ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_3
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ (∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).toWeakDualBCNN f) F (𝓝 (μ.toWeakDualBCNN f))) ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem nhdsWithin_insert_of_ne [T1Space X] {x y : X} {s : Set X} (hxy : x ≠ y) :
    𝓝[insert y s] x = 𝓝[s] x

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s : Set X
hxy : x ≠ y
⊢ 𝓝[insert y s] x = 𝓝[s] x

Tactic:
refine le_antisymm (Filter.le_def.2 fun t ht => ?_) (nhdsWithin_mono x <| subset_insert y s)

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
⊢ t ∈ 𝓝[insert y s] x

Proof state:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
o : Set X
ho : IsOpen o
hxo : x ∈ o
host : o ∩ s ⊆ t
⊢ t ∈ 𝓝[insert y s] x

Tactic:
refine mem_nhdsWithin.mpr ⟨o \ {y}, ho.sdiff isClosed_singleton, ⟨hxo, hxy⟩, ?_⟩

Result:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
o : Set X
ho : IsOpen o
hxo : x ∈ o
host : o ∩ s ⊆ t
⊢ o \ {y} ∩ insert y s ⊆ t

Proof state:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
o : Set X
ho : IsOpen o
hxo : x ∈ o
host : o ∩ s ⊆ t
⊢ o \ {y} ∩ insert y s ⊆ t

Tactic:
rw [inter_insert_of_not_mem <| not_mem_diff_of_mem (mem_singleton y)]

Result:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
o : Set X
ho : IsOpen o
hxo : x ∈ o
host : o ∩ s ⊆ t
⊢ o \ {y} ∩ s ⊆ t

Proof state:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
o : Set X
ho : IsOpen o
hxo : x ∈ o
host : o ∩ s ⊆ t
⊢ o \ {y} ∩ s ⊆ t

Tactic:
exact (inter_subset_inter diff_subset Subset.rfl).trans host

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
⊢ t ∈ 𝓝[insert y s] x

Tactic:
obtain ⟨o, ho, hxo, host⟩ := mem_nhdsWithin.mp ht

Result:
case intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x y : X
s : Set X
hxy : x ≠ y
t : Set X
ht : t ∈ 𝓝[s] x
o : Set X
ho : IsOpen o
hxo : x ∈ o
host : o ∩ s ⊆ t
⊢ t ∈ 𝓝[insert y s] x
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem sSup_simples_eq_top : sSup { m : Submodule R M | IsSimpleModule R m } = ⊤

Proof state:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ sSup {m | IsSimpleModule R ↥m} = ⊤

Tactic:
simpa only [isSimpleModule_iff_isAtom] using sSup_atoms_eq_top

Result:
no goals