harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/UniformSpace/Completion.lean
theorem uniformContinuous_extend {f : α → β} : UniformContinuous (extend f)

Proof state:
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : ¬UniformContinuous f
a _b : CauchyFilter α
⊢ f ⋯.some = f ⋯.some

Tactic:
congr

Result:
no goals

Proof state:
case pos
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (extend f)

Tactic:
rw [extend, if_pos hf]

Result:
case pos
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (⋯.extend f)

Proof state:
case neg
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (extend f)

Tactic:
rw [extend, if_neg hf]

Result:
case neg
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous fun x => f ⋯.some

Proof state:
case pos
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (⋯.extend f)

Tactic:
exact uniformContinuous_uniformly_extend isUniformInducing_pureCauchy denseRange_pureCauchy hf

Result:
no goals

Proof state:
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
⊢ UniformContinuous (extend f)

Tactic:
by_cases hf : UniformContinuous f

Result:
case pos
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (extend f)

case neg
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (extend f)

Proof state:
case neg
α : Type u
inst✝² : UniformSpace α
β : Type v
inst✝¹ : UniformSpace β
inst✝ : CompleteSpace β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous fun x => f ⋯.some

Tactic:
exact uniformContinuous_of_const fun a _b => by congr

Result:
no goals
-- Mathlib/Order/Fin/Tuple.lean
@[simp] lemma insertNthOrderIso_zero (α : Fin (n + 1) → Type*) [∀ i, LE (α i)] :
    insertNthOrderIso α 0 = consOrderIso α

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_2
inst✝ : (i : Fin (n + 1)) → LE (α i)
⊢ insertNthOrderIso α 0 = consOrderIso α

Tactic:
ext

Result:
case h.h.h
n : ℕ
α : Fin (n + 1) → Type u_2
inst✝ : (i : Fin (n + 1)) → LE (α i)
x✝¹ : α 0 × ((i : Fin n) → α (succAbove 0 i))
x✝ : Fin (n + 1)
⊢ (insertNthOrderIso α 0) x✝¹ x✝ = (consOrderIso α) x✝¹ x✝

Proof state:
case h.h.h
n : ℕ
α : Fin (n + 1) → Type u_2
inst✝ : (i : Fin (n + 1)) → LE (α i)
x✝¹ : α 0 × ((i : Fin n) → α (succAbove 0 i))
x✝ : Fin (n + 1)
⊢ (insertNthOrderIso α 0) x✝¹ x✝ = (consOrderIso α) x✝¹ x✝

