harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Divisors.lean
theorem dvd_of_mem_divisors {m : ℕ} (h : n ∈ divisors m) : n ∣ m

Proof state:
case zero
n : ℕ
h : n ∈ divisors 0
⊢ n ∣ 0

Tactic:
apply dvd_zero

Result:
no goals

Proof state:
n m : ℕ
h : n ∈ m.divisors
⊢ n ∣ m

Tactic:
cases m

Result:
case zero
n : ℕ
h : n ∈ divisors 0
⊢ n ∣ 0

case succ
n n✝ : ℕ
h : n ∈ (n✝ + 1).divisors
⊢ n ∣ n✝ + 1

Proof state:
case succ
n n✝ : ℕ
h : n ∈ (n✝ + 1).divisors
⊢ n ∣ n✝ + 1

Tactic:
simp [mem_divisors.1 h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem testBit_add_one (x i : Nat) : testBit x (i + 1) = testBit (x/2) i

Proof state:
x i : Nat
⊢ x.testBit (i + 1) = (x / 2).testBit i

Tactic:
unfold testBit

Result:
x i : Nat
⊢ (1 &&& x >>> (i + 1) != 0) = (1 &&& (x / 2) >>> i != 0)

Proof state:
x i : Nat
⊢ (1 &&& x >>> (i + 1) != 0) = (1 &&& (x / 2) >>> i != 0)

Tactic:
simp [shiftRight_succ_inside]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
lemma tendsto_measure_Icc_nhdsWithin_right (b : ℝ) :
    Tendsto (fun δ ↦ μ (Icc (b - δ) (b + δ))) (𝓝[≥] (0 : ℝ)) (𝓝 (μ {b}))

Proof state:
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b : ℝ
s : Set ℝ≥0∞
hs : s ∈ 𝓝 (μ {b})
⊢ μ (Icc (b - 0) (b + 0)) ∈ s

Tactic:
simpa using mem_of_mem_nhds hs

Result:
no goals

Proof state:
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ Tendsto (fun δ => μ (Icc (b - δ) (b + δ))) (𝓝[≥] 0) (𝓝 (μ {b}))

Tactic:
simp only [← nhdsWithin_right_sup_nhds_singleton, nhdsWithin_singleton, tendsto_sup,
  tendsto_measure_Icc_nhdsWithin_right' μ b, true_and, tendsto_pure_left]

Result:
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ ∀ s ∈ 𝓝 (μ {b}), μ (Icc (b - 0) (b + 0)) ∈ s

Proof state:
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b : ℝ
⊢ ∀ s ∈ 𝓝 (μ {b}), μ (Icc (b - 0) (b + 0)) ∈ s

Tactic:
intro s hs

Result:
μ : Measure ℝ
inst✝ : IsFiniteMeasureOnCompacts μ
b : ℝ
s : Set ℝ≥0∞
hs : s ∈ 𝓝 (μ {b})
⊢ μ (Icc (b - 0) (b + 0)) ∈ s
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Relabel.lean
theorem relabel_size_eq {entry : Entrypoint α} {r : α → β} :
    (entry.relabel r).aig.decls.size = entry.aig.decls.size

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
entry : Entrypoint α
r : α → β
⊢ (relabel r entry).aig.decls.size = entry.aig.decls.size

Tactic:
simp [relabel]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem algebraMap_apply_div :
    algebraMap (RatFunc F) F⸨X⸩ (algebraMap _ _ p / algebraMap _ _ q) =
      algebraMap F[X] F⸨X⸩ p / algebraMap _ _ q

Proof state:
F : Type u
inst✝ : Field F
p q : F[X]
⊢ (algebraMap (RatFunc F) F⸨X⸩) ((algebraMap F[X] (RatFunc F)) p / (algebraMap F[X] (RatFunc F)) q) =
    (algebraMap F[X] F⸨X⸩) p / (algebraMap F[X] F⸨X⸩) q

Tactic:
convert coe_div _ _ <;>
  rw [← mk_one, coe_def, coeAlgHom, mk_eq_div, liftAlgHom_apply_div, map_one, div_one,
    Algebra.ofId_apply]

Result:
no goals
-- Mathlib/Probability/Independence/Basic.lean
theorem iIndepSet.meas_biInter {f : ι → Set Ω} (h : iIndepSet f μ) (s : Finset ι) :
    μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)

Proof state:
Ω : Type u_1
ι : Type u_2
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : ι → Set Ω
h : iIndepSet f μ
s : Finset ι
⊢ μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)

