harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem push_pop_back (v : Vector α (n + 1)) : v.pop.push v.back = v

Proof state:
α : Type u_1
n : Nat
v : Vector α (n + 1)
i : Nat
x✝ : i < n + 1 - 1 + 1
h : ¬i < n
⊢ i = n + 1 - 1

Tactic:
omega

Result:
no goals

Proof state:
case pos
α : Type u_1
n : Nat
v : Vector α (n + 1)
i : Nat
x✝ : i < n + 1 - 1 + 1
h : i < n
⊢ (v.pop.push v.back)[i] = v[i]

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
α : Type u_1
n : Nat
v : Vector α (n + 1)
i : Nat
x✝ : i < n + 1 - 1 + 1
h : ¬i < n
⊢ (v.pop.push v.back)[i] = v[i]

Tactic:
replace h : i = v.size - 1 := by rw [size_toArray]; omega

Result:
case neg
α : Type u_1
n : Nat
v : Vector α (n + 1)
i : Nat
x✝ : i < n + 1 - 1 + 1
h : i = v.size - 1
⊢ (v.pop.push v.back)[i] = v[i]

Proof state:
case h
α : Type u_1
n : Nat
v : Vector α (n + 1)
i : Nat
x✝ : i < n + 1 - 1 + 1
⊢ (v.pop.push v.back)[i] = v[i]

Tactic:
by_cases h : i < n

Result:
case pos
α : Type u_1
n : Nat
v : Vector α (n + 1)
i : Nat
x✝ : i < n + 1 - 1 + 1
h : i < n
⊢ (v.pop.push v.back)[i] = v[i]

case neg
α : Type u_1
n : Nat
v : Vector α (n + 1)
i : Nat
x✝ : i < n + 1 - 1 + 1
h : ¬i < n
⊢ (v.pop.push v.back)[i] = v[i]

Proof state:
case neg
α : Type u_1
n : Nat
v : Vector α (n + 1)
x✝ : v.size - 1 < n + 1 - 1 + 1
⊢ (v.pop.push v.back)[v.size - 1] = v[v.size - 1]

Tactic:
simp [back]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
v : Vector α (n + 1)
⊢ v.pop.push v.back = v

Tactic:
ext i

Result:
case h
α : Type u_1
n : Nat
v : Vector α (n + 1)
i : Nat
x✝ : i < n + 1 - 1 + 1
⊢ (v.pop.push v.back)[i] = v[i]

Proof state:
α : Type u_1
n : Nat
v : Vector α (n + 1)
i : Nat
x✝ : i < n + 1 - 1 + 1
h : ¬i < n
⊢ i = v.size - 1

Tactic:
rw [size_toArray]

Result:
α : Type u_1
n : Nat
v : Vector α (n + 1)
i : Nat
x✝ : i < n + 1 - 1 + 1
h : ¬i < n
⊢ i = n + 1 - 1

Proof state:
case neg
α : Type u_1
n : Nat
v : Vector α (n + 1)
i : Nat
x✝ : i < n + 1 - 1 + 1
h : i = v.size - 1
⊢ (v.pop.push v.back)[i] = v[i]

Tactic:
subst h

Result:
case neg
α : Type u_1
n : Nat
v : Vector α (n + 1)
x✝ : v.size - 1 < n + 1 - 1 + 1
⊢ (v.pop.push v.back)[v.size - 1] = v[v.size - 1]
-- Mathlib/Algebra/Polynomial/Div.lean
lemma eq_of_monic_of_dvd_of_natDegree_le {R} [CommRing R] {p q : R[X]} (hp : p.Monic)
    (hq : q.Monic) (hdiv : p ∣ q) (hdeg : q.natDegree ≤ p.natDegree) : q = p

Proof state:
case h.e'_3
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
hdiv : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ p = C q.leadingCoeff * p