Tactic:
simp [insertNthOrderIso]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem lift_uniq (H' : Set.range g.base ⊆ Set.range f.base) (l : Y ⟶ X) (hl : l ≫ f = g) :
    l = lift f g H'

Proof state:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
l : Y ⟶ X
hl : l ≫ f = g
⊢ l = lift f g H'

Tactic:
rw [← cancel_mono f, hl, lift_fac]

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem biUnion_Ioc_eq_Ioi_self_iff {p : ι → Prop} {f : ∀ i, p i → α} {a : α} :
    ⋃ (i) (hi : p i), Ioc a (f i hi) = Ioi a ↔ ∀ x, a < x → ∃ i hi, x ≤ f i hi

Proof state:
ι : Sort u
α : Type v
inst✝ : LinearOrder α
p : ι → Prop
f : (i : ι) → p i → α
a : α
⊢ ⋃ i, ⋃ (hi : p i), Ioc a (f i hi) = Ioi a ↔ ∀ (x : α), a < x → ∃ i, ∃ (hi : p i), x ≤ f i hi

Tactic:
simp [← Ioi_inter_Iic, ← inter_iUnion, subset_def]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/Supported.lean
theorem disjoint_supported_supported_iff [Nontrivial M] {s t : Set α} :
    Disjoint (supported M R s) (supported M R t) ↔ Disjoint s t

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : Disjoint (supported M R s) (supported M R t)
x : α
hx1 : x ∈ s
hx2 : x ∈ t
⊢ False

Tactic:
rcases exists_ne (0 : M) with ⟨y, hy⟩

Result:
case intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : Disjoint (supported M R s) (supported M R t)
x : α
hx1 : x ∈ s
hx2 : x ∈ t
y : M
hy : y ≠ 0
⊢ False

Proof state:
case intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : Disjoint (supported M R s) (supported M R t)
x : α
hx1 : x ∈ s
hx2 : x ∈ t
y : M
hy : y ≠ 0
this : single x y ∈ ⊥
⊢ False

Tactic:
rw [mem_bot, single_eq_zero] at this

Result:
case intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : Disjoint (supported M R s) (supported M R t)
x : α
hx1 : x ∈ s
hx2 : x ∈ t
y : M
hy : y ≠ 0
this : y = 0
⊢ False

Proof state:
case intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : Disjoint (supported M R s) (supported M R t)
x : α
hx1 : x ∈ s
hx2 : x ∈ t
y : M
hy : y ≠ 0
⊢ False

Tactic:
have := h.le_bot ⟨single_mem_supported R y hx1, single_mem_supported R y hx2⟩

Result:
case intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : Disjoint (supported M R s) (supported M R t)
x : α
hx1 : x ∈ s
hx2 : x ∈ t
y : M
hy : y ≠ 0
this : single x y ∈ ⊥
⊢ False

Proof state:
case intro
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : Disjoint (supported M R s) (supported M R t)
x : α
hx1 : x ∈ s
hx2 : x ∈ t
y : M
hy : y ≠ 0
this : y = 0
⊢ False

Tactic:
exact hy this

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
⊢ Disjoint (supported M R s) (supported M R t) ↔ Disjoint s t

Tactic:
refine ⟨fun h => Set.disjoint_left.mpr fun x hx1 hx2 => ?_, disjoint_supported_supported⟩

Result:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
s t : Set α
h : Disjoint (supported M R s) (supported M R t)
x : α
hx1 : x ∈ s
hx2 : x ∈ t
⊢ False
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem UniformCauchySeqOn.prod_map {ι' α' β' : Type*} [UniformSpace β'] {F' : ι' → α' → β'}
    {p' : Filter ι'} {s' : Set α'} (h : UniformCauchySeqOn F p s)
    (h' : UniformCauchySeqOn F' p' s') :
    UniformCauchySeqOn (fun i : ι × ι' => Prod.map (F i.1) (F' i.2)) (p ×ˢ p') (s ×ˢ s')

Proof state:
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : v ×ˢ w ⊆ (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F m.1.1 a, F' m.1.2 b), F m.2.1 a, F' m.2.2 b) ∈ u

Tactic:
rw [← Set.image_subset_iff] at hvw

Result:
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) '' v ×ˢ w ⊆ u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F m.1.1 a, F' m.1.2 b), F m.2.1 a, F' m.2.2 b) ∈ u