Tactic:
simpa using Kernel.iIndepSet.meas_biInter h s

Result:
no goals
-- Mathlib/Algebra/QuadraticDiscriminant.lean
theorem discrim_lt_zero (ha : a ≠ 0) (h : ∀ x : K, 0 < a * (x * x) + b * x + c) :
    discrim a b c < 0

Proof state:
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
⊢ discrim a b c < 0

Tactic:
have : ∀ x : K, 0 ≤ a * (x * x) + b * x + c := fun x => le_of_lt (h x)

Result:
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
⊢ discrim a b c < 0

Proof state:
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this✝ : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
this : 0 < a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c
⊢ False

Tactic:
have : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0 := by
  rw [mul_assoc, quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))]

Result:
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this✝¹ : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
this✝ : 0 < a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c
this : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0
⊢ False

Proof state:
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this✝¹ : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
this✝ : 0 < a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c
this : a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0
⊢ False

Tactic:
linarith

Result:
no goals

Proof state:
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
⊢ False

Tactic:
have := h (-b / (2 * a))

Result:
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this✝ : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
this : 0 < a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c
⊢ False

Proof state:
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
⊢ discrim a b c < 0

Tactic:
refine lt_of_le_of_ne (discrim_le_zero this) fun h' ↦ ?_

Result:
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
⊢ False

Proof state:
K : Type u_1
inst✝ : LinearOrderedField K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this✝ : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
this : 0 < a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c
⊢ a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0

