harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Real/Cardinality.lean
theorem mk_Iio_real (a : ℝ) : #(Iio a) = 𝔠

Proof state:
a : ℝ
⊢ 𝔠 ≤ #↑(Iio a)

Tactic:
have h2 : (fun x => a + a - x) '' Iio a = Ioi a := by
  simp only [image_const_sub_Iio, add_sub_cancel_right]

Result:
a : ℝ
h2 : (fun x => a + a - x) '' Iio a = Ioi a
⊢ 𝔠 ≤ #↑(Iio a)

Proof state:
a : ℝ
⊢ (fun x => a + a - x) '' Iio a = Ioi a

Tactic:
simp only [image_const_sub_Iio, add_sub_cancel_right]

Result:
no goals

Proof state:
a : ℝ
h2 : (fun x => a + a - x) '' Iio a = Ioi a
⊢ 𝔠 ≤ #↑(Iio a)

Tactic:
exact mk_Ioi_real a ▸ h2 ▸ mk_image_le

Result:
no goals

Proof state:
a : ℝ
⊢ #↑(Iio a) = 𝔠

Tactic:
refine le_antisymm (mk_real ▸ mk_set_le _) ?_

Result:
a : ℝ
⊢ 𝔠 ≤ #↑(Iio a)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_insertMany_list_of_contains_eq_false [LawfulBEq α] (h : m.1.WF)
    {l : List ((a : α) × β a)} {k : α} {fallback : β k}
    (contains_eq_false : (l.map Sigma.fst).contains k = false) :
    (m.insertMany l).1.getD k fallback = m.getD k fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
l : List ((a : α) × β a)
k : α
fallback : β k
contains_eq_false : (List.map Sigma.fst l).contains k = false
⊢ (m.insertMany l).val.getD k fallback = m.getD k fallback

Tactic:
simp_to_model [insertMany] using List.getValueCastD_insertList_of_contains_eq_false

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem exists_not_mem_null_le_average (hμ : μ ≠ 0) (hf : Integrable f μ) (hN : μ N = 0) :
    ∃ x, x ∉ N ∧ f x ≤ ⨍ a, f a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
hN : μ N = 0
this : 0 < μ {x | f x ≤ ⨍ (a : α), f a ∂μ}
⊢ ∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ

Tactic:
rw [← measure_diff_null hN] at this

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
hN : μ N = 0
this : 0 < μ ({x | f x ≤ ⨍ (a : α), f a ∂μ} \ N)
⊢ ∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
hN : μ N = 0
this : 0 < μ ({x | f x ≤ ⨍ (a : α), f a ∂μ} \ N)
⊢ ∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ

Tactic:
obtain ⟨x, hx, hxN⟩ := nonempty_of_measure_ne_zero this.ne'

Result:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
hN : μ N = 0
this : 0 < μ ({x | f x ≤ ⨍ (a : α), f a ∂μ} \ N)
x : α
hx : x ∈ {x | f x ≤ ⨍ (a : α), f a ∂μ}
hxN : x ∉ N
⊢ ∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
hN : μ N = 0
⊢ ∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ

Tactic:
have := measure_le_average_pos hμ hf

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
hN : μ N = 0
this : 0 < μ {x | f x ≤ ⨍ (a : α), f a ∂μ}
⊢ ∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ

Proof state:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable f μ
hN : μ N = 0
this : 0 < μ ({x | f x ≤ ⨍ (a : α), f a ∂μ} \ N)
x : α
hx : x ∈ {x | f x ≤ ⨍ (a : α), f a ∂μ}
hxN : x ∉ N
⊢ ∃ x ∉ N, f x ≤ ⨍ (a : α), f a ∂μ

Tactic:
exact ⟨x, hxN, hx⟩

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem conj_neg_I : conj (-I) = I :=
  Complex.ext_iff.2 <| by simp

