harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
@[to_additive]
lemma prod_mul_prod_eq_prod_zipWith_mul_prod_drop :
    ∀ l l' : List M,
      l.prod * l'.prod =
        (zipWith (· * ·) l l').prod * (l.drop l'.length).prod * (l'.drop l.length).prod
  | [], ys => by simp [Nat.zero_le]
  | xs, [] => by simp [Nat.zero_le]
  | x :: xs, y :: ys => by
    simp only [drop, length, zipWith_cons_cons, prod_cons]
    conv =>
      lhs; rw [mul_assoc]; right; rw [mul_comm, mul_assoc]; right
      rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]
    simp [mul_assoc]

Proof state:
M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
⊢ x * (y * ((zipWith (fun x1 x2 => x1 * x2) xs ys).prod * (drop ys.length xs).prod * (drop xs.length ys).prod)) =
    x * y * (zipWith (fun x1 x2 => x1 * x2) xs ys).prod * (drop ys.length xs).prod * (drop xs.length ys).prod

Tactic:
simp [mul_assoc]

Result:
no goals

Proof state:
M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
⊢ (x :: xs).prod * (y :: ys).prod =
    (zipWith (fun x1 x2 => x1 * x2) (x :: xs) (y :: ys)).prod * (drop (y :: ys).length (x :: xs)).prod *
      (drop (x :: xs).length (y :: ys)).prod

Tactic:
simp only [drop, length, zipWith_cons_cons, prod_cons]

Result:
M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
⊢ x * xs.prod * (y * ys.prod) =
    x * y * (zipWith (fun x1 x2 => x1 * x2) xs ys).prod * (drop ys.length xs).prod * (drop xs.length ys).prod

Proof state:
M : Type u_4
inst✝ : CommMonoid M
xs : List M
⊢ xs.prod * [].prod = (zipWith (fun x1 x2 => x1 * x2) xs []).prod * (drop [].length xs).prod * (drop xs.length []).prod

Tactic:
simp [Nat.zero_le]

Result:
no goals

Proof state:
M : Type u_4
inst✝ : CommMonoid M
ys : List M
⊢ [].prod * ys.prod = (zipWith (fun x1 x2 => x1 * x2) [] ys).prod * (drop ys.length []).prod * (drop [].length ys).prod

Tactic:
simp [Nat.zero_le]

Result:
no goals

Proof state:
M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
⊢ x * xs.prod * (y * ys.prod) =
    x * y * (zipWith (fun x1 x2 => x1 * x2) xs ys).prod * (drop ys.length xs).prod * (drop xs.length ys).prod

Tactic:
conv =>
  lhs; rw [mul_assoc]; right; rw [mul_comm, mul_assoc]; right
  rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]

Result:
M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
⊢ x * (y * ((zipWith (fun x1 x2 => x1 * x2) xs ys).prod * (drop ys.length xs).prod * (drop xs.length ys).prod)) =
    x * y * (zipWith (fun x1 x2 => x1 * x2) xs ys).prod * (drop ys.length xs).prod * (drop xs.length ys).prod
-- Mathlib/AlgebraicGeometry/Noetherian.lean
lemma noetherianSpace_of_isAffineOpen (U : X.Opens) (hU : IsAffineOpen U)
    [IsNoetherianRing Γ(X, U)] :
    NoetherianSpace U

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
inst✝ : IsNoetherianRing ↑Γ(X, U)
⊢ NoetherianSpace ↑↑(↑U).toPresheafedSpace

Tactic:
have : IsNoetherianRing Γ(U, ⊤) := isNoetherianRing_of_ringEquiv _
  (Scheme.restrictFunctorΓ.app (op U)).symm.commRingCatIsoToRingEquiv

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
inst✝ : IsNoetherianRing ↑Γ(X, U)
this : IsNoetherianRing ↑Γ(↑U, ⊤)
⊢ NoetherianSpace ↑↑(↑U).toPresheafedSpace

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
inst✝ : IsNoetherianRing ↑Γ(X, U)
this : IsNoetherianRing ↑Γ(↑U, ⊤)
⊢ NoetherianSpace ↑↑(↑U).toPresheafedSpace