Tactic:
rw [mul_assoc, quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MutuallySingular.lean
@[simp]
lemma self_iff (μ : Measure α) : μ ⟂ₘ μ ↔ μ = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ ⟂ₘ μ ↔ μ = 0

Tactic:
refine ⟨?_, fun h ↦ by (rw [h]; exact zero_left)⟩

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ ⟂ₘ μ → μ = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : μ = 0
⊢ μ ⟂ₘ μ

Tactic:
rw [h]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : μ = 0
⊢ 0 ⟂ₘ 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : μ s = 0
hμs_compl : μ sᶜ = 0
this : μ univ = 0
⊢ μ = 0

Tactic:
rwa [measure_univ_eq_zero] at this

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : μ s = 0
hμs_compl : μ sᶜ = 0
⊢ μ = 0

Tactic:
suffices μ Set.univ = 0 by rwa [measure_univ_eq_zero] at this

Result:
case intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : μ s = 0
hμs_compl : μ sᶜ = 0
⊢ μ univ = 0

Proof state:
case intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : μ s = 0
hμs_compl : μ sᶜ = 0
⊢ μ univ = 0

Tactic:
rw [← Set.union_compl_self s, measure_union disjoint_compl_right hs.compl, hμs, hμs_compl,
  add_zero]

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ ⟂ₘ μ → μ = 0

Tactic:
rintro ⟨s, hs, hμs, hμs_compl⟩

Result:
case intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : μ s = 0
hμs_compl : μ sᶜ = 0
⊢ μ = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : μ = 0
⊢ 0 ⟂ₘ 0

Tactic:
exact zero_left

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : μ = 0
⊢ μ ⟂ₘ μ

Tactic:
(rw [h]; exact zero_left)

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma toMvPolynomial_mul (M : Matrix m n R) (N : Matrix n o R) (i : m) :
    (M * N).toMvPolynomial i = bind₁ N.toMvPolynomial (M.toMvPolynomial i)

Proof state:
m : Type u_1
n : Type u_2
o : Type u_3
R : Type u_4
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : CommSemiring R
M : Matrix m n R
N : Matrix n o R
i : m
⊢ (M * N).toMvPolynomial i = (bind₁ N.toMvPolynomial) (M.toMvPolynomial i)

Tactic:
simp only [toMvPolynomial, mul_apply, map_sum, Finset.sum_comm (γ := o), bind₁, aeval,
  AlgHom.coe_mk, coe_eval₂Hom, eval₂_monomial, algebraMap_apply, Algebra.id.map_eq_id,
  RingHom.id_apply, C_apply, pow_zero, Finsupp.prod_single_index, pow_one, Finset.mul_sum,
  monomial_mul, zero_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem sub_add_eq_max (a b : Nat) : a - b + b = max a b

Proof state:
a b : Nat
hl : a ≤ b
⊢ a - b + b = max a b

Tactic:
rw [Nat.max_eq_right hl, Nat.sub_eq_zero_iff_le.mpr hl, Nat.zero_add]

Result:
no goals

Proof state:
a b : Nat
⊢ a - b + b = max a b

Tactic:
match Nat.le_total a b with
| .inl hl => rw [Nat.max_eq_right hl, Nat.sub_eq_zero_iff_le.mpr hl, Nat.zero_add]
| .inr hr => rw [Nat.max_eq_left hr, Nat.sub_add_cancel hr]

Result:
no goals

Proof state:
a b : Nat
hr : b ≤ a
⊢ a - b + b = max a b

Tactic:
rw [Nat.max_eq_left hr, Nat.sub_add_cancel hr]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem pushoutIsoUnopPullback_inv_fst {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g]
    [HasPullback f.op g.op] :
    (pushoutIsoUnopPullback f g).inv.op ≫ pullback.fst f.op g.op = (pushout.inl f g).op

Proof state:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ ((pushoutIsoUnopPullback f g).inv.op ≫ pullback.fst f.op g.op).unop = (pushout.inl f g).op.unop

Tactic:
dsimp

Result:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ (pullback.fst f.op g.op).unop ≫ (pushoutIsoUnopPullback f g).inv = pushout.inl f g

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ (pushoutIsoUnopPullback f g).inv.op ≫ pullback.fst f.op g.op = (pushout.inl f g).op

Tactic:
apply Quiver.Hom.unop_inj

Result:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ ((pushoutIsoUnopPullback f g).inv.op ≫ pullback.fst f.op g.op).unop = (pushout.inl f g).op.unop

Proof state:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : X ⟶ Y
inst✝¹ : HasPushout f g
inst✝ : HasPullback f.op g.op
⊢ (pullback.fst f.op g.op).unop ≫ (pushoutIsoUnopPullback f g).inv = pushout.inl f g

Tactic:
rw [← pushoutIsoUnopPullback_inl_hom, Category.assoc, Iso.hom_inv_id, Category.comp_id]

Result:
no goals
-- Mathlib/Order/Bounds/Image.lean
theorem isLUB_pi {s : Set (∀ a, π a)} {f : ∀ a, π a} :
    IsLUB s f ↔ ∀ a, IsLUB (Function.eval a '' s) (f a)

Proof state:
case refine_1
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : IsLUB s f
a : α
b : π a
hb : b ∈ upperBounds (eval a '' s)
⊢ f a ≤ b

Tactic:
suffices h : Function.update f a b ∈ upperBounds s from Function.update_self a b f ▸ H.2 h a

Result:
case refine_1
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : IsLUB s f
a : α
b : π a
hb : b ∈ upperBounds (eval a '' s)
⊢ update f a b ∈ upperBounds s

Proof state:
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
⊢ IsLUB s f ↔ ∀ (a : α), IsLUB (eval a '' s) (f a)

Tactic:
refine
  ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => ?_⟩, fun H =>
    ⟨?_, ?_⟩⟩

Result:
case refine_1
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : IsLUB s f
a : α
b : π a
hb : b ∈ upperBounds (eval a '' s)
⊢ f a ≤ b

case refine_2
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ upperBounds s

case refine_3
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ lowerBounds (upperBounds s)

Proof state:
case refine_1
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : IsLUB s f
a : α
b : π a
hb : b ∈ upperBounds (eval a '' s)
⊢ update f a b ∈ upperBounds s

Tactic:
exact fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩

Result:
no goals

Proof state:
case refine_3
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ lowerBounds (upperBounds s)

Tactic:
exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg)

Result:
no goals

Proof state:
case refine_2
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ upperBounds s

Tactic:
exact fun g hg a => (H a).1 (mem_image_of_mem _ hg)

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem lift_comp : (f.lift hg).comp f.toMap = g

Proof state:
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x✝ : M
⊢ ((f.lift hg).comp f.toMap) x✝ = g x✝

Tactic:
exact f.lift_eq hg _

Result:
no goals

Proof state:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
⊢ (f.lift hg).comp f.toMap = g

Tactic:
ext

Result:
case h
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
x✝ : M
⊢ ((f.lift hg).comp f.toMap) x✝ = g x✝
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
protected lemma neg_comp {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (z₂ : Cochain G K n₂)
    (h : n₁ + n₂ = n₁₂) : (-z₁).comp z₂ h = -z₁.comp z₂ h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ p + n₁ + n₂ = q

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ (-z₁).comp z₂ h = -z₁.comp z₂ h

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ ((-z₁).comp z₂ h).v p q hpq = (-z₁.comp z₂ h).v p q hpq

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ ((-z₁).comp z₂ h).v p q hpq = (-z₁.comp z₂ h).v p q hpq

Tactic:
simp only [comp_v _ _ h p _ q rfl (by omega), neg_v, neg_comp]

Result:
no goals
-- Mathlib/Algebra/Order/Floor/Div.lean
@[simp] lemma ceilDiv_one [Nontrivial α] (b : β) : b ⌈/⌉ (1 : α) = b :=
  eq_of_forall_ge_iff <| fun c ↦ by simp [zero_lt_one' α]

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : OrderedSemiring α
inst✝³ : OrderedAddCommMonoid β
inst✝² : MulActionWithZero α β
inst✝¹ : CeilDiv α β
inst✝ : Nontrivial α
b c : β
⊢ b ⌈/⌉ 1 ≤ c ↔ b ≤ c

Tactic:
simp [zero_lt_one' α]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem data_drop (s : String) (n : Nat) : (s.drop n).1 = s.1.drop n

Proof state:
s : String
n : Nat
⊢ (s.drop n).data = List.drop n s.data

Tactic:
rw [drop_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/HashMap/Lemmas.lean
theorem getD_insertManyIfNewUnit_list
    {l : List α} {k : α} {fallback : Unit} :
    getD (insertManyIfNewUnit m l) k fallback = ()

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
m : HashMap α Unit
l : List α
k : α
fallback : Unit
⊢ (m.insertManyIfNewUnit l).getD k fallback = ()

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean
lemma rotate_distinguished_triangle (T : Triangle Cᵒᵖ) :
    T ∈ distinguishedTriangles C ↔ T.rotate ∈ distinguishedTriangles C

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles ↔
    (Opposite.unop ((triangleOpEquivalence C).inverse.obj T.rotate)).rotate ∈ Pretriangulated.distinguishedTriangles

Tactic:
exact distinguished_iff_of_iso (rotateTriangleOpEquivalenceInverseObjRotateUnopIso T).symm

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ T ∈ distinguishedTriangles C ↔ T.rotate ∈ distinguishedTriangles C

Tactic:
simp only [mem_distinguishedTriangles_iff, Pretriangulated.rotate_distinguished_triangle
  ((triangleOpEquivalence C).inverse.obj (T.rotate)).unop]

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles ↔
    (Opposite.unop ((triangleOpEquivalence C).inverse.obj T.rotate)).rotate ∈ Pretriangulated.distinguishedTriangles
-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem extend_mono' ⦃s₁ s₂ : Set α⦄ (h₁ : P s₁) (hs : s₁ ⊆ s₂) : extend m s₁ ≤ extend m s₂

Proof state:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s₁ s₂ : Set α
h₁ : P s₁
hs : s₁ ⊆ s₂
⊢ ∀ (i : P s₂), extend m s₁ ≤ m s₂ i

Tactic:
intro h₂

Result:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s₁ s₂ : Set α
h₁ : P s₁
hs : s₁ ⊆ s₂
h₂ : P s₂
⊢ extend m s₁ ≤ m s₂ h₂

Proof state:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s₁ s₂ : Set α
h₁ : P s₁
hs : s₁ ⊆ s₂
h₂ : P s₂
⊢ extend m s₁ ≤ m s₂ h₂

Tactic:
rw [extend_eq m h₁]

Result:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s₁ s₂ : Set α
h₁ : P s₁
hs : s₁ ⊆ s₂
h₂ : P s₂
⊢ m s₁ h₁ ≤ m s₂ h₂

Proof state:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s₁ s₂ : Set α
h₁ : P s₁
hs : s₁ ⊆ s₂
h₂ : P s₂
⊢ m s₁ h₁ ≤ m s₂ h₂

Tactic:
exact m_mono h₁ h₂ hs

Result:
no goals

Proof state:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s₁ s₂ : Set α
h₁ : P s₁
hs : s₁ ⊆ s₂
⊢ extend m s₁ ≤ extend m s₂

Tactic:
refine le_iInf ?_

Result:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂
s₁ s₂ : Set α
h₁ : P s₁
hs : s₁ ⊆ s₂
⊢ ∀ (i : P s₂), extend m s₁ ≤ m s₂ i
-- Mathlib/Data/List/Basic.lean
theorem Perm.disjoint_left {l₁ l₂ l : List α} (p : List.Perm l₁ l₂) :
    Disjoint l₁ l ↔ Disjoint l₂ l

Proof state:
α : Type u
l₁ l₂ l : List α
p : l₁ ~ l₂
⊢ l₁.Disjoint l ↔ l₂.Disjoint l

Tactic:
simp_rw [List.disjoint_left, p.mem_iff]

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem irrational_div_rat_iff : Irrational (x / q) ↔ q ≠ 0 ∧ Irrational x

Proof state:
q : ℚ
x : ℝ
⊢ Irrational (x / ↑q) ↔ q ≠ 0 ∧ Irrational x

Tactic:
rw [div_eq_mul_inv, ← cast_inv, irrational_mul_rat_iff, Ne, inv_eq_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem coordinate_eval_7 :
    (coordinate 7).eval
      (.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: t)) = a7

Proof state:
a0 a1 a2 a3 a4 a5 a6 a7 : Int
t : List Int
⊢ (coordinate 7).eval (Coeffs.ofList (a0 :: a1 :: a2 :: a3 :: a4 :: a5 :: a6 :: a7 :: t)) = a7

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem degree_compl [Fintype (Gᶜ.neighborSet v)] [Fintype V] :
    Gᶜ.degree v = Fintype.card V - 1 - G.degree v

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : Fintype ↑(Gᶜ.neighborSet v)
inst✝ : Fintype V
⊢ Gᶜ.degree v = Fintype.card V - 1 - G.degree v

Tactic:
rw [← card_neighborSet_union_compl_neighborSet G v, Set.toFinset_union]

Result:
V : Type u_1
G : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : Fintype ↑(Gᶜ.neighborSet v)
inst✝ : Fintype V
⊢ Gᶜ.degree v = #((G.neighborSet v).toFinset ∪ (Gᶜ.neighborSet v).toFinset) - G.degree v

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : Fintype ↑(Gᶜ.neighborSet v)
inst✝ : Fintype V
⊢ Gᶜ.degree v = #((G.neighborSet v).toFinset ∪ (Gᶜ.neighborSet v).toFinset) - G.degree v

Tactic:
simp [card_union_of_disjoint (Set.disjoint_toFinset.mpr (compl_neighborSet_disjoint G v))]

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : Fintype ↑(Gᶜ.neighborSet v)
inst✝ : Fintype V
⊢ Gᶜ.degree v = Fintype.card V - 1 - G.degree v

Tactic:
classical
  rw [← card_neighborSet_union_compl_neighborSet G v, Set.toFinset_union]
  simp [card_union_of_disjoint (Set.disjoint_toFinset.mpr (compl_neighborSet_disjoint G v))]

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourierCoeff_toLp (n : ℤ) :
    fourierCoeff (toLp (E := ℂ) 2 haarAddCircle ℂ f) n = fourierCoeff f n :=
  integral_congr_ae (Filter.EventuallyEq.mul (Filter.Eventually.of_forall (by tauto))
    (ContinuousMap.coeFn_toAEEqFun haarAddCircle f))

Proof state:
T : ℝ
hT : Fact (0 < T)
f : C(AddCircle T, ℂ)
n : ℤ
⊢ ∀ (x : AddCircle T), (fourier (-n)) x = (fourier (-n)) x

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivativeFinsupp_C (r : R) : derivativeFinsupp (C r : R[X]) = .single 0 (C r)

Proof state:
case h
R : Type u
inst✝ : Semiring R
r : R
i : ℕ
⊢ (derivativeFinsupp (C r)) i = (Finsupp.single 0 (C r)) i

Tactic:
match i with
| 0 => simp
| i + 1 => simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
r : R
i : ℕ
⊢ (derivativeFinsupp (C r)) 0 = (Finsupp.single 0 (C r)) 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
r : R
⊢ derivativeFinsupp (C r) = Finsupp.single 0 (C r)

Tactic:
ext i : 1

Result:
case h
R : Type u
inst✝ : Semiring R
r : R
i : ℕ
⊢ (derivativeFinsupp (C r)) i = (Finsupp.single 0 (C r)) i

Proof state:
R : Type u
inst✝ : Semiring R
r : R
i✝ i : ℕ
⊢ (derivativeFinsupp (C r)) (i + 1) = (Finsupp.single 0 (C r)) (i + 1)

Tactic:
simp

Result:
no goals