harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finsupp/Basic.lean
theorem mapRange.equiv_trans (f : M ≃ N) (hf : f 0 = 0) (hf') (f₂ : N ≃ P) (hf₂ : f₂ 0 = 0) (hf₂') :
    (mapRange.equiv (f.trans f₂) (by rw [Equiv.trans_apply, hf, hf₂])
          (by rw [Equiv.symm_trans_apply, hf₂', hf']) :
        (α →₀ _) ≃ _) =
      (mapRange.equiv f hf hf').trans (mapRange.equiv f₂ hf₂ hf₂') :=
  Equiv.ext <| mapRange_comp f₂ hf₂ f hf ((congrArg f₂ hf).trans hf₂)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M ≃ N
hf : f 0 = 0
hf' : f.symm 0 = 0
f₂ : N ≃ P
hf₂ : f₂ 0 = 0
hf₂' : f₂.symm 0 = 0
⊢ (f.trans f₂) 0 = 0

Tactic:
rw [Equiv.trans_apply, hf, hf₂]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
M' : Type u_6
N : Type u_7
P : Type u_8
G : Type u_9
H : Type u_10
R : Type u_11
S : Type u_12
inst✝² : Zero M
inst✝¹ : Zero N
inst✝ : Zero P
f : M ≃ N
hf : f 0 = 0
hf' : f.symm 0 = 0
f₂ : N ≃ P
hf₂ : f₂ 0 = 0
hf₂' : f₂.symm 0 = 0
⊢ (f.trans f₂).symm 0 = 0

Tactic:
rw [Equiv.symm_trans_apply, hf₂', hf']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_replicate_of_neg (h : ¬ p a) : (replicate n a).filter p = []

Proof state:
α✝ : Type u_1
p : α✝ → Bool
n : Nat
a : α✝
h : ¬p a = true
⊢ filter p (replicate n a) = []

Tactic:
simp [filter_replicate, h]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem eq_empty_or_nonempty (u : ZFSet) : u = ∅ ∨ u.Nonempty

Proof state:
u : ZFSet.{u_1}
⊢ u = ∅ ∨ u.Nonempty

Tactic:
rw [eq_empty, ← not_exists]

Result:
u : ZFSet.{u_1}
⊢ (¬∃ x, x ∈ u) ∨ u.Nonempty

Proof state:
u : ZFSet.{u_1}
⊢ (¬∃ x, x ∈ u) ∨ u.Nonempty

Tactic:
apply em'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem forall_apply_eq_imp_iff {f : α → β} {p : β → Prop} :
    (∀ b a, f a = b → p b) ↔ ∀ a, p (f a)

Proof state:
α : Sort ?u.15865
β : Sort u_1
f : α → β
p : β → Prop
⊢ (∀ (b : β) (a : α), f a = b → p b) ↔ ∀ (a : α), p (f a)

