harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.compl_mem_sets (hs : IsCompact s) {f : Filter X} (hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f) :
    sᶜ ∈ f

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : sᶜ ∉ f
⊢ ∃ x ∈ s, sᶜ ∉ 𝓝 x ⊓ f

Tactic:
simp only [not_mem_iff_inf_principal_compl, compl_compl, inf_assoc] at hf ⊢

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : (f ⊓ 𝓟 s).NeBot
⊢ ∃ x ∈ s, (𝓝 x ⊓ (f ⊓ 𝓟 s)).NeBot

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : (f ⊓ 𝓟 s).NeBot
⊢ ∃ x ∈ s, (𝓝 x ⊓ (f ⊓ 𝓟 s)).NeBot

Tactic:
exact @hs _ hf inf_le_right

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f
⊢ sᶜ ∈ f

Tactic:
contrapose! hf

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : sᶜ ∉ f
⊢ ∃ x ∈ s, sᶜ ∉ 𝓝 x ⊓ f
-- Mathlib/SetTheory/Cardinal/Basic.lean
lemma succ_natCast (n : ℕ) : Order.succ (n : Cardinal) = n + 1

Proof state:
n : ℕ
⊢ succ ↑n = ↑n + 1

Tactic:
rw [← Cardinal.nat_succ]

Result:
n : ℕ
⊢ ↑n.succ = ↑n + 1

