harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean
theorem compactlySupported_eq_top_iff [Nontrivial γ] :
    C_cb(α, γ) = ⊤ ↔ IsCompact (Set.univ : Set α)

Proof state:
α : Type u_1
γ : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : NonUnitalNormedRing γ
inst✝ : Nontrivial γ
⊢ C_cb(α, γ) = ⊤ ↔ IsCompact univ

Tactic:
refine ⟨fun h ↦ ?_, compactlySupported_eq_top_of_isCompact⟩

Result:
α : Type u_1
γ : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : NonUnitalNormedRing γ
inst✝ : Nontrivial γ
h : C_cb(α, γ) = ⊤
⊢ IsCompact univ

Proof state:
case intro
α : Type u_1
γ : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : NonUnitalNormedRing γ
inst✝ : Nontrivial γ
h : C_cb(α, γ) = ⊤
x : γ
hx : x ≠ 0
⊢ IsCompact univ

Tactic:
simpa [tsupport, Function.support_const hx]
  using (mem_compactlySupported (f := const α x).mp (by simp [h])).isCompact

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : NonUnitalNormedRing γ
inst✝ : Nontrivial γ
h : C_cb(α, γ) = ⊤
x : γ
hx : x ≠ 0
⊢ const α x ∈ C_cb(α, γ)

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : NonUnitalNormedRing γ
inst✝ : Nontrivial γ
h : C_cb(α, γ) = ⊤
⊢ IsCompact univ

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : γ)

Result:
case intro
α : Type u_1
γ : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : NonUnitalNormedRing γ
inst✝ : Nontrivial γ
h : C_cb(α, γ) = ⊤
x : γ
hx : x ≠ 0
⊢ IsCompact univ
-- Mathlib/Order/Interval/Finset/Box.lean
@[simp] lemma box_zero : (box 0 : Finset α) = {0}

Proof state:
α : Type u_1
inst✝² : OrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
⊢ box 0 = {0}

Tactic:
simp [box]

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Basic.lean
/-- If the `ChartedSpace` structure on a manifold `M` is given by an open embedding `e : M → H`,
then `e` is `C^n`. -/
lemma contMDiff_isOpenEmbedding [Nonempty M] :
    haveI := h.singletonChartedSpace; ContMDiff I I n e

Proof state:
case right
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this✝ : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source)
this : z ∈ ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
⊢ ↑I.symm z ∈ range e

Tactic:
have := this.1