Tactic:
simp [forall_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Basic.lean
@[reassoc (attr := simp)]
lemma _root_.CategoryTheory.Iso.inv_hom_id_triangle_hom₁ {A B : Triangle C} (e : A ≅ B) :
    e.inv.hom₁ ≫ e.hom.hom₁ = 𝟙 _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ e.inv.hom₁ ≫ e.hom.hom₁ = 𝟙 B.obj₁

Tactic:
rw [← comp_hom₁, e.inv_hom_id, id_hom₁]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_congr {a b : ℝ} (h : EqOn f g [[a, b]]) :
    ∫ x in a..b, f x ∂μ = ∫ x in a..b, g x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : ℝ → E
μ : Measure ℝ
a b : ℝ
h : EqOn f g [[a, b]]
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
rcases le_total a b with hab | hab <;>
  simpa [hab, integral_of_le, integral_of_ge] using
    setIntegral_congr_fun measurableSet_Ioc (h.mono Ioc_subset_Icc_self)

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem writtenInExtChartAt_chartAt {x : M} {y : E} (h : y ∈ (extChartAt I x).target) :
    writtenInExtChartAt I I x (chartAt H x) y = y

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
x : M
y : E
h : y ∈ (extChartAt I x).target
⊢ writtenInExtChartAt I I x (↑(chartAt H x)) y = y

Tactic:
simp_all only [mfld_simps]

Result:
no goals
-- Mathlib/Data/Finset/Insert.lean
theorem toList_cons {a : α} {s : Finset α} (h : a ∉ s) : (cons a s h).toList ~ a :: s.toList :=
  (List.perm_ext_iff_of_nodup (nodup_toList _) (by simp [h, nodup_toList s])).2 fun x => by
    simp only [List.mem_cons, Finset.mem_toList, Finset.mem_cons]

Proof state:
α : Type u_1
a : α
s : Finset α
h : a ∉ s
⊢ (a :: s.toList).Nodup

Tactic:
simp [h, nodup_toList s]

Result:
no goals

Proof state:
α : Type u_1
a : α
s : Finset α
h : a ∉ s
x : α
⊢ x ∈ (cons a s h).toList ↔ x ∈ a :: s.toList

Tactic:
simp only [List.mem_cons, Finset.mem_toList, Finset.mem_cons]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem inv_smul_integral_comp_sub_div (c d) :
    (c⁻¹ • ∫ x in a..b, f (d - x / c)) = ∫ x in d - b / c..d - a / c, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
⊢ c⁻¹ • ∫ (x : ℝ) in a..b, f (d - x / c) = ∫ (x : ℝ) in d - b / c..d - a / c, f x

Tactic:
by_cases hc : c = 0 <;> simp [hc, integral_comp_sub_div]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem smod_eq (x y : BitVec w) : x.smod y =
  match x.msb, y.msb with
  | false, false => x.umod y
  | false, true =>
    let u := x.umod (- y)
    (if u = 0#w then u else u + y)
  | true, false =>
    let u := umod (- x) y
    (if u = 0#w then u else y - u)
  | true, true => - ((- x).umod (- y))

Proof state:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
    | false, false => x.umod y
    | false, true =>
      let u := x.umod y.neg;
      if u = BitVec.zero w then u else u.add y
    | true, false =>
      let u := x.neg.umod y;
      if u = BitVec.zero w then u else y.sub u
    | true, true => (x.neg.umod y.neg).neg) =
    match x.msb, y.msb with
    | false, false => x.umod y
    | false, true =>
      let u := x.umod (-y);
      if u = 0#w then u else u + y
    | true, false =>
      let u := (-x).umod y;
      if u = 0#w then u else y - u
    | true, true => -(-x).umod (-y)

Tactic:
rcases x.msb <;> rcases y.msb <;> simp

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
⊢ x.smod y =
    match x.msb, y.msb with
    | false, false => x.umod y
    | false, true =>
      let u := x.umod (-y);
      if u = 0#w then u else u + y
    | true, false =>
      let u := (-x).umod y;
      if u = 0#w then u else y - u
    | true, true => -(-x).umod (-y)

Tactic:
rw [BitVec.smod]

Result:
w : Nat
x y : BitVec w
⊢ (match x.msb, y.msb with
    | false, false => x.umod y
    | false, true =>
      let u := x.umod y.neg;
      if u = BitVec.zero w then u else u.add y
    | true, false =>
      let u := x.neg.umod y;
      if u = BitVec.zero w then u else y.sub u
    | true, true => (x.neg.umod y.neg).neg) =
    match x.msb, y.msb with
    | false, false => x.umod y
    | false, true =>
      let u := x.umod (-y);
      if u = 0#w then u else u + y
    | true, false =>
      let u := (-x).umod y;
      if u = 0#w then u else y - u
    | true, true => -(-x).umod (-y)
-- Mathlib/Data/Holor.lean
theorem slice_eq (x : Holor α (d :: ds)) (y : Holor α (d :: ds)) (h : slice x = slice y) : x = y :=
  funext fun t : HolorIndex (d :: ds) =>
    holor_index_cons_decomp (fun t => x t = y t) t fun i is hiis =>
      have hiisdds : Forall₂ (· < ·) (i :: is) (d :: ds)

Proof state:
α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 => x1 < x2) (↑t) (d :: ds)

Tactic:
exact t.2

Result:
no goals

Proof state:
α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
hiisdds : Forall₂ (fun x1 x2 => x1 < x2) (i :: is) (d :: ds)
hid : i < d
hisds : Forall₂ (fun x1 x2 => x1 < x2) is ds
⊢ x.slice i hid ⟨is, hisds⟩ = y.slice i hid ⟨is, hisds⟩

Tactic:
rw [h]

Result:
no goals

Proof state:
α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 => x1 < x2) (i :: is) (d :: ds)

