harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
/-- `∏ i, (f i - g i) = (∏ i, f i) - ∑ i, g i * (∏ j < i, f j - g j) * (∏ j > i, f j)`. -/
lemma prod_sub_ordered [LinearOrder ι] (s : Finset ι) (f g : ι → α) :
    ∏ i ∈ s, (f i - g i) =
      (∏ i ∈ s, f i) -
        ∑ i ∈ s, g i * (∏ j ∈ s with j < i, (f j - g j)) * ∏ j ∈ s with i < j, f j

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommRing α
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → α
⊢ ∏ i ∈ s, (f i - g i) =
    ∏ i ∈ s, f i - ∑ i ∈ s, (g i * ∏ j ∈ filter (fun j => j < i) s, (f j - g j)) * ∏ j ∈ filter (fun j => i < j) s, f j

Tactic:
simp only [sub_eq_add_neg]

Result:
ι : Type u_1
α : Type u_3
inst✝¹ : CommRing α
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → α
⊢ ∏ x ∈ s, (f x + -g x) =
    ∏ i ∈ s, f i +
      -∑ x ∈ s, (g x * ∏ x ∈ filter (fun j => j < x) s, (f x + -g x)) * ∏ i ∈ filter (fun j => x < j) s, f i

Proof state:
case h.e'_3.h.e'_6
ι : Type u_1
α : Type u_3
inst✝¹ : CommRing α
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → α
⊢ -∑ x ∈ s, (g x * ∏ x ∈ filter (fun j => j < x) s, (f x + -g x)) * ∏ i ∈ filter (fun j => x < j) s, f i =
    ∑ i ∈ s, (-g i * ∏ j ∈ filter (fun j => j < i) s, (f j + -g j)) * ∏ j ∈ filter (fun j => i < j) s, f j

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommRing α
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → α
⊢ ∏ x ∈ s, (f x + -g x) =
    ∏ i ∈ s, f i +
      -∑ x ∈ s, (g x * ∏ x ∈ filter (fun j => j < x) s, (f x + -g x)) * ∏ i ∈ filter (fun j => x < j) s, f i

Tactic:
convert prod_add_ordered s f fun i => -g i

Result:
case h.e'_3.h.e'_6
ι : Type u_1
α : Type u_3
inst✝¹ : CommRing α
inst✝ : LinearOrder ι
s : Finset ι
f g : ι → α
⊢ -∑ x ∈ s, (g x * ∏ x ∈ filter (fun j => j < x) s, (f x + -g x)) * ∏ i ∈ filter (fun j => x < j) s, f i =
    ∑ i ∈ s, (-g i * ∏ j ∈ filter (fun j => j < i) s, (f j + -g j)) * ∏ j ∈ filter (fun j => i < j) s, f j
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem limit.map_post {D : Type u'} [Category.{v'} D] [HasLimitsOfShape J D] (H : C ⥤ D) :
    /- H (limit F) ⟶ H (limit G) ⟶ limit (G ⋙ H) vs
     H (limit F) ⟶ limit (F ⋙ H) ⟶ limit (G ⋙ H) -/
    H.map (limMap α) ≫ limit.post G H = limit.post F H ≫ limMap (whiskerRight α H)

Proof state:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasLimitsOfShape J D
H : C ⥤ D
⊢ H.map (limMap α) ≫ post G H = post F H ≫ limMap (whiskerRight α H)

Tactic:
ext

Result:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasLimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ (H.map (limMap α) ≫ post G H) ≫ π (G ⋙ H) j✝ = (post F H ≫ limMap (whiskerRight α H)) ≫ π (G ⋙ H) j✝

Proof state:
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasLimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ (H.map (limMap α) ≫ post G H) ≫ π (G ⋙ H) j✝ = (post F H ≫ limMap (whiskerRight α H)) ≫ π (G ⋙ H) j✝

Tactic:
simp only [whiskerRight_app, limMap_π, assoc, limit.post_π_assoc, limit.post_π, ← H.map_comp]

