harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_pos_iff_support_of_nonneg_ae {f : X → ℝ} (hf : 0 ≤ᵐ[μ.restrict s] f)
    (hfi : IntegrableOn f s μ) : (0 < ∫ x in s, f x ∂μ) ↔ 0 < μ (support f ∩ s)

Proof state:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ : Measure X
f : X → ℝ
hf : 0 ≤ᶠ[ae (μ.restrict s)] f
hfi : IntegrableOn f s μ
⊢ NullMeasurableSet (f ⁻¹' {0}ᶜ) (μ.restrict s)

Tactic:
exact hfi.aestronglyMeasurable.aemeasurable.nullMeasurable (measurableSet_singleton 0).compl

Result:
no goals

Proof state:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ : Measure X
f : X → ℝ
hf : 0 ≤ᶠ[ae (μ.restrict s)] f
hfi : IntegrableOn f s μ
⊢ NullMeasurableSet (support f) (μ.restrict s)

Tactic:
rw [support_eq_preimage]

Result:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ : Measure X
f : X → ℝ
hf : 0 ≤ᶠ[ae (μ.restrict s)] f
hfi : IntegrableOn f s μ
⊢ NullMeasurableSet (f ⁻¹' {0}ᶜ) (μ.restrict s)

Proof state:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ : Measure X
f : X → ℝ
hf : 0 ≤ᶠ[ae (μ.restrict s)] f
hfi : IntegrableOn f s μ
⊢ 0 < ∫ (x : X) in s, f x ∂μ ↔ 0 < μ (support f ∩ s)

Tactic:
rw [integral_pos_iff_support_of_nonneg_ae hf hfi, Measure.restrict_apply₀]

Result:
X : Type u_1
mX : MeasurableSpace X
s : Set X
μ : Measure X
f : X → ℝ
hf : 0 ≤ᶠ[ae (μ.restrict s)] f
hfi : IntegrableOn f s μ
⊢ NullMeasurableSet (support f) (μ.restrict s)
-- Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean
theorem isOpenImmersion_iff_stalk {f : X ⟶ Y} : IsOpenImmersion f ↔
    IsOpenEmbedding f.base ∧ ∀ x, IsIso (f.stalkMap x)

Proof state:
case mp
X Y : Scheme
f : X ⟶ Y
⊢ IsOpenImmersion f →
    IsOpenEmbedding ⇑(ConcreteCategory.hom f.base) ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (Scheme.Hom.stalkMap f x)

Tactic:
intro h

Result:
case mp
X Y : Scheme
f : X ⟶ Y
h : IsOpenImmersion f
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom f.base) ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (Scheme.Hom.stalkMap f x)

Proof state:
X Y : Scheme
f : X ⟶ Y
⊢ IsOpenImmersion f ↔
    IsOpenEmbedding ⇑(ConcreteCategory.hom f.base) ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (Scheme.Hom.stalkMap f x)

Tactic:
constructor

Result:
case mp
X Y : Scheme
f : X ⟶ Y
⊢ IsOpenImmersion f →
    IsOpenEmbedding ⇑(ConcreteCategory.hom f.base) ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (Scheme.Hom.stalkMap f x)

case mpr
X Y : Scheme
f : X ⟶ Y
⊢ (IsOpenEmbedding ⇑(ConcreteCategory.hom f.base) ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (Scheme.Hom.stalkMap f x)) →
    IsOpenImmersion f

Proof state:
case mp
X Y : Scheme
f : X ⟶ Y
h : IsOpenImmersion f
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom f.base) ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (Scheme.Hom.stalkMap f x)

Tactic:
exact ⟨h.1, inferInstance⟩

Result:
no goals

Proof state:
case mpr
X Y : Scheme
f : X ⟶ Y
⊢ (IsOpenEmbedding ⇑(ConcreteCategory.hom f.base) ∧ ∀ (x : ↑↑X.toPresheafedSpace), IsIso (Scheme.Hom.stalkMap f x)) →
    IsOpenImmersion f

