harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₈_of_isCharTwoJNeZeroNF : W.b₈ = W.a₆ + 4 * W.a₂ * W.a₆

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ 1 ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - 1 * 0 * 0 + W.a₂ * 0 ^ 2 - 0 ^ 2 = W.a₆ + 4 * W.a₂ * W.a₆

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ W.b₈ = W.a₆ + 4 * W.a₂ * W.a₆

Tactic:
rw [b₈, a₁_of_isCharTwoJNeZeroNF, a₃_of_isCharTwoJNeZeroNF, a₄_of_isCharTwoJNeZeroNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharTwoJNeZeroNF
⊢ 1 ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - 1 * 0 * 0 + W.a₂ * 0 ^ 2 - 0 ^ 2 = W.a₆ + 4 * W.a₂ * W.a₆
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.eq_of_same_basis (hl : l.HasBasis p s) (hl' : l'.HasBasis p s) : l = l'

Proof state:
α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p s
⊢ l = l'

Tactic:
ext t

Result:
case h
α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p s
t : Set α
⊢ t ∈ l ↔ t ∈ l'

Proof state:
case h
α : Type u_1
ι : Sort u_4
l l' : Filter α
p : ι → Prop
s : ι → Set α
hl : l.HasBasis p s
hl' : l'.HasBasis p s
t : Set α
⊢ t ∈ l ↔ t ∈ l'

Tactic:
rw [hl.mem_iff, hl'.mem_iff]

Result:
no goals
-- Mathlib/Control/Fold.lean
theorem foldrm_toList (f : α → β → m β) (x : β) (xs : t α) :
    foldrm f x xs = List.foldrM f x (toList xs)

Proof state:
α β : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
x : β
xs : t α
⊢ foldrm f x xs = (foldrM.ofFreeMonoid f) (FreeMonoid.ofList (toList xs)) x

Tactic:
simp only [foldrm, toList_spec, foldMap_hom_free (foldrM.ofFreeMonoid f),
  foldrm.ofFreeMonoid_comp_of, foldrM.get, FreeMonoid.ofList_toList]

Result:
no goals

Proof state:
α β : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
x : β
xs : t α
⊢ foldrm f x xs = List.foldrM f x (toList xs)

Tactic:
change _ = foldrM.ofFreeMonoid f (FreeMonoid.ofList <| toList xs) x

Result:
α β : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
x : β
xs : t α
⊢ foldrm f x xs = (foldrM.ofFreeMonoid f) (FreeMonoid.ofList (toList xs)) x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.denote_append (ctx : Context) (p q : Poly) : (p ++ q).denote ctx = p.denote ctx + q.denote ctx

Proof state:
ctx : Context
p q : Poly
⊢ denote ctx (p ++ q) = denote ctx p + denote ctx q

Tactic:
match p with
| []  => simp
| (k, v) :: p => simp [denote_append]

Result:
no goals

Proof state:
ctx : Context
p✝ q : Poly
k : Nat
v : Var
p : List (Nat × Var)
⊢ denote ctx ((k, v) :: p ++ q) = denote ctx ((k, v) :: p) + denote ctx q

Tactic:
simp [denote_append]

Result:
no goals

Proof state:
ctx : Context
p q : Poly
⊢ denote ctx ([] ++ q) = denote ctx [] + denote ctx q

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Compare.lean
theorem compare_eq_gt {a b : Nat} : compare a b = .gt ↔ b < a

Proof state:
case isFalse
a b : Nat
h✝ : ¬a < b
⊢ (if b < a then Ordering.gt else Ordering.eq) = Ordering.gt ↔ b < a

Tactic:
split

Result:
case isFalse.isTrue
a b : Nat
h✝¹ : ¬a < b
h✝ : b < a
⊢ Ordering.gt = Ordering.gt ↔ b < a

case isFalse.isFalse
a b : Nat
h✝¹ : ¬a < b
h✝ : ¬b < a
⊢ Ordering.eq = Ordering.gt ↔ b < a

Proof state:
a b : Nat
⊢ compare a b = Ordering.gt ↔ b < a

Tactic:
rw [compare_def_lt]

Result:
a b : Nat
⊢ (if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq) = Ordering.gt ↔ b < a

Proof state:
a b : Nat
⊢ (if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq) = Ordering.gt ↔ b < a

Tactic:
(repeat' split) <;> simp [Nat.le_of_lt, *]

Result:
no goals

Proof state:
a b : Nat
⊢ (if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq) = Ordering.gt ↔ b < a

Tactic:
repeat' split

Result:
case isTrue
a b : Nat
h✝ : a < b
⊢ Ordering.lt = Ordering.gt ↔ b < a

case isFalse.isTrue
a b : Nat
h✝¹ : ¬a < b
h✝ : b < a
⊢ Ordering.gt = Ordering.gt ↔ b < a

case isFalse.isFalse
a b : Nat
h✝¹ : ¬a < b
h✝ : ¬b < a
⊢ Ordering.eq = Ordering.gt ↔ b < a
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma ne_zero [NeZero (2 : R)] : (P.root i : M) ≠ 0 :=
  fun h ↦ NeZero.ne' (2 : R) <| by simpa [h] using P.root_coroot_two i

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
i : ι
inst✝ : NeZero 2
h : P.root i = 0
⊢ 0 = 2

Tactic:
simpa [h] using P.root_coroot_two i

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
lemma penultimate_cons_of_not_nil (h : G.Adj u v) (p : G.Walk v w) (hp : ¬ p.Nil) :
    (cons h p).penultimate = p.penultimate :=
  p.notNilRec (by simp) hp h

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
hp : ¬p.Nil
⊢ ∀ {u_1 v w : V} (h : G.Adj u_1 v) (q : G.Walk v w) (x : G.Adj u u_1),
    (cons x (cons h q)).penultimate = (cons h q).penultimate

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem normSq_neg (z : K) : normSq (-z) = normSq z

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ normSq (-z) = normSq z

Tactic:
simp only [normSq_eq_def', norm_neg]

Result:
no goals
-- Mathlib/Data/Multiset/Fold.lean
theorem fold_dedup_idem [DecidableEq α] [hi : Std.IdempotentOp op] (s : Multiset α) (b : α) :
    (dedup s).fold op b = s.fold op b :=
  Multiset.induction_on s (by simp) fun a s IH => by
    by_cases h : a ∈ s <;> simp [IH, h]
    show fold op b s = op a (fold op b s)
    rw [← cons_erase h, fold_cons_left, ← ha.assoc, hi.idempotent]

Proof state:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
⊢ fold op b (a ::ₘ s).dedup = fold op b (a ::ₘ s)

Tactic:
by_cases h : a ∈ s <;> simp [IH, h]

Result:
case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b s = op a (fold op b s)

Proof state:
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s : Multiset α
b : α
⊢ fold op b (dedup 0) = fold op b 0

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u_1
op : α → α → α
hc : Std.Commutative op
ha : Std.Associative op
inst✝ : DecidableEq α
hi : Std.IdempotentOp op
s✝ : Multiset α
b a : α
s : Multiset α
IH : fold op b s.dedup = fold op b s
h : a ∈ s
⊢ fold op b s = op a (fold op b s)

Tactic:
rw [← cons_erase h, fold_cons_left, ← ha.assoc, hi.idempotent]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem fst_comp_quotientMulEquivQuotientProd (I J : Ideal R) (coprime : IsCoprime I J) :
    (RingHom.fst _ _).comp
        (quotientMulEquivQuotientProd I J coprime : R ⧸ I * J →+* (R ⧸ I) × R ⧸ J) =
      Ideal.Quotient.factor mul_le_right

Proof state:
case h
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ ((fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime)).comp (Quotient.mk (I * J)) =
    (factor ⋯).comp (Quotient.mk (I * J))

Tactic:
ext

Result:
case h.a
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x✝ : R
⊢ (((fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime)).comp (Quotient.mk (I * J))) x✝ =
    ((factor ⋯).comp (Quotient.mk (I * J))) x✝

Proof state:
case h.a
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
x✝ : R
⊢ (((fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime)).comp (Quotient.mk (I * J))) x✝ =
    ((factor ⋯).comp (Quotient.mk (I * J))) x✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ (fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime) = factor ⋯

Tactic:
apply Quotient.ringHom_ext

Result:
case h
R : Type u_2
inst✝ : CommRing R
I J : Ideal R
coprime : IsCoprime I J
⊢ ((fst (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientMulEquivQuotientProd J coprime)).comp (Quotient.mk (I * J)) =
    (factor ⋯).comp (Quotient.mk (I * J))
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
theorem nullMeasurableSet_eq_fun {E} [MeasurableSpace E] [AddGroup E] [MeasurableSingletonClass E]
    [MeasurableSub₂ E] {f g : α → E} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    NullMeasurableSet { x | f x = g x } μ

Proof state:
α : Type u_3
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ NullMeasurableSet {x | f x = g x} μ

Tactic:
apply (measurableSet_eq_fun hf.measurable_mk hg.measurable_mk).nullMeasurableSet.congr

Result:
α : Type u_3
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ {x | AEMeasurable.mk f hf x = AEMeasurable.mk g hg x} =ᶠ[ae μ] {x | f x = g x}

Proof state:
case h
α : Type u_3
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : AEMeasurable f μ
hg : AEMeasurable g μ
x : α
hfx : f x = AEMeasurable.mk f hf x
hgx : g x = AEMeasurable.mk g hg x
⊢ (AEMeasurable.mk f hf x = AEMeasurable.mk g hg x) = (f x = g x)

Tactic:
simp only [hfx, hgx]

Result:
no goals

Proof state:
case h
α : Type u_3
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : AEMeasurable f μ
hg : AEMeasurable g μ
x : α
hfx : f x = AEMeasurable.mk f hf x
hgx : g x = AEMeasurable.mk g hg x
⊢ {x | AEMeasurable.mk f hf x = AEMeasurable.mk g hg x} x = {x | f x = g x} x

Tactic:
change (hf.mk f x = hg.mk g x) = (f x = g x)

Result:
case h
α : Type u_3
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : AEMeasurable f μ
hg : AEMeasurable g μ
x : α
hfx : f x = AEMeasurable.mk f hf x
hgx : g x = AEMeasurable.mk g hg x
⊢ (AEMeasurable.mk f hf x = AEMeasurable.mk g hg x) = (f x = g x)

Proof state:
α : Type u_3
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ {x | AEMeasurable.mk f hf x = AEMeasurable.mk g hg x} =ᶠ[ae μ] {x | f x = g x}

Tactic:
filter_upwards [hf.ae_eq_mk, hg.ae_eq_mk] with x hfx hgx

Result:
case h
α : Type u_3
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝³ : MeasurableSpace E
inst✝² : AddGroup E
inst✝¹ : MeasurableSingletonClass E
inst✝ : MeasurableSub₂ E
f g : α → E
hf : AEMeasurable f μ
hg : AEMeasurable g μ
x : α
hfx : f x = AEMeasurable.mk f hf x
hgx : g x = AEMeasurable.mk g hg x
⊢ {x | AEMeasurable.mk f hf x = AEMeasurable.mk g hg x} x = {x | f x = g x} x
-- Mathlib/MeasureTheory/Function/L2Space.lean
theorem eLpNorm_rpow_two_norm_lt_top (f : Lp F 2 μ) :
    eLpNorm (fun x => ‖f x‖ ^ (2 : ℝ)) 1 μ < ∞

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : ↥(Lp F 2 μ)
⊢ ENNReal.ofReal 2 = 2

Tactic:
simp [zero_le_one]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : ↥(Lp F 2 μ)
h_two : ENNReal.ofReal 2 = 2
⊢ eLpNorm (fun x => ‖↑↑f x‖ ^ 2) 1 μ < ⊤

Tactic:
rw [eLpNorm_norm_rpow f zero_lt_two, one_mul, h_two]

Result:
α : Type u_1
F : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : ↥(Lp F 2 μ)
h_two : ENNReal.ofReal 2 = 2
⊢ eLpNorm (↑↑f) 2 μ ^ 2 < ⊤

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : ↥(Lp F 2 μ)
⊢ eLpNorm (fun x => ‖↑↑f x‖ ^ 2) 1 μ < ⊤

Tactic:
have h_two : ENNReal.ofReal (2 : ℝ) = 2 := by simp [zero_le_one]

Result:
α : Type u_1
F : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : ↥(Lp F 2 μ)
h_two : ENNReal.ofReal 2 = 2
⊢ eLpNorm (fun x => ‖↑↑f x‖ ^ 2) 1 μ < ⊤

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : ↥(Lp F 2 μ)
h_two : ENNReal.ofReal 2 = 2
⊢ eLpNorm (↑↑f) 2 μ ^ 2 < ⊤

Tactic:
exact ENNReal.rpow_lt_top_of_nonneg zero_le_two (Lp.eLpNorm_ne_top f)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldrM_push' [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α)
    {start} (h : start = arr.size + 1) :
    (arr.push a).foldrM f init start = f a init >>= arr.foldrM f

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
f : α → β → m β
init : β
arr : Array α
a : α
start : Nat
h : start = arr.size + 1
⊢ foldrM f init (arr.push a) start = do
    let init ← f a init
    foldrM f init arr

Tactic:
simp [← foldrM_push, h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean
theorem mk (h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0) : μ ≪ ν

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0
⊢ μ ≪ ν

Tactic:
intro s hs

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0
s : Set α
hs : ν s = 0
⊢ μ s = 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0
s : Set α
hs : ν s = 0
⊢ μ s = 0

Tactic:
rcases exists_measurable_superset_of_null hs with ⟨t, h1t, h2t, h3t⟩

Result:
case intro.intro.intro
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0
s : Set α
hs : ν s = 0
t : Set α
h1t : s ⊆ t
h2t : MeasurableSet t
h3t : ν t = 0
⊢ μ s = 0

Proof state:
case intro.intro.intro
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0
s : Set α
hs : ν s = 0
t : Set α
h1t : s ⊆ t
h2t : MeasurableSet t
h3t : ν t = 0
⊢ μ s = 0

Tactic:
exact measure_mono_null h1t (h h2t h3t)

Result:
no goals
-- Mathlib/Geometry/Euclidean/Inversion/ImageHyperplane.lean
theorem preimage_inversion_perpBisector (hR : R ≠ 0) (hy : y ≠ c) :
    inversion c R ⁻¹' perpBisector c y = sphere (inversion c R y) (R ^ 2 / dist y c) \ {c}

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R ⁻¹' ↑(perpBisector c y) = sphere (inversion c R y) (R ^ 2 / dist y c) \ {c}

Tactic:
rw [← dist_inversion_center, ← preimage_inversion_perpBisector_inversion hR,
  inversion_inversion] <;> simp [*]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean
theorem measurable_extend (hf : MeasurableEmbedding f) {g : α → γ} {g' : β → γ} (hg : Measurable g)
    (hg' : Measurable g') : Measurable (extend f g g')

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (g' ∘ Subtype.val)

Tactic:
exact hg'.comp measurable_subtype_coe

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (extend f g g')

Tactic:
refine measurable_of_restrict_of_restrict_compl hf.measurableSet_range ?_ ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable ((range f).restrict (extend f g g'))

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable ((range f)ᶜ.restrict (extend f g g'))

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable ((range f)ᶜ.restrict (extend f g g'))

Tactic:
rw [restrict_extend_compl_range]

Result:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable (g' ∘ Subtype.val)

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable ((range f).restrict (extend f g g'))

Tactic:
rw [restrict_extend_range]

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable fun x => g (Exists.choose ⋯)

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
hf : MeasurableEmbedding f
g : α → γ
g' : β → γ
hg : Measurable g
hg' : Measurable g'
⊢ Measurable fun x => g (Exists.choose ⋯)

Tactic:
simpa only [rangeSplitting] using hg.comp hf.measurable_rangeSplitting

Result:
no goals
-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
@[simp 1100] lemma fourierPowSMulRight_apply {f : V → E} {v : V} {n : ℕ} {m : Fin n → W} :
    fourierPowSMulRight L f v n m = (- (2 * π * I))^n • (∏ i, L v (m i)) • f v

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
n : ℕ
m : Fin n → W
⊢ (fourierPowSMulRight L f v n) m = (-(2 * ↑π * I)) ^ n • (∏ i : Fin n, (L v) (m i)) • f v

Tactic:
simp [fourierPowSMulRight]

Result:
no goals
-- Mathlib/GroupTheory/HNNExtension.lean
theorem equiv_eq_conj (a : A) :
    (of (φ a : G) : HNNExtension G A B φ) = t * of (a : G) * t⁻¹

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
⊢ of ↑(φ a) = of ↑(φ a) * t * t⁻¹

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
⊢ of ↑(φ a) = t * of ↑a * t⁻¹

Tactic:
rw [t_mul_of]

Result:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
⊢ of ↑(φ a) = of ↑(φ a) * t * t⁻¹
-- Mathlib/Order/Filter/ZeroAndBoundedAtFilter.lean
theorem ZeroAtFilter.smul [TopologicalSpace β] [Zero 𝕜] [Zero β]
    [SMulWithZero 𝕜 β] [ContinuousConstSMul 𝕜 β] {l : Filter α} {f : α → β} (c : 𝕜)
    (hf : ZeroAtFilter l f) : ZeroAtFilter l (c • f)

Proof state:
𝕜 : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : TopologicalSpace β
inst✝³ : Zero 𝕜
inst✝² : Zero β
inst✝¹ : SMulWithZero 𝕜 β
inst✝ : ContinuousConstSMul 𝕜 β
l : Filter α
f : α → β
c : 𝕜
hf : l.ZeroAtFilter f
⊢ l.ZeroAtFilter (c • f)

Tactic:
simpa using hf.const_smul c

Result:
no goals
-- Mathlib/FieldTheory/Galois/Basic.lean
theorem IntermediateField.AdjoinSimple.card_aut_eq_finrank [FiniteDimensional F E] {α : E}
    (hα : IsIntegral F α) (h_sep : IsSeparable F α)
    (h_splits : (minpoly F α).Splits (algebraMap F F⟮α⟯)) :
    Fintype.card (F⟮α⟯ ≃ₐ[F] F⟮α⟯) = finrank F F⟮α⟯

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
hα : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)
⊢ Fintype.card (↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯) = finrank F ↥F⟮α⟯

Tactic:
letI : Fintype (F⟮α⟯ →ₐ[F] F⟮α⟯) := IntermediateField.fintypeOfAlgHomAdjoinIntegral F hα

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
hα : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)
this : Fintype (↥F⟮α⟯ →ₐ[F] ↥F⟮α⟯) := fintypeOfAlgHomAdjoinIntegral F hα
⊢ Fintype.card (↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯) = finrank F ↥F⟮α⟯

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
hα : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)
this : Fintype (↥F⟮α⟯ →ₐ[F] ↥F⟮α⟯) := fintypeOfAlgHomAdjoinIntegral F hα
⊢ Fintype.card (↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯) = (minpoly F α).natDegree

Tactic:
rw [← IntermediateField.card_algHom_adjoin_integral F hα h_sep h_splits]

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
hα : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)
this : Fintype (↥F⟮α⟯ →ₐ[F] ↥F⟮α⟯) := fintypeOfAlgHomAdjoinIntegral F hα
⊢ Fintype.card (↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯) = Fintype.card (↥F⟮α⟯ →ₐ[F] ↥F⟮α⟯)

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
hα : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)
this : Fintype (↥F⟮α⟯ →ₐ[F] ↥F⟮α⟯) := fintypeOfAlgHomAdjoinIntegral F hα
⊢ Fintype.card (↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯) = finrank F ↥F⟮α⟯

Tactic:
rw [IntermediateField.adjoin.finrank hα]

Result:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
hα : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)
this : Fintype (↥F⟮α⟯ →ₐ[F] ↥F⟮α⟯) := fintypeOfAlgHomAdjoinIntegral F hα
⊢ Fintype.card (↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯) = (minpoly F α).natDegree

Proof state:
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : FiniteDimensional F E
α : E
hα : IsIntegral F α
h_sep : IsSeparable F α
h_splits : Polynomial.Splits (algebraMap F ↥F⟮α⟯) (minpoly F α)
this : Fintype (↥F⟮α⟯ →ₐ[F] ↥F⟮α⟯) := fintypeOfAlgHomAdjoinIntegral F hα
⊢ Fintype.card (↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯) = Fintype.card (↥F⟮α⟯ →ₐ[F] ↥F⟮α⟯)

Tactic:
exact Fintype.card_congr (algEquivEquivAlgHom F F⟮α⟯)

Result:
no goals