Result:
no goals
-- Mathlib/Algebra/Quandle.lean
theorem self_invAct_invAct_eq {x y : R} : (x ◃⁻¹ x) ◃⁻¹ y = x ◃⁻¹ y

Proof state:
R : Type u_1
inst✝ : Rack R
x y : R
h : (op x ◃ op x) ◃ op y = op x ◃ op y
⊢ (x ◃⁻¹ x) ◃⁻¹ y = x ◃⁻¹ y

Tactic:
simpa using h

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Rack R
x y : R
⊢ (x ◃⁻¹ x) ◃⁻¹ y = x ◃⁻¹ y

Tactic:
have h := @self_act_act_eq _ _ (op x) (op y)

Result:
R : Type u_1
inst✝ : Rack R
x y : R
h : (op x ◃ op x) ◃ op y = op x ◃ op y
⊢ (x ◃⁻¹ x) ◃⁻¹ y = x ◃⁻¹ y
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem isPiSystem_Iic_rat : IsPiSystem (⋃ a : ℚ, {Iic (a : ℝ)})

Proof state:
case h.e'_2.h
x : Set ℝ
⊢ x ∈ ⋃ a, {Iic ↑a} ↔ x ∈ Iic '' (Rat.cast '' univ)

Tactic:
simp only [iUnion_singleton_eq_range, mem_range, image_univ, mem_image, exists_exists_eq_and]

Result:
no goals

Proof state:
case h.e'_2

⊢ ⋃ a, {Iic ↑a} = Iic '' (Rat.cast '' univ)

Tactic:
ext x

Result:
case h.e'_2.h
x : Set ℝ
⊢ x ∈ ⋃ a, {Iic ↑a} ↔ x ∈ Iic '' (Rat.cast '' univ)

Proof state:
⊢ IsPiSystem (⋃ a, {Iic ↑a})

Tactic:
convert isPiSystem_image_Iic (((↑) : ℚ → ℝ) '' univ)

Result:
case h.e'_2

⊢ ⋃ a, {Iic ↑a} = Iic '' (Rat.cast '' univ)
-- Mathlib/CategoryTheory/Triangulated/Yoneda.lean
lemma preadditiveCoyoneda_homologySequenceδ_apply
    (T : Triangle C) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁) {A : Cᵒᵖ} (x : A.unop ⟶ T.obj₃⟦n₀⟧) :
    (preadditiveCoyoneda.obj A).homologySequenceδ T n₀ n₁ h x =
      x ≫ T.mor₃⟦n₀⟧' ≫ (shiftFunctorAdd' C 1 n₀ n₁ (by omega)).inv.app _