Proof state:
⊢ ((starRingEnd ℂ) (-I)).re = I.re ∧ ((starRingEnd ℂ) (-I)).im = I.im

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Alternating/Topology.lean
theorem isUniformInducing_postcomp {G : Type*} [AddCommGroup G] [UniformSpace G] [UniformAddGroup G]
    [Module 𝕜 G] (g : F →L[𝕜] G) (hg : IsUniformInducing g) :
    IsUniformInducing (g.compContinuousAlternatingMap : (E [⋀^ι]→L[𝕜] F) → (E [⋀^ι]→L[𝕜] G))

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
G : Type u_5
inst✝³ : AddCommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformAddGroup G
inst✝ : Module 𝕜 G
g : F →L[𝕜] G
hg : IsUniformInducing ⇑g
⊢ IsUniformInducing g.compContinuousAlternatingMap

Tactic:
rw [← isUniformEmbedding_toContinuousMultilinearMap.1.of_comp_iff]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
G : Type u_5
inst✝³ : AddCommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformAddGroup G
inst✝ : Module 𝕜 G
g : F →L[𝕜] G
hg : IsUniformInducing ⇑g
⊢ IsUniformInducing (toContinuousMultilinearMap ∘ g.compContinuousAlternatingMap)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
ι : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : AddCommGroup F
inst✝⁶ : Module 𝕜 F
inst✝⁵ : UniformSpace F
inst✝⁴ : UniformAddGroup F
G : Type u_5
inst✝³ : AddCommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformAddGroup G
inst✝ : Module 𝕜 G
g : F →L[𝕜] G
hg : IsUniformInducing ⇑g
⊢ IsUniformInducing (toContinuousMultilinearMap ∘ g.compContinuousAlternatingMap)

Tactic:
exact (ContinuousMultilinearMap.isUniformInducing_postcomp g hg).comp
  isUniformEmbedding_toContinuousMultilinearMap.1

Result:
no goals
-- Mathlib/Computability/Encoding.lean
theorem Encoding.encode_injective {α : Type u} (e : Encoding α) : Function.Injective e.encode

Proof state:
α : Type u
e : Encoding α
x✝¹ x✝ : α
h : e.encode x✝¹ = e.encode x✝
⊢ some x✝¹ = some x✝

Tactic:
rw [← e.decode_encode, ← e.decode_encode, h]

Result:
no goals

Proof state:
α : Type u
e : Encoding α
⊢ Function.Injective e.encode

Tactic:
refine fun _ _ h => Option.some_injective _ ?_

Result:
α : Type u
e : Encoding α
x✝¹ x✝ : α
h : e.encode x✝¹ = e.encode x✝
⊢ some x✝¹ = some x✝
-- Mathlib/Data/List/ReduceOption.lean
theorem reduceOption_length_lt_iff {l : List (Option α)} :
    l.reduceOption.length < l.length ↔ none ∈ l

Proof state:
case cons
α : Type u_1
head✝ : Option α
tail✝ : List (Option α)
tail_ih✝ : (¬∀ (x : Option α), x ∈ tail✝ → x.isSome = true) ↔ none ∈ tail✝
⊢ head✝.isSome = true → none ∈ tail✝ ↔ none = head✝ ∨ none ∈ tail✝

Tactic:
rw [@eq_comm _ none, ← Option.not_isSome_iff_eq_none, Decidable.imp_iff_not_or]

Result:
no goals

Proof state:
α : Type u_1
l : List (Option α)
⊢ (¬∀ (x : Option α), x ∈ l → x.isSome = true) ↔ none ∈ l

Tactic:
induction l <;> simp

Result:
case cons
α : Type u_1
head✝ : Option α
tail✝ : List (Option α)
tail_ih✝ : (¬∀ (x : Option α), x ∈ tail✝ → x.isSome = true) ↔ none ∈ tail✝
⊢ head✝.isSome = true → none ∈ tail✝ ↔ none = head✝ ∨ none ∈ tail✝

Proof state:
α : Type u_1
l : List (Option α)
⊢ l.reduceOption.length < l.length ↔ none ∈ l

Tactic:
rw [Nat.lt_iff_le_and_ne, and_iff_right (reduceOption_length_le l), Ne,
  reduceOption_length_eq_iff]

Result:
α : Type u_1
l : List (Option α)
⊢ (¬∀ (x : Option α), x ∈ l → x.isSome = true) ↔ none ∈ l
-- Mathlib/CategoryTheory/Shift/Adjunction.lean
/--
The isomorphisms `Functor.CommShift.isoZero F` and `Functor.CommShift.isoZero G` are
compatible with the unit of an adjunction `F ⊣ G`.
-/
lemma compatibilityUnit_isoZero : CompatibilityUnit adj (Functor.CommShift.isoZero F A)
    (Functor.CommShift.isoZero G A)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