Tactic:
rw [← hiis]

Result:
α : Type
d : ℕ
ds : List ℕ
x y : Holor α (d :: ds)
h : x.slice = y.slice
t : HolorIndex (d :: ds)
i : ℕ
is : List ℕ
hiis : ↑t = i :: is
⊢ Forall₂ (fun x1 x2 => x1 < x2) (↑t) (d :: ds)
-- Mathlib/LinearAlgebra/Pi.lean
theorem lsum_single {ι R : Type*} [Fintype ι] [DecidableEq ι] [CommSemiring R] {M : ι → Type*}
    [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] :
    LinearMap.lsum R M R (LinearMap.single R M) = LinearMap.id :=
  LinearMap.ext fun x => by simp [Finset.univ_sum_single]

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁴ : Fintype ι
inst✝³ : DecidableEq ι
inst✝² : CommSemiring R
M : ι → Type u_3
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
x : (i : ι) → M i
⊢ ((lsum R M R) (single R M)) x = id x

Tactic:
simp [Finset.univ_sum_single]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem perm_append_comm : ∀ {l₁ l₂ : List α}, l₁ ++ l₂ ~ l₂ ++ l₁
  | [], _ => by simp
  | _ :: _, _ => (perm_append_comm.cons _).trans perm_middle.symm

Proof state:
α : Type u_1
x✝ : List α
⊢ [] ++ x✝ ~ x✝ ++ []

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem not_bddAbove_univ [NoMaxOrder α] : ¬BddAbove (univ : Set α)

Proof state:
α : Type u
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
⊢ ¬BddAbove univ

Tactic:
simp [BddAbove]

Result:
no goals
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem unifIntegrable_zero_meas [MeasurableSpace α] {p : ℝ≥0∞} {f : ι → α → β} :
    UnifIntegrable f p (0 : Measure α) :=
  fun ε _ => ⟨1, one_pos, fun i s _ _ => by simp⟩

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : NormedAddCommGroup β
inst✝ : MeasurableSpace α
p : ℝ≥0∞
f : ι → α → β
ε : ℝ
x✝² : 0 < ε
i : ι
s : Set α
x✝¹ : MeasurableSet s
x✝ : 0 s ≤ ENNReal.ofReal 1
⊢ eLpNorm (s.indicator (f i)) p 0 ≤ ENNReal.ofReal ε

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Comp.lean
theorem comp_apply' (η : Kernel β γ) (κ : Kernel α β) (a : α) {s : Set γ} (hs : MeasurableSet s) :
    (η ∘ₖ κ) a s = ∫⁻ b, η b s ∂κ a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
η : Kernel β γ
κ : Kernel α β
a : α
s : Set γ
hs : MeasurableSet s
⊢ ((η ∘ₖ κ) a) s = ∫⁻ (b : β), (η b) s ∂κ a

Tactic:
rw [comp_apply, Measure.bind_apply hs (Kernel.measurable _)]

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
lemma congr_postcomp {solution' : relations.Solution M} (h : solution = solution')
    (f : M →ₗ[A] N) : solution.postcomp f = solution'.postcomp f

Proof state:
A : Type u
inst✝⁴ : Ring A
relations : Relations A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
solution : relations.Solution M
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
solution' : relations.Solution M
h : solution = solution'
f : M →ₗ[A] N
⊢ solution.postcomp f = solution'.postcomp f

Tactic:
rw [h]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem transpose_nonsing_inv : A⁻¹ᵀ = Aᵀ⁻¹

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
⊢ A⁻¹ᵀ = Aᵀ⁻¹

Tactic:
rw [inv_def, inv_def, transpose_smul, det_transpose, adjugate_transpose]

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
@[simp] lemma mkRat_one (n : ℤ) : mkRat n 1 = n

Proof state:
n : ℤ
⊢ mkRat n 1 = ↑n

Tactic:
simp [mkRat_eq_divInt]

Result:
no goals
-- Mathlib/CategoryTheory/Category/Basic.lean
theorem cancel_epi_id (f : X ⟶ Y) [Epi f] {h : Y ⟶ Y} : f ≫ h = f ↔ h = 𝟙 Y

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : Y ⟶ Y
⊢ f ≫ h = f ↔ h = 𝟙 Y

Tactic:
convert cancel_epi f