Proof state:
C : Type u_1
inst✝² : Category.{?u.7709, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : Cᵒᵖ
x : unop A ⟶ (shiftFunctor C n₀).obj T.obj₃
⊢ 1 + n₀ = n₁

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasShift C ℤ
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : Cᵒᵖ
x : unop A ⟶ (shiftFunctor C n₀).obj T.obj₃
⊢ (ConcreteCategory.hom ((preadditiveCoyoneda.obj A).homologySequenceδ T n₀ n₁ h)) x =
    x ≫ (shiftFunctor C n₀).map T.mor₃ ≫ (shiftFunctorAdd' C 1 n₀ n₁ ⋯).inv.app T.obj₁

Tactic:
apply Category.assoc

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
@[reassoc (attr := simp)]
lemma ι₀_π : ι₀ K ≫ π K = 𝟙 K

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
⊢ ι₀ K ≫ π K = 𝟙 K

Tactic:
simp [π]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_const_sub_Ioi : (fun x => a - x) '' Ioi b = Iio (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ (fun x => a - x) '' Ioi b = Iio (a - b)

Tactic:
have := image_comp (fun x => a + x) fun x => -x

Result:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioi b = Iio (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioi b = Iio (a - b)

Tactic:
dsimp [Function.comp_def] at this

Result:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioi b = Iio (a - b)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' Ioi b = Iio (a - b)

Tactic:
simp [sub_eq_add_neg, this, add_comm]

Result:
no goals
-- Mathlib/Computability/DFA.lean
theorem pumping_lemma [Fintype σ] {x : List α} (hx : x ∈ M.accepts)
    (hlen : Fintype.card σ ≤ List.length x) :
    ∃ a b c,
      x = a ++ b ++ c ∧
        a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.accepts

Proof state:
case right.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
ab : List α
hab : ∃ a_1 ∈ {a}, ∃ b_1 ∈ {b}∗, a_1 ++ b_1 = ab
c' : List α
hc' : c' ∈ {c}
⊢ ab ++ c' ∈ M.accepts

Tactic:
rcases hab with ⟨a', ha', b', hb', rfl⟩

Result:
case right.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
c' : List α
hc' : c' ∈ {c}
a' : List α
ha' : a' ∈ {a}
b' : List α
hb' : b' ∈ {b}∗
⊢ a' ++ b' ++ c' ∈ M.accepts

Proof state:
case right.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
ab : List α
hab : ab ∈ {a} * {b}∗
c' : List α
hc' : c' ∈ {c}
⊢ ab ++ c' ∈ M.accepts

Tactic:
rw [Language.mem_mul] at hab

Result:
case right.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
ab : List α
hab : ∃ a_1 ∈ {a}, ∃ b_1 ∈ {b}∗, a_1 ++ b_1 = ab
c' : List α
hc' : c' ∈ {c}
⊢ ab ++ c' ∈ M.accepts

Proof state:
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx : x ∈ M.accepts
hlen : Fintype.card σ ≤ x.length
⊢ ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.accepts

Tactic:
obtain ⟨_, a, b, c, hx, hlen, hnil, rfl, hb, hc⟩ := M.evalFrom_split (s := M.start) hlen rfl

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
σ : Type v
M : DFA α σ
inst✝ : Fintype σ
x : List α
hx✝ : x ∈ M.accepts
hlen✝ : Fintype.card σ ≤ x.length
a b c : List α
hx : x = a ++ b ++ c
hlen : a.length + b.length ≤ Fintype.card σ
hnil : b ≠ []
hb : M.evalFrom (M.evalFrom M.start a) b = M.evalFrom M.start a
hc : M.evalFrom (M.evalFrom M.start a) c = M.evalFrom M.start x
⊢ ∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.accepts
-- Mathlib/Algebra/Group/Commute/Basic.lean
@[to_additive]
lemma SemiconjBy.function_semiconj_mul_right_swap (h : SemiconjBy a b c) :
    Function.Semiconj (· * a) (· * c) (· * b) := fun j ↦ by simp only [mul_assoc, ← h.eq]

Proof state:
G : Type u_1
inst✝ : Semigroup G
a b c : G
h : SemiconjBy a b c
j : G
⊢ (fun x => x * a) ((fun x => x * c) j) = (fun x => x * b) ((fun x => x * a) j)

Tactic:
simp only [mul_assoc, ← h.eq]

Result:
no goals
-- Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
theorem sumIDeriv_apply_of_le {p : R[X]} {n : ℕ} (hn : p.natDegree ≤ n) :
    sumIDeriv p = ∑ i ∈ range (n + 1), derivative^[i] p

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ sumIDeriv p = ∑ i ∈ range (n + 1), (⇑derivative)^[i] p

Tactic:
dsimp [sumIDeriv]

Result:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ ((derivativeFinsupp p).sum fun i => id) = ∑ i ∈ range (n + 1), (⇑derivative)^[i] p

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ (derivativeFinsupp p).support ⊆ range (n + 1)

Tactic:
simp [Nat.lt_succ, hn]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ ((derivativeFinsupp p).sum fun i => id) = ∑ i ∈ range (n + 1), (⇑derivative)^[i] p

Tactic:
exact Finsupp.sum_of_support_subset _ (by simp [Nat.lt_succ, hn]) _ (by simp)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree ≤ n
⊢ ∀ i ∈ range (n + 1), id 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Size.lean
theorem size_zero : size 0 = 0

Proof state:
⊢ size 0 = 0

Tactic:
simp [size]

Result:
no goals
-- Mathlib/Data/Sign.lean
@[simp]
lemma sign_intCast {α : Type*} [OrderedRing α] [Nontrivial α]
    [DecidableRel ((· < ·) : α → α → Prop)] (n : ℤ) :
    sign (n : α) = sign n

Proof state:
α : Type u_2
inst✝² : OrderedRing α
inst✝¹ : Nontrivial α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
n : ℤ
⊢ sign ↑n = sign n

Tactic:
simp only [sign_apply, Int.cast_pos, Int.cast_lt_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem Basis.det_unitsSMul (e : Basis ι R M) (w : ι → Rˣ) :
    (e.unitsSMul w).det = (↑(∏ i, w i)⁻¹ : R) • e.det

Proof state:
case H
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ (e.unitsSMul w).det f = (↑(∏ i : ι, w i)⁻¹ • e.det) f

Tactic:
change
  (Matrix.det fun i j => (e.unitsSMul w).repr (f j) i) =
    (↑(∏ i, w i)⁻¹ : R) • Matrix.det fun i j => e.repr (f j) i

Result:
case H
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ (Matrix.det fun i j => ((e.unitsSMul w).repr (f j)) i) = ↑(∏ i : ι, w i)⁻¹ • Matrix.det fun i j => (e.repr (f j)) i

Proof state:
case H
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ (Matrix.det fun i j => ((e.unitsSMul w).repr (f j)) i) = ↑(∏ i : ι, w i)⁻¹ • Matrix.det fun i j => (e.repr (f j)) i

Tactic:
simp only [e.repr_unitsSMul]

Result:
case H
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ (Matrix.det fun i j => (w i)⁻¹ • (e.repr (f j)) i) = ↑(∏ i : ι, w i)⁻¹ • Matrix.det fun i j => (e.repr (f j)) i

Proof state:
case H
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ (Matrix.det fun i j => (w i)⁻¹ • (e.repr (f j)) i) = ↑(∏ i : ι, w i)⁻¹ • Matrix.det fun i j => (e.repr (f j)) i

Tactic:
convert Matrix.det_mul_column (fun i => (↑(w i)⁻¹ : R)) fun i j => e.repr (f j) i

Result:
case h.e'_3.h.e'_1
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ ↑(∏ i : ι, w i)⁻¹ = ∏ i : ι, ↑(w i)⁻¹

Proof state:
case h.e'_3.h.e'_1
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ ↑(∏ i : ι, w i)⁻¹ = ∏ i : ι, ↑(w i)⁻¹

Tactic:
simp [← Finset.prod_inv_distrib]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
w : ι → Rˣ
⊢ (e.unitsSMul w).det = ↑(∏ i : ι, w i)⁻¹ • e.det

Tactic:
ext f

Result:
case H
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
e : Basis ι R M
w : ι → Rˣ
f : ι → M
⊢ (e.unitsSMul w).det f = (↑(∏ i : ι, w i)⁻¹ • e.det) f
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean
theorem go_get (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWidth curr : Nat)
    (hcurr : curr ≤ newWidth) (s : AIG.RefVec aig curr) :
    ∀ (idx : Nat) (hidx : idx < curr),
        (go aig w input newWidth curr hcurr s).vec.get idx (by omega)
          =
        (s.get idx hidx).cast (by apply go_le_size)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefVec w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefVec curr
⊢ ∀ (idx : Nat) (hidx : idx < curr), (go aig w input newWidth curr hcurr s).vec.get idx ⋯ = (s.get idx hidx).cast ⋯

Tactic:
intros

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefVec w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefVec curr
idx✝ : Nat
hidx✝ : idx✝ < curr
⊢ (go aig w input newWidth curr hcurr s).vec.get idx✝ ⋯ = (s.get idx✝ hidx✝).cast ⋯

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefVec w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefVec curr
idx✝ : Nat
hidx✝ : idx✝ < curr
⊢ (go aig w input newWidth curr hcurr s).vec.get idx✝ ⋯ = (s.get idx✝ hidx✝).cast ⋯

Tactic:
apply go_get_aux

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefVec w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
⊢ idx < newWidth

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
input : aig.RefVec w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefVec curr
idx : Nat
hidx : idx < curr
⊢ aig.decls.size ≤ (go aig w input newWidth curr hcurr s).aig.decls.size

Tactic:
apply go_le_size

Result:
no goals
-- Mathlib/NumberTheory/BernoulliPolynomials.lean
theorem bernoulli_eval_zero (n : ℕ) : (bernoulli n).eval 0 = _root_.bernoulli n

Proof state:
n : ℕ
⊢ ∑ x ∈ range n, _root_.bernoulli x * ↑(n.choose x) * 0 ^ (n - x) = 0

Tactic:
apply sum_eq_zero fun x hx => _

Result:
n : ℕ
⊢ ∀ x ∈ range n, _root_.bernoulli x * ↑(n.choose x) * 0 ^ (n - x) = 0

Proof state:
n : ℕ
⊢ ∑ x ∈ range n, eval 0 ((monomial (n - x)) (_root_.bernoulli x * ↑(n.choose x))) +
      eval 0 ((monomial (n - n)) (_root_.bernoulli n * ↑(n.choose n))) =
    _root_.bernoulli n

Tactic:
have : ∑ x ∈ range n, _root_.bernoulli x * n.choose x * 0 ^ (n - x) = 0 := by
  apply sum_eq_zero fun x hx => _
  intros x hx
  simp [tsub_eq_zero_iff_le, mem_range.1 hx]

Result:
n : ℕ
this : ∑ x ∈ range n, _root_.bernoulli x * ↑(n.choose x) * 0 ^ (n - x) = 0
⊢ ∑ x ∈ range n, eval 0 ((monomial (n - x)) (_root_.bernoulli x * ↑(n.choose x))) +
      eval 0 ((monomial (n - n)) (_root_.bernoulli n * ↑(n.choose n))) =
    _root_.bernoulli n

Proof state:
n : ℕ
⊢ eval 0 (bernoulli n) = _root_.bernoulli n

Tactic:
rw [bernoulli, eval_finset_sum, sum_range_succ]

Result:
n : ℕ
⊢ ∑ x ∈ range n, eval 0 ((monomial (n - x)) (_root_.bernoulli x * ↑(n.choose x))) +
      eval 0 ((monomial (n - n)) (_root_.bernoulli n * ↑(n.choose n))) =
    _root_.bernoulli n

Proof state:
n : ℕ
⊢ ∀ x ∈ range n, _root_.bernoulli x * ↑(n.choose x) * 0 ^ (n - x) = 0

Tactic:
intros x hx

Result:
n x : ℕ
hx : x ∈ range n
⊢ _root_.bernoulli x * ↑(n.choose x) * 0 ^ (n - x) = 0

Proof state:
n : ℕ
this : ∑ x ∈ range n, _root_.bernoulli x * ↑(n.choose x) * 0 ^ (n - x) = 0
⊢ ∑ x ∈ range n, eval 0 ((monomial (n - x)) (_root_.bernoulli x * ↑(n.choose x))) +
      eval 0 ((monomial (n - n)) (_root_.bernoulli n * ↑(n.choose n))) =
    _root_.bernoulli n

Tactic:
simp [this]

Result:
no goals

Proof state:
n x : ℕ
hx : x ∈ range n
⊢ _root_.bernoulli x * ↑(n.choose x) * 0 ^ (n - x) = 0

Tactic:
simp [tsub_eq_zero_iff_le, mem_range.1 hx]

Result:
no goals
-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
theorem snd_isOpenEmbedding_of_left {X Y S : TopCat} {f : X ⟶ S} (H : IsOpenEmbedding f)
    (g : Y ⟶ S) : IsOpenEmbedding <| ⇑(pullback.snd f g)

Proof state:
case h.e'_5
X Y S : TopCat
f : X ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ ⇑(ConcreteCategory.hom (pullback.snd f g)) =
    ⇑(homeoOfIso (asIso (pullback.snd (𝟙 S) g))) ∘ ⇑(ConcreteCategory.hom (pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) ⋯ ⋯))

Tactic:
simp [homeoOfIso, ← coe_comp]

Result:
no goals

Proof state:
X Y S : TopCat
f : X ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ g ≫ 𝟙 S = 𝟙 Y ≫ g

Tactic:
simp

Result:
no goals

Proof state:
X Y S : TopCat
f : X ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ IsOpenEmbedding ⇑(ConcreteCategory.hom (pullback.snd f g))

Tactic:
convert (homeoOfIso (asIso (pullback.snd (𝟙 S) g))).isOpenEmbedding.comp
    (pullback_map_isOpenEmbedding (i₂ := 𝟙 Y) f g (𝟙 _) g H
      (homeoOfIso (Iso.refl _)).isOpenEmbedding (𝟙 _) rfl (by simp))

Result:
case h.e'_5
X Y S : TopCat
f : X ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ ⇑(ConcreteCategory.hom (pullback.snd f g)) =
    ⇑(homeoOfIso (asIso (pullback.snd (𝟙 S) g))) ∘ ⇑(ConcreteCategory.hom (pullback.map f g (𝟙 S) g f (𝟙 Y) (𝟙 S) ⋯ ⋯))
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem rotation_oangle_eq_iff_norm_eq (x y : V) : o.rotation (o.oangle x y) x = y ↔ ‖x‖ = ‖y‖

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ (o.rotation (o.oangle x y)) x = y ↔ ‖x‖ = ‖y‖

Tactic:
constructor

Result:
case mp
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ (o.rotation (o.oangle x y)) x = y → ‖x‖ = ‖y‖

case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ ‖x‖ = ‖y‖ → (o.rotation (o.oangle x y)) x = y

Proof state:
case mp
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.rotation (o.oangle x y)) x = y
⊢ ‖x‖ = ‖y‖

Tactic:
rw [← h, LinearIsometryEquiv.norm_map]

Result:
no goals

Proof state:
case mp
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ (o.rotation (o.oangle x y)) x = y → ‖x‖ = ‖y‖

Tactic:
intro h

Result:
case mp
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.rotation (o.oangle x y)) x = y
⊢ ‖x‖ = ‖y‖

Proof state:
case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
⊢ (o.rotation (o.oangle x y)) x = y

Tactic:
rw [o.eq_iff_oangle_eq_zero_of_norm_eq] <;> simp [h]

Result:
no goals

Proof state:
case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ ‖x‖ = ‖y‖ → (o.rotation (o.oangle x y)) x = y

Tactic:
intro h

Result:
case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
⊢ (o.rotation (o.oangle x y)) x = y
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem neg_mkRat (n d) : -mkRat n d = mkRat (-n) d

Proof state:
n : Int
d : Nat
z : d = 0
⊢ -0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
n : Int
d : Nat
z : ¬d = 0
⊢ -mkRat n d = mkRat (-n) d

Tactic:
simp [← normalize_eq_mkRat z, neg_normalize]

Result:
no goals

Proof state:
n : Int
d : Nat
⊢ -mkRat n d = mkRat (-n) d

Tactic:
if z : d = 0 then simp [z]; rfl else simp [← normalize_eq_mkRat z, neg_normalize]

Result:
no goals

Proof state:
n : Int
d : Nat
z : d = 0
⊢ -mkRat n d = mkRat (-n) d

Tactic:
simp [z]

Result:
n : Int
d : Nat
z : d = 0
⊢ -0 = 0
-- Mathlib/Data/PNat/Prime.lean
theorem gcd_one {n : ℕ+} : gcd n 1 = 1

Proof state:
n : ℕ+
⊢ gcd 1 n = 1

Tactic:
apply one_gcd

Result:
no goals

Proof state:
n : ℕ+
⊢ n.gcd 1 = 1

Tactic:
rw [gcd_comm]

Result:
n : ℕ+
⊢ gcd 1 n = 1