X✝ : C
⊢ (shiftFunctor C 0).map (adj.unit.app X✝) =
    adj.unit.app ((shiftFunctor C 0).obj X✝) ≫
      G.map ((Functor.CommShift.isoZero F A).hom.app X✝) ≫ (Functor.CommShift.isoZero G A).hom.app (F.obj X✝)

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, Functor.CommShift.isoZero_hom_app,
  Functor.map_comp, assoc, unit_naturality_assoc,
  ← cancel_mono ((shiftFunctorZero C A).hom.app _), ← G.map_comp_assoc, Iso.inv_hom_id_app,
  Functor.id_obj, Functor.map_id, id_comp, NatTrans.naturality, Functor.id_map, assoc, comp_id]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
⊢ CompatibilityUnit adj (Functor.CommShift.isoZero F A) (Functor.CommShift.isoZero G A)

Tactic:
intro

Result:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_5, u_2} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
X✝ : C
⊢ (shiftFunctor C 0).map (adj.unit.app X✝) =
    adj.unit.app ((shiftFunctor C 0).obj X✝) ≫
      G.map ((Functor.CommShift.isoZero F A).hom.app X✝) ≫ (Functor.CommShift.isoZero G A).hom.app (F.obj X✝)
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoUniformlyOn_iff_tendstoUniformlyOnFilter :
    TendstoUniformlyOn F f p s ↔ TendstoUniformlyOnFilter F f p (𝓟 s)

Proof state:
case h
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ ∀ a ∈ 𝓤 β, (∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ a) ↔ ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, (f n.2, F n.1 n.2) ∈ a

Tactic:
simp_rw [eventually_prod_principal_iff]

Result:
case h
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ ∀ a ∈ 𝓤 β, True

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ (∀ u ∈ 𝓤 β, ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u) ↔
    ∀ u ∈ 𝓤 β, ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, (f n.2, F n.1 n.2) ∈ u

Tactic:
apply forall₂_congr

Result:
case h
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ ∀ a ∈ 𝓤 β, (∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ a) ↔ ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, (f n.2, F n.1 n.2) ∈ a

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ TendstoUniformlyOn F f p s ↔ TendstoUniformlyOnFilter F f p (𝓟 s)

Tactic:
simp only [TendstoUniformlyOn, TendstoUniformlyOnFilter]

Result:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ (∀ u ∈ 𝓤 β, ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u) ↔
    ∀ u ∈ 𝓤 β, ∀ᶠ (n : ι × α) in p ×ˢ 𝓟 s, (f n.2, F n.1 n.2) ∈ u