Tactic:
exact @noetherianSpace_of_isAffine _ hU _

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma Affine.CoordinateRing.mk_Ψ_sq (n : ℤ) : mk W (W.Ψ n) ^ 2 = mk W (C <| W.ΨSq n)

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (mk W) (W.Ψ n) ^ 2 = (mk W) (C (W.ΨSq n))

Tactic:
simp only [Ψ, ΨSq, map_one, map_mul, map_pow, one_pow, mul_pow, ite_pow, apply_ite C,
  apply_ite <| mk W, mk_ψ₂_sq]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem isLeast_csInf (hs : s.Nonempty) : IsLeast s (sInf s)

Proof state:
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
⊢ IsLeast s (sInf s)

Tactic:
rw [sInf_eq_argmin_on hs]

Result:
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
⊢ IsLeast s (argminOn id s hs)

Proof state:
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
s : Set α
inst✝ : WellFoundedLT α
hs : s.Nonempty
⊢ IsLeast s (argminOn id s hs)

Tactic:
exact ⟨argminOn_mem _ _ _, fun a ha => argminOn_le id _ ha⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem MeasurableSet.map_coe_volume {s : Set α} (hs : MeasurableSet s) :
    volume.map ((↑) : s → α) = restrict volume s

Proof state:
α : Type u_2
inst✝ : MeasureSpace α
s : Set α
hs : MeasurableSet s
⊢ Measure.map Subtype.val volume = volume.restrict s

Tactic:
rw [volume_set_coe_def, (MeasurableEmbedding.subtype_coe hs).map_comap volume, Subtype.range_coe]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivAt.comp_hasFDerivAt_of_eq {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x)
    (hh : HasDerivAt h₂ h₂' y) (hf : HasFDerivAt f f' x) (hy : y = f x) :
    HasFDerivAt (h₂ ∘ f) (h₂' • f') x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasDerivAt h₂ h₂' y
hf : HasFDerivAt f f' x
hy : y = f x
⊢ HasFDerivAt (h₂ ∘ f) (h₂' • f') x

Tactic:
rw [hy] at hh

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasDerivAt h₂ h₂' (f x)
hf : HasFDerivAt f f' x
hy : y = f x
⊢ HasFDerivAt (h₂ ∘ f) (h₂' • f') x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' y : 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
hh : HasDerivAt h₂ h₂' (f x)
hf : HasFDerivAt f f' x
hy : y = f x
⊢ HasFDerivAt (h₂ ∘ f) (h₂' • f') x

Tactic:
exact hh.comp_hasFDerivAt x hf

Result:
no goals
-- Mathlib/Data/Rat/Star.lean
@[simp]
lemma addSubmonoid_closure_range_mul_self : closure (range fun x : ℚ ↦ x * x) = nonneg _

Proof state:
⊢ closure (range fun x => x * x) = nonneg ℚ

Tactic:
simpa only [sq] using addSubmonoid_closure_range_pow two_ne_zero even_two

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Killing.lean
lemma lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg
    {α : Weight K H L} {e f : L} (heα : e ∈ rootSpace H α) (hfα : f ∈ rootSpace H (-α)) :
    ⁅e, f⁆ = killingForm K L e f • (cartanEquivDual H).symm α

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
⊢ ⁅e, f⁆ = ((killingForm K L) e) f • ↑((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α))

Tactic:
apply lie_eq_killingForm_smul_of_mem_rootSpace_of_mem_rootSpace_neg_aux heα hfα

Result:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
⊢ ∀ (h : ↥H), ⁅h, e⁆ = α h • e

Proof state:
K : Type u_2
L : Type u_3
inst✝⁷ : LieRing L
inst✝⁶ : Field K
inst✝⁵ : LieAlgebra K L
inst✝⁴ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝³ : H.IsCartanSubalgebra
inst✝² : IsKilling K L
inst✝¹ : IsTriangularizable K (↥H) L
inst✝ : PerfectField K
α : Weight K (↥H) L
e f : L
heα : e ∈ rootSpace H ⇑α
hfα : f ∈ rootSpace H (-⇑α)
⊢ ∀ (h : ↥H), ⁅h, e⁆ = α h • e

