harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Ordmap/Ordset.lean
theorem insert_eq_insertWith [DecidableRel (α := α) (· ≤ ·)] (x : α) :
    ∀ t, Ordnode.insert x t = insertWith (fun _ => x) x t
  | nil => rfl
  | node _ l y r => by
    unfold Ordnode.insert insertWith; cases cmpLE x y <;> simp [insert_eq_insertWith]

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match cmpLE x y with
    | Ordering.lt => (Ordnode.insert x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (Ordnode.insert x r)) =
    match cmpLE x y with
    | Ordering.lt => (insertWith (fun x_1 => x) x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (insertWith (fun x_1 => x) x r)

Tactic:
cases cmpLE x y <;> simp [insert_eq_insertWith]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ Ordnode.insert x (node size✝ l y r) = insertWith (fun x_1 => x) x (node size✝ l y r)

Tactic:
unfold Ordnode.insert insertWith

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
x : α
size✝ : ℕ
l : Ordnode α
y : α
r : Ordnode α
⊢ (match cmpLE x y with
    | Ordering.lt => (Ordnode.insert x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (Ordnode.insert x r)) =
    match cmpLE x y with
    | Ordering.lt => (insertWith (fun x_1 => x) x l).balanceL y r
    | Ordering.eq => node size✝ l x r
    | Ordering.gt => l.balanceR y (insertWith (fun x_1 => x) x r)
-- Mathlib/Topology/FiberBundle/Constructions.lean
theorem isInducing_toProd : IsInducing (TotalSpace.toProd B F) :=
  ⟨by simp only [instTopologicalSpaceProd, induced_inf, induced_compose]; rfl⟩

Proof state:
B : Type u_1
F : Type u_2
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
⊢ topologicalSpace B F =
    induced (Prod.fst ∘ ⇑(TotalSpace.toProd B F)) inst✝¹ ⊓ induced (Prod.snd ∘ ⇑(TotalSpace.toProd B F)) inst✝

Tactic:
rfl

Result:
no goals

Proof state:
B : Type u_1
F : Type u_2
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
⊢ topologicalSpace B F = induced (⇑(TotalSpace.toProd B F)) instTopologicalSpaceProd

Tactic:
simp only [instTopologicalSpaceProd, induced_inf, induced_compose]

Result:
B : Type u_1
F : Type u_2
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
⊢ topologicalSpace B F =
    induced (Prod.fst ∘ ⇑(TotalSpace.toProd B F)) inst✝¹ ⊓ induced (Prod.snd ∘ ⇑(TotalSpace.toProd B F)) inst✝
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem nnnorm_prod_le (s : Finset ι) (f : ι → E) : ‖∏ a ∈ s, f a‖₊ ≤ ∑ a ∈ s, ‖f a‖₊ :=
  NNReal.coe_le_coe.1 <| by
    push_cast
    exact norm_prod_le _ _

Proof state:
ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f : ι → E
⊢ ‖∏ a ∈ s, f a‖ ≤ ∑ x ∈ s, ‖f x‖

Tactic:
exact norm_prod_le _ _

Result:
no goals

Proof state:
ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f : ι → E
⊢ ↑‖∏ a ∈ s, f a‖₊ ≤ ↑(∑ a ∈ s, ‖f a‖₊)

Tactic:
push_cast

Result:
ι : Type u_3
E : Type u_5
inst✝ : SeminormedCommGroup E
s : Finset ι
f : ι → E
⊢ ‖∏ a ∈ s, f a‖ ≤ ∑ x ∈ s, ‖f x‖
-- Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
theorem lineMap_apply_module (p₀ p₁ : V1) (c : k) : lineMap p₀ p₁ c = (1 - c) • p₀ + c • p₁

Proof state:
k : Type u_1
V1 : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V1
inst✝ : Module k V1
p₀ p₁ : V1
c : k
⊢ (lineMap p₀ p₁) c = (1 - c) • p₀ + c • p₁

Tactic:
simp [lineMap_apply_module', smul_sub, sub_smul]

Result:
k : Type u_1
V1 : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V1
inst✝ : Module k V1
p₀ p₁ : V1
c : k
⊢ c • p₁ - c • p₀ + p₀ = p₀ - c • p₀ + c • p₁

Proof state:
k : Type u_1
V1 : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V1
inst✝ : Module k V1
p₀ p₁ : V1
c : k
⊢ c • p₁ - c • p₀ + p₀ = p₀ - c • p₀ + c • p₁

Tactic:
abel

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/NatCast.lean
lemma zero_le_two [Preorder α] [ZeroLEOneClass α] [AddLeftMono α] :
    (0 : α) ≤ 2

Proof state:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 1 + 1

Tactic:
exact add_nonneg zero_le_one zero_le_one

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 2

Tactic:
rw [← one_add_one_eq_two]

Result:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : Preorder α
inst✝¹ : ZeroLEOneClass α
inst✝ : AddLeftMono α
⊢ 0 ≤ 1 + 1
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma add_smul_equiv (P Q : Fin 3 → R) {u v : R} (hu : IsUnit u) (hv : IsUnit v) :
    W'.add (u • P) (v • Q) ≈ W'.add P Q

Proof state:
case neg
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : ¬P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

Tactic:
exact ⟨(hu.unit * hv.unit) ^ 2, by convert (add_smul_of_not_equiv h hu hv).symm⟩

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

Tactic:
by_cases h : P ≈ Q

Result:
case pos
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

case neg
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : ¬P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : ¬P ≈ Q
⊢ (fun m => m • W'.add P Q) ((hu.unit * hv.unit) ^ 2) = W'.add (u • P) (v • Q)

Tactic:
convert (add_smul_of_not_equiv h hu hv).symm

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : P ≈ Q
⊢ (fun m => m • W'.add P Q) (hu.unit ^ 4) = W'.add (u • P) (v • Q)

Tactic:
convert (add_smul_of_equiv h hu hv).symm

Result:
no goals

Proof state:
case pos
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
hu : IsUnit u
hv : IsUnit v
h : P ≈ Q
⊢ W'.add (u • P) (v • Q) ≈ W'.add P Q

Tactic:
exact ⟨hu.unit ^ 4, by convert (add_smul_of_equiv h hu hv).symm⟩

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/End.lean
@[reassoc]
lemma end_.condition {i j : J} (f : i ⟶ j) :
    π F i ≫ (F.obj (op i)).map f = π F j ≫ (F.map f.op).app j

Proof state:
J : Type u
inst✝² : Category.{v, u} J
C : Type u'
inst✝¹ : Category.{v', u'} C
F : Jᵒᵖ ⥤ J ⥤ C
inst✝ : HasEnd F
i j : J
f : i ⟶ j
⊢ π F i ≫ (F.obj (op i)).map f = π F j ≫ (F.map f.op).app j

Tactic:
apply Wedge.condition

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma eval_polynomialX_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    eval P W.polynomialX / P z ^ 2 = W.toAffine.polynomialX.evalEval (P x / P z) (P y / P z)

Proof state:
case a.a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomialX / P z ^ 2 +
        (W.a₁ * P y / P z * 1 + 2 * W.a₂ * P x / P z * (P z / P z) + W.a₄ * (P z ^ 2 / P z ^ 2)) -
      (Polynomial.evalEval (P x / P z) (P y / P z) (toAffine W).polynomialX +
        (W.a₁ * P y / P z * (P z / P z) + 2 * W.a₂ * P x / P z * 1 + W.a₄ * 1)) =
    0

Tactic:
rw [eval_polynomialX, Affine.evalEval_polynomialX]

Result:
case a.a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z + W.a₄ * P z ^ 2)) / P z ^ 2 +
        (W.a₁ * P y / P z * 1 + 2 * W.a₂ * P x / P z * (P z / P z) + W.a₄ * (P z ^ 2 / P z ^ 2)) -
      ((toAffine W).a₁ * (P y / P z) - (3 * (P x / P z) ^ 2 + 2 * (toAffine W).a₂ * (P x / P z) + (toAffine W).a₄) +
        (W.a₁ * P y / P z * (P z / P z) + 2 * W.a₂ * P x / P z * 1 + W.a₄ * 1)) =
    0

Proof state:
case a.a
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z + W.a₄ * P z ^ 2)) / P z ^ 2 +
        (W.a₁ * P y / P z * 1 + 2 * W.a₂ * P x / P z * (P z / P z) + W.a₄ * (P z ^ 2 / P z ^ 2)) -
      ((toAffine W).a₁ * (P y / P z) - (3 * (P x / P z) ^ 2 + 2 * (toAffine W).a₂ * (P x / P z) + (toAffine W).a₄) +
        (W.a₁ * P y / P z * (P z / P z) + 2 * W.a₂ * P x / P z * 1 + W.a₄ * 1)) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : Fin 3 → F
hPz : P z ≠ 0
⊢ (eval P) W.polynomialX / P z ^ 2 = Polynomial.evalEval (P x / P z) (P y / P z) (toAffine W).polynomialX

Tactic:
linear_combination (norm := (rw [eval_polynomialX, Affine.evalEval_polynomialX]; ring1))
  W.a₁ * P y / P z * div_self hPz - 2 * W.a₂ * P x / P z * div_self hPz
    - W.a₄ * div_self (pow_ne_zero 2 hPz)

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Submodule.lean
lemma localized₀_smul (I : Submodule R R) : (I • M').localized₀ p f = I • M'.localized₀ p f

Proof state:
case a.intro.intro.intro
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
r : R
hr : r ∈ I
a : M
ha : a ∈ M'
s : ↥p
⊢ r • IsLocalizedModule.mk' f a s ∈ localized₀ p f (I • M')

Tactic:
rw [← IsLocalizedModule.mk'_smul]

Result:
case a.intro.intro.intro
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
I : Submodule R R
r : R
hr : r ∈ I
a : M
ha : a ∈ M'
s : ↥p
⊢ IsLocalizedModule.mk' f (r • a) s ∈ localized₀ p f (I • M')
-- Mathlib/Data/Nat/Periodic.lean
theorem periodic_gcd (a : ℕ) : Periodic (gcd a) a

Proof state:
a : ℕ
⊢ Periodic a.gcd a

Tactic:
simp only [forall_const, gcd_add_self_right, eq_self_iff_true, Periodic]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem add_top (x : PartENat) : x + ⊤ = ⊤

Proof state:
x : PartENat
⊢ x + ⊤ = ⊤

Tactic:
rw [add_comm, top_add]

Result:
no goals
-- Mathlib/CategoryTheory/PathCategory/Basic.lean
theorem lift_spec {C} [Category C] (φ : V ⥤q C) : of ⋙q (lift φ).toPrefunctor = φ

Proof state:
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
⊢ ∀ (X : V), (of ⋙q (lift φ).toPrefunctor).obj X = φ.obj X

Tactic:
rintro X

Result:
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
X : V
⊢ (of ⋙q (lift φ).toPrefunctor).obj X = φ.obj X

Proof state:
case h_map.mk
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : V
f : X ⟶ Y
φo : V → C
φm : {X Y : V} → (X ⟶ Y) → (φo X ⟶ φo Y)
⊢ 𝟙 (φo X) ≫ φm f = φm f

Tactic:
simp only [Category.id_comp]

Result:
no goals

Proof state:
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
X Y : V
f : X ⟶ Y
⊢ (of ⋙q (lift φ).toPrefunctor).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Tactic:
rcases φ with ⟨φo, φm⟩

Result:
case h_map.mk
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : V
f : X ⟶ Y
φo : V → C
φm : {X Y : V} → (X ⟶ Y) → (φo X ⟶ φo Y)
⊢ (of ⋙q (lift { obj := φo, map := φm }).toPrefunctor).map f = Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := φo, map := φm }.map f))