Proof state:
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : v ×ˢ w ⊆ (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ x ∈ s ×ˢ s', ((fun i => Prod.map (F i.1) (F' i.2)) m.1 x, (fun i => Prod.map (F i.1) (F' i.2)) m.2 x) ∈ u

Tactic:
simp_rw [mem_prod, and_imp, Prod.forall, Prod.map_apply]

Result:
case intro.intro.intro.intro
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
s : Set α
p : Filter ι
ι' : Type u_1
α' : Type u_2
β' : Type u_3
inst✝ : UniformSpace β'
F' : ι' → α' → β'
p' : Filter ι'
s' : Set α'
h : UniformCauchySeqOn F p s
h' : UniformCauchySeqOn F' p' s'
u : Set ((β × β') × β × β')
v : Set (β × β)
hv : v ∈ 𝓤 β
w : Set (β' × β')
hw : w ∈ 𝓤 β'
hvw : v ×ˢ w ⊆ (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' u
⊢ ∀ᶠ (m : (ι × ι') × ι × ι') in (p ×ˢ p') ×ˢ p ×ˢ p',
    ∀ (a : α) (b : α'), a ∈ s → b ∈ s' → ((F m.1.1 a, F' m.1.2 b), F m.2.1 a, F' m.2.2 b) ∈ u
-- Mathlib/Algebra/Module/Torsion.lean
theorem torsionBySet_eq_torsionBySet_span :
    torsionBySet R M s = torsionBySet R M (Ideal.span s)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
hx : x ∈ torsionBySet R M s
⊢ x ∈ torsionBySet R M ↑(Ideal.span s)

Tactic:
rw [mem_torsionBySet_iff] at hx ⊢

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ ∀ (a : ↑↑(Ideal.span s)), ↑a • x = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
this : Ideal.span s ≤ Ideal.torsionOf R M x
⊢ ∀ (a : ↑↑(Ideal.span s)), ↑a • x = 0

Tactic:
rintro ⟨a, ha⟩

Result:
case mk
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
this : Ideal.span s ≤ Ideal.torsionOf R M x
a : R
ha : a ∈ ↑(Ideal.span s)
⊢ ↑⟨a, ha⟩ • x = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ ∀ (a : ↑↑(Ideal.span s)), ↑a • x = 0

Tactic:
suffices Ideal.span s ≤ Ideal.torsionOf R M x by
  rintro ⟨a, ha⟩
  exact this ha

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ Ideal.span s ≤ Ideal.torsionOf R M x

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ Ideal.span s ≤ Ideal.torsionOf R M x

Tactic:
rw [Ideal.span_le]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ s ⊆ ↑(Ideal.torsionOf R M x)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
⊢ torsionBySet R M s = torsionBySet R M ↑(Ideal.span s)

Tactic:
refine le_antisymm (fun x hx => ?_) (torsionBySet_le_torsionBySet_of_subset subset_span)

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
hx : x ∈ torsionBySet R M s
⊢ x ∈ torsionBySet R M ↑(Ideal.span s)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ s ⊆ ↑(Ideal.torsionOf R M x)

Tactic:
exact fun a ha => hx ⟨a, ha⟩

Result:
no goals

Proof state:
case mk
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
hx : ∀ (a : ↑s), ↑a • x = 0
this : Ideal.span s ≤ Ideal.torsionOf R M x
a : R
ha : a ∈ ↑(Ideal.span s)
⊢ ↑⟨a, ha⟩ • x = 0

Tactic:
exact this ha

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem insert_append {l₁ l₂ : List α} {a : α} :
    (l₁ ++ l₂).insert a = if a ∈ l₂ then l₁ ++ l₂ else l₁.insert a ++ l₂

Proof state:
case isTrue
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
h✝ : a ∈ l₁ ∨ a ∈ l₂
⊢ l₁ ++ l₂ = if a ∈ l₂ then l₁ ++ l₂ else (if a ∈ l₁ then l₁ else a :: l₁) ++ l₂

case isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
h✝ : ¬(a ∈ l₁ ∨ a ∈ l₂)
⊢ a :: (l₁ ++ l₂) = if a ∈ l₂ then l₁ ++ l₂ else (if a ∈ l₁ then l₁ else a :: l₁) ++ l₂

Tactic:
split

Result:
case isTrue.isTrue
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
h✝¹ : a ∈ l₁ ∨ a ∈ l₂
h✝ : a ∈ l₂
⊢ l₁ ++ l₂ = l₁ ++ l₂

case isTrue.isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
h✝¹ : a ∈ l₁ ∨ a ∈ l₂
h✝ : ¬a ∈ l₂
⊢ l₁ ++ l₂ = (if a ∈ l₁ then l₁ else a :: l₁) ++ l₂

case isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
h✝ : ¬(a ∈ l₁ ∨ a ∈ l₂)
⊢ a :: (l₁ ++ l₂) = if a ∈ l₂ then l₁ ++ l₂ else (if a ∈ l₁ then l₁ else a :: l₁) ++ l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
⊢ (if a ∈ l₁ ∨ a ∈ l₂ then l₁ ++ l₂ else a :: (l₁ ++ l₂)) =
    if a ∈ l₂ then l₁ ++ l₂ else (if a ∈ l₁ then l₁ else a :: l₁) ++ l₂

Tactic:
repeat split

Result:
case isTrue.isTrue
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
h✝¹ : a ∈ l₁ ∨ a ∈ l₂
h✝ : a ∈ l₂
⊢ l₁ ++ l₂ = l₁ ++ l₂

case isTrue.isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
h✝¹ : a ∈ l₁ ∨ a ∈ l₂
h✝ : ¬a ∈ l₂
⊢ l₁ ++ l₂ = (if a ∈ l₁ then l₁ else a :: l₁) ++ l₂

case isFalse
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
h✝ : ¬(a ∈ l₁ ∨ a ∈ l₂)
⊢ a :: (l₁ ++ l₂) = if a ∈ l₂ then l₁ ++ l₂ else (if a ∈ l₁ then l₁ else a :: l₁) ++ l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
⊢ List.insert a (l₁ ++ l₂) = if a ∈ l₂ then l₁ ++ l₂ else List.insert a l₁ ++ l₂

Tactic:
simp only [insert_eq, mem_append]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
⊢ (if a ∈ l₁ ∨ a ∈ l₂ then l₁ ++ l₂ else a :: (l₁ ++ l₂)) =
    if a ∈ l₂ then l₁ ++ l₂ else (if a ∈ l₁ then l₁ else a :: l₁) ++ l₂

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l₁ l₂ : List α
a : α
⊢ (if a ∈ l₁ ∨ a ∈ l₂ then l₁ ++ l₂ else a :: (l₁ ++ l₂)) =
    if a ∈ l₂ then l₁ ++ l₂ else (if a ∈ l₁ then l₁ else a :: l₁) ++ l₂

Tactic:
(repeat split) <;> simp_all

Result:
no goals
-- Mathlib/NumberTheory/Modular.lean
theorem eq_zero_of_mem_fdo_of_T_zpow_mem_fdo {n : ℤ} (hz : z ∈ 𝒟ᵒ) (hg : T ^ n • z ∈ 𝒟ᵒ) :
    n = 0

Proof state:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
h₁ : |z.re| < 1 / 2
h₂ : |z.re + ↑n| < 1 / 2
⊢ |↑n| < 1

Tactic:
calc
  |(n : ℝ)| ≤ |z.re| + |z.re + (n : ℝ)| := abs_add' (n : ℝ) z.re
  _ < 1 / 2 + 1 / 2 := add_lt_add h₁ h₂
  _ = 1 := add_halves 1

Result:
no goals

Proof state:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
⊢ |↑n| < 1

Tactic:
have h₁ := hz.2

Result:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
h₁ : |z.re| < 1 / 2
⊢ |↑n| < 1

Proof state:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
h₁ : |z.re| < 1 / 2
h₂ : |(T ^ n • z).re| < 1 / 2
⊢ |↑n| < 1

Tactic:
rw [re_T_zpow_smul] at h₂

Result:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
h₁ : |z.re| < 1 / 2
h₂ : |z.re + ↑n| < 1 / 2
⊢ |↑n| < 1

Proof state:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
h₁ : |z.re| < 1 / 2
⊢ |↑n| < 1

Tactic:
have h₂ := hg.2

Result:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
h₁ : |z.re| < 1 / 2
h₂ : |(T ^ n • z).re| < 1 / 2
⊢ |↑n| < 1

Proof state:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
⊢ n = 0

Tactic:
suffices |(n : ℝ)| < 1 by
  rwa [← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff] at this

Result:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
⊢ |↑n| < 1

Proof state:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
this : |↑n| < 1
⊢ n = 0

Tactic:
rwa [← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff] at this

Result:
no goals
-- Mathlib/Data/Setoid/Partition.lean
theorem eq_eqv_class_of_mem {c : Set (Set α)} (H : ∀ a, ∃! b ∈ c, a ∈ b) {s y}
    (hs : s ∈ c) (hy : y ∈ s) : s = { x | mkClasses c H x y }

Proof state:
case h.mp
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
hx : x ∈ s
_s' : Set α
hs' : _s' ∈ c
hx' : x ∈ _s'
⊢ y ∈ _s'

Tactic:
rwa [eq_of_mem_eqv_class H hs' hx' hs hx]

Result:
no goals

Proof state:
case h.mp
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ s → x ∈ {x | (mkClasses c H) x y}

Tactic:
intro hx _s' hs' hx'

Result:
case h.mp
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
hx : x ∈ s
_s' : Set α
hs' : _s' ∈ c
hx' : x ∈ _s'
⊢ y ∈ _s'

Proof state:
case h.mpr.intro.intro.intro
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
hx : x ∈ {x | (mkClasses c H) x y}
b' : Set α
right✝ : ∀ (y : Set α), (fun b => b ∈ c ∧ x ∈ b) y → y = b'
hc : b' ∈ c
hb' : x ∈ b'
⊢ x ∈ s

Tactic:
rwa [eq_of_mem_eqv_class H hs hy hc (hx b' hc hb')]

Result:
no goals

Proof state:
case h.mpr
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
hx : x ∈ {x | (mkClasses c H) x y}
⊢ x ∈ s

Tactic:
obtain ⟨b', ⟨hc, hb'⟩, _⟩ := H x

Result:
case h.mpr.intro.intro.intro
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
hx : x ∈ {x | (mkClasses c H) x y}
b' : Set α
right✝ : ∀ (y : Set α), (fun b => b ∈ c ∧ x ∈ b) y → y = b'
hc : b' ∈ c
hb' : x ∈ b'
⊢ x ∈ s

Proof state:
case h.mpr
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ {x | (mkClasses c H) x y} → x ∈ s

Tactic:
intro hx

Result:
case h.mpr
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
hx : x ∈ {x | (mkClasses c H) x y}
⊢ x ∈ s

Proof state:
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
⊢ s = {x | (mkClasses c H) x y}

Tactic:
ext x

Result:
case h
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ s ↔ x ∈ {x | (mkClasses c H) x y}

Proof state:
case h
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ s ↔ x ∈ {x | (mkClasses c H) x y}

Tactic:
constructor

Result:
case h.mp
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ s → x ∈ {x | (mkClasses c H) x y}

case h.mpr
α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
s : Set α
y : α
hs : s ∈ c
hy : y ∈ s
x : α
⊢ x ∈ {x | (mkClasses c H) x y} → x ∈ s
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem factors_mul (a b : Associates α) : (a * b).factors = a.factors + b.factors

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
a✝ : Nontrivial α
⊢ (a * b).factors = a.factors + b.factors

Tactic:
refine eq_of_prod_eq_prod <| eq_of_factors_eq_factors ?_

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
a✝ : Nontrivial α
⊢ (a * b).factors.prod.factors = (a.factors + b.factors).prod.factors

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
a✝ : Nontrivial α
⊢ (a * b).factors.prod.factors = (a.factors + b.factors).prod.factors

Tactic:
rw [prod_add, factors_prod, factors_prod, factors_prod]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
⊢ (a * b).factors = a.factors + b.factors

Tactic:
nontriviality α

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : Associates α
a✝ : Nontrivial α
⊢ (a * b).factors = a.factors + b.factors
-- Mathlib/Analysis/Calculus/Deriv/ZPow.lean
theorem deriv_zpow (m : ℤ) (x : 𝕜) : deriv (fun x => x ^ m) x = m * x ^ (m - 1)

Proof state:
case pos
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : x ≠ 0 ∨ 0 ≤ m
⊢ deriv (fun x => x ^ m) x = ↑m * x ^ (m - 1)

Tactic:
exact (hasDerivAt_zpow m x H).deriv

Result:
no goals

Proof state:
case neg
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : ¬(x ≠ 0 ∨ 0 ≤ m)
⊢ 0 = ↑m * x ^ (m - 1)

Tactic:
push_neg at H

Result:
case neg
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : x = 0 ∧ m < 0
⊢ 0 = ↑m * x ^ (m - 1)

Proof state:
case neg.intro
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
hm : m < 0
⊢ 0 = ↑m * 0 ^ (m - 1)

Tactic:
rw [zero_zpow _ ((sub_one_lt _).trans hm).ne, mul_zero]

Result:
no goals

Proof state:
case neg
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : x = 0 ∧ m < 0
⊢ 0 = ↑m * x ^ (m - 1)

Tactic:
rcases H with ⟨rfl, hm⟩

Result:
case neg.intro
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
hm : m < 0
⊢ 0 = ↑m * 0 ^ (m - 1)

Proof state:
case neg
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : ¬(x ≠ 0 ∨ 0 ≤ m)
⊢ deriv (fun x => x ^ m) x = ↑m * x ^ (m - 1)

Tactic:
rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_zpow.1 H)]

Result:
case neg
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : ¬(x ≠ 0 ∨ 0 ≤ m)
⊢ 0 = ↑m * x ^ (m - 1)

Proof state:
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
⊢ deriv (fun x => x ^ m) x = ↑m * x ^ (m - 1)

Tactic:
by_cases H : x ≠ 0 ∨ 0 ≤ m

Result:
case pos
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : x ≠ 0 ∨ 0 ≤ m
⊢ deriv (fun x => x ^ m) x = ↑m * x ^ (m - 1)

case neg
𝕜 : Type u
inst✝ : NontriviallyNormedField 𝕜
m : ℤ
x : 𝕜
H : ¬(x ≠ 0 ∨ 0 ≤ m)
⊢ deriv (fun x => x ^ m) x = ↑m * x ^ (m - 1)
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
/-- An element in a non-unital C⋆-algebra is selfadjoint if and only if it is normal and its
quasispectrum is contained in `ℝ`. -/
lemma isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts {a : A} :
    IsSelfAdjoint a ↔ IsStarNormal a ∧ QuasispectrumRestricts a Complex.reCLM

Proof state:
case refine_2
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal
a : A
⊢ IsStarNormal a ∧ QuasispectrumRestricts a ⇑Complex.reCLM → IsSelfAdjoint a

Tactic:
rintro ⟨ha₁, ha₂⟩

Result:
case refine_2.intro
A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ IsStarNormal
a : A
ha₁ : IsStarNormal a
ha₂ : QuasispectrumRestricts a ⇑Complex.reCLM
⊢ IsSelfAdjoint a
-- Mathlib/Computability/ContextFreeGrammar.lean
@[simp] lemma language_reverse : g.reverse.language = g.language.reverse

Proof state:
T : Type u_1
g : ContextFreeGrammar T
⊢ g.reverse.language = g.language.reverse

Tactic:
ext

Result:
case h
T : Type u_1
g : ContextFreeGrammar T
x✝ : List T
⊢ x✝ ∈ g.reverse.language ↔ x✝ ∈ g.language.reverse

Proof state:
case h
T : Type u_1
g : ContextFreeGrammar T
x✝ : List T
⊢ x✝ ∈ g.reverse.language ↔ x✝ ∈ g.language.reverse

Tactic:
simp

Result:
no goals