Tactic:
exact lie_eq_smul_of_mem_rootSpace heα

Result:
no goals
-- Mathlib/Data/Int/Cast/Basic.lean
theorem cast_subNatNat (m n) : ((Int.subNatNat m n : ℤ) : R) = m - n

Proof state:
case succ
R : Type u
inst✝ : AddGroupWithOne R
m n n✝ : ℕ
e : n - m = n✝ + 1
⊢ ↑(match n✝ + 1 with
      | 0 => ofNat (m - n)
      | k.succ => -[k+1]) =
    ↑m - ↑n

Tactic:
rw [cast_negSucc, ← e, Nat.cast_sub <| _root_.le_of_lt <| Nat.lt_of_sub_eq_succ e, neg_sub]

Result:
no goals

Proof state:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(subNatNat m n) = ↑m - ↑n

Tactic:
unfold subNatNat

Result:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(match n - m with
      | 0 => ofNat (m - n)
      | k.succ => -[k+1]) =
    ↑m - ↑n

Proof state:
case zero
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
e : n - m = 0
⊢ ↑↑(m - n) = ↑m - ↑n

Tactic:
simp [e, Nat.le_of_sub_eq_zero e]

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
e : n - m = 0
⊢ ↑(match 0 with
      | 0 => ofNat (m - n)
      | k.succ => -[k+1]) =
    ↑m - ↑n

Tactic:
simp only [ofNat_eq_coe]

Result:
case zero
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
e : n - m = 0
⊢ ↑↑(m - n) = ↑m - ↑n

Proof state:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑(match n - m with
      | 0 => ofNat (m - n)
      | k.succ => -[k+1]) =
    ↑m - ↑n

Tactic:
cases e : n - m

Result:
case zero
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
e : n - m = 0
⊢ ↑(match 0 with
      | 0 => ofNat (m - n)
      | k.succ => -[k+1]) =
    ↑m - ↑n

case succ
R : Type u
inst✝ : AddGroupWithOne R
m n n✝ : ℕ
e : n - m = n✝ + 1
⊢ ↑(match n✝ + 1 with
      | 0 => ofNat (m - n)
      | k.succ => -[k+1]) =
    ↑m - ↑n
-- Mathlib/Data/List/MinMax.lean
theorem argmax_concat (f : α → β) (a : α) (l : List α) :
    argmax f (l ++ [a]) =
      Option.casesOn (argmax f l) (some a) fun c => if f c < f a then some a else some c

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableRel fun x1 x2 => x1 < x2
f : α → β
a : α
l : List α
⊢ argmax f (l ++ [a]) = Option.casesOn (argmax f l) (some a) fun c => if f c < f a then some a else some c

Tactic:
rw [argmax, argmax]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableRel fun x1 x2 => x1 < x2
f : α → β
a : α
l : List α
⊢ foldl (argAux fun b c => f c < f b) none (l ++ [a]) =
    Option.casesOn (foldl (argAux fun b c => f c < f b) none l) (some a) fun c => if f c < f a then some a else some c

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder β
inst✝ : DecidableRel fun x1 x2 => x1 < x2
f : α → β
a : α
l : List α
⊢ foldl (argAux fun b c => f c < f b) none (l ++ [a]) =
    Option.casesOn (foldl (argAux fun b c => f c < f b) none l) (some a) fun c => if f c < f a then some a else some c

Tactic:
simp [argAux]

Result:
no goals
-- Mathlib/SetTheory/Game/Impartial.lean
theorem nonpos : ¬0 < G

Proof state:
G : PGame
inst✝ : G.Impartial
x✝ : 0 < G
⊢ G < 0

Tactic:
rwa [← neg_lt_neg_iff, neg_zero, ← lt_congr_right (neg_equiv_self G)]

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem cgf_neg : cgf (-X) μ t = cgf X μ (-t)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
⊢ cgf (-X) μ t = cgf X μ (-t)

Tactic:
simp_rw [cgf, mgf_neg]

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Lemmas.lean
/-- The conjugate of a multiplicative character with values in `ℂ` is its inverse. -/
lemma star_eq_inv (χ : MulChar R ℂ) : star χ = χ⁻¹

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Finite Rˣ
χ : MulChar R ℂ
val✝ : Fintype Rˣ
⊢ star χ = χ⁻¹