Proof state:
n : ℕ
⊢ ↑n.succ = ↑n + 1

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem _root_.HasFDerivAt.linear_multilinear_comp [DecidableEq ι] {a : H → E} {a' : H →L[𝕜] E}
    {b : ∀ i, H → G i} {b' : ∀ i, H →L[𝕜] G i} {x : H}
    (ha : HasFDerivAt a a' x) (hb : ∀ i, HasFDerivAt (b i) (b' i) x)
    (f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F) :
    HasFDerivAt (fun y ↦ f (a y) (fun i ↦ b i y))
      ((f.flipMultilinear (fun i ↦ b i x)) ∘L a' +
        ∑ i, ((f (a x)).toContinuousLinearMap (fun j ↦ b j x) i) ∘L (b' i)) x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type v
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
ι : Type u_2
G : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (G i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (G i)
inst✝³ : Fintype ι
H : Type u_4
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : DecidableEq ι
a : H → E
a' : H →L[𝕜] E
b : (i : ι) → H → G i
b' : (i : ι) → H →L[𝕜] G i
x : H
f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F
ha : HasFDerivWithinAt a a' univ x
hb : ∀ (i : ι), HasFDerivWithinAt (b i) (b' i) univ x
⊢ HasFDerivWithinAt (fun y => (f (a y)) fun i => b i y)
    ((f.flipMultilinear fun i => b i x).comp a' +
      ∑ i : ι, ((f (a x)).toContinuousLinearMap (fun j => b j x) i).comp (b' i))
    univ x

Tactic:
exact HasFDerivWithinAt.linear_multilinear_comp ha hb f

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type v
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
ι : Type u_2
G : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (G i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (G i)
inst✝³ : Fintype ι
H : Type u_4
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : DecidableEq ι
a : H → E
a' : H →L[𝕜] E
b : (i : ι) → H → G i
b' : (i : ι) → H →L[𝕜] G i
x : H
ha : HasFDerivAt a a' x
hb : ∀ (i : ι), HasFDerivAt (b i) (b' i) x
f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F
⊢ HasFDerivAt (fun y => (f (a y)) fun i => b i y)
    ((f.flipMultilinear fun i => b i x).comp a' +
      ∑ i : ι, ((f (a x)).toContinuousLinearMap (fun j => b j x) i).comp (b' i))
    x

Tactic:
simp_rw [← hasFDerivWithinAt_univ] at ha hb ⊢

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type v
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
ι : Type u_2
G : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (G i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (G i)
inst✝³ : Fintype ι
H : Type u_4
inst✝² : NormedAddCommGroup H
inst✝¹ : NormedSpace 𝕜 H
inst✝ : DecidableEq ι
a : H → E
a' : H →L[𝕜] E
b : (i : ι) → H → G i
b' : (i : ι) → H →L[𝕜] G i
x : H
f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F
ha : HasFDerivWithinAt a a' univ x
hb : ∀ (i : ι), HasFDerivWithinAt (b i) (b' i) univ x
⊢ HasFDerivWithinAt (fun y => (f (a y)) fun i => b i y)
    ((f.flipMultilinear fun i => b i x).comp a' +
      ∑ i : ι, ((f (a x)).toContinuousLinearMap (fun j => b j x) i).comp (b' i))
    univ x
-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem toAffineIsometry_linearIsometry : f.toAffineIsometry.linearIsometry = f

Proof state:
case h
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : NormedSpace 𝕜 V₂
f : V →ₗᵢ[𝕜] V₂
x✝ : V
⊢ f.toAffineIsometry.linearIsometry x✝ = f x✝

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : NormedSpace 𝕜 V₂
f : V →ₗᵢ[𝕜] V₂
⊢ f.toAffineIsometry.linearIsometry = f

Tactic:
ext

Result:
case h
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
inst✝⁴ : NormedField 𝕜
inst✝³ : SeminormedAddCommGroup V
inst✝² : NormedSpace 𝕜 V
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : NormedSpace 𝕜 V₂
f : V →ₗᵢ[𝕜] V₂
x✝ : V
⊢ f.toAffineIsometry.linearIsometry x✝ = f x✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue!_eraseKey {β : Type v} [BEq α] [PartialEquivBEq α] [Inhabited β]
    {l : List ((_ : α) × β)} {k a : α} (hl : DistinctKeys l) :
    getValue! a (eraseKey k l) = if k == a then default else getValue! a l

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : PartialEquivBEq α
inst✝ : Inhabited β
l : List ((_ : α) × β)
k a : α
hl : DistinctKeys l
⊢ getValue! a (eraseKey k l) = if (k == a) = true then default else getValue! a l

Tactic:
simp [getValue!_eq_getValue?, getValue?_eraseKey hl, apply_ite Option.get!]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_pi_neBot {I : Set ι} {s : ∀ i, Set (π i)} {x : ∀ i, π i} :
    (𝓝[pi I s] x).NeBot ↔ ∀ i ∈ I, (𝓝[s i] x i).NeBot

Proof state:
ι : Type u_5
π : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (π i)
I : Set ι
s : (i : ι) → Set (π i)
x : (i : ι) → π i
⊢ (𝓝[I.pi s] x).NeBot ↔ ∀ i ∈ I, (𝓝[s i] x i).NeBot

Tactic:
simp [neBot_iff, nhdsWithin_pi_eq_bot]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeff_sub (p q : R[X]) (n : ℕ) : coeff (p - q) n = coeff p n - coeff q n

Proof state:
case ofFinsupp.ofFinsupp
R : Type u
inst✝ : Ring R
n : ℕ
toFinsupp✝¹ toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝¹ } - { toFinsupp := toFinsupp✝ }).coeff n =
    { toFinsupp := toFinsupp✝¹ }.coeff n - { toFinsupp := toFinsupp✝ }.coeff n

Tactic:
rw [← ofFinsupp_sub, coeff, coeff, coeff, Finsupp.sub_apply]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
n : ℕ
⊢ (p - q).coeff n = p.coeff n - q.coeff n

Tactic:
rcases p with ⟨⟩

Result:
case ofFinsupp
R : Type u
inst✝ : Ring R
q : R[X]
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ } - q).coeff n = { toFinsupp := toFinsupp✝ }.coeff n - q.coeff n

Proof state:
case ofFinsupp
R : Type u
inst✝ : Ring R
q : R[X]
n : ℕ
toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝ } - q).coeff n = { toFinsupp := toFinsupp✝ }.coeff n - q.coeff n

Tactic:
rcases q with ⟨⟩

Result:
case ofFinsupp.ofFinsupp
R : Type u
inst✝ : Ring R
n : ℕ
toFinsupp✝¹ toFinsupp✝ : R[ℕ]
⊢ ({ toFinsupp := toFinsupp✝¹ } - { toFinsupp := toFinsupp✝ }).coeff n =
    { toFinsupp := toFinsupp✝¹ }.coeff n - { toFinsupp := toFinsupp✝ }.coeff n
-- Mathlib/Analysis/Calculus/FDeriv/Basic.lean
theorem fderivWithin_zero_of_isolated (h : 𝓝[s \ {x}] x = ⊥) : fderivWithin 𝕜 f s x = 0

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
h : 𝓝[s \ {x}] x = ⊥
⊢ fderivWithin 𝕜 f s x = 0

Tactic:
rw [fderivWithin, if_pos (.of_nhdsWithin_eq_bot h)]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem adjoin_attach_biUnion [DecidableEq A] {α : Type*} {s : Finset α} (f : s → Finset A) :
    adjoin R (s.attach.biUnion f : Set A) = ⨆ x, adjoin R (f x)

Proof state:
R : Type uR
A : Type uA
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : DecidableEq A
α : Type u_1
s : Finset α
f : { x // x ∈ s } → Finset A
⊢ adjoin R ↑(s.attach.biUnion f) = ⨆ x, adjoin R ↑(f x)

Tactic:
simp [adjoin_iUnion]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
theorem PInfty_add_QInfty : (PInfty : K[X] ⟶ _) + QInfty = 𝟙 _

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty + (𝟙 K[X] - PInfty) = 𝟙 K[X]

Tactic:
simp only [add_sub_cancel]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty + QInfty = 𝟙 K[X]

Tactic:
dsimp only [QInfty]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty + (𝟙 K[X] - PInfty) = 𝟙 K[X]
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem coordinate_eval_6 :
    (coordinate 6).eval (.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: t)) = a6

Proof state:
a0 a1 a2 a3 a4 a5 a6 : Int
t : List Int
⊢ (coordinate 6).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: t)) = a6

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem norm_div_tan_oangle_sub_left_of_oangle_eq_pi_div_two {x y : V}
    (h : o.oangle x y = ↑(π / 2)) : ‖y‖ / Real.Angle.tan (o.oangle (x - y) x) = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ ‖y‖ / (o.oangle (x - y) x).tan = ‖x‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ‖y‖ / ((-o).oangle x (x - y)).tan = ‖x‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ ‖y‖ / ((-o).oangle x (x - y)).tan = ‖x‖

Tactic:
exact (-o).norm_div_tan_oangle_sub_right_of_oangle_eq_pi_div_two h

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_indicator_const₀ {s : Set α} (hs : NullMeasurableSet s μ) (c : ℝ≥0∞) :
    ∫⁻ a, s.indicator (fun _ => c) a ∂μ = c * μ s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
c : ℝ≥0∞
⊢ ∫⁻ (a : α), s.indicator (fun x => c) a ∂μ = c * μ s

Tactic:
rw [lintegral_indicator₀ hs, setLIntegral_const]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean
theorem IsInvertedBy.iff_of_iso (W : MorphismProperty C) {F₁ F₂ : C ⥤ D} (e : F₁ ≅ F₂) :
    W.IsInvertedBy F₁ ↔ W.IsInvertedBy F₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
⊢ W.IsInvertedBy F₁ ↔ W.IsInvertedBy F₂

Tactic:
dsimp [IsInvertedBy]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
⊢ (∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsIso (F₁.map f)) ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsIso (F₂.map f)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
⊢ (∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsIso (F₁.map f)) ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsIso (F₂.map f)

Tactic:
simp only [NatIso.isIso_map_iff e]

Result:
no goals
-- Mathlib/LinearAlgebra/FreeModule/PID.lean
theorem dvd_generator_iff {I : Ideal R} [I.IsPrincipal] {x : R} (hx : x ∈ I) :
    x ∣ generator I ↔ I = Ideal.span {x}

Proof state:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
I : Ideal R
inst✝ : IsPrincipal I
x : R
hx : x ∈ I
⊢ x ∣ generator I ↔ I = Ideal.span {x}

Tactic:
conv_rhs => rw [← span_singleton_generator I]

Result:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
I : Ideal R
inst✝ : IsPrincipal I
x : R
hx : x ∈ I
⊢ x ∣ generator I ↔ span R {generator I} = Ideal.span {x}

Proof state:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
I : Ideal R
inst✝ : IsPrincipal I
x : R
hx : x ∈ I
⊢ x ∣ generator I ↔ x ∈ I ∧ x ∣ generator I

Tactic:
exact ⟨fun h ↦ ⟨hx, h⟩, fun h ↦ h.2⟩

Result:
no goals

Proof state:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
I : Ideal R
inst✝ : IsPrincipal I
x : R
hx : x ∈ I
⊢ x ∣ generator I ↔ span R {generator I} = Ideal.span {x}

Tactic:
rw [Ideal.submodule_span_eq, Ideal.span_singleton_eq_span_singleton, ← dvd_dvd_iff_associated,
  ← mem_iff_generator_dvd]

Result:
R : Type u_2
inst✝² : CommRing R
inst✝¹ : IsDomain R
I : Ideal R
inst✝ : IsPrincipal I
x : R
hx : x ∈ I
⊢ x ∣ generator I ↔ x ∈ I ∧ x ∣ generator I
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem forIn'_yield_eq_foldlM [Monad m] [LawfulMonad m]
    (l : Vector α n) (f : (a : α) → a ∈ l → β → m γ) (g : (a : α) → a ∈ l → β → γ → β) (init : β) :
    forIn' l init (fun a m b => (fun c => .yield (g a m b c)) <$> f a m b) =
      l.attach.foldlM (fun b ⟨a, m⟩ => g a m b <$> f a m b) init

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : Vector α n
f : (a : α) → a ∈ l → β → m γ
g : (a : α) → a ∈ l → β → γ → β
init : β
⊢ (forIn' l init fun a m_1 b => (fun c => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) =
    foldlM
      (fun b x =>
        match x with
        | ⟨a, m_1⟩ => g a m_1 b <$> f a m_1 b)
      init l.attach

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
inst✝ : LawfulMonad m
init : β
l : Array α
f : (a : α) → a ∈ { toArray := l, size_toArray := ⋯ } → β → m γ
g : (a : α) → a ∈ { toArray := l, size_toArray := ⋯ } → β → γ → β
⊢ (forIn' { toArray := l, size_toArray := ⋯ } init fun a m_1 b =>
      (fun c => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) =
    foldlM
      (fun b x =>
        match x with
        | ⟨a, m_1⟩ => g a m_1 b <$> f a m_1 b)
      init { toArray := l, size_toArray := ⋯ }.attach

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β γ : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
init : β
l : Array α
f : (a : α) → a ∈ { toArray := l, size_toArray := ⋯ } → β → m γ
g : (a : α) → a ∈ { toArray := l, size_toArray := ⋯ } → β → γ → β
⊢ (forIn' { toArray := l, size_toArray := ⋯ } init fun a m_1 b =>
      (fun c => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) =
    foldlM
      (fun b x =>
        match x with
        | ⟨a, m_1⟩ => g a m_1 b <$> f a m_1 b)
      init { toArray := l, size_toArray := ⋯ }.attach

Tactic:
simp

Result:
no goals
-- Mathlib/Logic/Equiv/Option.lean
lemma optionSubtypeNe_symm_self (a : α) : (optionSubtypeNe a).symm a = none

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ (optionSubtypeNe a).symm a = none

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/UniqueProds/Basic.lean
theorem toIsLeftCancelMul [UniqueProds G] : IsLeftCancelMul G where
  mul_left_cancel a b1 b2 he

Proof state:
case intro.intro.intro.intro.refl.inl
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b2 b : G
ha : a ∈ {a}
he : a * b = a * b2
this : b ∈ {b, b2}
hu : UniqueMul {a} {b, b2} a b
⊢ b = b2

Tactic:
exact (hu ha (mem_insert_of_mem <| mem_singleton_self b2) he.symm).2.symm

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b2 : G
he : a * b1 = a * b2
⊢ b1 = b2

Tactic:
have := mem_insert_self b1 {b2}

Result:
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b2 : G
he : a * b1 = a * b2
this : b1 ∈ {b1, b2}
⊢ b1 = b2

Proof state:
case intro.intro.intro.intro
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a✝ b1 b2 : G
he : a✝ * b1 = a✝ * b2
this : b1 ∈ {b1, b2}
a : G
ha : a ∈ {a✝}
b : G
hb : b ∈ {b1, b2}
hu : UniqueMul {a✝} {b1, b2} a b
⊢ b1 = b2

Tactic:
cases mem_singleton.mp ha

Result:
case intro.intro.intro.intro.refl
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b2 : G
he : a * b1 = a * b2
this : b1 ∈ {b1, b2}
b : G
hb : b ∈ {b1, b2}
ha : a ∈ {a}
hu : UniqueMul {a} {b1, b2} a b
⊢ b1 = b2

Proof state:
case intro.intro.intro.intro.refl.inr
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b : G
ha : a ∈ {a}
he : a * b1 = a * b
this : b1 ∈ {b1, b}
hu : UniqueMul {a} {b1, b} a b
⊢ b1 = b

Tactic:
exact (hu ha this he).2

Result:
no goals

Proof state:
case intro.intro.intro.intro.refl
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b2 : G
he : a * b1 = a * b2
this : b1 ∈ {b1, b2}
b : G
ha : a ∈ {a}
hu : UniqueMul {a} {b1, b2} a b
hb : b = b1 ∨ b = b2
⊢ b1 = b2

Tactic:
obtain rfl | rfl := hb

Result:
case intro.intro.intro.intro.refl.inl
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b2 b : G
ha : a ∈ {a}
he : a * b = a * b2
this : b ∈ {b, b2}
hu : UniqueMul {a} {b, b2} a b
⊢ b = b2

case intro.intro.intro.intro.refl.inr
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b : G
ha : a ∈ {a}
he : a * b1 = a * b
this : b1 ∈ {b1, b}
hu : UniqueMul {a} {b1, b} a b
⊢ b1 = b

Proof state:
case intro.intro.intro.intro.refl
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b2 : G
he : a * b1 = a * b2
this : b1 ∈ {b1, b2}
b : G
hb : b ∈ {b1, b2}
ha : a ∈ {a}
hu : UniqueMul {a} {b1, b2} a b
⊢ b1 = b2

Tactic:
simp_rw [mem_insert, mem_singleton] at hb

Result:
case intro.intro.intro.intro.refl
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b2 : G
he : a * b1 = a * b2
this : b1 ∈ {b1, b2}
b : G
ha : a ∈ {a}
hu : UniqueMul {a} {b1, b2} a b
hb : b = b1 ∨ b = b2
⊢ b1 = b2

Proof state:
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b2 : G
he : a * b1 = a * b2
this : b1 ∈ {b1, b2}
⊢ b1 = b2

Tactic:
obtain ⟨a, ha, b, hb, hu⟩ := uniqueMul_of_nonempty ⟨a, mem_singleton_self a⟩ ⟨b1, this⟩

Result:
case intro.intro.intro.intro
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a✝ b1 b2 : G
he : a✝ * b1 = a✝ * b2
this : b1 ∈ {b1, b2}
a : G
ha : a ∈ {a✝}
b : G
hb : b ∈ {b1, b2}
hu : UniqueMul {a✝} {b1, b2} a b
⊢ b1 = b2
-- Mathlib/NumberTheory/Pell.lean
theorem y_pow_succ_pos {a : Solution₁ d} (hax : 0 < a.x) (hay : 0 < a.y) (n : ℕ) :
    0 < (a ^ n.succ).y

Proof state:
case succ
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
ih : 0 < (a ^ n.succ).y
⊢ 0 < (a * a ^ (n + 1)).y

Tactic:
exact y_mul_pos hax hay (x_pow_pos hax _) ih

Result:
no goals

Proof state:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ 0 < (a ^ n.succ).y

Tactic:
induction n with
| zero => simp only [pow_one, hay]
| succ n ih => rw [pow_succ']; exact y_mul_pos hax hay (x_pow_pos hax _) ih

Result:
no goals

Proof state:
case zero
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
⊢ 0 < (a ^ Nat.succ 0).y

Tactic:
simp only [pow_one, hay]

Result:
no goals

Proof state:
case succ
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
ih : 0 < (a ^ n.succ).y
⊢ 0 < (a ^ (n + 1).succ).y

Tactic:
rw [pow_succ']

Result:
case succ
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
ih : 0 < (a ^ n.succ).y
⊢ 0 < (a * a ^ (n + 1)).y
-- Mathlib/Topology/Bases.lean
lemma isSeparable_pi {ι : Type*} [Countable ι] {α : ι → Type*} {s : ∀ i, Set (α i)}
    [∀ i, TopologicalSpace (α i)] (h : ∀ i, IsSeparable (s i)) :
    IsSeparable {f : ∀ i, α i | ∀ i, f i ∈ s i}

Proof state:
ι : Type u_2
inst✝¹ : Countable ι
α : ι → Type u_3
s : (i : ι) → Set (α i)
inst✝ : (i : ι) → TopologicalSpace (α i)
h : ∀ (i : ι), IsSeparable (s i)
⊢ IsSeparable {f | ∀ (i : ι), f i ∈ s i}

Tactic:
simpa only [← mem_univ_pi] using IsSeparable.univ_pi h

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
theorem smul_opposite_image_mul_preimage' (g : G) (h : Gᵐᵒᵖ) (s : Set G) :
    (fun y => h • y) '' ((g * ·) ⁻¹' s) = (g * ·) ⁻¹' ((fun y => h • y) '' s)

Proof state:
G : Type u_2
inst✝ : Group G
g : G
h : Gᵐᵒᵖ
s : Set G
⊢ (fun y => h • y) '' ((fun x => g * x) ⁻¹' s) = (fun x => g * x) ⁻¹' ((fun y => h • y) '' s)

Tactic:
simp [preimage_preimage, mul_assoc]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_take_succ (L : List M) (i : ℕ) (p : i < L.length) :
    (L.take (i + 1)).prod = (L.take i).prod * L[i]

Proof state:
M : Type u_4
inst✝ : Monoid M
L : List M
i : ℕ
p : i < L.length
⊢ (take i L).prod * [L[i]].prod = (take i L).prod * L[i]

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_4
inst✝ : Monoid M
L : List M
i : ℕ
p : i < L.length
⊢ (take (i + 1) L).prod = (take i L).prod * L[i]

Tactic:
rw [← take_concat_get' _ _ p, prod_append]

Result:
M : Type u_4
inst✝ : Monoid M
L : List M
i : ℕ
p : i < L.length
⊢ (take i L).prod * [L[i]].prod = (take i L).prod * L[i]
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem neg_le_of_neg_le {a b : Int} (h : -a ≤ b) : -b ≤ a

Proof state:
a b : Int
h✝ : -a ≤ b
h : -b ≤ - -a
⊢ -b ≤ a

Tactic:
rwa [Int.neg_neg] at h

Result:
no goals

Proof state:
a b : Int
h : -a ≤ b
⊢ -b ≤ a

Tactic:
have h := Int.neg_le_neg h

Result:
a b : Int
h✝ : -a ≤ b
h : -b ≤ - -a
⊢ -b ≤ a
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma Hom.iInf_ker_openCover_map_comp (f : X ⟶ Y) [QuasiCompact f] (𝒰 : X.OpenCover) :
    ⨅ i, (𝒰.map i ≫ f).ker = f.ker

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
⊢ ⨅ i, ker (𝒰.map i ≫ f) ≤ ker f

Tactic:
refine iInf_le_iff.mpr fun I hI U ↦ ?_

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
I : Y.IdealSheafData
hI : ∀ (i : 𝒰.J), I ≤ ker (𝒰.map i ≫ f)
U : ↑Y.affineOpens
⊢ I.ideal U ≤ (ker f).ideal U

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
I : Y.IdealSheafData
hI : ∀ (i : 𝒰.J), I ≤ ker (𝒰.map i ≫ f)
U : ↑Y.affineOpens
⊢ ∀ (i : 𝒰.J), I.ideal U ≤ (ker (𝒰.map i ≫ f)).ideal U

Tactic:
exact fun i ↦ hI i U

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
I : Y.IdealSheafData
hI : ∀ (i : 𝒰.J), I ≤ ker (𝒰.map i ≫ f)
U : ↑Y.affineOpens
⊢ I.ideal U ≤ (ker f).ideal U

Tactic:
rw [← f.iInf_ker_openCover_map_comp_apply 𝒰, le_iInf_iff]

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
I : Y.IdealSheafData
hI : ∀ (i : 𝒰.J), I ≤ ker (𝒰.map i ≫ f)
U : ↑Y.affineOpens
⊢ ∀ (i : 𝒰.J), I.ideal U ≤ (ker (𝒰.map i ≫ f)).ideal U

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
⊢ ⨅ i, ker (𝒰.map i ≫ f) = ker f

Tactic:
refine le_antisymm ?_ (le_iInf fun i ↦ f.le_ker_comp (𝒰.map i))

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
⊢ ⨅ i, ker (𝒰.map i ≫ f) ≤ ker f