harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem of_diff_eq_zero_of_symmDiff_eq_zero_negative (hu : MeasurableSet u) (hv : MeasurableSet v)
    (hsu : s ≤[u] 0) (hsv : s ≤[v] 0) (hs : s (u ∆ v) = 0) : s (u \ v) = 0 ∧ s (v \ u) = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : ↑s (u ∆ v) = 0
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

Tactic:
have := of_diff_eq_zero_of_symmDiff_eq_zero_positive hu hv hsu hsv

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : ↑s (u ∆ v) = 0
this : ↑(-s) (u ∆ v) = 0 → ↑(-s) (u \ v) = 0 ∧ ↑(-s) (v \ u) = 0
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : ↑s (u ∆ v) = 0
this : ↑(-s) (u ∆ v) = 0 → ↑(-s) (u \ v) = 0 ∧ ↑(-s) (v \ u) = 0
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

Tactic:
simp only [Pi.neg_apply, neg_eq_zero, coe_neg] at this

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : ↑s (u ∆ v) = 0
this : ↑s (u ∆ v) = 0 → ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : s ≤[u] 0
hsv : s ≤[v] 0
hs : ↑s (u ∆ v) = 0
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

Tactic:
rw [← s.neg_le_neg_iff _ hu, neg_zero] at hsu

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] -s
hsv : s ≤[v] 0
hs : ↑s (u ∆ v) = 0
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : ↑s (u ∆ v) = 0
this : ↑s (u ∆ v) = 0 → ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

Tactic:
exact this hs

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] -s
hsv : s ≤[v] 0
hs : ↑s (u ∆ v) = 0
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0

Tactic:
rw [← s.neg_le_neg_iff _ hv, neg_zero] at hsv