Tactic:
rw [hq.leadingCoeff, C_1, one_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
hdiv : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ q = p

Tactic:
convert eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le hp hdiv hdeg

Result:
case h.e'_3
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hp : p.Monic
hq : q.Monic
hdiv : p ∣ q
hdeg : q.natDegree ≤ p.natDegree
⊢ p = C q.leadingCoeff * p
-- Mathlib/Data/ZMod/Basic.lean
theorem cast_add (h : m ∣ n) (a b : ZMod n) : (cast (a + b : ZMod n) : R) = cast a + cast b

Proof state:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ (a + b).cast = a.cast + b.cast

Tactic:
symm

Result:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ a.cast + b.cast = (a + b).cast

Proof state:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ ↑↑a + ↑↑b = ↑↑(a + b)

Tactic:
rw [← Nat.cast_add, Fin.val_add, ← sub_eq_zero, ← Nat.cast_sub (Nat.mod_le _ _),
  @CharP.cast_eq_zero_iff R _ m]

Result:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ m ∣ ↑a + ↑b - (↑a + ↑b) % (n✝ + 1)

Proof state:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ a.cast + b.cast = (a + b).cast

Tactic:
dsimp [ZMod, ZMod.cast, ZMod.val]

Result:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ ↑↑a + ↑↑b = ↑↑(a + b)

Proof state:
case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ m ∣ ↑a + ↑b - (↑a + ↑b) % (n✝ + 1)

Tactic:
exact h.trans (Nat.dvd_sub_mod _)

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0
a b : ZMod 0
⊢ (a + b).cast = a.cast + b.cast

Tactic:
apply Int.cast_add

Result:
no goals

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ n
a b : ZMod n
⊢ (a + b).cast = a.cast + b.cast

Tactic:
cases n

Result:
case zero
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
h : m ∣ 0
a b : ZMod 0
⊢ (a + b).cast = a.cast + b.cast

case succ
R : Type u_1
inst✝¹ : Ring R
m : ℕ
inst✝ : CharP R m
n✝ : ℕ
h : m ∣ n✝ + 1
a b : ZMod (n✝ + 1)
⊢ (a + b).cast = a.cast + b.cast
-- Mathlib/LinearAlgebra/SymplecticGroup.lean
theorem mem_iff {A : Matrix (l ⊕ l) (l ⊕ l) R} :
    A ∈ symplecticGroup l R ↔ A * J l R * Aᵀ = J l R

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
⊢ A ∈ symplecticGroup l R ↔ A * J l R * Aᵀ = J l R

Tactic:
simp [symplecticGroup]

Result:
no goals
-- Mathlib/Analysis/Convex/Continuous.lean
lemma ConcaveOn.locallyLipschitzOn_iff_continuousOn (hC : IsOpen C) (hf : ConcaveOn ℝ C f) :
    LocallyLipschitzOn C f ↔ ContinuousOn f C

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen C
hf : ConcaveOn ℝ C f
⊢ LocallyLipschitzOn C f ↔ ContinuousOn f C

Tactic:
simpa using hf.neg.locallyLipschitzOn_iff_continuousOn hC

Result:
no goals
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem FamilyOfElements.Compatible.functorPullback (h : x.Compatible) :
    (x.functorPullback F).Compatible

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
Z : D
T : Presieve (F.obj Z)
x : FamilyOfElements P T
h : x.Compatible
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ Z
f₂ : Z₂ ⟶ Z
h₁ : Presieve.functorPullback F T f₁
h₂ : Presieve.functorPullback F T f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ F.map g₁ ≫ F.map f₁ = F.map g₂ ≫ F.map f₂

Tactic:
simp only [← F.map_comp, eq]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
Z : D
T : Presieve (F.obj Z)
x : FamilyOfElements P T
h : x.Compatible
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ Z
f₂ : Z₂ ⟶ Z
h₁ : Presieve.functorPullback F T f₁
h₂ : Presieve.functorPullback F T f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (F.op ⋙ P).map g₁.op (FamilyOfElements.functorPullback F x f₁ h₁) =
    (F.op ⋙ P).map g₂.op (FamilyOfElements.functorPullback F x f₂ h₂)

Tactic:
exact h (F.map g₁) (F.map g₂) h₁ h₂ (by simp only [← F.map_comp, eq])

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
Z : D
T : Presieve (F.obj Z)
x : FamilyOfElements P T
h : x.Compatible
⊢ (FamilyOfElements.functorPullback F x).Compatible

Tactic:
intro Z₁ Z₂ W g₁ g₂ f₁ f₂ h₁ h₂ eq

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
Z : D
T : Presieve (F.obj Z)
x : FamilyOfElements P T
h : x.Compatible
Z₁ Z₂ W : D
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ Z
f₂ : Z₂ ⟶ Z
h₁ : Presieve.functorPullback F T f₁
h₂ : Presieve.functorPullback F T f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (F.op ⋙ P).map g₁.op (FamilyOfElements.functorPullback F x f₁ h₁) =
    (F.op ⋙ P).map g₂.op (FamilyOfElements.functorPullback F x f₂ h₂)
-- Mathlib/Data/Vector/Mem.lean
theorem mem_iff_get (v : Vector α n) : a ∈ v.toList ↔ ∃ i, v.get i = a

Proof state:
α : Type u_1
n : ℕ
a : α
v : Vector α n
x✝ : ∃ i, ∃ (h : i < n), v.toList.get (Fin.cast ⋯ ⟨i, h⟩) = a
i : ℕ
hi : i < n
h : v.toList.get (Fin.cast ⋯ ⟨i, hi⟩) = a
⊢ i < v.toList.length

Tactic:
rwa [toList_length]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
a : α
v : Vector α n
⊢ (∃ i, ∃ (h : i < v.toList.length), v.toList.get ⟨i, h⟩ = a) ↔ ∃ i, ∃ (h : i < n), v.toList.get (Fin.cast ⋯ ⟨i, h⟩) = a

Tactic:
exact
  ⟨fun ⟨i, hi, h⟩ => ⟨i, by rwa [toList_length] at hi, h⟩, fun ⟨i, hi, h⟩ =>
    ⟨i, by rwa [toList_length], h⟩⟩

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
a : α
v : Vector α n
⊢ a ∈ v.toList ↔ ∃ i, v.get i = a

Tactic:
simp only [List.mem_iff_get, Fin.exists_iff, Vector.get_eq_get_toList]

Result:
α : Type u_1
n : ℕ
a : α
v : Vector α n
⊢ (∃ i, ∃ (h : i < v.toList.length), v.toList.get ⟨i, h⟩ = a) ↔ ∃ i, ∃ (h : i < n), v.toList.get (Fin.cast ⋯ ⟨i, h⟩) = a

Proof state:
α : Type u_1
n : ℕ
a : α
v : Vector α n
x✝ : ∃ i, ∃ (h : i < v.toList.length), v.toList.get ⟨i, h⟩ = a
i : ℕ
hi : i < v.toList.length
h : v.toList.get ⟨i, hi⟩ = a
⊢ i < n

Tactic:
rwa [toList_length] at hi

Result:
no goals
-- Mathlib/Order/Heyting/Boundary.lean
theorem boundary_hnot_hnot (a : α) : ∂ (￢￢a) = ∂ (￢a)

Proof state:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ ∂ (￢￢a) = ∂ (￢a)

Tactic:
simp_rw [boundary, hnot_hnot_hnot, inf_comm]

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
lemma rdrop_append_of_le_length {l₁ l₂ : List α} (k : ℕ) :
    k ≤ length l₂ → List.rdrop (l₁ ++ l₂) k = l₁ ++ List.rdrop l₂ k

Proof state:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.length
⊢ (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k

Tactic:
rw [← length_reverse] at hk

Result:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.reverse.length
⊢ (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k

Proof state:
α : Type u_1
l₁ l₂ : List α
k : ℕ
⊢ k ≤ l₂.length → (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k

Tactic:
intro hk

Result:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.length
⊢ (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k

Proof state:
α : Type u_1
l₁ l₂ : List α
k : ℕ
hk : k ≤ l₂.reverse.length
⊢ (l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k

Tactic:
rw [rdrop_eq_reverse_drop_reverse, reverse_append, drop_append_of_le_length hk,
  reverse_append, reverse_reverse, ← rdrop_eq_reverse_drop_reverse]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_eq_integral {s : ℂ} (hs : 0 < s.re) : Gamma s = GammaIntegral s :=
  Gamma_eq_GammaAux s 0 (by norm_cast; linarith)

Proof state:
s : ℂ
hs : 0 < s.re
⊢ -s.re < 0

Tactic:
linarith

Result:
no goals

Proof state:
s : ℂ
hs : 0 < s.re
⊢ -s.re < ↑0

Tactic:
norm_cast

Result:
s : ℂ
hs : 0 < s.re
⊢ -s.re < 0
-- Mathlib/Dynamics/Ergodic/Conservative.lean
theorem ae_mem_imp_frequently_image_mem (hf : Conservative f μ) (hs : NullMeasurableSet s μ) :
    ∀ᵐ x ∂μ, x ∈ s → ∃ᶠ n in atTop, f^[n] x ∈ s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
n : ℕ
⊢ ∀ᵐ (a : α) ∂μ, a ∈ s → ∃ b ≥ n, f^[b] a ∈ s

Tactic:
filter_upwards [measure_zero_iff_ae_nmem.1 (hf.measure_mem_forall_ge_image_not_mem_eq_zero hs n)]

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
n : ℕ
⊢ ∀ (a : α), ¬(a ∈ s ∧ ∀ m ≥ n, f^[m] a ∉ s) → a ∈ s → ∃ b ≥ n, f^[b] a ∈ s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
⊢ ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, a ∈ s → ∃ b ≥ i, f^[b] a ∈ s

Tactic:
intro n

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
n : ℕ
⊢ ∀ᵐ (a : α) ∂μ, a ∈ s → ∃ b ≥ n, f^[b] a ∈ s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → ∃ᶠ (n : ℕ) in atTop, f^[n] x ∈ s

Tactic:
simp only [frequently_atTop, @forall_swap (_ ∈ s), ae_all_iff]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
⊢ ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, a ∈ s → ∃ b ≥ i, f^[b] a ∈ s

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
hf : Conservative f μ
hs : NullMeasurableSet s μ
n : ℕ
⊢ ∀ (a : α), ¬(a ∈ s ∧ ∀ m ≥ n, f^[m] a ∉ s) → a ∈ s → ∃ b ≥ n, f^[b] a ∈ s

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Basic.lean
theorem epi_of_cokernel_π_eq_zero (h : cokernel.π f = 0) : Epi f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : cokernel.π f = 0
⊢ IsColimit (CokernelCofork.ofπ (cokernel.π f) ⋯)

Tactic:
exact IsColimit.ofIsoColimit (colimit.isColimit (parallelPair f 0)) (isoOfπ _)

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : cokernel.π f = 0
⊢ Epi f

Tactic:
apply NormalMonoCategory.epi_of_zero_cokernel _ (cokernel f)

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : cokernel.π f = 0
⊢ IsColimit (CokernelCofork.ofπ 0 ⋯)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : cokernel.π f = 0
⊢ IsColimit (CokernelCofork.ofπ 0 ⋯)

Tactic:
simp_rw [← h]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : cokernel.π f = 0
⊢ IsColimit (CokernelCofork.ofπ (cokernel.π f) ⋯)
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_le_mul_norm_add' (u v : E) : ‖v‖ ≤ ‖u * v‖ + ‖u‖ :=
  calc
    ‖v‖ = ‖u⁻¹ * (u * v)‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖v‖ = ‖u⁻¹ * (u * v)‖

Tactic:
rw [← mul_assoc, inv_mul_cancel, one_mul]

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖u⁻¹‖ + ‖u * v‖ = ‖u * v‖ + ‖u‖

Tactic:
rw [norm_inv', add_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem map_comp_rTensor (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (f' : S →ₗ[R] M) :
    (map f g).comp (f'.rTensor _) = map (f.comp f') g

Proof state:
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : AddCommMonoid P
inst✝⁶ : AddCommMonoid Q
inst✝⁵ : AddCommMonoid S
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R Q
inst✝¹ : Module R S
inst✝ : Module R P
f : M →ₗ[R] P
g : N →ₗ[R] Q
f' : S →ₗ[R] M
⊢ map f g ∘ₗ rTensor N f' = map (f ∘ₗ f') g

Tactic:
simp only [lTensor, rTensor, ← map_comp, id_comp, comp_id]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem sSup_toSubmodule_eq_iSup (S : Set (LieSubmodule R L M)) :
    (↑(sSup S) : Submodule R M) = ⨆ N ∈ S, (N : Submodule R M)

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
S : Set (LieSubmodule R L M)
⊢ ↑(sSup S) = ⨆ N ∈ S, ↑N

Tactic:
rw [sSup_toSubmodule, ← Set.image, sSup_image]

Result:
no goals
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem degree_multiset_prod_of_monic [Nontrivial R] (h : ∀ f ∈ t, Monic f) :
    t.prod.degree = (t.map degree).sum

Proof state:
R : Type u
inst✝¹ : CommSemiring R
t : Multiset R[X]
inst✝ : Nontrivial R
h : ∀ f ∈ t, f.Monic
⊢ t.prod.degree = (Multiset.map degree t).sum

Tactic:
have : t.prod ≠ 0 := Monic.ne_zero <| by simpa using monic_multiset_prod_of_monic _ _ h

Result:
R : Type u
inst✝¹ : CommSemiring R
t : Multiset R[X]
inst✝ : Nontrivial R
h : ∀ f ∈ t, f.Monic
this : t.prod ≠ 0
⊢ t.prod.degree = (Multiset.map degree t).sum

Proof state:
R : Type u
inst✝¹ : CommSemiring R
t : Multiset R[X]
inst✝ : Nontrivial R
h : ∀ f ∈ t, f.Monic
⊢ t.prod.Monic

Tactic:
simpa using monic_multiset_prod_of_monic _ _ h

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommSemiring R
t : Multiset R[X]
inst✝ : Nontrivial R
h : ∀ f ∈ t, f.Monic
this : t.prod ≠ 0
⊢ t.prod.degree = (Multiset.map degree t).sum

Tactic:
rw [degree_eq_natDegree this, natDegree_multiset_prod_of_monic _ h, Nat.cast_multiset_sum,
  Multiset.map_map, Function.comp_def,
  Multiset.map_congr rfl (fun f hf => (degree_eq_natDegree (h f hf).ne_zero).symm)]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem exists_isTwoBlockDiagonal_of_ne_zero (hM : M (inr unit) (inr unit) ≠ 0) :
    ∃ L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜),
      IsTwoBlockDiagonal ((L.map toMatrix).prod * M * (L'.map toMatrix).prod)

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn fun i => { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
i : Fin r
⊢ inr () ≠ inl i

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn fun i => { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn fun i => { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
⊢ ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal

Tactic:
have A : L.map toMatrix = listTransvecCol M := by simp [L, listTransvecCol, Function.comp_def]

Result:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn fun i => { i := inl i, j := inr (), hij := ⋯, c := -M (inl i) (inr ()) / M (inr ()) (inr ()) }
L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
  List.ofFn fun i => { i := inr (), j := inl i, hij := ⋯, c := -M (inr ()) (inl i) / M (inr ()) (inr ()) }
A : List.map toMatrix L = listTransvecCol M
⊢ ((List.map toMatrix L).prod * M * (List.map toMatrix L').prod).IsTwoBlockDiagonal
-- Mathlib/MeasureTheory/Measure/Haar/Quotient.lean
/-- The `essSup` of a function `g` on the quotient space `G ⧸ Γ` with respect to the pushforward
  of the restriction, `μ_𝓕`, of a right-invariant measure `μ` to a fundamental domain `𝓕`, is the
  same as the `essSup` of `g`'s lift to the universal cover `G` with respect to `μ`. -/
@[to_additive "The `essSup` of a function `g` on the additive quotient space `G ⧸ Γ` with respect
  to the pushforward of the restriction, `μ_𝓕`, of a right-invariant measure `μ` to a fundamental
  domain `𝓕`, is the same as the `essSup` of `g`'s lift to the universal cover `G` with respect
  to `μ`."]
lemma essSup_comp_quotientGroup_mk [μ.IsMulRightInvariant] {g : G ⧸ Γ → ℝ≥0∞}
    (g_ae_measurable : AEMeasurable g μ_𝓕) : essSup g μ_𝓕 = essSup (fun (x : G) ↦ g x) μ

Proof state:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable g (map QuotientGroup.mk (μ.restrict 𝓕))
hπ : Measurable QuotientGroup.mk
γ : Gᵐᵒᵖ
hγ : γ ∈ Γ.op
x : G
⊢ (g ∘ QuotientGroup.mk) (⟨γ, hγ⟩ • x) = (g ∘ QuotientGroup.mk) x

Tactic:
dsimp

Result:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : MeasurableSpace G
inst✝⁶ : TopologicalSpace G
inst✝⁵ : IsTopologicalGroup G
inst✝⁴ : BorelSpace G
μ : Measure G
Γ : Subgroup G
𝓕 : Set G
h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ
inst✝³ : Countable ↥Γ
inst✝² : MeasurableSpace (G ⧸ Γ)
inst✝¹ : BorelSpace (G ⧸ Γ)
inst✝ : μ.IsMulRightInvariant
g : G ⧸ Γ → ℝ≥0∞
g_ae_measurable : AEMeasurable g (map QuotientGroup.mk (μ.restrict 𝓕))
hπ : Measurable QuotientGroup.mk
γ : Gᵐᵒᵖ
hγ : γ ∈ Γ.op
x : G
⊢ g ↑(x * MulOpposite.unop γ) = g ↑x
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem injective_iff_ker_eq_bot : Function.Injective f ↔ ker f = ⊥

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
⊢ Function.Injective ⇑f ↔ ker f = ⊥

Tactic:
rw [SetLike.ext'_iff, ker_eq, Set.ext_iff]

Result:
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
⊢ Function.Injective ⇑f ↔ ∀ (x : R), x ∈ ⇑f ⁻¹' {0} ↔ x ∈ ↑⊥

Proof state:
R : Type u
S : Type v
F : Type u_1
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
⊢ Function.Injective ⇑f ↔ ∀ (x : R), x ∈ ⇑f ⁻¹' {0} ↔ x ∈ ↑⊥

Tactic:
exact injective_iff_map_eq_zero' f

Result:
no goals
-- Mathlib/Algebra/Ring/Semiconj.lean
theorem neg_left (h : SemiconjBy a x y) : SemiconjBy (-a) x y

Proof state:
R : Type u
inst✝¹ : Mul R
inst✝ : HasDistribNeg R
a x y : R
h : SemiconjBy a x y
⊢ SemiconjBy (-a) x y

Tactic:
simp only [SemiconjBy, h.eq, neg_mul, mul_neg]

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem rel_of_liftRel {R : α → β → Prop} {ca cb} :
    LiftRel R ca cb → ∀ {a b}, a ∈ ca → b ∈ cb → R a b
  | ⟨l, _⟩, a, b, ma, mb => by
    let ⟨b', mb', ab'⟩ := l ma
    rw [mem_unique mb mb']; exact ab'

Proof state:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b
right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab' : R a b'
⊢ R a b

Tactic:
rw [mem_unique mb mb']

Result:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b
right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab' : R a b'
⊢ R a b'

Proof state:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b
right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab' : R a b'
⊢ R a b'

Tactic:
exact ab'

Result:
no goals

Proof state:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b
right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
⊢ R a b

Tactic:
let ⟨b', mb', ab'⟩ := l ma

Result:
α : Type u
β : Type v
R : α → β → Prop
ca : Computation α
cb : Computation β
l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b
right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b
a : α
b : β
ma : a ∈ ca
mb : b ∈ cb
b' : β
mb' : b' ∈ cb
ab' : R a b'
⊢ R a b
-- Mathlib/Algebra/Group/Basic.lean
theorem div_eq_div_mul_div (a b c : G) : a / b = c / b * (a / c)

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b c : G
⊢ a / b = c / b * (a / c)

Tactic:
simp [mul_left_comm c]

Result:
no goals
-- Mathlib/Data/List/Destutter.lean
theorem length_destutter_le_length_destutter_cons [IsEquiv α Rᶜ] :
    ∀ {l : List α}, (l.destutter R).length ≤ ((a :: l).destutter R).length
  | [] => by simp [destutter]
  | b :: l => le_length_destutter'_cons

Proof state:
α : Type u_1
R : α → α → Prop
inst✝¹ : DecidableRel R
a : α
inst✝ : IsEquiv α Rᶜ
⊢ (destutter R []).length ≤ (destutter R [a]).length

Tactic:
simp [destutter]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem List.Sorted.lt_ord_of_lt [LinearOrder α] [WellFoundedLT α] {l m : List α}
    {o : Ordinal} (hl : l.Sorted (· > ·)) (hm : m.Sorted (· > ·)) (hmltl : m < l)
    (hlt : ∀ i ∈ l, Ordinal.typein (α := α) (· < ·) i < o) :
      ∀ i ∈ m, Ordinal.typein (α := α) (· < ·) i < o

Proof state:
case cons.cons
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : Sorted (fun x1 x2 => x1 > x2) (a :: as)
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : Sorted (fun x1 x2 => x1 > x2) (b :: bs)
hmltl : Lex (fun x1 x2 => x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
⊢ i ≤ a

Tactic:
cases hi with
| head as => exact List.head_le_of_lt hmltl
| tail b hi => exact le_of_lt (lt_of_lt_of_le (List.rel_of_sorted_cons hm _ hi)
    (List.head_le_of_lt hmltl))

Result:
no goals