harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem support_smul [SMulZeroClass S R] (r : S) (p : R[X]) :
    support (r • p) ⊆ support p

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
p : R[X]
i : ℕ
hi : ¬r • p.coeff i = 0
⊢ ¬p.coeff i = 0

Tactic:
contrapose! hi

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
p : R[X]
i : ℕ
hi : p.coeff i = 0
⊢ r • p.coeff i = 0

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
p : R[X]
i : ℕ
hi : i ∈ (r • p).support
⊢ i ∈ p.support

Tactic:
simp? [mem_support_iff] at hi ⊢ says simp only [mem_support_iff, coeff_smul, ne_eq] at hi ⊢

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
p : R[X]
i : ℕ
hi : ¬r • p.coeff i = 0
⊢ ¬p.coeff i = 0

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
p : R[X]
⊢ (r • p).support ⊆ p.support

Tactic:
intro i hi

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
p : R[X]
i : ℕ
hi : i ∈ (r • p).support
⊢ i ∈ p.support

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
p : R[X]
i : ℕ
hi : p.coeff i = 0
⊢ r • p.coeff i = 0

Tactic:
simp [hi]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
p : R[X]
i : ℕ
hi : i ∈ (r • p).support
⊢ i ∈ p.support

Tactic:
simp only [mem_support_iff, coeff_smul, ne_eq] at hi ⊢

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : SMulZeroClass S R
r : S
p : R[X]
i : ℕ
hi : ¬r • p.coeff i = 0
⊢ ¬p.coeff i = 0
-- Mathlib/Computability/Encoding.lean
theorem decode_encodeNum : ∀ n, decodeNum (encodeNum n) = n

Proof state:
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else Num.pos n) =
    Num.pos n

Tactic:
exact if_neg (encodePosNum_nonempty n)

Result:
no goals

Proof state:
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else ↑n) =
    Num.pos n

Tactic:
rw [PosNum.cast_to_num]

Result:
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else Num.pos n) =
    Num.pos n

Proof state:
n : Num
⊢ decodeNum (encodeNum n) = n

Tactic:
obtain - | n := n <;> unfold encodeNum decodeNum

Result:
case zero