Result:
case h.e'_1.h.e'_3.h
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : Y ⟶ Y
⊢ f = f ≫ 𝟙 Y

Proof state:
case h.e'_1.h.e'_3.h
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : Y ⟶ Y
⊢ f = f ≫ 𝟙 Y

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem isLimit_of_principal_add (ho₁ : 1 < o) (ho : Principal (· + ·) o) : o.IsLimit

Proof state:
o : Ordinal.{u}
ho₁ : 1 < o
ho : Principal (fun x1 x2 => x1 + x2) o
⊢ o.IsLimit

Tactic:
rw [isLimit_iff, isSuccPrelimit_iff_succ_lt]

Result:
o : Ordinal.{u}
ho₁ : 1 < o
ho : Principal (fun x1 x2 => x1 + x2) o
⊢ o ≠ 0 ∧ ∀ a < o, succ a < o

Proof state:
o : Ordinal.{u}
ho₁ : 1 < o
ho : Principal (fun x1 x2 => x1 + x2) o
⊢ o ≠ 0 ∧ ∀ a < o, succ a < o

Tactic:
exact ⟨ho₁.ne_bot, fun _ ha ↦ ho ha ho₁⟩

Result:
no goals
-- Mathlib/Analysis/Normed/Ring/SeminormFromBounded.lean
theorem seminormFromBounded_nonzero (f_ne_zero : f ≠ 0) (f_nonneg : 0 ≤ f)
    (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) :
    seminormFromBounded' f ≠ 0

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
⊢ seminormFromBounded' f ≠ 0

Tactic:
obtain ⟨x, hx⟩ := Function.ne_iff.mp f_ne_zero

Result:
case intro
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x ≠ 0 x
⊢ seminormFromBounded' f ≠ 0

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x ≠ 0 x
⊢ ¬f x = 0

Tactic:
exact hx

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x ≠ 0 x
⊢ seminormFromBounded' f x ≠ 0 x

Tactic:
rw [ne_eq, Pi.zero_apply, seminormFromBounded_eq_zero_iff f_nonneg f_mul x]

Result:
case h
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x ≠ 0 x
⊢ ¬f x = 0

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x ≠ 0 x
⊢ ∃ a, seminormFromBounded' f a ≠ 0 a

Tactic:
use x

Result:
case h
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x ≠ 0 x
⊢ seminormFromBounded' f x ≠ 0 x

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x ≠ 0 x
⊢ seminormFromBounded' f ≠ 0

Tactic:
rw [Function.ne_iff]

Result:
case intro
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x ≠ 0 x
⊢ ∃ a, seminormFromBounded' f a ≠ 0 a
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem Directed.disjoint_iSup_left (h : Directed (· ≤ ·) f) :
    Disjoint (⨆ i, f i) a ↔ ∀ i, Disjoint (f i) a

Proof state:
ι : Sort u_1
α : Type u_2
inst✝¹ : CompleteLattice α
f : ι → α
inst✝ : IsCompactlyGenerated α
a : α
h : Directed (fun x1 x2 => x1 ≤ x2) f
⊢ Disjoint (⨆ i, f i) a ↔ ∀ (i : ι), Disjoint (f i) a

Tactic:
simp_rw [disjoint_iff, h.iSup_inf_eq, iSup_eq_bot]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Vector/Lemmas.lean
theorem uget_mk (a : Array α) (h : a.size = n) (i) (hi : i.toNat < n) :
    (Vector.mk a h).uget i hi = a.uget i (by simp [h, hi]) := rfl

Proof state:
α : Type ?u.1334
n : Nat
a : Array α
h : a.size = n
i : USize
hi : i.toNat < n
⊢ i.toNat < a.size

Tactic:
simp [h, hi]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
theorem map_whiskerLeft (X : C) {Y Z : C} (f : Y ⟶ Z) :
    F.map (X ◁ f) = δ F X Y ≫ F.obj X ◁ F.map f ≫ μ F X Z

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
F : C ⥤ D
inst✝ : F.Monoidal
X Y Z : C
f : Y ⟶ Z
⊢ F.map (X ◁ f) = δ F X Y ≫ F.obj X ◁ F.map f ≫ μ F X Z

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem ground_eq_empty_iff : (M.E = ∅) ↔ M = emptyOn α

Proof state:
α : Type u_1
M : Matroid α
h : M.E = ∅
⊢ ∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)

