harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/NAry.lean
theorem mem_image2_iff (hf : Injective2 f) : f a b ∈ image2 f s t ↔ a ∈ s ∧ b ∈ t :=
  ⟨by
    rintro ⟨a', ha', b', hb', h⟩
    rcases hf h with ⟨rfl, rfl⟩
    exact ⟨ha', hb'⟩, fun ⟨ha, hb⟩ => mem_image2_of_mem ha hb⟩

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
hf : Injective2 f
a' : α
ha' : a' ∈ s
b' : β
hb' : b' ∈ t
h : f a' b' = f a b
⊢ a ∈ s ∧ b ∈ t

Tactic:
rcases hf h with ⟨rfl, rfl⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
hf : Injective2 f
a' : α
ha' : a' ∈ s
b' : β
hb' : b' ∈ t
h : f a' b' = f a' b'
⊢ a' ∈ s ∧ b' ∈ t

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
hf : Injective2 f
a' : α
ha' : a' ∈ s
b' : β
hb' : b' ∈ t
h : f a' b' = f a' b'
⊢ a' ∈ s ∧ b' ∈ t

Tactic:
exact ⟨ha', hb'⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
hf : Injective2 f
⊢ f a b ∈ image2 f s t → a ∈ s ∧ b ∈ t

Tactic:
rintro ⟨a', ha', b', hb', h⟩

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
t : Set β
a : α
b : β
hf : Injective2 f
a' : α
ha' : a' ∈ s
b' : β
hb' : b' ∈ t
h : f a' b' = f a b
⊢ a ∈ s ∧ b ∈ t
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem one_lt_card {o} : 1 < card o ↔ 1 < o

Proof state:
o : Ordinal.{u_1}
⊢ 1 < o.card ↔ 1 < o

Tactic:
simpa using nat_lt_card (n := 1)

Result:
no goals
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
theorem Γ_Spec_left_triangle : toSpecΓ (Γ.obj (op X)) ≫ X.toΓSpec.c.app (op ⊤) = 𝟙 _

Proof state:
X : LocallyRingedSpace
⊢ (toOpen (↑(Γ.obj (op X))) (basicOpen 1) ≫ X.toΓSpec.c.app (op (basicOpen 1))) ≫
      ((pushforward CommRingCat X.toΓSpec.base).obj X.presheaf).map (eqToHom ⋯).op =
    𝟙 (Γ.obj (op X))

Tactic:
erw [X.toΓSpecSheafedSpace_app_spec 1, ← Functor.map_comp]

Result:
X : LocallyRingedSpace
⊢ X.presheaf.map ((X.toΓSpecMapBasicOpen 1).leTop.op ≫ (Opens.map X.toΓSpec.base).op.map (eqToHom ⋯).op) =
    𝟙 (Γ.obj (op X))

Proof state:
X : LocallyRingedSpace
⊢ toOpen ↑(Γ.obj (op X)) ⊤ ≫ X.toΓSpec.c.app (op ⊤) = 𝟙 (Γ.obj (op X))

Tactic:
rw [← toOpen_res _ (basicOpen (1 : Γ.obj (op X))) ⊤ (eqToHom basicOpen_one.symm),
  Category.assoc, NatTrans.naturality, ← Category.assoc]

Result:
X : LocallyRingedSpace
⊢ (toOpen (↑(Γ.obj (op X))) (basicOpen 1) ≫ X.toΓSpec.c.app (op (basicOpen 1))) ≫
      ((pushforward CommRingCat X.toΓSpec.base).obj X.presheaf).map (eqToHom ⋯).op =
    𝟙 (Γ.obj (op X))

Proof state:
X : LocallyRingedSpace
⊢ X.presheaf.map ((X.toΓSpecMapBasicOpen 1).leTop.op ≫ (Opens.map X.toΓSpec.base).op.map (eqToHom ⋯).op) =
    𝟙 (Γ.obj (op X))

Tactic:
convert eqToHom_map X.presheaf _

Result:
case convert_3
X : LocallyRingedSpace
⊢ op ⊤ = (Opens.map X.toΓSpec.base).op.obj (op ⊤)

Proof state:
X : LocallyRingedSpace
⊢ toSpecΓ (Γ.obj (op X)) ≫ X.toΓSpec.c.app (op ⊤) = 𝟙 (Γ.obj (op X))

Tactic:
unfold toSpecΓ