Proof state:
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of ⋙q (lift φ).toPrefunctor).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Tactic:
rintro X Y f

Result:
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
X Y : V
f : X ⟶ Y
⊢ (of ⋙q (lift φ).toPrefunctor).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))

Proof state:
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
X : V
⊢ (of ⋙q (lift φ).toPrefunctor).obj X = φ.obj X

Tactic:
rfl

Result:
no goals

Proof state:
case h_map.mk
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : V
f : X ⟶ Y
φo : V → C
φm : {X Y : V} → (X ⟶ Y) → (φo X ⟶ φo Y)
⊢ (of ⋙q (lift { obj := φo, map := φm }).toPrefunctor).map f = Eq.recOn ⋯ (Eq.recOn ⋯ ({ obj := φo, map := φm }.map f))

Tactic:
dsimp [lift, Quiver.Hom.toPath]

Result:
case h_map.mk
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : V
f : X ⟶ Y
φo : V → C
φm : {X Y : V} → (X ⟶ Y) → (φo X ⟶ φo Y)
⊢ 𝟙 (φo X) ≫ φm f = φm f

Proof state:
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
⊢ of ⋙q (lift φ).toPrefunctor = φ

Tactic:
fapply Prefunctor.ext

Result:
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
⊢ ∀ (X : V), (of ⋙q (lift φ).toPrefunctor).obj X = φ.obj X