Proof state:
case h
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ ∀ a ∈ 𝓤 β, True

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/Module.lean
theorem sub_eq_eval {R₁ R₂ S₁ S₂ : Type*} [AddCommGroup M] [Ring R] [Module R M] [Semiring R₁]
    [Module R₁ M] [Semiring R₂] [Module R₂ M] [Semiring S₁] [Module S₁ M] [Semiring S₂]
    [Module S₂ M] {l₁ l₂ l : NF R M} {l₁' : NF R₁ M} {l₂' : NF R₂ M} {l₁'' : NF S₁ M}
    {l₂'' : NF S₂ M} {x₁ x₂ : M} (hx₁ : x₁ = l₁''.eval) (hx₂ : x₂ = l₂''.eval)
    (h₁' : l₁'.eval = l₁''.eval) (h₂' : l₂'.eval = l₂''.eval) (h₁ : l₁.eval = l₁'.eval)
    (h₂ : l₂.eval = l₂'.eval) (h : l₁.eval - l₂.eval = l.eval) :
    x₁ - x₂ = l.eval

Proof state:
R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
S₁ : Type u_6
S₂ : Type u_7
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Ring R
inst✝⁸ : Module R M
inst✝⁷ : Semiring R₁
inst✝⁶ : Module R₁ M
inst✝⁵ : Semiring R₂
inst✝⁴ : Module R₂ M
inst✝³ : Semiring S₁
inst✝² : Module S₁ M
inst✝¹ : Semiring S₂
inst✝ : Module S₂ M
l₁ l₂ l : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
l₁'' : NF S₁ M
l₂'' : NF S₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁''.eval
hx₂ : x₂ = l₂''.eval
h₁' : l₁'.eval = l₁''.eval
h₂' : l₂'.eval = l₂''.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval - l₂.eval = l.eval
⊢ x₁ - x₂ = l.eval

Tactic:
rw [hx₁, hx₂, ← h₁', ← h₂', ← h₁, ← h₂, h]

Result:
no goals
-- Mathlib/Algebra/Field/Subfield/Defs.lean
theorem zpow_mem {x : K} (hx : x ∈ s) (n : ℤ) : x ^ n ∈ s

Proof state:
K : Type u
inst✝ : DivisionRing K
s : Subfield K
x : K
hx : x ∈ s
n : ℤ
⊢ x ^ n ∈ s

Tactic:
cases n

Result:
case ofNat
K : Type u
inst✝ : DivisionRing K
s : Subfield K
x : K
hx : x ∈ s
a✝ : ℕ
⊢ x ^ Int.ofNat a✝ ∈ s

case negSucc
K : Type u
inst✝ : DivisionRing K
s : Subfield K
x : K
hx : x ∈ s
a✝ : ℕ
⊢ x ^ Int.negSucc a✝ ∈ s

Proof state:
case ofNat
K : Type u
inst✝ : DivisionRing K
s : Subfield K
x : K
hx : x ∈ s
a✝ : ℕ
⊢ x ^ Int.ofNat a✝ ∈ s

Tactic:
simpa using s.pow_mem hx _

Result:
no goals

Proof state:
case negSucc
K : Type u
inst✝ : DivisionRing K
s : Subfield K
x : K
hx : x ∈ s
a✝ : ℕ
⊢ x ^ Int.negSucc a✝ ∈ s

Tactic:
simpa [pow_succ'] using s.inv_mem (s.mul_mem hx (s.pow_mem hx _))

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Exact.lean
theorem exact_iff_of_forks {cg : KernelFork S.g} (hg : IsLimit cg) {cf : CokernelCofork S.f}
    (hf : IsColimit cf) : S.Exact ↔ cg.ι ≫ cf.π = 0

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
⊢ Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom

Tactic:
have eq₁ := IsLimit.conePointUniqueUpToIso_inv_comp (kernelIsKernel S.g) hg (.zero)

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
cg : KernelFork S.g
hg : IsLimit cg
cf : CokernelCofork S.f
hf : IsColimit cf
e₁ : (Fork.ofι (kernel.ι S.g) ⋯).pt ≅ cg.pt := (kernelIsKernel S.g).conePointUniqueUpToIso hg
e₂ : (Cofork.ofπ (cokernel.π S.f) ⋯).pt ≅ cf.pt := (cokernelIsCokernel S.f).coconePointUniqueUpToIso hf
eq₁ :
  ((kernelIsKernel S.g).conePointUniqueUpToIso hg).inv ≫ (Fork.ofι (kernel.ι S.g) ⋯).π.app WalkingParallelPair.zero =
    cg.π.app WalkingParallelPair.zero
⊢ Fork.ι cg ≫ Cofork.π cf = e₁.inv ≫ kernel.ι S.g ≫ cokernel.π S.f ≫ e₂.hom
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_neg_eq_arg_sub_pi_of_im_pos {x : ℂ} (hi : 0 < x.im) : arg (-x) = arg x - π

Proof state:
x : ℂ
hi : 0 < x.im
⊢ -Real.arccos ((-x).re / ‖-x‖) = Real.arccos (x.re / ‖x‖) - π

Tactic:
simp [neg_div, Real.arccos_neg]

Result:
no goals

Proof state:
x : ℂ
hi : 0 < x.im
⊢ (-x).arg = x.arg - π

Tactic:
rw [arg_of_im_pos hi, arg_of_im_neg (show (-x).im < 0 from Left.neg_neg_iff.2 hi)]

Result:
x : ℂ
hi : 0 < x.im
⊢ -Real.arccos ((-x).re / ‖-x‖) = Real.arccos (x.re / ‖x‖) - π
-- Mathlib/Combinatorics/Enumerative/DyckWord.lean
lemma le_add_self (p q : DyckWord) : q ≤ p + q

Proof state:
case neg
p q : DyckWord
h : ¬p = 0
this : p.outsidePart.semilength < p.semilength
⊢ q ≤ p + q

Tactic:
exact (le_add_self p.outsidePart q).trans
  (Relation.ReflTransGen.single (Or.inr (outsidePart_add h).symm))

Result:
no goals

Proof state:
case neg
p q : DyckWord
h : ¬p = 0
⊢ q ≤ p + q

Tactic:
have := semilength_outsidePart_lt h

Result:
case neg
p q : DyckWord
h : ¬p = 0
this : p.outsidePart.semilength < p.semilength
⊢ q ≤ p + q

Proof state:
p q : DyckWord
⊢ q ≤ p + q

Tactic:
by_cases h : p = 0

Result:
case pos
p q : DyckWord
h : p = 0
⊢ q ≤ p + q

case neg
p q : DyckWord
h : ¬p = 0
⊢ q ≤ p + q

Proof state:
case pos
p q : DyckWord
h : p = 0
⊢ q ≤ p + q

Tactic:
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem unattach_reverse {p : α → Prop} {l : List { x // p x }} :
    l.reverse.unattach = l.unattach.reverse

Proof state:
α : Type u_1
p : α → Prop
l : List { x // p x }
⊢ l.reverse.unattach = l.unattach.reverse

Tactic:
simp [unattach, -map_subtype]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/SmallHom.lean
lemma equiv_equiv_symm (L : C ⥤ D) [L.IsLocalization W]
    (L' : C ⥤ D') [L'.IsLocalization W] (G : D ⥤ D')
    (e : L ⋙ G ≅ L') {X Y : C} [HasSmallLocalizedHom.{w} W X Y]
    (f : L.obj X ⟶ L.obj Y) :
    equiv W L' ((equiv W L).symm f) =
      e.inv.app X ≫ G.map f ≫ e.hom.app Y

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
D' : Type u₃
inst✝³ : Category.{v₃, u₃} D'
L : C ⥤ D
inst✝² : L.IsLocalization W
L' : C ⥤ D'
inst✝¹ : L'.IsLocalization W
G : D ⥤ D'
e : L ⋙ G ≅ L'
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
⊢ (homEquiv W L L') f = e.inv.app X ≫ G.map f ≫ e.hom.app Y

Tactic:
apply homEquiv_eq

Result:
no goals

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
D' : Type u₃
inst✝³ : Category.{v₃, u₃} D'
L : C ⥤ D
inst✝² : L.IsLocalization W
L' : C ⥤ D'
inst✝¹ : L'.IsLocalization W
G : D ⥤ D'
e : L ⋙ G ≅ L'
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
⊢ (equiv W L') ((equiv W L).symm f) = e.inv.app X ≫ G.map f ≫ e.hom.app Y

Tactic:
dsimp [equiv]

Result:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
D' : Type u₃
inst✝³ : Category.{v₃, u₃} D'
L : C ⥤ D
inst✝² : L.IsLocalization W
L' : C ⥤ D'
inst✝¹ : L'.IsLocalization W
G : D ⥤ D'
e : L ⋙ G ≅ L'
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
⊢ (homEquiv W W.Q L')
      ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) ((homEquiv W L W.Q) f))) =
    e.inv.app X ≫ G.map f ≫ e.hom.app Y

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
D' : Type u₃
inst✝³ : Category.{v₃, u₃} D'
L : C ⥤ D
inst✝² : L.IsLocalization W
L' : C ⥤ D'
inst✝¹ : L'.IsLocalization W
G : D ⥤ D'
e : L ⋙ G ≅ L'
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
⊢ (homEquiv W W.Q L')
      ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)).symm ((equivShrink (W.Q.obj X ⟶ W.Q.obj Y)) ((homEquiv W L W.Q) f))) =
    e.inv.app X ≫ G.map f ≫ e.hom.app Y

Tactic:
rw [Equiv.symm_apply_apply, homEquiv_trans]

Result:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
D' : Type u₃
inst✝³ : Category.{v₃, u₃} D'
L : C ⥤ D
inst✝² : L.IsLocalization W
L' : C ⥤ D'
inst✝¹ : L'.IsLocalization W
G : D ⥤ D'
e : L ⋙ G ≅ L'
X Y : C
inst✝ : HasSmallLocalizedHom W X Y
f : L.obj X ⟶ L.obj Y
⊢ (homEquiv W L L') f = e.inv.app X ≫ G.map f ≫ e.hom.app Y
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem cos_eq_zero_iff {θ : Angle} : cos θ = 0 ↔ θ = (π / 2 : ℝ) ∨ θ = (-π / 2 : ℝ)

Proof state:
θ : Angle
⊢ θ.cos = 0 ↔ θ = ↑(π / 2) ∨ θ = ↑(-π / 2)

Tactic:
rw [← cos_pi_div_two, ← cos_coe, cos_eq_iff_eq_or_eq_neg, ← coe_neg, ← neg_div]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem mul_comm (a b : Fin n) : a * b = b * a :=
  Fin.ext <| by rw [mul_def, mul_def, Nat.mul_comm]

Proof state:
n : Nat
a b : Fin n
⊢ ↑(a * b) = ↑(b * a)

Tactic:
rw [mul_def, mul_def, Nat.mul_comm]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem cardDistinctFactors_one : ω 1 = 0

Proof state:
⊢ ω 1 = 0

Tactic:
simp [cardDistinctFactors]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem head_support {G : SimpleGraph V} {a b : V} (p : G.Walk a b) :
    p.support.head (by simp) = a

Proof state:
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
a b : V
p : G.Walk a b
⊢ p.support ≠ []

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
⊢ p.support.head ⋯ = a

Tactic:
cases p <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Connected.lean
theorem IsColimit.pullback_zero_ext [HasZeroMorphisms C] [HasPullbacks C] [HasColimitsOfShape J C]
    [HasExactColimitsOfShape J C] {F : J ⥤ C} {c : Cocone F} (hc : IsColimit c) {X Y : C}
    {f : X ⟶ c.pt} {g : c.pt ⟶ Y} (hf : ∀ j, pullback.snd (c.ι.app j) f ≫ f ≫ g = 0) :
    f ≫ g = 0

Proof state:
J : Type w
inst✝⁶ : Category.{w', w} J
inst✝⁵ : IsConnected J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g : c.pt ⟶ Y
hf : ∀ (j : J), pullback.snd (c.ι.app j) f ≫ f ≫ g = 0
⊢ ∀ (j : J), pullback.snd (c.ι.app j) f ≫ f ≫ g = pullback.snd (c.ι.app j) f ≫ f ≫ 0

Tactic:
simpa using hf

Result:
no goals

Proof state:
J : Type w
inst✝⁶ : Category.{w', w} J
inst✝⁵ : IsConnected J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g : c.pt ⟶ Y
hf : ∀ (j : J), pullback.snd (c.ι.app j) f ≫ f ≫ g = 0
⊢ f ≫ g = 0

Tactic:
suffices f ≫ g = f ≫ 0 by simpa

Result:
J : Type w
inst✝⁶ : Category.{w', w} J
inst✝⁵ : IsConnected J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g : c.pt ⟶ Y
hf : ∀ (j : J), pullback.snd (c.ι.app j) f ≫ f ≫ g = 0
⊢ f ≫ g = f ≫ 0

Proof state:
J : Type w
inst✝⁶ : Category.{w', w} J
inst✝⁵ : IsConnected J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g : c.pt ⟶ Y
hf : ∀ (j : J), pullback.snd (c.ι.app j) f ≫ f ≫ g = 0
⊢ f ≫ g = f ≫ 0

Tactic:
exact hc.pullback_hom_ext (by simpa using hf)

Result:
no goals

Proof state:
J : Type w
inst✝⁶ : Category.{w', w} J
inst✝⁵ : IsConnected J
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasPullbacks C
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasExactColimitsOfShape J C
F : J ⥤ C
c : Cocone F
hc : IsColimit c
X Y : C
f : X ⟶ c.pt
g : c.pt ⟶ Y
hf : ∀ (j : J), pullback.snd (c.ι.app j) f ≫ f ≫ g = 0
this : f ≫ g = f ≫ 0
⊢ f ≫ g = 0

Tactic:
simpa

Result:
no goals