harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_congr {s₁ s₂ : Finset α} {f g : α → β} (h₁ : s₁ = s₂)
    (h₂ : ∀ x ∈ s₂, f x = g x) (comm) :
    noncommProd s₁ f comm =
      noncommProd s₂ g fun x hx y hy h => by
        dsimp only [Function.onFun]
        rw [← h₂ _ hx, ← h₂ _ hy]
        subst h₁
        exact comm hx hy h

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
⊢ s₁.noncommProd f comm = s₂.noncommProd g ⋯

Tactic:
simp_rw [noncommProd, Multiset.map_congr (congr_arg _ h₁) h₂]

Result:
no goals

Proof state:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (g x) (g y)

Tactic:
rw [← h₂ _ hx, ← h₂ _ hy]

Result:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (f x) (f y)

Proof state:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ (Commute on g) x y

Tactic:
dsimp only [Function.onFun]

Result:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (g x) (g y)

Proof state:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (f x) (f y)

Tactic:
subst h₁

Result:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ : Finset α
f g : α → β
comm : (↑s₁).Pairwise (Commute on f)
x y : α
h : x ≠ y
h₂ : ∀ x ∈ s₁, f x = g x
hx : x ∈ ↑s₁
hy : y ∈ ↑s₁
⊢ Commute (f x) (f y)

Proof state:
F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ : Finset α
f g : α → β
comm : (↑s₁).Pairwise (Commute on f)
x y : α
h : x ≠ y
h₂ : ∀ x ∈ s₁, f x = g x
hx : x ∈ ↑s₁
hy : y ∈ ↑s₁
⊢ Commute (f x) (f y)

Tactic:
exact comm hx hy h

Result:
no goals
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.smul_mem (hs : StarConvex 𝕜 0 s) (hx : x ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t)
    (ht₁ : t ≤ 1) : t • x ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 0 s
hx : x ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ t • x ∈ s

Tactic:
simpa using hs.add_smul_mem (by simpa using hx) ht₀ ht₁

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 0 s
hx : x ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ 0 + x ∈ s