Tactic:
rintro ⟨h₁, h₂⟩

Result:
case mpr.intro
X Y : Scheme
f : X ⟶ Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), IsIso (Scheme.Hom.stalkMap f x)
⊢ IsOpenImmersion f

Proof state:
case mpr.intro
X Y : Scheme
f : X ⟶ Y
h₁ : IsOpenEmbedding ⇑(ConcreteCategory.hom f.base)
h₂ : ∀ (x : ↑↑X.toPresheafedSpace), IsIso (Scheme.Hom.stalkMap f x)
⊢ IsOpenImmersion f

Tactic:
exact IsOpenImmersion.of_stalk_iso f h₁

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
theorem MulEquivClass.map_nonZeroDivisors {M₀ S F : Type*} [MonoidWithZero M₀] [MonoidWithZero S]
    [EquivLike F M₀ S] [MulEquivClass F M₀ S] (h : F) :
    Submonoid.map h (nonZeroDivisors M₀) = nonZeroDivisors S

Proof state:
M₀ : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero S
inst✝¹ : EquivLike F M₀ S
inst✝ : MulEquivClass F M₀ S
h✝ : F
h : M₀ ≃* S := ↑h✝
⊢ Submonoid.map h✝ M₀⁰ = S⁰

Tactic:
show Submonoid.map h.toMonoidHom _ = _

Result:
M₀ : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero S
inst✝¹ : EquivLike F M₀ S
inst✝ : MulEquivClass F M₀ S
h✝ : F
h : M₀ ≃* S := ↑h✝
⊢ Submonoid.map h.toMonoidHom M₀⁰ = S⁰

Proof state:
M₀ : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero S
inst✝¹ : EquivLike F M₀ S
inst✝ : MulEquivClass F M₀ S
h : F
⊢ Submonoid.map h M₀⁰ = S⁰

Tactic:
let h : M₀ ≃* S := h

Result:
M₀ : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero S
inst✝¹ : EquivLike F M₀ S
inst✝ : MulEquivClass F M₀ S
h✝ : F
h : M₀ ≃* S := ↑h✝
⊢ Submonoid.map h✝ M₀⁰ = S⁰

Proof state:
case h
M₀ : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero S
inst✝¹ : EquivLike F M₀ S
inst✝ : MulEquivClass F M₀ S
h✝ : F
h : M₀ ≃* S := ↑h✝
x✝ : S
⊢ x✝ ∈ Submonoid.map h.toMonoidHom M₀⁰ ↔ x✝ ∈ S⁰

Tactic:
simp_rw [Submonoid.map_equiv_eq_comap_symm, Submonoid.mem_comap, mem_nonZeroDivisors_iff,
  ← h.symm.forall_congr_right, h.symm.coe_toMonoidHom, h.symm.toEquiv_eq_coe, h.symm.coe_toEquiv,
  ← map_mul, map_eq_zero_iff _ h.symm.injective]

Result:
no goals

Proof state:
M₀ : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero S
inst✝¹ : EquivLike F M₀ S
inst✝ : MulEquivClass F M₀ S
h✝ : F
h : M₀ ≃* S := ↑h✝
⊢ Submonoid.map h.toMonoidHom M₀⁰ = S⁰

Tactic:
ext

Result:
case h
M₀ : Type u_4
S : Type u_5
F : Type u_6
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero S
inst✝¹ : EquivLike F M₀ S
inst✝ : MulEquivClass F M₀ S
h✝ : F
h : M₀ ≃* S := ↑h✝
x✝ : S
⊢ x✝ ∈ Submonoid.map h.toMonoidHom M₀⁰ ↔ x✝ ∈ S⁰
-- Mathlib/Analysis/Convex/Exposed.lean
theorem inter_left (hC : IsExposed 𝕜 A C) (hCB : C ⊆ B) : IsExposed 𝕜 (A ∩ B) C

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 A C
hCB : C ⊆ B
w : E
hw : w ∈ C
⊢ ∃ l, C = {x | x ∈ A ∩ B ∧ ∀ y ∈ A ∩ B, l y ≤ l x}