Result:
X : LocallyRingedSpace
⊢ toOpen ↑(Γ.obj (op X)) ⊤ ≫ X.toΓSpec.c.app (op ⊤) = 𝟙 (Γ.obj (op X))

Proof state:
case convert_3
X : LocallyRingedSpace
⊢ op ⊤ = (Opens.map X.toΓSpec.base).op.obj (op ⊤)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Real.lean
theorem interior_closedBall (x : E) {r : ℝ} (hr : r ≠ 0) :
    interior (closedBall x r) = ball x r

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
hfc : Continuous f
⊢ y ∈ ball x (dist y x)

Tactic:
have hf1 : (1 : ℝ) ∈ f ⁻¹' interior (closedBall x <| dist y x) := by simpa [f]

Result:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
hr✝ : dist y x ≠ 0
hr : 0 < dist y x
hy : y ∈ interior (closedBall x (dist y x))
f : ℝ → E := fun c => c • (y - x) + x
this : f ⁻¹' closedBall x (dist y x) ⊆ Icc (-1) 1
hfc : Continuous f
hf1 : 1 ∈ f ⁻¹' interior (closedBall x (dist y x))
⊢ y ∈ ball x (dist y x)
-- Mathlib/LinearAlgebra/Prod.lean
theorem range_inl : range (inl R M M₂) = ker (snd R M M₂)

Proof state:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ x ∈ range (inl R M M₂) ↔ x ∈ ker (snd R M M₂)

Tactic:
simp only [mem_ker, mem_range]

Result:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (∃ y, (inl R M M₂) y = x) ↔ (snd R M M₂) x = 0

Proof state:
case h.mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
h : (snd R M M₂) x = 0
⊢ ∃ y, (inl R M M₂) y = x

Tactic:
exact ⟨x.fst, Prod.ext rfl h.symm⟩

Result:
no goals

Proof state:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (∃ y, (inl R M M₂) y = x) ↔ (snd R M M₂) x = 0

Tactic:
constructor

Result:
case h.mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (∃ y, (inl R M M₂) y = x) → (snd R M M₂) x = 0

case h.mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (snd R M M₂) x = 0 → ∃ y, (inl R M M₂) y = x

Proof state:
case h.mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (snd R M M₂) x = 0 → ∃ y, (inl R M M₂) y = x

Tactic:
intro h

Result:
case h.mpr
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
h : (snd R M M₂) x = 0
⊢ ∃ y, (inl R M M₂) y = x

Proof state:
case h.mp.intro
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
y : M
⊢ (snd R M M₂) ((inl R M M₂) y) = 0

Tactic:
rfl

Result:
no goals

Proof state:
case h.mp
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ (∃ y, (inl R M M₂) y = x) → (snd R M M₂) x = 0

Tactic:
rintro ⟨y, rfl⟩

Result:
case h.mp.intro
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
y : M
⊢ (snd R M M₂) ((inl R M M₂) y) = 0

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ range (inl R M M₂) = ker (snd R M M₂)

Tactic:
ext x

Result:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x : M × M₂
⊢ x ∈ range (inl R M M₂) ↔ x ∈ ker (snd R M M₂)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_insertMany_list_of_mem [LawfulBEq α] (h : m.WF)
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    (m.insertMany l).get? k' = some (cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ (m.insertMany l).get? k' = some (cast ⋯ v)

Tactic:
simp_to_raw using Raw₀.get?_insertMany_list_of_mem

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Proof state:
case e_a
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem pow_succ_factorization_not_dvd {n p : ℕ} (hn : n ≠ 0) (hp : p.Prime) :
    ¬p ^ (n.factorization p + 1) ∣ n

Proof state:
n p : ℕ
hn : n ≠ 0
hp : Prime p
⊢ ¬p ^ (n.factorization p + 1) ∣ n

Tactic:
intro h

Result:
n p : ℕ
hn : n ≠ 0
hp : Prime p
h : p ^ (n.factorization p + 1) ∣ n
⊢ False

Proof state:
n p : ℕ
hn : n ≠ 0
hp : Prime p
h : (p ^ (n.factorization p + 1)).factorization ≤ n.factorization
⊢ False

Tactic:
simpa [hp.factorization] using h p

Result:
no goals

Proof state:
n p : ℕ
hn : n ≠ 0
hp : Prime p
h : p ^ (n.factorization p + 1) ∣ n
⊢ False