Result:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
u v : Set α
hu : MeasurableSet u
hv : MeasurableSet v
hsu : 0 ≤[u] -s
hsv : 0 ≤[v] -s
hs : ↑s (u ∆ v) = 0
⊢ ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem mul_nonneg {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b

Proof state:
a b : Int
ha : 0 ≤ a
hb : 0 ≤ b
n : Nat
hn : a = ↑n
⊢ 0 ≤ a * b

Tactic:
let ⟨m, hm⟩ := eq_ofNat_of_zero_le hb

Result:
a b : Int
ha : 0 ≤ a
hb : 0 ≤ b
n : Nat
hn : a = ↑n
m : Nat
hm : b = ↑m
⊢ 0 ≤ a * b

Proof state:
a b : Int
ha : 0 ≤ a
hb : 0 ≤ b
n : Nat
hn : a = ↑n
m : Nat
hm : b = ↑m
⊢ 0 ≤ ↑(n * m)

Tactic:
apply ofNat_nonneg

Result:
no goals

Proof state:
a b : Int
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b

Tactic:
let ⟨n, hn⟩ := eq_ofNat_of_zero_le ha

Result:
a b : Int
ha : 0 ≤ a
hb : 0 ≤ b
n : Nat
hn : a = ↑n
⊢ 0 ≤ a * b

Proof state:
a b : Int
ha : 0 ≤ a
hb : 0 ≤ b
n : Nat
hn : a = ↑n
m : Nat
hm : b = ↑m
⊢ 0 ≤ a * b

Tactic:
rw [hn, hm, ← ofNat_mul]

Result:
a b : Int
ha : 0 ≤ a
hb : 0 ≤ b
n : Nat
hn : a = ↑n
m : Nat
hm : b = ↑m
⊢ 0 ≤ ↑(n * m)
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem row_eq_prod {μ : YoungDiagram} {i : ℕ} : μ.row i = {i} ×ˢ Finset.range (μ.rowLen i)

Proof state:
case h.mk
μ : YoungDiagram
a b : ℕ
⊢ b < μ.rowLen a ↔ b < μ.rowLen a

Tactic:
rfl

Result:
no goals

Proof state:
case h.mk
μ : YoungDiagram
i a b : ℕ
⊢ (a, b) ∈ μ.row i ↔ (a, b) ∈ {i} ×ˢ Finset.range (μ.rowLen i)

Tactic:
simp only [Finset.mem_product, Finset.mem_singleton, Finset.mem_range, mem_row_iff,
  mem_iff_lt_rowLen, and_comm, and_congr_right_iff]

Result:
case h.mk
μ : YoungDiagram
i a b : ℕ
⊢ a = i → (b < μ.rowLen a ↔ b < μ.rowLen i)

Proof state:
μ : YoungDiagram
i : ℕ
⊢ μ.row i = {i} ×ˢ Finset.range (μ.rowLen i)

Tactic:
ext ⟨a, b⟩

Result:
case h.mk
μ : YoungDiagram
i a b : ℕ
⊢ (a, b) ∈ μ.row i ↔ (a, b) ∈ {i} ×ˢ Finset.range (μ.rowLen i)

Proof state:
case h.mk
μ : YoungDiagram
i a b : ℕ
⊢ a = i → (b < μ.rowLen a ↔ b < μ.rowLen i)

Tactic:
rintro rfl

Result:
case h.mk
μ : YoungDiagram
a b : ℕ
⊢ b < μ.rowLen a ↔ b < μ.rowLen a
-- Mathlib/Data/Finsupp/MonomialOrder.lean
theorem MonomialOrder.lex_le_iff_of_unique [Unique σ] {c d : σ →₀ ℕ} :
    c ≼[lex] d ↔ c default ≤ d default

Proof state:
σ : Type u_1
inst✝¹ : LinearOrder σ
inst✝ : Unique σ
c d : σ →₀ ℕ
⊢ lex.toSyn c ≤ lex.toSyn d ↔ c default ≤ d default

Tactic:
simp only [MonomialOrder.lex_le_iff, Finsupp.lex_le_iff_of_unique, ofLex_toLex]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
@[simp] -- not as useful as a simp lemma as it looks, due to the coe on the left
lemma coheight_bot_eq_krullDim [OrderBot α] : coheight (⊥ : α) = krullDim α

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderBot α
⊢ ↑(coheight ⊥) = krullDim α

Tactic:
rw [← krullDim_orderDual]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderBot α
⊢ ↑(coheight ⊥) = krullDim αᵒᵈ

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : OrderBot α
⊢ ↑(coheight ⊥) = krullDim αᵒᵈ

Tactic:
exact height_top_eq_krullDim (α := αᵒᵈ)

Result:
no goals
-- Mathlib/AlgebraicTopology/MooreComplex.lean
theorem d_squared (n : ℕ) : objD X (n + 1) ≫ objD X n = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ 0 ∈ Finset.univ

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ objD X (n + 1) ≫ objD X n = 0

Tactic:
rcases n with _ | n <;> dsimp [objD]

Result:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ (Finset.univ.inf fun k => kernelSubobject (X.δ k.succ)).factorThru
        ((Finset.univ.inf fun k => kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ ≫
      (Finset.univ.inf fun k => kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ inv ⊤.arrow =
    0

case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ (Finset.univ.inf fun k => kernelSubobject (X.δ k.succ)).factorThru
        ((Finset.univ.inf fun k => kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ ≫
      (Finset.univ.inf fun k => kernelSubobject (X.δ k.succ)).factorThru
        ((Finset.univ.inf fun k => kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ =
    0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ 0 ∈ Finset.univ

Tactic:
simp

Result:
no goals

Proof state:
case succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
n : ℕ
⊢ (Finset.univ.inf fun k => kernelSubobject (X.δ k.succ)).factorThru
        ((Finset.univ.inf fun k => kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ ≫
      (Finset.univ.inf fun k => kernelSubobject (X.δ k.succ)).factorThru
        ((Finset.univ.inf fun k => kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ =
    0

Tactic:
rw [factorThru_right, factorThru_eq_zero, factorThru_arrow_assoc, Category.assoc,
  ← Fin.castSucc_zero,
  ← X.δ_comp_δ (Fin.zero_le (0 : Fin (n + 3))),
  ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin (n + 3)) (by simp)),
  Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]

Result:
no goals

Proof state:
case zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : SimplicialObject C
⊢ (Finset.univ.inf fun k => kernelSubobject (X.δ k.succ)).factorThru
        ((Finset.univ.inf fun k => kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0) ⋯ ≫
      (Finset.univ.inf fun k => kernelSubobject (X.δ k.succ)).arrow ≫ X.δ 0 ≫ inv ⊤.arrow =
    0

Tactic:
rw [Subobject.factorThru_arrow_assoc, Category.assoc, ← Fin.castSucc_zero,
  ← X.δ_comp_δ_assoc (Fin.zero_le (0 : Fin 2)),
  ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ (0 : Fin 2) (by simp)),
  Category.assoc, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]

Result:
no goals
-- Mathlib/NumberTheory/SiegelsLemma.lean
private lemma N_le_P_add_one (i : α) : N i ≤ P i + 1

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
⊢ ∀ i_1 ∈ univ, 0 ≤ ↑B * (A i i_1)⁺

Tactic:
intro j _

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
j : β
a✝ : j ∈ univ
⊢ 0 ≤ ↑B * (A i j)⁺

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
j : β
a✝ : j ∈ univ
⊢ 0 ≤ ↑B * (A i j)⁺

Tactic:
exact mul_nonneg (Nat.cast_nonneg B) (posPart_nonneg (A i j))

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
⊢ 0 ≤ P i + 1

Tactic:
apply le_trans (Finset.sum_nonneg _) (Int.le_add_one (le_refl P i))

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
⊢ ∀ i_1 ∈ univ, 0 ≤ ↑B * (A i i_1)⁺

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
⊢ ∀ i_1 ∈ univ, ↑B * -(A i i_1)⁻ ≤ 0

Tactic:
intro j _

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
j : β
a✝ : j ∈ univ
⊢ ↑B * -(A i j)⁻ ≤ 0

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
j : β
a✝ : j ∈ univ
⊢ ↑B * -(A i j)⁻ ≤ 0

Tactic:
simp only [mul_neg, Left.neg_nonpos_iff]

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
j : β
a✝ : j ∈ univ
⊢ 0 ≤ ↑B * (A i j)⁻

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
⊢ N i ≤ P i + 1

Tactic:
calc N i
_ ≤ 0 := by
  apply Finset.sum_nonpos
  intro j _
  simp only [mul_neg, Left.neg_nonpos_iff]
  exact mul_nonneg (Nat.cast_nonneg B) (negPart_nonneg (A i j))
_ ≤ P i + 1 := by
  apply le_trans (Finset.sum_nonneg _) (Int.le_add_one (le_refl P i))
  intro j _
  exact mul_nonneg (Nat.cast_nonneg B) (posPart_nonneg (A i j))

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
j : β
a✝ : j ∈ univ
⊢ 0 ≤ ↑B * (A i j)⁻

Tactic:
exact mul_nonneg (Nat.cast_nonneg B) (negPart_nonneg (A i j))

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
⊢ N i ≤ 0

Tactic:
apply Finset.sum_nonpos

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
⊢ ∀ i_1 ∈ univ, ↑B * -(A i i_1)⁻ ≤ 0
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addXYZ_neg {P : Fin 3 → R} (hP : W'.Equation P) :
    W'.addXYZ P (W'.neg P) = -W'.dblZ P • ![1, 1, 0]

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addXYZ P (W'.neg P) = -W'.dblZ P • ![1, 1, 0]

Tactic:
erw [addXYZ, addX_neg hP, addY_neg hP, addZ_neg, smul_fin3, neg_sq, mul_one,
  Odd.neg_pow <| by decide, mul_one, mul_zero]

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ Odd 3

Tactic:
decide

Result:
no goals
-- Mathlib/RingTheory/Ideal/Over.lean
theorem LiesOver.tower_bot [hp : 𝔓.LiesOver p] [hP : 𝔓.LiesOver P] : P.LiesOver p where
  over

Proof state:
A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : CommSemiring B
C : Type u_4
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
𝔓 : Ideal C
P : Ideal B
p : Ideal A
hp : 𝔓.LiesOver p
hP : 𝔓.LiesOver P
⊢ p = under A P

Tactic:
rw [𝔓.over_def p, 𝔓.over_def P, under_under]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Divisibility.lean
theorem isRelPrime_of_no_nonunits_factors [MonoidWithZero α] {x y : α} (nonzero : ¬(x = 0 ∧ y = 0))
    (H : ∀ z, ¬ IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y) : IsRelPrime x y

Proof state:
α : Type u_1
inst✝ : MonoidWithZero α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y
hx : 0 ∣ x
hy : 0 ∣ y
h : ¬IsUnit 0
⊢ False

Tactic:
exact nonzero ⟨zero_dvd_iff.1 hx, zero_dvd_iff.1 hy⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MonoidWithZero α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y
z : α
hx : z ∣ x
hy : z ∣ y
h : ¬IsUnit z
⊢ z ≠ 0

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝ : MonoidWithZero α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y
hx : 0 ∣ x
hy : 0 ∣ y
h : ¬IsUnit 0
⊢ False

Proof state:
α : Type u_1
inst✝ : MonoidWithZero α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y
⊢ IsRelPrime x y

Tactic:
refine fun z hx hy ↦ by_contra fun h ↦ H z h ?_ hx hy

Result:
α : Type u_1
inst✝ : MonoidWithZero α
x y : α
nonzero : ¬(x = 0 ∧ y = 0)
H : ∀ (z : α), ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y
z : α
hx : z ∣ x
hy : z ∣ y
h : ¬IsUnit z
⊢ z ≠ 0
-- Mathlib/CategoryTheory/Monoidal/Functor.lean
@[simp] lemma prod'_ε_snd : (ε (prod' F G)).2 = ε G

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).2 ≫ G.map (𝟙 (𝟙_ (C × C)).2) = ε G

Tactic:
rw [Functor.map_id, Category.comp_id]

Result:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).2 = ε G

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).2 = ε G

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod' G)).2 = ε G

Tactic:
change _ ≫ G.map (𝟙 _) = _

Result:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).2 ≫ G.map (𝟙 (𝟙_ (C × C)).2) = ε G
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
theorem measure_union₀ (ht : NullMeasurableSet t μ) (hd : AEDisjoint μ s t) :
    μ (s ∪ t) = μ s + μ t

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ μ (s ∪ t) = μ s + μ t

Tactic:
rw [← measure_union_add_inter₀ s ht, hd, add_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem whiskerRight_iff {f g : a ⟶ b} (η θ : f ⟶ g) : η ▷ 𝟙 b = θ ▷ 𝟙 b ↔ η = θ

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η θ : f ⟶ g
⊢ η ▷ 𝟙 b = θ ▷ 𝟙 b ↔ η = θ

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/CommSq.lean
theorem map_commSq (s : CommSq f g h i) : CommSq (F.map f) (F.map g) (F.map h) (F.map i) :=
  ⟨by simpa using congr_arg (fun k : W ⟶ Z => F.map k) s.w⟩

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
D : Type u_2
inst✝ : Category.{u_4, u_2} D
F : C ⥤ D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
s : CommSq f g h i
⊢ F.map f ≫ F.map h = F.map g ≫ F.map i

Tactic:
simpa using congr_arg (fun k : W ⟶ Z => F.map k) s.w

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma Localization.exists_leftFraction {X Y : C} (f : L.obj X ⟶ L.obj Y) :
    ∃ (φ : W.LeftFraction X Y), f = φ.map L (Localization.inverts L W)

Proof state:
case intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
E : MorphismProperty.LeftFraction.Localization W ≌ D := uniq (MorphismProperty.LeftFraction.Localization.Q W) L W
e : MorphismProperty.LeftFraction.Localization.Q W ⋙ E.functor ≅ L :=
  compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W
f' : E.functor.obj X ⟶ E.functor.obj Y
⊢ ∃ φ, e.inv.app X ≫ f' ≫ e.hom.app Y = φ.map L ⋯

Tactic:
obtain ⟨g, rfl⟩ := E.functor.map_surjective f'

Result:
case intro.intro
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
E : MorphismProperty.LeftFraction.Localization W ≌ D := uniq (MorphismProperty.LeftFraction.Localization.Q W) L W
e : MorphismProperty.LeftFraction.Localization.Q W ⋙ E.functor ≅ L :=
  compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W
g : X ⟶ Y
⊢ ∃ φ, e.inv.app X ≫ E.functor.map g ≫ e.hom.app Y = φ.map L ⋯
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseIdx_of_length_le {l : List α} {k : Nat} (h : length l ≤ k) : eraseIdx l k = l

Proof state:
α : Type u_1
l : List α
k : Nat
h : l.length ≤ k
⊢ l.eraseIdx k = l

Tactic:
rw [eraseIdx_eq_self.2 h]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
theorem posDef_prod_iff [PartialOrder P] [AddLeftMono P]
    {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} :
    (Q₁.prod Q₂).PosDef ↔ Q₁.PosDef ∧ Q₂.PosDef

Proof state:
case mpr.intro.intro.intro.mk
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
hle₁ : ∀ (x : M₁), 0 ≤ Q₁ x
ha₁ : Q₁.Anisotropic
hle₂ : ∀ (x : M₂), 0 ≤ Q₂ x
ha₂ : Q₂.Anisotropic
x₁ : M₁
x₂ : M₂
hx : Q₁ x₁ + Q₂ x₂ = 0
⊢ (x₁, x₂) = 0

Tactic:
rw [add_eq_zero_iff_of_nonneg (hle₁ x₁) (hle₂ x₂), ha₁.eq_zero_iff, ha₂.eq_zero_iff] at hx

Result:
case mpr.intro.intro.intro.mk
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
hle₁ : ∀ (x : M₁), 0 ≤ Q₁ x
ha₁ : Q₁.Anisotropic
hle₂ : ∀ (x : M₂), 0 ≤ Q₂ x
ha₂ : Q₂.Anisotropic
x₁ : M₁
x₂ : M₂
hx : x₁ = 0 ∧ x₂ = 0
⊢ (x₁, x₂) = 0

Proof state:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x) ∧ (Q₁.prod Q₂).Anisotropic ↔
    ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ Q₁.Anisotropic) ∧ (∀ (x : M₂), 0 ≤ Q₂ x) ∧ Q₂.Anisotropic

Tactic:
constructor

Result:
case mp
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x) ∧ (Q₁.prod Q₂).Anisotropic →
    ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ Q₁.Anisotropic) ∧ (∀ (x : M₂), 0 ≤ Q₂ x) ∧ Q₂.Anisotropic

case mpr
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R P
inst✝¹ : PartialOrder P
inst✝ : AddLeftMono P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
⊢ ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ Q₁.Anisotropic) ∧ (∀ (x : M₂), 0 ≤ Q₂ x) ∧ Q₂.Anisotropic →
    ((∀ (x : M₁), 0 ≤ Q₁ x) ∧ ∀ (x : M₂), 0 ≤ Q₂ x) ∧ (Q₁.prod Q₂).Anisotropic
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
@[simp]
lemma norm_mul_cos_arg (x : ℂ) : ‖x‖ * Real.cos (arg x) = x.re

Proof state:
x : ℂ
⊢ ‖x‖ * Real.cos x.arg = x.re

Tactic:
simpa [-norm_mul_cos_add_sin_mul_I] using congr_arg re (norm_mul_cos_add_sin_mul_I x)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Basic.lean
theorem Rat.normalize.reduced {num : Int} {den g : Nat} (den_nz : den ≠ 0)
    (e : g = num.natAbs.gcd den) : (num.tdiv g).natAbs.Coprime (den / g) :=
  have : Int.natAbs (num.tdiv ↑g) = num.natAbs / g

Proof state:
num : Int
den g : Nat
den_nz : den ≠ 0
w✝ : Nat
e : g = (↑w✝).natAbs.gcd den
⊢ ((↑w✝).tdiv ↑g).natAbs = (↑w✝).natAbs / g

Tactic:
rfl

Result:
no goals

Proof state:
num : Int
den g : Nat
den_nz : den ≠ 0
w✝ : Nat
e : g = (-↑w✝).natAbs.gcd den
⊢ ((-↑w✝).tdiv ↑g).natAbs = (-↑w✝).natAbs / g

Tactic:
rw [Int.neg_tdiv, Int.natAbs_neg, Int.natAbs_neg]

Result:
num : Int
den g : Nat
den_nz : den ≠ 0
w✝ : Nat
e : g = (-↑w✝).natAbs.gcd den
⊢ ((↑w✝).tdiv ↑g).natAbs = (↑w✝).natAbs / g

Proof state:
num : Int
den g : Nat
den_nz : den ≠ 0
w✝ : Nat
e : g = (-↑w✝).natAbs.gcd den
⊢ ((↑w✝).tdiv ↑g).natAbs = (↑w✝).natAbs / g

Tactic:
rfl

Result:
no goals

Proof state:
num : Int
den g : Nat
den_nz : den ≠ 0
e : g = num.natAbs.gcd den
⊢ (num.tdiv ↑g).natAbs = num.natAbs / g

Tactic:
match num, num.eq_nat_or_neg with
| _, ⟨_, .inl rfl⟩ => rfl
| _, ⟨_, .inr rfl⟩ => rw [Int.neg_tdiv, Int.natAbs_neg, Int.natAbs_neg]; rfl

Result:
no goals
-- Mathlib/Data/Int/Interval.lean
theorem Icc_eq_pair : Finset.Icc a (a + 1) = {a, a + 1}

Proof state:
case h
a a✝ : ℤ
⊢ a✝ ∈ Icc a (a + 1) ↔ a✝ ∈ {a, a + 1}

Tactic:
simp

Result:
case h
a a✝ : ℤ
⊢ a ≤ a✝ ∧ a✝ ≤ a + 1 ↔ a✝ = a ∨ a✝ = a + 1

Proof state:
case h
a a✝ : ℤ
⊢ a ≤ a✝ ∧ a✝ ≤ a + 1 ↔ a✝ = a ∨ a✝ = a + 1

Tactic:
omega

Result:
no goals

Proof state:
a : ℤ
⊢ Icc a (a + 1) = {a, a + 1}

Tactic:
ext

Result:
case h
a a✝ : ℤ
⊢ a✝ ∈ Icc a (a + 1) ↔ a✝ ∈ {a, a + 1}