Tactic:
obtain ⟨l, rfl⟩ := hC ⟨w, hw⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
w : E
l : E →L[𝕜] 𝕜
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hCB : {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} ⊆ B
hw : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
⊢ ∃ l_1, {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} = {x | x ∈ A ∩ B ∧ ∀ y ∈ A ∩ B, l_1 y ≤ l_1 x}

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
w : E
l : E →L[𝕜] 𝕜
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hCB : {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} ⊆ B
hw : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
⊢ ∃ l_1, {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} = {x | x ∈ A ∩ B ∧ ∀ y ∈ A ∩ B, l_1 y ≤ l_1 x}

Tactic:
exact ⟨l, Subset.antisymm (fun x hx => ⟨⟨hx.1, hCB hx⟩, fun y hy => hx.2 y hy.1⟩)
  fun x ⟨⟨hxC, _⟩, hx⟩ => ⟨hxC, fun y hy => (hw.2 y hy).trans (hx w ⟨hC.subset hw, hCB hw⟩)⟩⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 A C
hCB : C ⊆ B
⊢ IsExposed 𝕜 (A ∩ B) C

Tactic:
rintro ⟨w, hw⟩

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 A C
hCB : C ⊆ B
w : E
hw : w ∈ C
⊢ ∃ l, C = {x | x ∈ A ∩ B ∧ ∀ y ∈ A ∩ B, l y ≤ l x}
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem Decidable.or_congr_left' [Decidable c] (h : ¬c → (a ↔ b)) : a ∨ c ↔ b ∨ c

Proof state:
c a b : Prop
inst✝ : Decidable c
h : ¬c → (a ↔ b)
⊢ a ∨ c ↔ b ∨ c

Tactic:
rw [or_iff_not_imp_right, or_iff_not_imp_right]

Result:
c a b : Prop
inst✝ : Decidable c
h : ¬c → (a ↔ b)
⊢ ¬c → a ↔ ¬c → b

Proof state:
c a b : Prop
inst✝ : Decidable c
h : ¬c → (a ↔ b)
⊢ ¬c → a ↔ ¬c → b

Tactic:
exact imp_congr_right h

Result:
no goals
-- Mathlib/Topology/Algebra/TopologicallyNilpotent.lean
theorem mul_left_of_commute [IsLinearTopology R R] {a b : R}
    (hb : IsTopologicallyNilpotent b) (hab : Commute a b) :
    IsTopologicallyNilpotent (a * b)

Proof state:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
hb : IsTopologicallyNilpotent b
hab : Commute a b
⊢ Tendsto (fun x => a ^ x * b ^ x) atTop (𝓝 0)

Tactic:
exact IsLinearTopology.tendsto_mul_zero_of_right _ _ hb

Result:
no goals

Proof state:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
hb : IsTopologicallyNilpotent b
hab : Commute a b
⊢ IsTopologicallyNilpotent (a * b)

Tactic:
simp_rw [IsTopologicallyNilpotent, hab.mul_pow]

Result:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : Ring R
inst✝ : IsLinearTopology R R
a b : R
hb : IsTopologicallyNilpotent b
hab : Commute a b
⊢ Tendsto (fun x => a ^ x * b ^ x) atTop (𝓝 0)
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem δ_comp_δ_self' {n} {j : Fin (n + 3)} {i : Fin (n + 2)} (H : j = Fin.castSucc i) :
    X.δ j ≫ X.δ i = X.δ i.succ ≫ X.δ i

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
j : Fin (n + 3)
i : Fin (n + 2)
H : j = i.castSucc
⊢ X.δ j ≫ X.δ i = X.δ i.succ ≫ X.δ i