Tactic:
rw [← factorization_le_iff_dvd (pow_pos hp.pos _).ne' hn] at h

Result:
n p : ℕ
hn : n ≠ 0
hp : Prime p
h : (p ^ (n.factorization p + 1)).factorization ≤ n.factorization
⊢ False
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma stieltjesOfMeasurableRat_unit_prod (hf : Measurable f) (a : α) :
    stieltjesOfMeasurableRat (fun (p : Unit × α) ↦ f p.2) (hf.comp measurable_snd) ((), a)
      = stieltjesOfMeasurableRat f hf a

Proof state:
case e_toFun.h.e_f.h
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
a : α
x : ℝ
p : Unit × α
⊢ toRatCDF (fun p => f p.2) p = toRatCDF f p.2

Tactic:
cases p with
| mk _ b => rw [← toRatCDF_unit_prod b]

Result:
no goals

Proof state:
case e_toFun.h.e_f.h.mk
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
a : α
x : ℝ
fst✝ : Unit
b : α
⊢ toRatCDF (fun p => f p.2) (fst✝, b) = toRatCDF f (fst✝, b).2

Tactic:
rw [← toRatCDF_unit_prod b]

Result:
no goals

Proof state:
case e_toFun.h
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
a : α
x : ℝ
⊢ IsMeasurableRatCDF.stieltjesFunctionAux (toRatCDF fun p => f p.2) ((), a) x =
    IsMeasurableRatCDF.stieltjesFunctionAux (fun p => toRatCDF f p.2) ((), a) x

Tactic:
congr 1 with p : 1

Result:
case e_toFun.h.e_f.h
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
a : α
x : ℝ
p : Unit × α
⊢ toRatCDF (fun p => f p.2) p = toRatCDF f p.2

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
a : α
⊢ stieltjesOfMeasurableRat (fun p => f p.2) ⋯ ((), a) = stieltjesOfMeasurableRat f hf a

Tactic:
simp_rw [stieltjesOfMeasurableRat,IsMeasurableRatCDF.stieltjesFunction,
  ← IsMeasurableRatCDF.stieltjesFunctionAux_unit_prod a]

Result:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
a : α
⊢ { toFun := IsMeasurableRatCDF.stieltjesFunctionAux (toRatCDF fun p => f p.2) ((), a), mono' := ⋯,
      right_continuous' := ⋯ } =
    { toFun := IsMeasurableRatCDF.stieltjesFunctionAux (fun p => toRatCDF f p.2) ((), a), mono' := ⋯,
      right_continuous' := ⋯ }

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
a : α
⊢ { toFun := IsMeasurableRatCDF.stieltjesFunctionAux (toRatCDF fun p => f p.2) ((), a), mono' := ⋯,
      right_continuous' := ⋯ } =
    { toFun := IsMeasurableRatCDF.stieltjesFunctionAux (fun p => toRatCDF f p.2) ((), a), mono' := ⋯,
      right_continuous' := ⋯ }

Tactic:
congr with x

Result:
case e_toFun.h
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
a : α
x : ℝ
⊢ IsMeasurableRatCDF.stieltjesFunctionAux (toRatCDF fun p => f p.2) ((), a) x =
    IsMeasurableRatCDF.stieltjesFunctionAux (fun p => toRatCDF f p.2) ((), a) x
-- Mathlib/Algebra/Order/Group/PosPart.lean
@[to_additive abs_add_eq_two_nsmul_posPart]
lemma mabs_mul_eq_oneLePart_sq (a : α) : |a|ₘ * a = a⁺ᵐ ^ 2

Proof state:
α : Type u_1
inst✝² : Lattice α
inst✝¹ : CommGroup α
inst✝ : MulLeftMono α
a : α
⊢ mabs a * a = a⁺ᵐ ^ 2

Tactic:
rw [sq, ← mul_mul_div_cancel a⁺ᵐ, oneLePart_mul_leOnePart, oneLePart_div_leOnePart]

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
@[simp]
lemma add_hom (α β : Ext X Y n) : (α + β).hom = α.hom + β.hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).hom.comp α'.hom ⋯ + (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).hom.comp β'.hom ⋯ = α.hom + β.hom

Tactic:
congr

Result:
case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).hom.comp α'.hom ⋯ = α.hom

case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).hom.comp β'.hom ⋯ = β.hom

Proof state:
case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).hom.comp ((mk₀ biprod.fst).comp α ⋯).hom ⋯ = α.hom

Tactic:
rw [comp_hom, mk₀_hom, mk₀_hom]

Result:
case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (ShiftedHom.mk₀ ↑0 ⋯ ((singleFunctor C 0).map (biprod.lift (𝟙 X) (𝟙 X)))).comp
      ((ShiftedHom.mk₀ ↑0 ⋯ ((singleFunctor C 0).map biprod.fst)).comp α.hom ⋯) ⋯ =
    α.hom
-- Mathlib/Algebra/Lie/Subalgebra.lean
theorem subset_lieSpan : s ⊆ lieSpan R L s

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
⊢ s ⊆ ↑(lieSpan R L s)

Tactic:
intro m hm

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
m : L
hm : m ∈ s
⊢ m ∈ ↑(lieSpan R L s)

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
m : L
hm : m ∈ s
K : LieSubalgebra R L
hK : s ⊆ ↑K
⊢ m ∈ K

Tactic:
exact hK hm

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
m : L
hm : m ∈ s
⊢ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → m ∈ K

Tactic:
intro K hK

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
m : L
hm : m ∈ s
K : LieSubalgebra R L
hK : s ⊆ ↑K
⊢ m ∈ K

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
m : L
hm : m ∈ s
⊢ m ∈ ↑(lieSpan R L s)

Tactic:
rw [SetLike.mem_coe, mem_lieSpan]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
s : Set L
m : L
hm : m ∈ s
⊢ ∀ (K : LieSubalgebra R L), s ⊆ ↑K → m ∈ K
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_insertMany_empty_list [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)} :
    (insertMany empty l).1.1.isEmpty = l.isEmpty

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
⊢ (empty.insertMany l).val.val.isEmpty = l.isEmpty