Tactic:
simpa using hx

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem TendstoUniformlyOnFilter.uniformCauchySeqOnFilter (hF : TendstoUniformlyOnFilter F f p p') :
    UniformCauchySeqOnFilter F p p'

Proof state:
case intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈
        t ∧
      (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈
        t
⊢ ∀ (x : (ι × ι) × α),
    (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2,
            F (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.1
              (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).1.2) ∈
          t ∧
        (f (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2,
            F (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.1
              (((x.1, x.2, x.2).1.1, (x.1, x.2, x.2).2.1), (x.1, x.2, x.2).1.2, (x.1, x.2, x.2).2.2).2.2) ∈
          t →
      (F x.1.1 x.2, F x.1.2 x.2) ∈ u

Tactic:
simp only [and_imp, Prod.forall]

Result:
case intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈
        t ∧
      (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈
        t
⊢ ∀ (a b : ι) (b_1 : α), (f b_1, F a b_1) ∈ t → (f b_1, F b b_1) ∈ t → (F a b_1, F b b_1) ∈ u

Proof state:
case intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : t ○ t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈
        t ∧
      (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈
        t
n1 n2 : ι
x : α
hl : (f x, F n1 x) ∈ t
hr : (f x, F n2 x) ∈ t
⊢ (F n1 x, F n2 x) ∈ u

Tactic:
exact Set.mem_of_mem_of_subset (prod_mk_mem_compRel (htsymm hl) hr) htmem

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem ringEquivOfRingEquiv_symm {j : R ≃+* P} (H : M.map j.toMonoidHom = T) :
    (ringEquivOfRingEquiv S Q j H).symm =
      ringEquivOfRingEquiv Q S j.symm (show T.map j.symm.toMonoidHom = M by
        erw [← H, ← Submonoid.comap_equiv_eq_map_symm,
          Submonoid.comap_map_eq_of_injective j.injective]) := rfl

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
P : Type u_3
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
hg : ∀ (y : ↥M), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝² : CommSemiring Q
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
j : R ≃+* P
H : Submonoid.map j.toMonoidHom M = T
⊢ Submonoid.map j.symm.toMonoidHom T = M

Tactic:
erw [← H, ← Submonoid.comap_equiv_eq_map_symm,
  Submonoid.comap_map_eq_of_injective j.injective]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Defs.lean
theorem map_subtype_embedding_Ici (hp : ∀ ⦃a x⦄, a ≤ x → p a → p x) :
    (Ici a).map (Embedding.subtype p) = (Ici a : Finset α)

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Ici a) = Ici ↑a

Tactic:
rw [subtype_Ici_eq]

Result:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ici ↑a)) = Ici ↑a

Proof state:
α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ici ↑a)) = Ici ↑a

Tactic:
exact Finset.subtype_map_of_mem fun x hx => hp (mem_Ici.1 hx) a.prop

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem sUnion_mem_empty_univ {S : Set (Set α)} (h : S ⊆ {∅, univ}) :
    ⋃₀ S ∈ ({∅, univ} : Set (Set α))

Proof state:
α : Type u_1
S : Set (Set α)
h : S ⊆ {∅, univ}
⊢ ⋃₀ S ∈ {∅, univ}

Tactic:
simp only [mem_insert_iff, mem_singleton_iff, or_iff_not_imp_left, sUnion_eq_empty, not_forall]

Result:
α : Type u_1
S : Set (Set α)
h : S ⊆ {∅, univ}
⊢ (∃ x, ∃ (_ : x ∈ S), ¬x = ∅) → ⋃₀ S = univ

Proof state:
case intro.intro
α : Type u_1
S : Set (Set α)
h : S ⊆ {∅, univ}
hs : univ ∈ S
hne : ¬univ = ∅
⊢ ⋃₀ S = univ

Tactic:
exact univ_subset_iff.1 <| subset_sUnion_of_mem hs

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
S : Set (Set α)
h : S ⊆ {∅, univ}
s : Set α
hs : s ∈ S
hne : ¬s = ∅
⊢ ⋃₀ S = univ

Tactic:
obtain rfl : s = univ := (h hs).resolve_left hne

Result:
case intro.intro
α : Type u_1
S : Set (Set α)
h : S ⊆ {∅, univ}
hs : univ ∈ S
hne : ¬univ = ∅
⊢ ⋃₀ S = univ

Proof state:
α : Type u_1
S : Set (Set α)
h : S ⊆ {∅, univ}
⊢ (∃ x, ∃ (_ : x ∈ S), ¬x = ∅) → ⋃₀ S = univ

Tactic:
rintro ⟨s, hs, hne⟩

Result:
case intro.intro
α : Type u_1
S : Set (Set α)
h : S ⊆ {∅, univ}
s : Set α
hs : s ∈ S
hne : ¬s = ∅
⊢ ⋃₀ S = univ
-- Mathlib/Data/Matroid/Basic.lean
theorem Indep.exists_isBase_subset_union_isBase (hI : M.Indep I) (hB : M.IsBase B) :
    ∃ B', M.IsBase B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hB : M.IsBase B
B' : Set α
hB' : M.IsBasis B' (I ∪ B)
hIB' : I ⊆ B'
⊢ ∃ B', M.IsBase B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B

Tactic:
exact ⟨B', hB.isBase_of_isBasis_superset subset_union_right hB', hIB', hB'.subset⟩

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hB : M.IsBase B
⊢ ∃ B', M.IsBase B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B

Tactic:
obtain ⟨B', hB', hIB'⟩ := hI.subset_isBasis_of_subset <| subset_union_left (t := B)

Result:
case intro.intro
α : Type u_1
M : Matroid α
B I : Set α
hI : M.Indep I
hB : M.IsBase B
B' : Set α
hB' : M.IsBasis B' (I ∪ B)
hIB' : I ⊆ B'
⊢ ∃ B', M.IsBase B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsCircuit.rotate {u v : V} {c : G.Walk v v} (hc : c.IsCircuit)
    (h : u ∈ c.support) : (c.rotate h).IsCircuit

Proof state:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ v
hc : (cons h✝ p✝).IsCircuit
h : u ∈ (cons h✝ p✝).support
hn : (cons h✝ p✝).rotate h = nil
hn' : (cons h✝ p✝).length = nil.length
⊢ False

Tactic:
simp at hn'

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
hc : c.IsCircuit
h : u ∈ c.support
⊢ (c.rotate h).IsCircuit

Tactic:
refine ⟨hc.isTrail.rotate _, ?_⟩

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
hc : c.IsCircuit
h : u ∈ c.support
⊢ c.rotate h ≠ nil

Proof state:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
hc : nil.IsCircuit
h : u ∈ nil.support
⊢ nil.rotate h ≠ nil

Tactic:
exact (hc.ne_nil rfl).elim

Result:
no goals

Proof state:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ v
hc : (cons h✝ p✝).IsCircuit
h : u ∈ (cons h✝ p✝).support
hn : (cons h✝ p✝).rotate h = nil
⊢ False

Tactic:
have hn' := congr_arg length hn

Result:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ v
hc : (cons h✝ p✝).IsCircuit
h : u ∈ (cons h✝ p✝).support
hn : (cons h✝ p✝).rotate h = nil
hn' : ((cons h✝ p✝).rotate h).length = nil.length
⊢ False

Proof state:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ v
hc : (cons h✝ p✝).IsCircuit
h : u ∈ (cons h✝ p✝).support
⊢ (cons h✝ p✝).rotate h ≠ nil

Tactic:
intro hn

Result:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ v
hc : (cons h✝ p✝).IsCircuit
h : u ∈ (cons h✝ p✝).support
hn : (cons h✝ p✝).rotate h = nil
⊢ False

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
hc : c.IsCircuit
h : u ∈ c.support
⊢ c.rotate h ≠ nil

Tactic:
cases c

Result:
case nil
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
hc : nil.IsCircuit
h : u ∈ nil.support
⊢ nil.rotate h ≠ nil

case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ v
hc : (cons h✝ p✝).IsCircuit
h : u ∈ (cons h✝ p✝).support
⊢ (cons h✝ p✝).rotate h ≠ nil

Proof state:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ v
hc : (cons h✝ p✝).IsCircuit
h : u ∈ (cons h✝ p✝).support
hn : (cons h✝ p✝).rotate h = nil
hn' : ((cons h✝ p✝).rotate h).length = nil.length
⊢ False

Tactic:
rw [rotate, length_append, add_comm, ← length_append, take_spec] at hn'

Result:
case cons
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v v✝ : V
h✝ : G.Adj v v✝
p✝ : G.Walk v✝ v
hc : (cons h✝ p✝).IsCircuit
h : u ∈ (cons h✝ p✝).support
hn : (cons h✝ p✝).rotate h = nil
hn' : (cons h✝ p✝).length = nil.length
⊢ False
-- Mathlib/Order/Heyting/Basic.lean
theorem le_himp_iff' : a ≤ b ⇨ c ↔ b ⊓ a ≤ c

Proof state:
α : Type u_2
inst✝ : GeneralizedHeytingAlgebra α
a b c : α
⊢ a ≤ b ⇨ c ↔ b ⊓ a ≤ c

Tactic:
rw [le_himp_iff, inf_comm]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem toWithTop_le {x y : PartENat} [hx : Decidable x.Dom] [hy : Decidable y.Dom] :
    toWithTop x ≤ toWithTop y ↔ x ≤ y

Proof state:
case a.a
n✝ : ℕ
hy : Decidable (↑n✝).Dom
hx : Decidable ⊤.Dom
⊢ ⊤.toWithTop ≤ (↑n✝).toWithTop ↔ ⊤ ≤ ↑n✝

Tactic:
simp

Result:
no goals

Proof state:
case a
x : PartENat
hx : Decidable x.Dom
hy : Decidable ⊤.Dom
⊢ x.toWithTop ≤ ⊤.toWithTop ↔ x ≤ ⊤

Tactic:
simp

Result:
no goals

Proof state:
case a
x : PartENat
hx : Decidable x.Dom
n✝ : ℕ
hy : Decidable (↑n✝).Dom
⊢ x.toWithTop ≤ (↑n✝).toWithTop ↔ x ≤ ↑n✝

Tactic:
induction x using PartENat.casesOn generalizing hx

Result:
case a.a
n✝ : ℕ
hy : Decidable (↑n✝).Dom
hx : Decidable ⊤.Dom
⊢ ⊤.toWithTop ≤ (↑n✝).toWithTop ↔ ⊤ ≤ ↑n✝

case a.a
n✝¹ : ℕ
hy : Decidable (↑n✝¹).Dom
n✝ : ℕ
hx : Decidable (↑n✝).Dom
⊢ (↑n✝).toWithTop ≤ (↑n✝¹).toWithTop ↔ ↑n✝ ≤ ↑n✝¹

Proof state:
case a.a
n✝¹ : ℕ
hy : Decidable (↑n✝¹).Dom
n✝ : ℕ
hx : Decidable (↑n✝).Dom
⊢ (↑n✝).toWithTop ≤ (↑n✝¹).toWithTop ↔ ↑n✝ ≤ ↑n✝¹

Tactic:
simp

Result:
no goals

Proof state:
x y : PartENat
hx : Decidable x.Dom
hy : Decidable y.Dom
⊢ x.toWithTop ≤ y.toWithTop ↔ x ≤ y

Tactic:
induction y using PartENat.casesOn generalizing hy

Result:
case a
x : PartENat
hx : Decidable x.Dom
hy : Decidable ⊤.Dom
⊢ x.toWithTop ≤ ⊤.toWithTop ↔ x ≤ ⊤

case a
x : PartENat
hx : Decidable x.Dom
n✝ : ℕ
hy : Decidable (↑n✝).Dom
⊢ x.toWithTop ≤ (↑n✝).toWithTop ↔ x ≤ ↑n✝
-- Mathlib/Data/Finset/Insert.lean
theorem coe_insert (a : α) (s : Finset α) : ↑(insert a s) = (insert a s : Set α) :=
  Set.ext fun x => by simp only [mem_coe, mem_insert, Set.mem_insert_iff]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
x : α
⊢ x ∈ ↑(insert a s) ↔ x ∈ insert a ↑s

Tactic:
simp only [mem_coe, mem_insert, Set.mem_insert_iff]

Result:
no goals
-- Mathlib/Analysis/Complex/ReImTopology.lean
theorem frontier_setOf_im_lt (a : ℝ) : frontier { z : ℂ | z.im < a } = { z | z.im = a }

Proof state:
a : ℝ
⊢ frontier {z | z.im < a} = {z | z.im = a}

Tactic:
simpa only [frontier_Iio] using frontier_preimage_im (Iio a)

Result:
no goals
-- Mathlib/CategoryTheory/Filtered/Final.lean
theorem Functor.final_of_exists_of_isFiltered [IsFilteredOrEmpty C]
    (h₁ : ∀ d, ∃ c, Nonempty (d ⟶ F.obj c)) (h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c),
      ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t) : Functor.Final F

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
h₁ : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
⊢ F.Final

Tactic:
suffices ∀ d, IsFiltered (StructuredArrow d F) from final_of_isFiltered_structuredArrow F

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
h₁ : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
⊢ ∀ (d : D), IsFiltered (StructuredArrow d F)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
h₁ : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {d : D} {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
⊢ ∀ (d : D), IsFiltered (StructuredArrow d F)

Tactic:
exact isFiltered_structuredArrow_of_isFiltered_of_exists F h₁ h₂

Result:
no goals
-- Mathlib/LinearAlgebra/Projection.lean
theorem IsProj.eq_conj_prodMap {f : E →ₗ[R] E} (h : IsProj p f) :
    f = (p.prodEquivOfIsCompl (ker f) h.isCompl).conj (prodMap id 0)

Proof state:
R : Type u_1
inst✝² : CommRing R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f = (↑(p.prodEquivOfIsCompl (ker f) ⋯) ∘ₗ id.prodMap 0) ∘ₗ ↑(p.prodEquivOfIsCompl (ker f) ⋯).symm

Tactic:
exact h.eq_conj_prod_map'

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f = (p.prodEquivOfIsCompl (ker f) ⋯).conj (id.prodMap 0)

Tactic:
rw [LinearEquiv.conj_apply]

Result:
R : Type u_1
inst✝² : CommRing R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f = (↑(p.prodEquivOfIsCompl (ker f) ⋯) ∘ₗ id.prodMap 0) ∘ₗ ↑(p.prodEquivOfIsCompl (ker f) ⋯).symm
-- Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
theorem initial.to_comp [HasInitial C] {P Q : C} (f : P ⟶ Q) : initial.to P ≫ f = initial.to Q

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasInitial C
P Q : C
f : P ⟶ Q
⊢ «to» P ≫ f = «to» Q

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean
theorem quadraticCharFun_eq_pow_of_char_ne_two (hF : ringChar F ≠ 2) {a : F} (ha : a ≠ 0) :
    quadraticCharFun F a = if a ^ (Fintype.card F / 2) = 1 then 1 else -1

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ quadraticCharFun F a = if a ^ (Fintype.card F / 2) = 1 then 1 else -1

Tactic:
simp only [quadraticCharFun, ha, if_false]

Result:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (if IsSquare a then 1 else -1) = if a ^ (Fintype.card F / 2) = 1 then 1 else -1

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Fintype F
inst✝ : DecidableEq F
hF : ringChar F ≠ 2
a : F
ha : a ≠ 0
⊢ (if IsSquare a then 1 else -1) = if a ^ (Fintype.card F / 2) = 1 then 1 else -1

Tactic:
simp_rw [FiniteField.isSquare_iff hF ha]

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
@[simp]
lemma singleton_biUnion {a : α} : Finset.biUnion {a} t = t a

Proof state:
α : Type u_1
β : Type u_2
t : α → Finset β
inst✝ : DecidableEq β
a : α
⊢ {a}.biUnion t = t a

Tactic:
classical rw [← insert_emptyc_eq, biUnion_insert, biUnion_empty, union_empty]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
t : α → Finset β
inst✝ : DecidableEq β
a : α
⊢ {a}.biUnion t = t a

Tactic:
rw [← insert_emptyc_eq, biUnion_insert, biUnion_empty, union_empty]

Result:
no goals
-- Mathlib/Topology/Bornology/Basic.lean
theorem isBounded_singleton : IsBounded ({x} : Set α)

Proof state:
α : Type u_2
x✝ : Bornology α
x : α
⊢ {x}ᶜ ∈ cobounded α

Tactic:
exact le_cofinite _ (finite_singleton x).compl_mem_cofinite

Result:
no goals

Proof state:
α : Type u_2
x✝ : Bornology α
x : α
⊢ IsBounded {x}

Tactic:
rw [isBounded_def]

Result:
α : Type u_2
x✝ : Bornology α
x : α
⊢ {x}ᶜ ∈ cobounded α
-- Mathlib/MeasureTheory/Measure/Content.lean
theorem is_mul_left_invariant_outerMeasure [Group G] [IsTopologicalGroup G]
    (h : ∀ (g : G) {K : Compacts G}, μ (K.map _ <| continuous_mul_left g) = μ K) (g : G)
    (A : Set G) : μ.outerMeasure ((g * ·) ⁻¹' A) = μ.outerMeasure A

Proof state:
G : Type w
inst✝³ : TopologicalSpace G
μ : Content G
inst✝² : R1Space G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
h : ∀ (g : G) {K : Compacts G}, μ (Compacts.map (fun b => g * b) ⋯ K) = μ K
g : G
A : Set G
⊢ μ.outerMeasure ((fun x => g * x) ⁻¹' A) = μ.outerMeasure A

Tactic:
convert μ.outerMeasure_preimage (Homeomorph.mulLeft g) (fun K => h g) A

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem IsUniformInducing.comp {g : β → γ} (hg : IsUniformInducing g) {f : α → β}
    (hf : IsUniformInducing f) : IsUniformInducing (g ∘ f) :=
  ⟨by rw [← hf.1, ← hg.1, comap_comap]; rfl⟩

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
hf : IsUniformInducing f
⊢ comap (fun x => ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ) = comap ((fun x => (g x.1, g x.2)) ∘ fun x => (f x.1, f x.2)) (𝓤 γ)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
hf : IsUniformInducing f
⊢ comap (fun x => ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ) = 𝓤 α

Tactic:
rw [← hf.1, ← hg.1, comap_comap]

Result:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : IsUniformInducing g
f : α → β
hf : IsUniformInducing f
⊢ comap (fun x => ((g ∘ f) x.1, (g ∘ f) x.2)) (𝓤 γ) = comap ((fun x => (g x.1, g x.2)) ∘ fun x => (f x.1, f x.2)) (𝓤 γ)
-- Mathlib/Order/Basic.lean
lemma ltByCases_comm {h₁ : x < y → P} {h₂ : x = y → P} {h₃ : y < x → P}
    (p : y = x → x = y := fun h' => h'.symm) :
    ltByCases x y h₁ h₂ h₃ = ltByCases y x h₃ (h₂ ∘ p) h₁

Proof state:
case refine_1
α : Type u_2
inst✝ : LinearOrder α
P : Sort u_5
x y : α
h₁ : x < y → P
h₂ : x = y → P
h₃ : y < x → P
p : optParam (y = x → x = y) ⋯
h : x < y
⊢ ltByCases x y h₁ h₂ h₃ = ltByCases y x h₃ (h₂ ∘ p) h₁

Tactic:
rw [ltByCases_lt h, ltByCases_gt h]

Result:
no goals

Proof state:
case refine_3
α : Type u_2
inst✝ : LinearOrder α
P : Sort u_5
x y : α
h₁ : x < y → P
h₂ : x = y → P
h₃ : y < x → P
p : optParam (y = x → x = y) ⋯
h : y < x
⊢ ltByCases x y h₁ h₂ h₃ = ltByCases y x h₃ (h₂ ∘ p) h₁

Tactic:
rw [ltByCases_lt h, ltByCases_gt h]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
P : Sort u_5
x y : α
h₁ : x < y → P
h₂ : x = y → P
h₃ : y < x → P
p : optParam (y = x → x = y) ⋯
⊢ ltByCases x y h₁ h₂ h₃ = ltByCases y x h₃ (h₂ ∘ p) h₁

Tactic:
refine ltByCases x y (fun h => ?_) (fun h => ?_) (fun h => ?_)

Result:
case refine_1
α : Type u_2
inst✝ : LinearOrder α
P : Sort u_5
x y : α
h₁ : x < y → P
h₂ : x = y → P
h₃ : y < x → P
p : optParam (y = x → x = y) ⋯
h : x < y
⊢ ltByCases x y h₁ h₂ h₃ = ltByCases y x h₃ (h₂ ∘ p) h₁

case refine_2
α : Type u_2
inst✝ : LinearOrder α
P : Sort u_5
x y : α
h₁ : x < y → P
h₂ : x = y → P
h₃ : y < x → P
p : optParam (y = x → x = y) ⋯
h : x = y
⊢ ltByCases x y h₁ h₂ h₃ = ltByCases y x h₃ (h₂ ∘ p) h₁

case refine_3
α : Type u_2
inst✝ : LinearOrder α
P : Sort u_5
x y : α
h₁ : x < y → P
h₂ : x = y → P
h₃ : y < x → P
p : optParam (y = x → x = y) ⋯
h : y < x
⊢ ltByCases x y h₁ h₂ h₃ = ltByCases y x h₃ (h₂ ∘ p) h₁

Proof state:
case refine_2
α : Type u_2
inst✝ : LinearOrder α
P : Sort u_5
x y : α
h₁ : x < y → P
h₂ : x = y → P
h₃ : y < x → P
p : optParam (y = x → x = y) ⋯
h : x = y
⊢ ltByCases x y h₁ h₂ h₃ = ltByCases y x h₃ (h₂ ∘ p) h₁

Tactic:
rw [ltByCases_eq h, ltByCases_eq h.symm, comp_apply]

Result:
no goals