Tactic:
subst H

Result:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.δ i.castSucc ≫ X.δ i = X.δ i.succ ≫ X.δ i

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
⊢ X.δ i.castSucc ≫ X.δ i = X.δ i.succ ≫ X.δ i

Tactic:
rw [δ_comp_δ_self]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem WF.out {t : RBNode α} (h : t.WF cmp) : t.Ordered cmp ∧ ∃ c n, t.Balanced c n

Proof state:
case erase
α : Type u_1
cmp : α → α → Ordering
t t✝ : RBNode α
cut✝ : α → Ordering
a✝ : WF cmp t✝
ih : Ordered cmp t✝ ∧ ∃ c n, t✝.Balanced c n
o : Ordered cmp t✝
w✝¹ : RBColor
w✝ : Nat
h : t✝.Balanced w✝¹ w✝
⊢ Ordered cmp (RBNode.erase cut✝ t✝) ∧ ∃ c n, (RBNode.erase cut✝ t✝).Balanced c n

Tactic:
exact ⟨o.erase, _, h.erase⟩

Result:
no goals

Proof state:
case erase
α : Type u_1
cmp : α → α → Ordering
t t✝ : RBNode α
cut✝ : α → Ordering
a✝ : WF cmp t✝
ih : Ordered cmp t✝ ∧ ∃ c n, t✝.Balanced c n
⊢ Ordered cmp (RBNode.erase cut✝ t✝) ∧ ∃ c n, (RBNode.erase cut✝ t✝).Balanced c n

Tactic:
have ⟨o, _, _, h⟩ := ih

Result:
case erase
α : Type u_1
cmp : α → α → Ordering
t t✝ : RBNode α
cut✝ : α → Ordering
a✝ : WF cmp t✝
ih : Ordered cmp t✝ ∧ ∃ c n, t✝.Balanced c n
o : Ordered cmp t✝
w✝¹ : RBColor
w✝ : Nat
h : t✝.Balanced w✝¹ w✝
⊢ Ordered cmp (RBNode.erase cut✝ t✝) ∧ ∃ c n, (RBNode.erase cut✝ t✝).Balanced c n

Proof state:
case insert
α : Type u_1
cmp : α → α → Ordering
t t✝ : RBNode α
a✝¹ : α
a✝ : WF cmp t✝
ih : Ordered cmp t✝ ∧ ∃ c n, t✝.Balanced c n
⊢ Ordered cmp (RBNode.insert cmp t✝ a✝¹) ∧ ∃ c n, (RBNode.insert cmp t✝ a✝¹).Balanced c n

Tactic:
have ⟨o, _, _, h⟩ := ih

Result:
case insert
α : Type u_1
cmp : α → α → Ordering
t t✝ : RBNode α
a✝¹ : α
a✝ : WF cmp t✝
ih : Ordered cmp t✝ ∧ ∃ c n, t✝.Balanced c n
o : Ordered cmp t✝
w✝¹ : RBColor
w✝ : Nat
h : t✝.Balanced w✝¹ w✝
⊢ Ordered cmp (RBNode.insert cmp t✝ a✝¹) ∧ ∃ c n, (RBNode.insert cmp t✝ a✝¹).Balanced c n

Proof state:
case mk
α : Type u_1
cmp : α → α → Ordering
t t✝ : RBNode α
c✝ : RBColor
n✝ : Nat
o : Ordered cmp t✝
h : t✝.Balanced c✝ n✝
⊢ Ordered cmp t✝ ∧ ∃ c n, t✝.Balanced c n

Tactic:
exact ⟨o, _, _, h⟩

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
t : RBNode α
h : WF cmp t
⊢ Ordered cmp t ∧ ∃ c n, t.Balanced c n