Tactic:
ext1 a

Result:
case intro.h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Finite Rˣ
χ : MulChar R ℂ
val✝ : Fintype Rˣ
a : Rˣ
⊢ (star χ) ↑a = χ⁻¹ ↑a

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Finite Rˣ
χ : MulChar R ℂ
⊢ star χ = χ⁻¹

Tactic:
cases nonempty_fintype Rˣ

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Finite Rˣ
χ : MulChar R ℂ
val✝ : Fintype Rˣ
⊢ star χ = χ⁻¹

Proof state:
case intro.h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Finite Rˣ
χ : MulChar R ℂ
val✝ : Fintype Rˣ
a : Rˣ
⊢ (star χ) ↑a = (χ ↑a)⁻¹

Tactic:
exact (inv_eq_conj <| norm_eq_one_of_mem_rootsOfUnity <| χ.apply_mem_rootsOfUnity a).symm

Result:
no goals

Proof state:
case intro.h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Finite Rˣ
χ : MulChar R ℂ
val✝ : Fintype Rˣ
a : Rˣ
⊢ (star χ) ↑a = χ⁻¹ ↑a

Tactic:
simp only [inv_apply_eq_inv']

Result:
case intro.h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Finite Rˣ
χ : MulChar R ℂ
val✝ : Fintype Rˣ
a : Rˣ
⊢ (star χ) ↑a = (χ ↑a)⁻¹
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem lt_sup'_iff : a < s.sup' H f ↔ ∃ b ∈ s, a < f b

Proof state:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ a < s.sup' H f ↔ ∃ b ∈ s, a < f b

Tactic:
rw [← WithBot.coe_lt_coe, coe_sup', Finset.lt_sup_iff]

Result:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ (∃ b ∈ s, ↑a < (WithBot.some ∘ f) b) ↔ ∃ b ∈ s, a < f b

Proof state:
α : Type u_2
ι : Type u_5
inst✝ : LinearOrder α
s : Finset ι
H : s.Nonempty
f : ι → α
a : α
⊢ (∃ b ∈ s, ↑a < (WithBot.some ∘ f) b) ↔ ∃ b ∈ s, a < f b

Tactic:
exact exists_congr (fun _ => and_congr_right' WithBot.coe_lt_coe)

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/TriangleShift.lean
@[simp]
lemma shiftFunctorAdd'_eq (a b c : ℤ) (h : a + b = c) :
    CategoryTheory.shiftFunctorAdd' (Triangle C) a b c h =
      Triangle.shiftFunctorAdd' C a b c h

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
h : a + b = c
⊢ CategoryTheory.shiftFunctorAdd' (Triangle C) a b c h = shiftFunctorAdd' C a b c h

Tactic:
subst h

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
⊢ CategoryTheory.shiftFunctorAdd' (Triangle C) a b (a + b) ⋯ = shiftFunctorAdd' C a b (a + b) ⋯

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
⊢ CategoryTheory.shiftFunctorAdd' (Triangle C) a b (a + b) ⋯ = shiftFunctorAdd' C a b (a + b) ⋯

Tactic:
rw [shiftFunctorAdd'_eq_shiftFunctorAdd]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
⊢ shiftFunctorAdd (Triangle C) a b = shiftFunctorAdd' C a b (a + b) ⋯

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
⊢ shiftFunctorAdd (Triangle C) a b = shiftFunctorAdd' C a b (a + b) ⋯

Tactic:
apply shiftFunctorAdd_eq

Result:
no goals
-- Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
theorem reflexive_left : IsReflexive R M where
  bijective_dual_eval'

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
⊢ Bijective ⇑(Dual.eval R M)

Tactic:
rw [← p.toDualRight_symm_comp_toDualLeft]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
⊢ Bijective ⇑(↑p.toDualRight.symm.dualMap ∘ₗ ↑p.toDualLeft)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
⊢ Bijective ⇑(↑p.toDualRight.symm.dualMap ∘ₗ ↑p.toDualLeft)

Tactic:
exact p.bijective_toDualRight_symm_toDualLeft

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem DifferentiableAt.derivWithin (h : DifferentiableAt 𝕜 f x) (hxs : UniqueDiffWithinAt 𝕜 s x) :
    derivWithin f s x = deriv f x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : DifferentiableAt 𝕜 f x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ _root_.derivWithin f s x = deriv f x

Tactic:
unfold _root_.derivWithin deriv

Result:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : DifferentiableAt 𝕜 f x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 f s x) 1 = (fderiv 𝕜 f x) 1

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : DifferentiableAt 𝕜 f x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ (fderivWithin 𝕜 f s x) 1 = (fderiv 𝕜 f x) 1

Tactic:
rw [h.fderivWithin hxs]

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem uniformity_eq_comap_inv_mul_nhds_one_swapped :
    𝓤 α = comap (fun x : α × α => x.2⁻¹ * x.1) (𝓝 (1 : α))

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ comap ((fun x => x.1⁻¹ * x.2) ∘ Prod.swap) (𝓝 1) = comap (fun x => x.2⁻¹ * x.1) (𝓝 1)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ 𝓤 α = comap (fun x => x.2⁻¹ * x.1) (𝓝 1)

Tactic:
rw [← comap_swap_uniformity, uniformity_eq_comap_inv_mul_nhds_one, comap_comap]

Result:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
⊢ comap ((fun x => x.1⁻¹ * x.2) ∘ Prod.swap) (𝓝 1) = comap (fun x => x.2⁻¹ * x.1) (𝓝 1)
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrix'_comp [Fintype l] [DecidableEq l] (f : (n → R) →ₗ[R] m → R)
    (g : (l → R) →ₗ[R] n → R) :
    LinearMap.toMatrix' (f.comp g) = LinearMap.toMatrix' f * LinearMap.toMatrix' g

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
⊢ f ∘ₗ g = toLin' (toMatrix' f * toMatrix' g)

Tactic:
rw [Matrix.toLin'_mul, Matrix.toLin'_toMatrix', Matrix.toLin'_toMatrix']

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
⊢ toMatrix' (f ∘ₗ g) = toMatrix' f * toMatrix' g

Tactic:
suffices f.comp g = Matrix.toLin' (LinearMap.toMatrix' f * LinearMap.toMatrix' g) by
  rw [this, LinearMap.toMatrix'_toLin']

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
⊢ f ∘ₗ g = toLin' (toMatrix' f * toMatrix' g)

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : Fintype l
inst✝ : DecidableEq l
f : (n → R) →ₗ[R] m → R
g : (l → R) →ₗ[R] n → R
this : f ∘ₗ g = toLin' (toMatrix' f * toMatrix' g)
⊢ toMatrix' (f ∘ₗ g) = toMatrix' f * toMatrix' g

Tactic:
rw [this, LinearMap.toMatrix'_toLin']

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma stableUnderSpecialization_singleton {x : PrimeSpectrum R} :
    StableUnderSpecialization {x} ↔ x.asIdeal.IsMaximal

Proof state:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ (a : PrimeSpectrum R), x ≤ a → a = x) ↔ IsMax x

Tactic:
exact ⟨fun H a h ↦ (H a h).le, fun H a h ↦ le_antisymm (H h) h⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ StableUnderSpecialization {x} ↔ x.asIdeal.IsMaximal

Tactic:
simp_rw [← isMax_iff, StableUnderSpecialization, ← le_iff_specializes, Set.mem_singleton_iff,
  @forall_comm _ (_ = _), forall_eq]

Result:
R : Type u
inst✝ : CommSemiring R
x : PrimeSpectrum R
⊢ (∀ (a : PrimeSpectrum R), x ≤ a → a = x) ↔ IsMax x
-- Mathlib/Algebra/Polynomial/Degree/SmallDegree.lean
theorem le_natDegree_of_coe_le_degree (hdeg : ↑n ≤ p.degree) : n ≤ p.natDegree :=
  WithBot.coe_le_coe.mp <| by
    rwa [degree_eq_natDegree <| ne_zero_of_coe_le_degree hdeg] at hdeg

Proof state:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
hdeg : ↑n ≤ p.degree
⊢ ↑n ≤ ↑p.natDegree

Tactic:
rwa [degree_eq_natDegree <| ne_zero_of_coe_le_degree hdeg] at hdeg

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
@[simp] lemma even_two : Even (2 : α) := ⟨1, by rw [one_add_one_eq_two]⟩

Proof state:
α : Type u_2
inst✝ : Semiring α
⊢ 2 = 1 + 1

Tactic:
rw [one_add_one_eq_two]

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem eta_fin_two (A : Matrix (Fin 2) (Fin 2) α) : A = !![A 0 0, A 0 1; A 1 0, A 1 1]

Proof state:
α : Type u
A : Matrix (Fin 2) (Fin 2) α
⊢ A = !![A 0 0, A 0 1; A 1 0, A 1 1]

Tactic:
ext i j

Result:
case a
α : Type u
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ A i j = !![A 0 0, A 0 1; A 1 0, A 1 1] i j

Proof state:
case a
α : Type u
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ A i j = !![A 0 0, A 0 1; A 1 0, A 1 1] i j

Tactic:
fin_cases i <;> fin_cases j <;> rfl

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem exists_normAtPlace_ne_zero_iff {x : mixedSpace K} :
    (∃ w, normAtPlace w x ≠ 0) ↔ x ≠ 0

Proof state:
K : Type u_1
inst✝ : Field K
x : mixedSpace K
⊢ (∃ w, (normAtPlace w) x ≠ 0) ↔ x ≠ 0

Tactic:
rw [ne_eq, ← forall_normAtPlace_eq_zero_iff, not_forall]

Result:
no goals
-- Mathlib/Computability/TMConfig.lean
theorem zero'_eval : zero'.eval = fun v => pure (0 :: v)

Proof state:
⊢ zero'.eval = fun v => pure (0 :: v)

Tactic:
simp [eval]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem Cauchy.exists_lb_coeff_ne {ℱ : Filter K⸨X⸩} (hℱ : Cauchy ℱ) :
    ∃ N, ∀ᶠ f : K⸨X⸩ in ℱ, ∀ d < N, coeff hℱ d = f.coeff d

Proof state:
case intro.intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
N₁ : ℤ
hN₁ : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N₁, f.coeff n = 0
N₂ : ℤ
hN₂ : ∀ n < N₂, coeff hℱ n = 0
⊢ ∃ N, ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d

Tactic:
refine ⟨min N₁ N₂, ℱ.3 hN₁ fun _ hf d hd ↦ ?_⟩

Result:
case intro.intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
N₁ : ℤ
hN₁ : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N₁, f.coeff n = 0
N₂ : ℤ
hN₂ : ∀ n < N₂, coeff hℱ n = 0
x✝ : K⸨X⸩
hf : x✝ ∈ {x | (fun f => ∀ n < N₁, f.coeff n = 0) x}
d : ℤ
hd : d < N₁ ⊓ N₂
⊢ coeff hℱ d = x✝.coeff d

Proof state:
case intro.intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
N₁ : ℤ
hN₁ : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N₁, f.coeff n = 0
N₂ : ℤ
hN₂ : ∀ n < N₂, coeff hℱ n = 0
x✝ : K⸨X⸩
hf : x✝ ∈ {x | (fun f => ∀ n < N₁, f.coeff n = 0) x}
d : ℤ
hd : d < N₁ ⊓ N₂
⊢ coeff hℱ d = x✝.coeff d

Tactic:
rw [hf d (lt_of_lt_of_le hd (min_le_left _ _)), hN₂ d (lt_of_lt_of_le hd (min_le_right _ _))]

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
⊢ ∃ N, ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d

Tactic:
obtain ⟨⟨N₁, hN₁⟩, ⟨N₂, hN₂⟩⟩ := exists_lb_eventual_support hℱ, exists_lb_support hℱ

Result:
case intro.intro
K : Type u_2
inst✝ : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
N₁ : ℤ
hN₁ : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N₁, f.coeff n = 0
N₂ : ℤ
hN₂ : ∀ n < N₂, coeff hℱ n = 0
⊢ ∃ N, ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d