Tactic:
simp [h, subset_empty_iff]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
⊢ M.E = ∅ ↔ M = emptyOn α

Tactic:
simp only [emptyOn, ext_iff_indep, iff_self_and]

Result:
α : Type u_1
M : Matroid α
⊢ M.E = ∅ → ∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)

Proof state:
α : Type u_1
M : Matroid α
⊢ M.E = ∅ → ∀ ⦃I : Set α⦄, I ⊆ M.E → (M.Indep I ↔ I = ∅)

Tactic:
exact fun h ↦ by simp [h, subset_empty_iff]

Result:
no goals
-- Mathlib/Order/Category/Preord.lean
lemma hom_inv_apply {X Y : Preord} (e : X ≅ Y) (s : Y) : e.hom (e.inv s) = s

Proof state:
X Y : Preord
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toReal_add_le : (a + b).toReal ≤ a.toReal + b.toReal :=
  if ha : a = ∞ then by simp only [ha, top_add, top_toReal, zero_add, toReal_nonneg]
  else
    if hb : b = ∞ then by simp only [hb, add_top, top_toReal, add_zero, toReal_nonneg]
    else le_of_eq (toReal_add ha hb)

Proof state:
a b : ℝ≥0∞
ha : a = ⊤
⊢ (a + b).toReal ≤ a.toReal + b.toReal

Tactic:
simp only [ha, top_add, top_toReal, zero_add, toReal_nonneg]

Result:
no goals

Proof state:
a b : ℝ≥0∞
ha : ¬a = ⊤
hb : b = ⊤
⊢ (a + b).toReal ≤ a.toReal + b.toReal

Tactic:
simp only [hb, add_top, top_toReal, add_zero, toReal_nonneg]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem coe_eq_empty : (s : Set α) = ∅ ↔ s = ⊥

Proof state:
α : Type u_1
inst✝ : LE α
s : LowerSet α
⊢ ↑s = ∅ ↔ s = ⊥