Tactic:
induction h with
| mk o h => exact ⟨o, _, _, h⟩
| insert _ ih => have ⟨o, _, _, h⟩ := ih; exact ⟨o.insert, h.insert⟩
| erase _ ih => have ⟨o, _, _, h⟩ := ih; exact ⟨o.erase, _, h.erase⟩

Result:
no goals

Proof state:
case insert
α : Type u_1
cmp : α → α → Ordering
t t✝ : RBNode α
a✝¹ : α
a✝ : WF cmp t✝
ih : Ordered cmp t✝ ∧ ∃ c n, t✝.Balanced c n
o : Ordered cmp t✝
w✝¹ : RBColor
w✝ : Nat
h : t✝.Balanced w✝¹ w✝
⊢ Ordered cmp (RBNode.insert cmp t✝ a✝¹) ∧ ∃ c n, (RBNode.insert cmp t✝ a✝¹).Balanced c n

Tactic:
exact ⟨o.insert, h.insert⟩

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem length_copy {u v u' v'} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
    (p.copy hu hv).length = p.length

Proof state:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).length = p.length

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
hu : u = u'
hv : v = v'
⊢ (p.copy hu hv).length = p.length

Tactic:
subst_vars

Result:
V : Type u
G : SimpleGraph V
u' v' : V
p : G.Walk u' v'
⊢ (p.copy ⋯ ⋯).length = p.length
-- Mathlib/CategoryTheory/Adjunction/Unique.lean
theorem leftAdjointUniq_hom_app_counit {F F' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G)
    (x : D) :
    (leftAdjointUniq adj1 adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ (adj1.leftAdjointUniq adj2).hom.app (G.obj x) ≫ adj2.counit.app x =
    (whiskerLeft G (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit).app x

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ (adj1.leftAdjointUniq adj2).hom.app (G.obj x) ≫ adj2.counit.app x = adj1.counit.app x

Tactic:
rw [← leftAdjointUniq_hom_counit adj1 adj2]

Result:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
x : D
⊢ (adj1.leftAdjointUniq adj2).hom.app (G.obj x) ≫ adj2.counit.app x =
    (whiskerLeft G (adj1.leftAdjointUniq adj2).hom ≫ adj2.counit).app x
-- Mathlib/Algebra/Polynomial/Laurent.lean
lemma involutive_invert : Involutive (invert (R := R)) := fun _ ↦ by ext; simp

Proof state:
R : Type u_3
inst✝ : CommSemiring R
x✝ : R[T;T⁻¹]
⊢ invert (invert x✝) = x✝

Tactic:
ext

Result:
case h
R : Type u_3
inst✝ : CommSemiring R
x✝ : R[T;T⁻¹]
a✝ : ℤ
⊢ (invert (invert x✝)) a✝ = x✝ a✝

Proof state:
case h
R : Type u_3
inst✝ : CommSemiring R
x✝ : R[T;T⁻¹]
a✝ : ℤ
⊢ (invert (invert x✝)) a✝ = x✝ a✝

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Products/Basic.lean
/-- Any morphism in a product factors as a morphsim whose left component is an identity
followed by a morphism whose right component is an identity. -/
@[reassoc]
lemma fac {x y : C × D} (f : x ⟶ y) :
    f = ((𝟙 x.1, f.2) : _ ⟶ ⟨x.1, y.2⟩) ≫ (f.1, 𝟙 y.2)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
x y : C × D
f : x ⟶ y
⊢ f = (𝟙 x.1, f.2) ≫ (f.1, 𝟙 y.2)

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean
theorem delete_subset (f : DefaultFormula n) (arr : Array Nat) (c : DefaultClause n) :
    c ∈ toList (delete f arr) → c ∈ toList f

Proof state:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
f' : DefaultFormula n
ih : c ∈ f'.toList → c ∈ f.toList
id : Nat
x✝ : id ∈ arr.toList
h : c ∈ (f'.deleteOne id).toList
⊢ c ∈ f.toList

Tactic:
exact ih <| deleteOne_subset f' id c h

Result:
no goals

Proof state:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
⊢ c ∈ (f.delete arr).toList → c ∈ f.toList

Tactic:
simp only [delete, ← Array.foldl_toList]

Result:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.toList).toList → c ∈ f.toList

Proof state:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
f' : DefaultFormula n
ih : c ∈ f'.toList → c ∈ f.toList
id : Nat
x✝ : id ∈ arr.toList
⊢ c ∈ (f'.deleteOne id).toList → c ∈ f.toList

Tactic:
intro h

Result:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
f' : DefaultFormula n
ih : c ∈ f'.toList → c ∈ f.toList
id : Nat
x✝ : id ∈ arr.toList
h : c ∈ (f'.deleteOne id).toList
⊢ c ∈ f.toList

Proof state:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.toList).toList → c ∈ f.toList

Tactic:
have hb : c ∈ toList f → c ∈ toList f := id

Result:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.toList).toList → c ∈ f.toList

Proof state:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.toList).toList → c ∈ f.toList

Tactic:
have hl (f' : DefaultFormula n) (ih : c ∈ toList f' → c ∈ toList f) (id : Nat) (_ : id ∈ arr.toList) :
  c ∈ toList (deleteOne f' id) → c ∈ toList f := by intro h; exact ih <| deleteOne_subset f' id c h

Result:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
hl :
  ∀ (f' : DefaultFormula n),
    (c ∈ f'.toList → c ∈ f.toList) → ∀ (id : Nat), id ∈ arr.toList → c ∈ (f'.deleteOne id).toList → c ∈ f.toList
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.toList).toList → c ∈ f.toList

Proof state:
n : Nat
f : DefaultFormula n
arr : Array Nat
c : DefaultClause n
hb : c ∈ f.toList → c ∈ f.toList
hl :
  ∀ (f' : DefaultFormula n),
    (c ∈ f'.toList → c ∈ f.toList) → ∀ (id : Nat), id ∈ arr.toList → c ∈ (f'.deleteOne id).toList → c ∈ f.toList
⊢ c ∈ (List.foldl (fun f id => f.deleteOne id) f arr.toList).toList → c ∈ f.toList

Tactic:
exact List.foldlRecOn arr.toList deleteOne f hb hl

Result:
no goals
-- Mathlib/Data/Finset/Max.lean
theorem min_erase_ne_self {s : Finset α} : (s.erase x).min ≠ x

Proof state:
case h.e'_2.h.h.h.e'_3.h.h
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
e_1✝¹ : WithTop α = WithBot αᵒᵈ
e_1✝ : α = αᵒᵈ
a✝ : α
⊢ a✝ ∈ s ↔ a✝ ∈ map toDual.toEmbedding s

Tactic:
simp only [mem_map_equiv]

Result:
case h.e'_2.h.h.h.e'_3.h.h
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
e_1✝¹ : WithTop α = WithBot αᵒᵈ
e_1✝ : α = αᵒᵈ
a✝ : α
⊢ a✝ ∈ s ↔ toDual.symm a✝ ∈ s

Proof state:
case h.e'_2.h.h.h.e'_3.h.h
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
e_1✝¹ : WithTop α = WithBot αᵒᵈ
e_1✝ : α = αᵒᵈ
a✝ : α
⊢ a✝ ∈ s ↔ toDual.symm a✝ ∈ s

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
case h.e'_2.h
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
e_1✝ : WithTop α = WithBot αᵒᵈ
⊢ (s.erase x).min = ((map toDual.toEmbedding s).erase (toDual x)).max

Tactic:
apply congr_arg

Result:
case h.e'_2.h.h
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
e_1✝ : WithTop α = WithBot αᵒᵈ
⊢ s.erase x = (map toDual.toEmbedding s).erase (toDual x)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
⊢ (s.erase x).min ≠ ↑x

Tactic:
convert @max_erase_ne_self αᵒᵈ _ (toDual x) (s.map toDual.toEmbedding) using 1

Result:
case h.e'_2.h
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
e_1✝ : WithTop α = WithBot αᵒᵈ
⊢ (s.erase x).min = ((map toDual.toEmbedding s).erase (toDual x)).max

Proof state:
case h.e'_2.h.h.h.e'_3.h
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
e_1✝¹ : WithTop α = WithBot αᵒᵈ
e_1✝ : α = αᵒᵈ
⊢ s = map toDual.toEmbedding s

Tactic:
ext

Result:
case h.e'_2.h.h.h.e'_3.h.h
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
e_1✝¹ : WithTop α = WithBot αᵒᵈ
e_1✝ : α = αᵒᵈ
a✝ : α
⊢ a✝ ∈ s ↔ a✝ ∈ map toDual.toEmbedding s

Proof state:
case h.e'_2.h.h
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
e_1✝ : WithTop α = WithBot αᵒᵈ
⊢ s.erase x = (map toDual.toEmbedding s).erase (toDual x)

Tactic:
congr!

Result:
case h.e'_2.h.h.h.e'_3.h
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
e_1✝¹ : WithTop α = WithBot αᵒᵈ
e_1✝ : α = αᵒᵈ
⊢ s = map toDual.toEmbedding s
-- Mathlib/Analysis/InnerProductSpace/LinearMap.lean
@[simp] lemma flip_innerₗ : (innerₗ F).flip = innerₗ F

Proof state:
case h.h
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
⊢ ((innerₗ F).flip v) w = ((innerₗ F) v) w

Tactic:
exact real_inner_comm v w

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
⊢ (innerₗ F).flip = innerₗ F

Tactic:
ext v w

Result:
case h.h
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
⊢ ((innerₗ F).flip v) w = ((innerₗ F) v) w
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_alter [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} (h : m.WF) :
    (Const.alter m k f).isEmpty = ((m.isEmpty || (m.size == 1 && m.contains k)) &&
      (f (get? m k)).isNone)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : Option β → Option β
h : m.WF
⊢ (alter m k f).isEmpty = ((m.isEmpty || m.size == 1 && m.contains k) && (f (get? m k)).isNone)

Tactic:
simp_to_raw using Raw₀.Const.isEmpty_alter

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
@[simp] lemma reverse_mul_X (p : R[X]) : reverse (p * X) = reverse p

Proof state:
case inr
R : Type u_1
inst✝ : Semiring R
p : R[X]
a✝ : Nontrivial R
hp : p ≠ 0
⊢ (p * X).reverse = p.reverse

Tactic:
simp [reverse, hp]

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝ : Semiring R
a✝ : Nontrivial R
⊢ (0 * X).reverse = reverse 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (p * X).reverse = p.reverse

Tactic:
nontriviality R

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
a✝ : Nontrivial R
⊢ (p * X).reverse = p.reverse

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
a✝ : Nontrivial R
⊢ (p * X).reverse = p.reverse

Tactic:
rcases eq_or_ne p 0 with rfl | hp

Result:
case inl
R : Type u_1
inst✝ : Semiring R
a✝ : Nontrivial R
⊢ (0 * X).reverse = reverse 0

case inr
R : Type u_1
inst✝ : Semiring R
p : R[X]
a✝ : Nontrivial R
hp : p ≠ 0
⊢ (p * X).reverse = p.reverse
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem add_one_mul_add_one (a b : Nat) : (a + 1) * (b + 1) = a * b + a + b + 1

Proof state:
a b : Nat
⊢ (a + 1) * (b + 1) = a * b + a + b + 1

Tactic:
rw [add_one_mul, mul_add_one]

Result:
a b : Nat
⊢ a * b + a + (b + 1) = a * b + a + b + 1

Proof state:
a b : Nat
⊢ a * b + a + (b + 1) = a * b + a + b + 1

Tactic:
rfl

Result:
no goals