⊢ (if
        (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.zero

case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.pos n

Proof state:
⊢ ∀ (n : Num), decodeNum (encodeNum n) = n

Tactic:
intro n

Result:
n : Num
⊢ decodeNum (encodeNum n) = n

Proof state:
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.pos n

Tactic:
rw [decode_encodePosNum n]

Result:
case pos
n : PosNum
⊢ (if
        (match Num.pos n with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else ↑n) =
    Num.pos n

Proof state:
case zero

⊢ (if
        (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n) =
          [] then
      Num.zero
    else
      ↑(decodePosNum
          (match Num.zero with
          | Num.zero => []
          | Num.pos n => encodePosNum n))) =
    Num.zero

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.add_neg (a : BitVec w) : a + (~~~a + 1#w) = 0#w

Proof state:
w : Nat
a : BitVec w
⊢ a - a = 0#w

Tactic:
rw [BitVec.sub_self]

Result:
no goals

Proof state:
w : Nat
a : BitVec w
⊢ a + (~~~a + 1#w) = 0#w

Tactic:
rw [← BitVec.neg_eq_not_add]

Result:
w : Nat
a : BitVec w
⊢ a + -a = 0#w

Proof state:
w : Nat
a : BitVec w
⊢ a + -a = 0#w

Tactic:
rw [← BitVec.sub_toAdd]

Result:
w : Nat
a : BitVec w
⊢ a - a = 0#w
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.flatten {l₁ l₂ : List (List α)} (h : l₁ ~ l₂) : l₁.flatten ~ l₂.flatten

Proof state:
case nil
α : Type u_1
l₁ l₂ : List (List α)
⊢ [].flatten ~ [].flatten

Tactic:
rfl

Result:
no goals

Proof state:
case swap
α : Type u_1
l₁ l₂ : List (List α)
x✝ y✝ : List α
l✝ : List (List α)
⊢ (y✝ :: x✝ :: l✝).flatten ~ (x✝ :: y✝ :: l✝).flatten

Tactic:
simp only [flatten_cons, ← append_assoc, perm_append_right_iff]

Result:
case swap
α : Type u_1
l₁ l₂ : List (List α)
x✝ y✝ : List α
l✝ : List (List α)
⊢ y✝ ++ x✝ ~ x✝ ++ y✝

Proof state:
case cons
α : Type u_1
l₁ l₂ : List (List α)
x✝ : List α
l₁✝ l₂✝ : List (List α)
a✝ : l₁✝ ~ l₂✝
ih : l₁✝.flatten ~ l₂✝.flatten
⊢ (x✝ :: l₁✝).flatten ~ (x✝ :: l₂✝).flatten

Tactic:
simp only [flatten_cons, perm_append_left_iff, ih]

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : List (List α)
h : l₁ ~ l₂
⊢ l₁.flatten ~ l₂.flatten

Tactic:
induction h with
| nil => rfl
| cons _ _ ih => simp only [flatten_cons, perm_append_left_iff, ih]
| swap => simp only [flatten_cons, ← append_assoc, perm_append_right_iff]; exact perm_append_comm ..
| trans _ _ ih₁ ih₂ => exact trans ih₁ ih₂

Result:
no goals

Proof state:
case swap
α : Type u_1
l₁ l₂ : List (List α)
x✝ y✝ : List α
l✝ : List (List α)
⊢ y✝ ++ x✝ ~ x✝ ++ y✝

Tactic:
exact perm_append_comm ..

Result:
no goals

Proof state:
case trans
α : Type u_1
l₁ l₂ l₁✝ l₂✝ l₃✝ : List (List α)
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁ : l₁✝.flatten ~ l₂✝.flatten
ih₂ : l₂✝.flatten ~ l₃✝.flatten
⊢ l₁✝.flatten ~ l₃✝.flatten

Tactic:
exact trans ih₁ ih₂

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Basic.lean
lemma zpow_add_one₀ (ha : a ≠ 0) : ∀ n : ℤ, a ^ (n + 1) = a ^ n * a
  | (n : ℕ) => by simp only [← Int.ofNat_succ, zpow_natCast, pow_succ]
  | .negSucc 0 => by simp [ha]
  | .negSucc (n + 1) => by
    rw [Int.negSucc_eq, zpow_neg, Int.neg_add, Int.neg_add_cancel_right, zpow_neg, ← Int.ofNat_succ,
      zpow_natCast, zpow_natCast, pow_succ' _ (n + 1), mul_inv_rev, mul_assoc, inv_mul_cancel₀ ha,
      mul_one]

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
⊢ a ^ (Int.negSucc 0 + 1) = a ^ Int.negSucc 0 * a

Tactic:
simp [ha]

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (↑n + 1) = a ^ ↑n * a

Tactic:
simp only [← Int.ofNat_succ, zpow_natCast, pow_succ]

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a : G₀
ha : a ≠ 0
n : ℕ
⊢ a ^ (Int.negSucc (n + 1) + 1) = a ^ Int.negSucc (n + 1) * a

Tactic:
rw [Int.negSucc_eq, zpow_neg, Int.neg_add, Int.neg_add_cancel_right, zpow_neg, ← Int.ofNat_succ,
  zpow_natCast, zpow_natCast, pow_succ' _ (n + 1), mul_inv_rev, mul_assoc, inv_mul_cancel₀ ha,
  mul_one]

Result:
no goals
-- Mathlib/Data/List/Duplicate.lean
theorem Duplicate.mem (h : x ∈+ l) : x ∈ l

Proof state:
α : Type u_1
l : List α
x : α
h : x ∈+ l
⊢ x ∈ l

Tactic:
induction h with
| cons_mem => exact mem_cons_self _ _
| cons_duplicate _ hm => exact mem_cons_of_mem _ hm

Result:
no goals

Proof state:
case cons_mem
α : Type u_1
l : List α
x : α
l✝ : List α
a✝ : x ∈ l✝
⊢ x ∈ x :: l✝

Tactic:
exact mem_cons_self _ _

Result:
no goals

Proof state:
case cons_duplicate
α : Type u_1
l : List α
x y✝ : α
l✝ : List α
a✝ : x ∈+ l✝
hm : x ∈ l✝
⊢ x ∈ y✝ :: l✝

Tactic:
exact mem_cons_of_mem _ hm

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
lemma continuous_uncurry_of_multilinear (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F) :
    Continuous (fun (p : G × (Π i, E i)) ↦ f p.1 p.2)

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
F : Type u_4
inst✝¹¹ : NormedField 𝕜
inst✝¹⁰ : Finite ι
inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝⁷ : TopologicalSpace F
inst✝⁶ : AddCommGroup F
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : Module 𝕜 F
G : Type u_5
inst✝³ : AddCommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : Module 𝕜 G
inst✝ : ContinuousConstSMul 𝕜 F
f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
⊢ Continuous fun p => (f p.1) p.2

Tactic:
fun_prop

Result:
no goals
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
@[simp]
lemma support_bot : support (X := X) ⊥ = Set.univ

Proof state:
X : Scheme
⊢ ⊥.support = Set.univ

Tactic:
ext

Result:
case h
X : Scheme
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ⊥.support ↔ x✝ ∈ Set.univ

Proof state:
case h
X : Scheme
x✝ : ↑↑X.toPresheafedSpace
⊢ x✝ ∈ ⊥.support ↔ x✝ ∈ Set.univ

Tactic:
simp [support]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
theorem parallelepiped_basis_eq (b : Basis ι ℝ E) :
    parallelepiped b = {x | ∀ i, b.repr x i ∈ Set.Icc 0 1}

Proof state:
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
b : Basis ι ℝ E
⊢ parallelepiped ⇑b = {x | ∀ (i : ι), (b.repr x) i ∈ Icc 0 1}

Tactic:
classical
ext x
simp_rw [mem_parallelepiped_iff, mem_setOf_eq, b.ext_elem_iff, _root_.map_sum,
  _root_.map_smul, Finset.sum_apply', Basis.repr_self, Finsupp.smul_single, smul_eq_mul,
  mul_one, Finsupp.single_apply, Finset.sum_ite_eq', Finset.mem_univ, ite_true, mem_Icc,
  Pi.le_def, Pi.zero_apply, Pi.one_apply, ← forall_and]
aesop

Result:
no goals

Proof state:
case h
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
b : Basis ι ℝ E
x : E
⊢ (∃ t, ∀ (x_1 : ι), (0 ≤ t x_1 ∧ t x_1 ≤ 1) ∧ (b.repr x) x_1 = t x_1) ↔ ∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1

Tactic:
aesop

Result:
no goals

Proof state:
case h
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
b : Basis ι ℝ E
x : E
⊢ x ∈ parallelepiped ⇑b ↔ x ∈ {x | ∀ (i : ι), (b.repr x) i ∈ Icc 0 1}

Tactic:
simp_rw [mem_parallelepiped_iff, mem_setOf_eq, b.ext_elem_iff, _root_.map_sum,
  _root_.map_smul, Finset.sum_apply', Basis.repr_self, Finsupp.smul_single, smul_eq_mul,
  mul_one, Finsupp.single_apply, Finset.sum_ite_eq', Finset.mem_univ, ite_true, mem_Icc,
  Pi.le_def, Pi.zero_apply, Pi.one_apply, ← forall_and]

Result:
case h
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
b : Basis ι ℝ E
x : E
⊢ (∃ t, ∀ (x_1 : ι), (0 ≤ t x_1 ∧ t x_1 ≤ 1) ∧ (b.repr x) x_1 = t x_1) ↔ ∀ (i : ι), 0 ≤ (b.repr x) i ∧ (b.repr x) i ≤ 1

Proof state:
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
b : Basis ι ℝ E
⊢ parallelepiped ⇑b = {x | ∀ (i : ι), (b.repr x) i ∈ Icc 0 1}

Tactic:
ext x

Result:
case h
ι : Type u_1
E : Type u_3
inst✝² : Fintype ι
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
b : Basis ι ℝ E
x : E
⊢ x ∈ parallelepiped ⇑b ↔ x ∈ {x | ∀ (i : ι), (b.repr x) i ∈ Icc 0 1}
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.mem_prod_nhdsSet_of_forall {K : Set Y} {X} {l : Filter X} {s : Set (X × Y)}
    (hK : IsCompact K) (hs : ∀ y ∈ K, s ∈ l ×ˢ 𝓝 y) : s ∈ l ×ˢ 𝓝ˢ K :=
  (hK.prod_nhdsSet_eq_biSup l).symm ▸ by simpa using hs

Proof state:
Y : Type v
inst✝ : TopologicalSpace Y
K : Set Y
X : Type u_2
l : Filter X
s : Set (X × Y)
hK : IsCompact K
hs : ∀ y ∈ K, s ∈ l ×ˢ 𝓝 y
⊢ s ∈ ⨆ y ∈ K, l ×ˢ 𝓝 y

Tactic:
simpa using hs

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem haarMeasure_self {K₀ : PositiveCompacts G} : haarMeasure K₀ K₀ = 1

Proof state:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
⊢ (haarMeasure K₀) ↑K₀ = 1

Tactic:
haveI : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group

Result:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ (haarMeasure K₀) ↑K₀ = 1

Proof state:
case ht
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ (haarContent K₀).outerMeasure (closure ↑K₀) ≠ ⊤

Tactic:
exact (Content.outerMeasure_lt_top_of_isCompact _ K₀.isCompact.closure).ne

Result:
no goals

Proof state:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ ((haarContent K₀).measure ↑K₀)⁻¹ * (haarContent K₀).measure ↑K₀ = 1

Tactic:
rw [← K₀.isCompact.measure_closure,
  Content.measure_apply _ isClosed_closure.measurableSet, ENNReal.inv_mul_cancel]

Result:
case h0
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ (haarContent K₀).outerMeasure (closure ↑K₀) ≠ 0

case ht
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ (haarContent K₀).outerMeasure (closure ↑K₀) ≠ ⊤

Proof state:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ (haarMeasure K₀) ↑K₀ = 1

Tactic:
simp only [haarMeasure, coe_smul, Pi.smul_apply, smul_eq_mul]

Result:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ ((haarContent K₀).measure ↑K₀)⁻¹ * (haarContent K₀).measure ↑K₀ = 1

Proof state:
case h0
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
this : LocallyCompactSpace G
⊢ (haarContent K₀).outerMeasure (closure ↑K₀) ≠ 0

Tactic:
exact (haarContent_outerMeasure_closure_pos K₀).ne'

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
theorem limit_obj_ext {H : J ⥤ K ⥤ C} [HasLimitsOfShape J C] {k : K} {W : C}
    {f g : W ⟶ (limit H).obj k}
    (w : ∀ j, f ≫ (Limits.limit.π H j).app k = g ≫ (Limits.limit.π H j).app k) : f = g

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasLimitsOfShape J C
k : K
W : C
f g : W ⟶ (limit H).obj k
w : ∀ (j : J), f ≫ (limit.π H j).app k = g ≫ (limit.π H j).app k
⊢ f ≫ (limitObjIsoLimitCompEvaluation H k).hom = g ≫ (limitObjIsoLimitCompEvaluation H k).hom

Tactic:
ext j

Result:
case w
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasLimitsOfShape J C
k : K
W : C
f g : W ⟶ (limit H).obj k
w : ∀ (j : J), f ≫ (limit.π H j).app k = g ≫ (limit.π H j).app k
j : J
⊢ (f ≫ (limitObjIsoLimitCompEvaluation H k).hom) ≫ limit.π (H ⋙ (evaluation K C).obj k) j =
    (g ≫ (limitObjIsoLimitCompEvaluation H k).hom) ≫ limit.π (H ⋙ (evaluation K C).obj k) j

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasLimitsOfShape J C
k : K
W : C
f g : W ⟶ (limit H).obj k
w : ∀ (j : J), f ≫ (limit.π H j).app k = g ≫ (limit.π H j).app k
⊢ f = g

Tactic:
apply (cancel_mono (limitObjIsoLimitCompEvaluation H k).hom).1

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasLimitsOfShape J C
k : K
W : C
f g : W ⟶ (limit H).obj k
w : ∀ (j : J), f ≫ (limit.π H j).app k = g ≫ (limit.π H j).app k
⊢ f ≫ (limitObjIsoLimitCompEvaluation H k).hom = g ≫ (limitObjIsoLimitCompEvaluation H k).hom

Proof state:
case w
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
H : J ⥤ K ⥤ C
inst✝ : HasLimitsOfShape J C
k : K
W : C
f g : W ⟶ (limit H).obj k
w : ∀ (j : J), f ≫ (limit.π H j).app k = g ≫ (limit.π H j).app k
j : J
⊢ (f ≫ (limitObjIsoLimitCompEvaluation H k).hom) ≫ limit.π (H ⋙ (evaluation K C).obj k) j =
    (g ≫ (limitObjIsoLimitCompEvaluation H k).hom) ≫ limit.π (H ⋙ (evaluation K C).obj k) j

Tactic:
simpa using w j

Result:
no goals
-- Mathlib/Tactic/LinearCombination/Lemmas.lean
theorem lt_of_lt [OrderedCancelAddCommMonoid α] (p : (a:α) < b) (H : a' + b ≤ b' + a) :
    a' < b'

Proof state:
α : Type u_1
a a' b b' : α
inst✝ : OrderedCancelAddCommMonoid α
p : a < b
H : a' + b ≤ b' + a
⊢ b' + a < b' + b

Tactic:
apply add_lt_add_left p

Result:
no goals

Proof state:
α : Type u_1
a a' b b' : α
inst✝ : OrderedCancelAddCommMonoid α
p : a < b
H : a' + b ≤ b' + a
⊢ a' + b < b' + b

Tactic:
apply H.trans_lt

Result:
α : Type u_1
a a' b b' : α
inst✝ : OrderedCancelAddCommMonoid α
p : a < b
H : a' + b ≤ b' + a
⊢ b' + a < b' + b

Proof state:
α : Type u_1
a a' b b' : α
inst✝ : OrderedCancelAddCommMonoid α
p : a < b
H : a' + b ≤ b' + a
⊢ a' < b'

Tactic:
rw [← add_lt_add_iff_right b]

Result:
α : Type u_1
a a' b b' : α
inst✝ : OrderedCancelAddCommMonoid α
p : a < b
H : a' + b ≤ b' + a
⊢ a' + b < b' + b
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_erase [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    {a : α} (h : Raw.WFImp m.1) :
    Perm (toListModel (m.erase a).1.buckets) (eraseKey a (toListModel m.1.buckets))

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
⊢ toListModel (m.erase a).val.buckets ~ eraseKey a (toListModel m.val.buckets)

Tactic:
rw [erase_eq_eraseₘ]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
⊢ toListModel (m.eraseₘ a).val.buckets ~ eraseKey a (toListModel m.val.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
⊢ toListModel (m.eraseₘ a).val.buckets ~ eraseKey a (toListModel m.val.buckets)

Tactic:
exact toListModel_eraseₘ h

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eval_interpolate_at_node (hvs : Set.InjOn v s) (hi : i ∈ s) :
    eval (v i) (interpolate s v r) = r i

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ eval (v i) ((interpolate s v) r) = r i

Tactic:
rw [interpolate_apply, eval_finset_sum, ← add_sum_erase _ _ hi]

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ eval (v i) (C (r i) * Lagrange.basis s v i) + ∑ x ∈ s.erase i, eval (v i) (C (r x) * Lagrange.basis s v x) = r i

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ eval (v i) (C (r i) * Lagrange.basis s v i) + ∑ x ∈ s.erase i, eval (v i) (C (r x) * Lagrange.basis s v x) = r i

Tactic:
simp_rw [eval_mul, eval_C, eval_basis_self hvs hi, mul_one, add_right_eq_self]

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ∑ x ∈ s.erase i, r x * eval (v i) (Lagrange.basis s v x) = 0

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
⊢ ∑ x ∈ s.erase i, r x * eval (v i) (Lagrange.basis s v x) = 0

Tactic:
refine sum_eq_zero fun j H => ?_

Result:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ s.erase i
⊢ r j * eval (v i) (Lagrange.basis s v j) = 0

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
i : ι
v r : ι → F
hvs : Set.InjOn v ↑s
hi : i ∈ s
j : ι
H : j ∈ s.erase i
⊢ r j * eval (v i) (Lagrange.basis s v j) = 0

Tactic:
rw [eval_basis_of_ne (mem_erase.mp H).1 hi, mul_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
lemma isIso_cyclesMap'_of_isIso_of_mono (φ : S₁ ⟶ S₂) (h₂ : IsIso φ.τ₂) (h₃ : Mono φ.τ₃)
    (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData) :
    IsIso (cyclesMap' φ h₁ h₂)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₃ : Mono φ.τ₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ IsIso (cyclesMap' φ h₁ h₂)

Tactic:
refine ⟨h₁.liftK (h₂.i ≫ inv φ.τ₂) ?_, ?_, ?_⟩

Result:
case refine_1
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₃ : Mono φ.τ₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ (h₂.i ≫ inv φ.τ₂) ≫ S₁.g = 0

case refine_2
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₃ : Mono φ.τ₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ cyclesMap' φ h₁ h₂ ≫ h₁.liftK (h₂.i ≫ inv φ.τ₂) ?refine_1 = 𝟙 h₁.K

case refine_3
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₃ : Mono φ.τ₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ h₁.liftK (h₂.i ≫ inv φ.τ₂) ?refine_1 ≫ cyclesMap' φ h₁ h₂ = 𝟙 h₂.K

Proof state:
case refine_2
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₃ : Mono φ.τ₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ cyclesMap' φ h₁ h₂ ≫ h₁.liftK (h₂.i ≫ inv φ.τ₂) ⋯ = 𝟙 h₁.K

Tactic:
simp only [← cancel_mono h₁.i, assoc, h₁.liftK_i, cyclesMap'_i_assoc,
  IsIso.hom_inv_id, comp_id, id_comp]

Result:
no goals

Proof state:
case refine_3
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₃ : Mono φ.τ₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ h₁.liftK (h₂.i ≫ inv φ.τ₂) ⋯ ≫ cyclesMap' φ h₁ h₂ = 𝟙 h₂.K

Tactic:
simp only [← cancel_mono h₂.i, assoc, cyclesMap'_i, h₁.liftK_i_assoc,
  IsIso.inv_hom_id, comp_id, id_comp]

Result:
no goals

Proof state:
case refine_1
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₂✝ : IsIso φ.τ₂
h₃ : Mono φ.τ₃
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ (h₂.i ≫ inv φ.τ₂) ≫ S₁.g = 0

Tactic:
simp only [assoc, ← cancel_mono φ.τ₃, zero_comp, ← φ.comm₂₃, IsIso.inv_hom_id_assoc, h₂.wi]

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem Dep.of_isRestriction (hX : N.Dep X) (hNM : N ≤r M) : M.Dep X

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
X R : Set α
hR : R ⊆ M.E
hX : ¬M.Indep X ∧ X ⊆ R
⊢ M.Dep X

Tactic:
exact ⟨hX.1, hX.2.trans hR⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
X R : Set α
hR : R ⊆ M.E
hX : (M ↾ R).Dep X
⊢ M.Dep X

Tactic:
rw [restrict_dep_iff] at hX

Result:
case intro.intro
α : Type u_1
M : Matroid α
X R : Set α
hR : R ⊆ M.E
hX : ¬M.Indep X ∧ X ⊆ R
⊢ M.Dep X

Proof state:
α : Type u_1
M : Matroid α
X : Set α
N : Matroid α
hX : N.Dep X
hNM : N ≤r M
⊢ M.Dep X

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM

Result:
case intro.intro
α : Type u_1
M : Matroid α
X R : Set α
hR : R ⊆ M.E
hX : (M ↾ R).Dep X
⊢ M.Dep X
-- Mathlib/Order/WithBot.lean
theorem lt_coe_bot [OrderBot α] : x < (⊥ : α) ↔ x = ⊥

Proof state:
α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : OrderBot α
⊢ x < ↑⊥ ↔ x = ⊥

Tactic:
cases x <;> simp

Result:
no goals