Tactic:
simp [SetLike.ext'_iff]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_union_of_disjoint {α : Type u} {S T : Set α} (H : Disjoint S T) :
    #(S ∪ T : Set α) = #S + #T

Proof state:
α : Type u
S T : Set α
H : Disjoint S T
⊢ #↑(S ∪ T) = #↑S + #↑T

Tactic:
exact Quot.sound ⟨Equiv.Set.union H⟩

Result:
no goals

Proof state:
α : Type u
S T : Set α
H : Disjoint S T
⊢ #↑(S ∪ T) = #↑S + #↑T

Tactic:
classical
exact Quot.sound ⟨Equiv.Set.union H⟩

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem mem_lists_iff_coe_eq {s : Cycle α} {l : List α} : l ∈ s.lists ↔ (l : Cycle α) = s :=
  Quotient.inductionOn' s fun l => by
    rw [lists, Quotient.liftOn'_mk'']
    simp

Proof state:
α : Type u_1
s : Cycle α
l✝ l : List α
⊢ l✝ ∈ ↑l.cyclicPermutations ↔ ↑l✝ = Quotient.mk'' l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s : Cycle α
l✝ l : List α
⊢ l✝ ∈ lists (Quotient.mk'' l) ↔ ↑l✝ = Quotient.mk'' l

Tactic:
rw [lists, Quotient.liftOn'_mk'']

Result:
α : Type u_1
s : Cycle α
l✝ l : List α
⊢ l✝ ∈ ↑l.cyclicPermutations ↔ ↑l✝ = Quotient.mk'' l
-- Mathlib/RingTheory/Generators.lean
lemma Hom.toAlgHom_monomial (f : Generators.Hom P P') (v r) :
    f.toAlgHom (monomial v r) = r • v.prod (f.val · ^ ·)

Proof state:
R : Type u
S : Type v
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
P : Generators R S
R' : Type u_1
S' : Type u_2
inst✝⁴ : CommRing R'
inst✝³ : CommRing S'
inst✝² : Algebra R' S'
P' : Generators R' S'
inst✝¹ : Algebra R R'
inst✝ : Algebra S S'
f : P.Hom P'
v : P.vars →₀ ℕ
r : R
⊢ f.toAlgHom ((monomial v) r) = r • v.prod fun x1 x2 => f.val x1 ^ x2

Tactic:
rw [toAlgHom, aeval_monomial, Algebra.smul_def]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem expand_eq_sum {f : R[X]} : expand R p f = f.sum fun e a => C a * (X ^ p) ^ e

Proof state:
R : Type u
inst✝ : CommSemiring R
p : ℕ
f : R[X]
⊢ (expand R p) f = f.sum fun e a => C a * (X ^ p) ^ e

Tactic:
simp [expand, eval₂]

Result:
no goals
-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
@[simp]
lemma basisDeriv_apply (i j : P.rels) :
    P.basisDeriv i j = (aeval P.val) (pderiv (P.map j) (P.relation i))

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
i j : P.rels
⊢ P.basisDeriv i j = (aeval P.val) ((pderiv (P.map j)) (P.relation i))

Tactic:
classical
simp [basisDeriv]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : SubmersivePresentation R S
i j : P.rels
⊢ P.basisDeriv i j = (aeval P.val) ((pderiv (P.map j)) (P.relation i))

Tactic:
simp [basisDeriv]

Result:
no goals
-- Mathlib/Order/InitialSeg.lean
theorem eq [IsWellOrder β s] (f g : r ≼i s) (a) : f a = g a

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f g : r ≼i s
a : α
⊢ f a = g a

Tactic:
rw [Subsingleton.elim f g]

Result:
no goals
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma empty_nmem_disjointOfDiffUnion (hC : IsSetSemiring C) (hs : s ∈ C)
    (hI : ↑I ⊆ C) :
    ∅ ∉ hC.disjointOfDiffUnion hs hI

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ∅ ∉ hC.disjointOfDiffUnion hs hI

Tactic:
simp only [disjointOfDiffUnion, mem_sdiff, Finset.mem_singleton, eq_self_iff_true,
  not_true, and_false, not_false_iff]

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ∅ ∉ hC.disjointOfDiffUnion hs hI

Tactic:
classical
simp only [disjointOfDiffUnion, mem_sdiff, Finset.mem_singleton, eq_self_iff_true,
  not_true, and_false, not_false_iff]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem mem_sSup_iff : a ∈ sSup S ↔ ∃ s ∈ S, a ∈ s :=
  mem_iUnion₂.trans <| by simp only [exists_prop, SetLike.mem_coe]

Proof state:
α : Type u_1
inst✝ : LE α
S : Set (LowerSet α)
a : α
⊢ (∃ i, ∃ (_ : i ∈ S), a ∈ ↑i) ↔ ∃ s ∈ S, a ∈ s

Tactic:
simp only [exists_prop, SetLike.mem_coe]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem leadingCoeff_mul_monic {p q : R[X]} (hq : Monic q) :
    leadingCoeff (p * q) = leadingCoeff p :=
  letI := Classical.decEq R
  Decidable.byCases
    (fun H : leadingCoeff p = 0 => by
      rw [H, leadingCoeff_eq_zero.1 H, zero_mul, leadingCoeff_zero])
    fun H : leadingCoeff p ≠ 0 => by
      rw [leadingCoeff_mul', hq.leadingCoeff, mul_one]
      rwa [hq.leadingCoeff, mul_one]

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Tactic:
rwa [hq.leadingCoeff, mul_one]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff ≠ 0
⊢ (p * q).leadingCoeff = p.leadingCoeff

Tactic:
rw [leadingCoeff_mul', hq.leadingCoeff, mul_one]

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
H : p.leadingCoeff = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff

Tactic:
rw [H, leadingCoeff_eq_zero.1 H, zero_mul, leadingCoeff_zero]

Result:
no goals
-- Mathlib/RingTheory/Trace/Basic.lean
theorem trace_eq_finrank_mul_minpoly_nextCoeff [FiniteDimensional K L] (x : L) :
    trace K L x = finrank K⟮x⟯ L * -(minpoly K x).nextCoeff

Proof state:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
⊢ (algebraMap ℕ K) (finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff = ↑(finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff

Tactic:
rfl

Result:
no goals

Proof state:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
⊢ (Algebra.trace K L) x = ↑(finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff

Tactic:
rw [trace_eq_trace_adjoin, trace_adjoinSimpleGen (.of_finite K x), Algebra.smul_def]

Result:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
x : L
⊢ (algebraMap ℕ K) (finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff = ↑(finrank (↥K⟮x⟯) L) * -(minpoly K x).nextCoeff