Result:
case right
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this✝¹ : IsManifold I ω M
x : M
y : H
z : E
hz : z ∈ (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (e ⁻¹' (extChartAt I y).source)
this✝ : z ∈ ↑I.symm ⁻¹' (chartAt H x).target ∩ range ↑I
this : z ∈ ↑I.symm ⁻¹' (chartAt H x).target
⊢ ↑I.symm z ∈ range e

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
⊢ ContMDiff I I n e

Tactic:
haveI := h.isManifold_singleton (I := I) (n := ω)

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this : IsManifold I ω M
⊢ ContMDiff I I n e
-- Mathlib/NumberTheory/LSeries/ZMod.lean
lemma completedLFunction_def_even (hΦ : Φ.Even) (s : ℂ) :
    completedLFunction Φ s = N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
this : ∑ j : ZMod N, Φ j * completedHurwitzZetaOdd (toAddCircle j) s = 0
⊢ completedLFunction Φ s = ↑N ^ (-s) * ∑ j : ZMod N, Φ j * completedHurwitzZetaEven (toAddCircle j) s

Tactic:
rw [completedLFunction, this, mul_zero, add_zero]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
⊢ ∑ j : ZMod N, Φ j * completedHurwitzZetaOdd (toAddCircle j) s = 0

Tactic:
refine (hΦ.mul_odd fun j ↦ ?_).sum_eq_zero

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
j : ZMod N
⊢ completedHurwitzZetaOdd (toAddCircle (-j)) s = -completedHurwitzZetaOdd (toAddCircle j) s

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
⊢ completedLFunction Φ s = ↑N ^ (-s) * ∑ j : ZMod N, Φ j * completedHurwitzZetaEven (toAddCircle j) s

Tactic:
suffices ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s = 0 by
  rw [completedLFunction, this, mul_zero, add_zero]

Result:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
⊢ ∑ j : ZMod N, Φ j * completedHurwitzZetaOdd (toAddCircle j) s = 0

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
j : ZMod N
⊢ completedHurwitzZetaOdd (toAddCircle (-j)) s = -completedHurwitzZetaOdd (toAddCircle j) s

Tactic:
rw [map_neg, completedHurwitzZetaOdd_neg]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem mem_lieSpan {x : M} : x ∈ lieSpan R L s ↔ ∀ N : LieSubmodule R L M, s ⊆ N → x ∈ N

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
x : M
⊢ x ∈ ↑(lieSpan R L s) ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N

Tactic:
rw [lieSpan, sInf_coe]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
x : M
⊢ x ∈ ⋂ s_1 ∈ {N | s ⊆ ↑N}, ↑s_1 ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
x : M
⊢ x ∈ lieSpan R L s ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N

Tactic:
change x ∈ (lieSpan R L s : Set M) ↔ _

Result:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
x : M
⊢ x ∈ ↑(lieSpan R L s) ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
s : Set M
x : M
⊢ x ∈ ⋂ s_1 ∈ {N | s ⊆ ↑N}, ↑s_1 ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N

Tactic:
exact mem_iInter₂

Result:
no goals
-- Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean
lemma isIntegralCurveAt_comp_sub {dt : ℝ} :
    IsIntegralCurveAt γ v t₀ ↔ IsIntegralCurveAt (γ ∘ (· - dt)) v (t₀ + dt)

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
t₀ dt : ℝ
⊢ IsIntegralCurveAt γ v t₀ ↔ IsIntegralCurveAt (γ ∘ fun x => x - dt) v (t₀ + dt)

Tactic:
simpa using isIntegralCurveAt_comp_add (dt := -dt)

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_list_eq_max_mk_aleph0 (α : Type u) [Nonempty α] : #(List α) = max #α ℵ₀

Proof state:
case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ ℵ₀ ≤ #α

Tactic:
exact aleph0_le_mk α

Result:
no goals

Proof state:
α : Type u
inst✝ : Nonempty α
⊢ #(List α) = #α ⊔ ℵ₀

Tactic:
cases finite_or_infinite α

Result:
case inl
α : Type u
inst✝ : Nonempty α
h✝ : Finite α
⊢ #(List α) = #α ⊔ ℵ₀

case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ #(List α) = #α ⊔ ℵ₀

Proof state:
case inl
α : Type u
inst✝ : Nonempty α
h✝ : Finite α
⊢ #α ≤ ℵ₀

Tactic:
exact mk_le_aleph0

Result:
no goals

Proof state:
case inl
α : Type u
inst✝ : Nonempty α
h✝ : Finite α
⊢ #(List α) = #α ⊔ ℵ₀

Tactic:
rw [mk_list_eq_aleph0, eq_comm, max_eq_right]

Result:
case inl
α : Type u
inst✝ : Nonempty α
h✝ : Finite α
⊢ #α ≤ ℵ₀

Proof state:
case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ #(List α) = #α ⊔ ℵ₀

Tactic:
rw [mk_list_eq_mk, eq_comm, max_eq_left]

Result:
case inr
α : Type u
inst✝ : Nonempty α
h✝ : Infinite α
⊢ ℵ₀ ≤ #α
-- Mathlib/MeasureTheory/MeasurableSpace/Card.lean
theorem generateMeasurableRec_mono (s : Set (Set α)) : Monotone (generateMeasurableRec s)

Proof state:
case inl
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i ≤ i
⊢ x ∈ generateMeasurableRec s i

Tactic:
exact hx

Result:
no goals

Proof state:
case inr
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h✝ : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i < j
⊢ x ∈ generateMeasurableRec s j

Tactic:
convert iUnion_mem_generateMeasurableRec fun _ => ⟨i, h, hx⟩

Result:
case h.e'_5
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h✝ : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i < j
⊢ x = ⋃ n, x

Proof state:
α : Type u
s : Set (Set α)
⊢ Monotone (generateMeasurableRec s)

Tactic:
intro i j h x hx

Result:
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
⊢ x ∈ generateMeasurableRec s j

Proof state:
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
⊢ x ∈ generateMeasurableRec s j

Tactic:
rcases h.eq_or_lt with (rfl | h)

Result:
case inl
α : Type u
s : Set (Set α)
i : Ordinal.{u_1}
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i ≤ i
⊢ x ∈ generateMeasurableRec s i

case inr
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h✝ : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i < j
⊢ x ∈ generateMeasurableRec s j

Proof state:
case h.e'_5
α : Type u
s : Set (Set α)
i j : Ordinal.{u_1}
h✝ : i ≤ j
x : Set α
hx : x ∈ generateMeasurableRec s i
h : i < j
⊢ x = ⋃ n, x

Tactic:
exact (iUnion_const x).symm

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Basic.lean
theorem subsingleton_orbit_iff_mem_fixedPoints {a : α} :
    (orbit M a).Subsingleton ↔ a ∈ fixedPoints M α

Proof state:
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
⊢ (orbit M a).Subsingleton ↔ ∀ (m : M), m • a = a

Tactic:
constructor

Result:
case mp
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
⊢ (orbit M a).Subsingleton → ∀ (m : M), m • a = a

case mpr
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
⊢ (∀ (m : M), m • a = a) → (orbit M a).Subsingleton

Proof state:
case mpr.intro.intro
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
h : ∀ (m : M), m • a = a
m p : M
⊢ (fun m => m • a) m = (fun m => m • a) p

Tactic:
simp only [h]

Result:
no goals

Proof state:
case mp
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
⊢ (orbit M a).Subsingleton → ∀ (m : M), m • a = a

Tactic:
exact fun h m ↦ h (mem_orbit a m) (mem_orbit_self a)

Result:
no goals

Proof state:
case mpr
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
⊢ (∀ (m : M), m • a = a) → (orbit M a).Subsingleton

Tactic:
rintro h _ ⟨m, rfl⟩ y ⟨p, rfl⟩

Result:
case mpr.intro.intro
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
h : ∀ (m : M), m • a = a
m p : M
⊢ (fun m => m • a) m = (fun m => m • a) p

Proof state:
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
⊢ (orbit M a).Subsingleton ↔ a ∈ fixedPoints M α

Tactic:
rw [mem_fixedPoints]

Result:
M : Type u
inst✝¹ : Monoid M
α : Type v
inst✝ : MulAction M α
a : α
⊢ (orbit M a).Subsingleton ↔ ∀ (m : M), m • a = a
-- Mathlib/GroupTheory/Complement.lean
theorem equiv_snd_eq_self_of_mem_of_one_mem {g : G} (h1 : 1 ∈ S) (hg : g ∈ T) :
    (hST.equiv g).snd = ⟨g, hg⟩

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
this : hST.equiv.symm (⟨1, h1⟩, ⟨g, hg⟩) = g
⊢ (hST.equiv g).2 = ⟨g, hg⟩

Tactic:
conv_lhs => rw [← this, Equiv.apply_symm_apply]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ { toFun := fun x => ↑x.1 * ↑x.2, invFun := surjInv ⋯, left_inv := ⋯, right_inv := ⋯ }.symm.symm (⟨1, h1⟩, ⟨g, hg⟩) = g

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ hST.equiv.symm (⟨1, h1⟩, ⟨g, hg⟩) = g

Tactic:
rw [equiv, Equiv.ofBijective]

Result:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ { toFun := fun x => ↑x.1 * ↑x.2, invFun := surjInv ⋯, left_inv := ⋯, right_inv := ⋯ }.symm.symm (⟨1, h1⟩, ⟨g, hg⟩) = g

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
⊢ (hST.equiv g).2 = ⟨g, hg⟩

Tactic:
have : hST.equiv.symm (⟨1, h1⟩, ⟨g, hg⟩) = g := by
  rw [equiv, Equiv.ofBijective]; simp

Result:
G : Type u_1
inst✝ : Group G
S T : Set G
hST : IsComplement S T
g : G
h1 : 1 ∈ S
hg : g ∈ T
this : hST.equiv.symm (⟨1, h1⟩, ⟨g, hg⟩) = g
⊢ (hST.equiv g).2 = ⟨g, hg⟩
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/OfFn.lean
theorem ofFn_succ {n} (f : Fin (n + 1) → α) : ofFn f = f 0 :: ofFn fun i => f i.succ :=
  ext_get (by simp) (fun i hi₁ hi₂ => by
    cases i
    · simp
    · simp)

Proof state:
α : Type u_1
n : Nat
f : Fin (n + 1) → α
i : Nat
hi₁ : i < (ofFn f).length
hi₂ : i < (f 0 :: ofFn fun i => f i.succ).length
⊢ (ofFn f).get ⟨i, hi₁⟩ = (f 0 :: ofFn fun i => f i.succ).get ⟨i, hi₂⟩

Tactic:
cases i

Result:
case zero
α : Type u_1
n : Nat
f : Fin (n + 1) → α
hi₁ : 0 < (ofFn f).length
hi₂ : 0 < (f 0 :: ofFn fun i => f i.succ).length
⊢ (ofFn f).get ⟨0, hi₁⟩ = (f 0 :: ofFn fun i => f i.succ).get ⟨0, hi₂⟩

case succ
α : Type u_1
n : Nat
f : Fin (n + 1) → α
n✝ : Nat
hi₁ : n✝ + 1 < (ofFn f).length
hi₂ : n✝ + 1 < (f 0 :: ofFn fun i => f i.succ).length
⊢ (ofFn f).get ⟨n✝ + 1, hi₁⟩ = (f 0 :: ofFn fun i => f i.succ).get ⟨n✝ + 1, hi₂⟩

Proof state:
case succ
α : Type u_1
n : Nat
f : Fin (n + 1) → α
n✝ : Nat
hi₁ : n✝ + 1 < (ofFn f).length
hi₂ : n✝ + 1 < (f 0 :: ofFn fun i => f i.succ).length
⊢ (ofFn f).get ⟨n✝ + 1, hi₁⟩ = (f 0 :: ofFn fun i => f i.succ).get ⟨n✝ + 1, hi₂⟩

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
f : Fin (n + 1) → α
⊢ (ofFn f).length = (f 0 :: ofFn fun i => f i.succ).length

Tactic:
simp

Result:
no goals

Proof state:
case zero
α : Type u_1
n : Nat
f : Fin (n + 1) → α
hi₁ : 0 < (ofFn f).length
hi₂ : 0 < (f 0 :: ofFn fun i => f i.succ).length
⊢ (ofFn f).get ⟨0, hi₁⟩ = (f 0 :: ofFn fun i => f i.succ).get ⟨0, hi₂⟩

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/AlgebraicClosure.lean
theorem map_mem_algebraicClosure_iff (i : E →ₐ[F] K) {x : E} :
    i x ∈ algebraicClosure F K ↔ x ∈ algebraicClosure F E

Proof state:
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type u_3
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
x : E
⊢ i x ∈ algebraicClosure F K ↔ x ∈ algebraicClosure F E

Tactic:
simp_rw [mem_algebraicClosure_iff', ← minpoly.ne_zero_iff, minpoly.algHom_eq i i.injective]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma twoTorsionPolynomial_of_char_two : W.twoTorsionPolynomial = ⟨0, W.b₂, 0, W.b₆⟩

Proof state:
case c
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ 2 * W.b₄ = 0

Tactic:
linear_combination W.b₄ * CharP.cast_eq_zero R 2

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.twoTorsionPolynomial = { a := 0, b := W.b₂, c := 0, d := W.b₆ }

Tactic:
rw [twoTorsionPolynomial]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ } = { a := 0, b := W.b₂, c := 0, d := W.b₆ }

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ { a := 4, b := W.b₂, c := 2 * W.b₄, d := W.b₆ } = { a := 0, b := W.b₂, c := 0, d := W.b₆ }

Tactic:
ext <;> dsimp

Result:
case a
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ 4 = 0

case c
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ 2 * W.b₄ = 0

Proof state:
case a
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ 4 = 0

Tactic:
linear_combination 2 * CharP.cast_eq_zero R 2

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Split.lean
theorem iUnion_split (I : Box ι) (i : ι) (x : ℝ) : (split I i x).iUnion = I

Proof state:
ι : Type u_1
I : Box ι
i : ι
x : ℝ
⊢ (split I i x).iUnion = ↑I

Tactic:
simp [split, ← inter_union_distrib_left, ← setOf_or, le_or_lt]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean
lemma mem_distTriang_op_iff (T : Triangle Cᵒᵖ) :
    (T ∈ distTriang Cᵒᵖ) ↔ ((triangleOpEquivalence C).inverse.obj T).unop ∈ distTriang C

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ T ∈ distinguishedTriangles ↔ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ distinguishedTriangles

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/PEquiv.lean
theorem trans_refl (f : α ≃. β) : f.trans (PEquiv.refl β) = f

Proof state:
case h.a
α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ a✝ ∈ (f.trans (PEquiv.refl β)) x✝ ↔ a✝ ∈ f x✝

Tactic:
dsimp [PEquiv.trans]

Result:
case h.a
α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ a✝ ∈ (f x✝).bind ⇑(PEquiv.refl β) ↔ a✝ ∈ f x✝

Proof state:
case h.a
α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ a✝ ∈ (f x✝).bind ⇑(PEquiv.refl β) ↔ a✝ ∈ f x✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α ≃. β
⊢ f.trans (PEquiv.refl β) = f

Tactic:
ext

Result:
case h.a
α : Type u
β : Type v
f : α ≃. β
x✝ : α
a✝ : β
⊢ a✝ ∈ (f.trans (PEquiv.refl β)) x✝ ↔ a✝ ∈ f x✝
-- Mathlib/CategoryTheory/Iso.lean
theorem of_isIso_comp_left {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [IsIso (f ≫ g)] :
    IsIso g

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso (f ≫ g)
⊢ IsIso g

Tactic:
rw [← id_comp g, ← inv_hom_id f, assoc]

Result:
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso (f ≫ g)
⊢ IsIso (inv f ≫ f ≫ g)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsIso f
inst✝ : IsIso (f ≫ g)
⊢ IsIso (inv f ≫ f ≫ g)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/LinearMap.lean
theorem pow_apply_mem_of_forall_mem {p : Submodule R M} (n : ℕ) (h : ∀ x ∈ p, f' x ∈ p) (x : M)
    (hx : x ∈ p) : (f' ^ n) x ∈ p

Proof state:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
p : Submodule R M
n : ℕ
h : ∀ x ∈ p, f' x ∈ p
x : M
hx : x ∈ p
⊢ (f' ^ n) x ∈ p

Tactic:
induction n generalizing x with
| zero => simpa
| succ n ih =>
  simpa only [iterate_succ, coe_comp, Function.comp_apply, restrict_apply] using ih _ (h _ hx)

Result:
no goals

Proof state:
case succ
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
p : Submodule R M
h : ∀ x ∈ p, f' x ∈ p
n : ℕ
ih : ∀ x ∈ p, (f' ^ n) x ∈ p
x : M
hx : x ∈ p
⊢ (f' ^ (n + 1)) x ∈ p

Tactic:
simpa only [iterate_succ, coe_comp, Function.comp_apply, restrict_apply] using ih _ (h _ hx)

Result:
no goals

Proof state:
case zero
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
p : Submodule R M
h : ∀ x ∈ p, f' x ∈ p
x : M
hx : x ∈ p
⊢ (f' ^ 0) x ∈ p

Tactic:
simpa

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem trans_apply (γ : Path x y) (γ' : Path y z) (t : I) :
    (γ.trans γ') t =
      if h : (t : ℝ) ≤ 1 / 2 then γ ⟨2 * t, (mul_pos_mem_iff zero_lt_two).2 ⟨t.2.1, h⟩⟩
      else γ' ⟨2 * t - 1, two_mul_sub_one_mem_iff.2 ⟨(not_le.1 h).le, t.2.2⟩⟩ :=
  show ite _ _ _ = _ by split_ifs <;> rw [extend_extends]

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x y z : X
γ : Path x y
γ' : Path y z
t : ↑I
⊢ (if ↑t ≤ 1 / 2 then γ.extend (2 * ↑t) else γ'.extend (2 * ↑t - 1)) =
    if h : ↑t ≤ 1 / 2 then γ ⟨2 * ↑t, ⋯⟩ else γ' ⟨2 * ↑t - 1, ⋯⟩

Tactic:
split_ifs <;> rw [extend_extends]

Result:
no goals
-- Mathlib/SetTheory/Surreal/Basic.lean
theorem lf_asymm {x y : PGame} (ox : Numeric x) (oy : Numeric y) : x ⧏ y → ¬y ⧏ x

Proof state:
x y : PGame
ox : x.Numeric
oy : y.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), (xL i).Numeric
_oxr : ∀ (i : xr), (xR i).Numeric
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xR i)
⊢ (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (mk xl xr xL xR)

Tactic:
refine numeric_rec fun yl yr yL yR hy oyl oyr _IHyl _IHyr => ?_

Result:
x y : PGame
ox : x.Numeric
oy : y.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), (xL i).Numeric
_oxr : ∀ (i : xr), (xR i).Numeric
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xR i)
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
hy : ∀ (i : yl) (j : yr), yL i < yR j
oyl : ∀ (i : yl), (yL i).Numeric
oyr : ∀ (i : yr), (yR i).Numeric
_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR
_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR
⊢ mk xl xr xL xR ⧏ mk yl yr yL yR → ¬mk yl yr yL yR ⧏ mk xl xr xL xR

Proof state:
x y : PGame
ox : x.Numeric
oy : y.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), (xL i).Numeric
_oxr : ∀ (i : xr), (xR i).Numeric
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xR i)
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
hy : ∀ (i : yl) (j : yr), yL i < yR j
oyl : ∀ (i : yl), (yL i).Numeric
oyr : ∀ (i : yr), (yR i).Numeric
_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR
_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR
⊢ mk xl xr xL xR ⧏ mk yl yr yL yR → ¬mk yl yr yL yR ⧏ mk xl xr xL xR

Tactic:
rw [mk_lf_mk, mk_lf_mk]

Result:
x y : PGame
ox : x.Numeric
oy : y.Numeric
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
hx : ∀ (i : xl) (j : xr), xL i < xR j
_oxl : ∀ (i : xl), (xL i).Numeric
_oxr : ∀ (i : xr), (xR i).Numeric
IHxl : ∀ (i : xl), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xL i)
IHxr : ∀ (i : xr), (fun x => ∀ (z : PGame), z.Numeric → x ⧏ z → ¬z ⧏ x) (xR i)
yl yr : Type u_1
yL : yl → PGame
yR : yr → PGame
hy : ∀ (i : yl) (j : yr), yL i < yR j
oyl : ∀ (i : yl), (yL i).Numeric
oyr : ∀ (i : yr), (yR i).Numeric
_IHyl : ∀ (i : yl), mk xl xr xL xR ⧏ yL i → ¬yL i ⧏ mk xl xr xL xR
_IHyr : ∀ (i : yr), mk xl xr xL xR ⧏ yR i → ¬yR i ⧏ mk xl xr xL xR
⊢ ((∃ i, mk xl xr xL xR ≤ yL i) ∨ ∃ j, xR j ≤ mk yl yr yL yR) →
    ¬((∃ i, mk yl yr yL yR ≤ xL i) ∨ ∃ j, yR j ≤ mk xl xr xL xR)
-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
theorem toClifford_ι (m : M) : toClifford (TensorAlgebra.ι R m) = CliffordAlgebra.ι Q m

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ toClifford ((ι R) m) = (CliffordAlgebra.ι Q) m

Tactic:
simp [toClifford]

Result:
no goals