Tactic:
simp [isEmpty_insertMany_list _ Raw.WF.empty₀]

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/EulerMascheroni.lean
lemma eulerMascheroniConstant_lt_eulerMascheroniSeq' (n : ℕ) :
    eulerMascheroniConstant < eulerMascheroniSeq' n

Proof state:
n : ℕ
⊢ eulerMascheroniConstant < eulerMascheroniSeq' n

Tactic:
refine lt_of_le_of_lt ?_ (strictAnti_eulerMascheroniSeq' (Nat.lt_succ_self n))

Result:
n : ℕ
⊢ eulerMascheroniConstant ≤ eulerMascheroniSeq' n.succ

Proof state:
n : ℕ
⊢ eulerMascheroniConstant ≤ eulerMascheroniSeq' n.succ

Tactic:
apply strictAnti_eulerMascheroniSeq'.antitone.le_of_tendsto tendsto_eulerMascheroniSeq'

Result:
no goals
-- Mathlib/Algebra/QuadraticDiscriminant.lean
theorem exists_quadratic_eq_zero (ha : a ≠ 0) (h : ∃ s, discrim a b c = s * s) :
    ∃ x, a * (x * x) + b * x + c = 0

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
h : ∃ s, discrim a b c = s * s
⊢ ∃ x, a * (x * x) + b * x + c = 0

Tactic:
rcases h with ⟨s, hs⟩

Result:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
hs : discrim a b c = s * s
⊢ ∃ x, a * (x * x) + b * x + c = 0

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
hs : discrim a b c = s * s
⊢ a * ((-b + s) / (2 * a) * ((-b + s) / (2 * a))) + b * ((-b + s) / (2 * a)) + c = 0

Tactic:
rw [quadratic_eq_zero_iff ha hs]

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
hs : discrim a b c = s * s
⊢ (-b + s) / (2 * a) = (-b + s) / (2 * a) ∨ (-b + s) / (2 * a) = (-b - s) / (2 * a)

Proof state:
case intro
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
hs : discrim a b c = s * s
⊢ ∃ x, a * (x * x) + b * x + c = 0

Tactic:
use (-b + s) / (2 * a)

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
hs : discrim a b c = s * s
⊢ a * ((-b + s) / (2 * a) * ((-b + s) / (2 * a))) + b * ((-b + s) / (2 * a)) + c = 0

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NeZero 2
a b c : K
ha : a ≠ 0
s : K
hs : discrim a b c = s * s
⊢ (-b + s) / (2 * a) = (-b + s) / (2 * a) ∨ (-b + s) / (2 * a) = (-b - s) / (2 * a)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem and_not_self (x : BitVec n) : x &&& ~~~x = 0

Proof state:
n : Nat
x : BitVec n
⊢ x &&& ~~~x = 0

Tactic:
ext i

Result:
case pred
n : Nat
x : BitVec n
i : Nat
a✝ : i < n
⊢ (x &&& ~~~x).getLsbD i = getLsbD 0 i

Proof state:
case pred
n : Nat
x : BitVec n
i : Nat
a✝ : i < n
⊢ (x &&& ~~~x).getLsbD i = getLsbD 0 i

Tactic:
simp_all

Result:
no goals
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem isAmalgamation_sieveExtend {R : Presieve X} (x : FamilyOfElements P R) (t : P.obj (op X))
    (ht : x.IsAmalgamation t) : x.sieveExtend.IsAmalgamation t

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : (generate R).arrows f
⊢ P.map f.op t = P.map ⋯.choose.op (x ⋯.choose ⋯)

Tactic:
rw [← ht _, ← FunctorToTypes.map_comp_apply, ← op_comp, hf.choose_spec.choose_spec.choose_spec.2]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
⊢ x.sieveExtend.IsAmalgamation t

Tactic:
intro Y f hf

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : (generate R).arrows f
⊢ P.map f.op t = x.sieveExtend f hf

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : (generate R).arrows f
⊢ P.map f.op t = x.sieveExtend f hf

Tactic:
dsimp [FamilyOfElements.sieveExtend]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y : C
f : Y ⟶ X
hf : (generate R).arrows f
⊢ P.map f.op t = P.map ⋯.choose.op (x ⋯.choose ⋯)
-- Mathlib/Algebra/Algebra/Operations.lean
theorem sup_smul : (I ⊔ J) • N = I • N ⊔ J • N :=
  le_antisymm (smul_le.mpr fun mn hmn p hp ↦ by
    obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn
    rw [add_smul]; exact add_mem_sup (smul_mem_smul hm hp) <| smul_mem_smul hn hp)
    (sup_le (smul_mono_left le_sup_left) <| smul_mono_left le_sup_right)

Proof state:
case intro.intro.intro.intro
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
I J : Submodule R A
N : Submodule R M
p : M
hp : p ∈ N
m : A
hm : m ∈ I
n : A
hn : n ∈ J
hmn : m + n ∈ I ⊔ J
⊢ (m + n) • p ∈ I • N ⊔ J • N

Tactic:
rw [add_smul]

Result:
case intro.intro.intro.intro
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
I J : Submodule R A
N : Submodule R M
p : M
hp : p ∈ N
m : A
hm : m ∈ I
n : A
hn : n ∈ J
hmn : m + n ∈ I ⊔ J
⊢ m • p + n • p ∈ I • N ⊔ J • N

Proof state:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
I J : Submodule R A
N : Submodule R M
mn : A
hmn : mn ∈ I ⊔ J
p : M
hp : p ∈ N
⊢ mn • p ∈ I • N ⊔ J • N

Tactic:
obtain ⟨m, hm, n, hn, rfl⟩ := mem_sup.mp hmn

Result:
case intro.intro.intro.intro
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
I J : Submodule R A
N : Submodule R M
p : M
hp : p ∈ N
m : A
hm : m ∈ I
n : A
hn : n ∈ J
hmn : m + n ∈ I ⊔ J
⊢ (m + n) • p ∈ I • N ⊔ J • N

Proof state:
case intro.intro.intro.intro
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
I J : Submodule R A
N : Submodule R M
p : M
hp : p ∈ N
m : A
hm : m ∈ I
n : A
hn : n ∈ J
hmn : m + n ∈ I ⊔ J
⊢ m • p + n • p ∈ I • N ⊔ J • N

Tactic:
exact add_mem_sup (smul_mem_smul hm hp) <| smul_mem_smul hn hp

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive (attr := simp)]
lemma inv_univ [Fintype α] : (univ : Finset α)⁻¹ = univ

Proof state:
case h
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : InvolutiveInv α
inst✝ : Fintype α
a✝ : α
⊢ a✝ ∈ univ⁻¹ ↔ a✝ ∈ univ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : InvolutiveInv α
inst✝ : Fintype α
⊢ univ⁻¹ = univ

Tactic:
ext

Result:
case h
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : InvolutiveInv α
inst✝ : Fintype α
a✝ : α
⊢ a✝ ∈ univ⁻¹ ↔ a✝ ∈ univ