case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{u_2, u_1} C
φ : V ⥤q C
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of ⋙q (lift φ).toPrefunctor).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))
-- Mathlib/Data/Nat/Digits.lean
@[simp]
lemma digits_of_two_le_of_pos {b : ℕ} (hb : 2 ≤ b) (hn : 0 < n) :
    Nat.digits b n = n % b :: Nat.digits b (n / b)

Proof state:
n b : ℕ
hb : 2 ≤ b
hn : 0 < n
⊢ b.digits n = n % b :: b.digits (n / b)

Tactic:
rw [Nat.eq_add_of_sub_eq hb rfl, Nat.eq_add_of_sub_eq hn rfl, Nat.digits_add_two_add_one]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
@[simp]
lemma snd_prod [IsProbabilityMeasure μ] : (μ.prod ν).snd = ν

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : IsProbabilityMeasure μ
s : Set β
hs : MeasurableSet s
⊢ (μ.prod ν).snd s = ν s

Tactic:
rw [snd_apply hs, ← univ_prod, prod_prod, measure_univ, one_mul]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : IsProbabilityMeasure μ
⊢ (μ.prod ν).snd = ν

Tactic:
ext1 s hs

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
inst✝ : IsProbabilityMeasure μ
s : Set β
hs : MeasurableSet s
⊢ (μ.prod ν).snd s = ν s
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem Hom.ext_zero_left {n : SimplexCategory} (f g : ⦋0⦌ ⟶ n)
    (h0 : f.toOrderHom 0 = g.toOrderHom 0

Proof state:
n : SimplexCategory
f g : ⦋0⦌ ⟶ n
h0 : autoParam ((toOrderHom f) 0 = (toOrderHom g) 0) _auto✝
i : Fin (⦋0⦌.len + 1)
⊢ ↑((toOrderHom f) 0) = ↑((toOrderHom g) 0)

Tactic:
exact h0 ▸ rfl

Result:
no goals

Proof state:
case a.h.h.h
n : SimplexCategory
f g : ⦋0⦌ ⟶ n
h0 : autoParam ((toOrderHom f) 0 = (toOrderHom g) 0) _auto✝
i : Fin (⦋0⦌.len + 1)
⊢ ↑((toOrderHom f) i) = ↑((toOrderHom g) i)

Tactic:
match i with | 0 => exact h0 ▸ rfl

Result:
no goals

Proof state:
n : SimplexCategory
f g : ⦋0⦌ ⟶ n
h0 : autoParam ((toOrderHom f) 0 = (toOrderHom g) 0) _auto✝
⊢ f = g

Tactic:
ext i

Result:
case a.h.h.h
n : SimplexCategory
f g : ⦋0⦌ ⟶ n
h0 : autoParam ((toOrderHom f) 0 = (toOrderHom g) 0) _auto✝
i : Fin (⦋0⦌.len + 1)
⊢ ↑((toOrderHom f) i) = ↑((toOrderHom g) i)
-- Mathlib/CategoryTheory/Limits/Cones.lean
theorem coconeOfConeLeftOp_ι_app (c : Cone F.leftOp) (j) :
    (coconeOfConeLeftOp c).ι.app j = (c.π.app (op j)).op

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ Cᵒᵖ
c : Cone F.leftOp
j : J
⊢ (coconeOfConeLeftOp c).ι.app j = (c.π.app (op j)).op

Tactic:
dsimp only [coconeOfConeLeftOp]

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ Cᵒᵖ
c : Cone F.leftOp
j : J
⊢ (NatTrans.removeLeftOp c.π).app j = (c.π.app (op j)).op

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ Cᵒᵖ
c : Cone F.leftOp
j : J
⊢ (NatTrans.removeLeftOp c.π).app j = (c.π.app (op j)).op

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem all_eq {xs : Vector α n} {p : α → Bool} : xs.all p = decide (∀ i, (_ : i < n) → p xs[i])

Proof state:
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
⊢ xs.all p = decide (∀ (i : Nat) (x : i < n), p xs[i] = true)

Tactic:
by_cases h : xs.all p

Result:
case pos
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : xs.all p = true
⊢ xs.all p = decide (∀ (i : Nat) (x : i < n), p xs[i] = true)

case neg
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : ¬xs.all p = true
⊢ xs.all p = decide (∀ (i : Nat) (x : i < n), p xs[i] = true)

Proof state:
case neg
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : ∃ i x, ¬p xs[i] = true
⊢ false = decide (∀ (i : Nat) (x : i < n), p xs[i] = true)

Tactic:
simpa using h

Result:
no goals

Proof state:
case neg
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : xs.all p = false
⊢ false = decide (∀ (i : Nat) (x : i < n), p xs[i] = true)

Tactic:
simp only [all_eq_false] at h

Result:
case neg
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : ∃ i x, ¬p xs[i] = true
⊢ false = decide (∀ (i : Nat) (x : i < n), p xs[i] = true)

Proof state:
case pos
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : xs.all p = true
⊢ xs.all p = decide (∀ (i : Nat) (x : i < n), p xs[i] = true)

Tactic:
simp_all [all_eq_true]

Result:
no goals

Proof state:
case neg
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : xs.all p = false
⊢ xs.all p = decide (∀ (i : Nat) (x : i < n), p xs[i] = true)

Tactic:
simp only [h]

Result:
case neg
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : xs.all p = false
⊢ false = decide (∀ (i : Nat) (x : i < n), p xs[i] = true)

Proof state:
case neg
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : ¬xs.all p = true
⊢ xs.all p = decide (∀ (i : Nat) (x : i < n), p xs[i] = true)

Tactic:
simp only [Bool.not_eq_true] at h

Result:
case neg
α : Type u_1
n : Nat
xs : Vector α n
p : α → Bool
h : xs.all p = false
⊢ xs.all p = decide (∀ (i : Nat) (x : i < n), p xs[i] = true)
-- Mathlib/Data/List/Permutation.lean
theorem length_permutationsAux2 (t : α) (ts : List α) (ys : List α) (f : List α → β) :
    length (permutationsAux2 t ts [] ys f).2 = length ys

Proof state:
α : Type u_1
β : Type u_2
t : α
ts ys : List α
f : List α → β
⊢ (permutationsAux2 t ts [] ys f).2.length = ys.length

Tactic:
induction ys generalizing f <;> simp [*]

Result:
no goals
-- Mathlib/RingTheory/PowerBasis.lean
theorem aeval_minpolyGen (pb : PowerBasis A S) : aeval pb.gen (minpolyGen pb) = 0

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ pb.gen ^ pb.dim - ∑ x : Fin pb.dim, (pb.basis.repr (pb.gen ^ pb.dim)) x • pb.gen ^ ↑x = 0

Tactic:
refine sub_eq_zero.mpr ((pb.basis.linearCombination_repr (pb.gen ^ pb.dim)).symm.trans ?_)

Result:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ (linearCombination A ⇑pb.basis) (pb.basis.repr (pb.gen ^ pb.dim)) =
    ∑ x : Fin pb.dim, (pb.basis.repr (pb.gen ^ pb.dim)) x • pb.gen ^ ↑x

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ (linearCombination A ⇑pb.basis) (pb.basis.repr (pb.gen ^ pb.dim)) =
    ∑ x : Fin pb.dim, (pb.basis.repr (pb.gen ^ pb.dim)) x • pb.gen ^ ↑x

Tactic:
rw [Finsupp.linearCombination_apply, Finsupp.sum_fintype] <;>
  simp only [pb.coe_basis, zero_smul, eq_self_iff_true, imp_true_iff]

Result:
no goals

Proof state:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ (aeval pb.gen) pb.minpolyGen = 0

Tactic:
simp_rw [minpolyGen, map_sub, map_sum, map_mul, map_pow, aeval_C, ← Algebra.smul_def, aeval_X]

Result:
S : Type u_2
inst✝² : Ring S
A : Type u_4
inst✝¹ : CommRing A
inst✝ : Algebra A S
pb : PowerBasis A S
⊢ pb.gen ^ pb.dim - ∑ x : Fin pb.dim, (pb.basis.repr (pb.gen ^ pb.dim)) x • pb.gen ^ ↑x = 0
-- Mathlib/Data/Finset/Max.lean
theorem map_ofDual_min (s : Finset αᵒᵈ) : s.min.map ofDual = (s.image ofDual).max

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithTop.map (⇑ofDual) s.min = s.sup (WithBot.some ∘ ⇑ofDual)

Tactic:
exact congr_fun Option.map_id _

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithTop.map (⇑ofDual) s.min = (image (⇑ofDual) s).max

Tactic:
rw [max_eq_sup_withBot, sup_image]

Result:
α : Type u_2
inst✝ : LinearOrder α
s : Finset αᵒᵈ
⊢ WithTop.map (⇑ofDual) s.min = s.sup (WithBot.some ∘ ⇑ofDual)
-- Mathlib/Algebra/Group/Pointwise/Set/Card.lean
@[to_additive]
lemma natCard_mul_le : Nat.card (s * t) ≤ Nat.card s * Nat.card t

Proof state:
case inr
M : Type u_2
inst✝¹ : Mul M
s t : Set M
inst✝ : IsCancelMul M
h : (s * t).Finite
⊢ #↑s * #↑t < ℵ₀

Tactic:
aesop (add simp [Cardinal.mul_lt_aleph0_iff, finite_mul])

Result:
no goals

Proof state:
M : Type u_2
inst✝¹ : Mul M
s t : Set M
inst✝ : IsCancelMul M
⊢ Nat.card ↑(s * t) ≤ Nat.card ↑s * Nat.card ↑t

Tactic:
obtain h | h := (s * t).infinite_or_finite

Result:
case inl
M : Type u_2
inst✝¹ : Mul M
s t : Set M
inst✝ : IsCancelMul M
h : (s * t).Infinite
⊢ Nat.card ↑(s * t) ≤ Nat.card ↑s * Nat.card ↑t

case inr
M : Type u_2
inst✝¹ : Mul M
s t : Set M
inst✝ : IsCancelMul M
h : (s * t).Finite
⊢ Nat.card ↑(s * t) ≤ Nat.card ↑s * Nat.card ↑t

Proof state:
case inr
M : Type u_2
inst✝¹ : Mul M
s t : Set M
inst✝ : IsCancelMul M
h : (s * t).Finite
⊢ Nat.card ↑(s * t) ≤ Nat.card ↑s * Nat.card ↑t

Tactic:
simp only [Nat.card, ← Cardinal.toNat_mul]

Result:
case inr
M : Type u_2
inst✝¹ : Mul M
s t : Set M
inst✝ : IsCancelMul M
h : (s * t).Finite
⊢ Cardinal.toNat #↑(s * t) ≤ Cardinal.toNat (#↑s * #↑t)

Proof state:
case inr
M : Type u_2
inst✝¹ : Mul M
s t : Set M
inst✝ : IsCancelMul M
h : (s * t).Finite
⊢ Cardinal.toNat #↑(s * t) ≤ Cardinal.toNat (#↑s * #↑t)

Tactic:
refine Cardinal.toNat_le_toNat Cardinal.mk_mul_le ?_

Result:
case inr
M : Type u_2
inst✝¹ : Mul M
s t : Set M
inst✝ : IsCancelMul M
h : (s * t).Finite
⊢ #↑s * #↑t < ℵ₀

Proof state:
case inl
M : Type u_2
inst✝¹ : Mul M
s t : Set M
inst✝ : IsCancelMul M
h : (s * t).Infinite
⊢ Nat.card ↑(s * t) ≤ Nat.card ↑s * Nat.card ↑t

Tactic:
simp [Set.Infinite.card_eq_zero h]

Result:
no goals