harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Complex/Basic.lean
theorem conj_ofReal (r : ℝ) : conj (r : ℂ) = r :=
  Complex.ext_iff.2 <| by simp [star]

Proof state:
r : ℝ
⊢ ((starRingEnd ℂ) ↑r).re = (↑r).re ∧ ((starRingEnd ℂ) ↑r).im = (↑r).im

Tactic:
simp [star]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
/-- Given any pair of coprime elements of `R`, there exists a matrix in `SL(2, R)` having those
entries as its left or right column. -/
lemma exists_SL2_col {a b : R} (hab : IsCoprime a b) (j : Fin 2) :
    ∃ g : SL(2, R), g 0 j = a ∧ g 1 j = b

Proof state:
case intro.intro.refine_2
R : Type u_1
inst✝ : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ !![v, a; -u, b].det = 1

Tactic:
rw [Matrix.det_fin_two_of, ← h]

Result:
case intro.intro.refine_2
R : Type u_1
inst✝ : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ v * b - a * -u = u * a + v * b

Proof state:
R : Type u_1
inst✝ : CommRing R
a b : R
hab : IsCoprime a b
j : Fin 2
⊢ ∃ g, ↑g 0 j = a ∧ ↑g 1 j = b

Tactic:
obtain ⟨u, v, h⟩ := hab

Result:
case intro.intro
R : Type u_1
inst✝ : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ ∃ g, ↑g 0 j = a ∧ ↑g 1 j = b

Proof state:
case intro.intro.refine_2
R : Type u_1
inst✝ : CommRing R
a b : R
j : Fin 2
u v : R
h : u * a + v * b = 1
⊢ v * b - a * -u = u * a + v * b

Tactic:
ring

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem toFractionRingRingEquiv_symm_eq :
    (toFractionRingRingEquiv K).symm = (IsLocalization.algEquiv K[X]⁰ _ _).toRingEquiv

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
⊢ (toFractionRingRingEquiv K).symm = (IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) (RatFunc K)).toRingEquiv

Tactic:
ext x

Result:
case h
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x : FractionRing K[X]
⊢ (toFractionRingRingEquiv K).symm x = (IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) (RatFunc K)).toRingEquiv x

Proof state:
case h
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x : FractionRing K[X]
⊢ (toFractionRingRingEquiv K).symm x = (IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) (RatFunc K)).toRingEquiv x

Tactic:
simp [toFractionRingRingEquiv, ofFractionRing_eq, AlgEquiv.coe_ringEquiv']

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem ofDigits_mod_eq_head! (b : ℕ) (l : List ℕ) : ofDigits b l % b = l.head! % b

Proof state:
b : ℕ
l : List ℕ
⊢ ofDigits b l % b = l.head! % b

Tactic:
induction l <;> simp [Nat.ofDigits, Int.ModEq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
    (m.erase k).1.size = if m.contains k then m.1.size - 1 else m.1.size

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
⊢ (m.erase k).val.size = if m.contains k = true then m.val.size - 1 else m.val.size

Tactic:
simp_to_model [erase] using List.length_eraseKey

Result:
no goals
-- Mathlib/Algebra/BigOperators/Balance.lean
@[simp] lemma map_balance [FunLike F G H] [LinearMapClass F ℚ≥0 G H] (g : F) (f : ι → G) (a : ι) :
    g (balance f a) = balance (g ∘ f) a

Proof state:
ι : Type u_1
H : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup G
inst✝⁴ : Module ℚ≥0 G
inst✝³ : AddCommGroup H
inst✝² : Module ℚ≥0 H
inst✝¹ : FunLike F G H
inst✝ : LinearMapClass F ℚ≥0 G H
g : F
f : ι → G
a : ι
⊢ g (balance f a) = balance (⇑g ∘ f) a

Tactic:
simp [balance, map_expect]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Positive.lean
theorem isPositive_iff_complex (T : E' →L[ℂ] E') :
    IsPositive T ↔ ∀ x, (re ⟪T x, x⟫_ℂ : ℂ) = ⟪T x, x⟫_ℂ ∧ 0 ≤ re ⟪T x, x⟫_ℂ

Proof state:
E' : Type u_4
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℂ E'
inst✝ : CompleteSpace E'
T : E' →L[ℂ] E'
⊢ ((∀ (v : E'), ↑(re ⟪↑T v, v⟫_ℂ) = ⟪↑T v, v⟫_ℂ) ∧ ∀ (x : E'), 0 ≤ T.reApplyInnerSelf x) ↔
    (∀ (x : E'), ↑(re ⟪T x, x⟫_ℂ) = ⟪T x, x⟫_ℂ) ∧ ∀ (x : E'), 0 ≤ re ⟪T x, x⟫_ℂ

Tactic:
rfl

Result:
no goals

Proof state:
E' : Type u_4
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℂ E'
inst✝ : CompleteSpace E'
T : E' →L[ℂ] E'
⊢ T.IsPositive ↔ ∀ (x : E'), ↑(re ⟪T x, x⟫_ℂ) = ⟪T x, x⟫_ℂ ∧ 0 ≤ re ⟪T x, x⟫_ℂ

Tactic:
simp_rw [IsPositive, forall_and, isSelfAdjoint_iff_isSymmetric,
  LinearMap.isSymmetric_iff_inner_map_self_real, conj_eq_iff_re]

Result:
E' : Type u_4
inst✝² : NormedAddCommGroup E'
inst✝¹ : InnerProductSpace ℂ E'
inst✝ : CompleteSpace E'
T : E' →L[ℂ] E'
⊢ ((∀ (v : E'), ↑(re ⟪↑T v, v⟫_ℂ) = ⟪↑T v, v⟫_ℂ) ∧ ∀ (x : E'), 0 ≤ T.reApplyInnerSelf x) ↔
    (∀ (x : E'), ↑(re ⟪T x, x⟫_ℂ) = ⟪T x, x⟫_ℂ) ∧ ∀ (x : E'), 0 ≤ re ⟪T x, x⟫_ℂ
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma lieBracket_eq_zero_of_eq_zero (hV : V x = 0) (hW : W x = 0) :
    lieBracket 𝕜 V W x = 0

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
x : E
hV : V x = 0
hW : W x = 0
⊢ lieBracket 𝕜 V W x = 0

Tactic:
simp [lieBracket, hV, hW]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem finrank_matrix (m n : Type*) [Fintype m] [Fintype n] :
    finrank R (Matrix m n M) = card m * card n * finrank R M

Proof state:
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : StrongRankCondition R
inst✝² : Free R M
m : Type u_2
n : Type u_3
inst✝¹ : Fintype m
inst✝ : Fintype n
⊢ finrank R (Matrix m n M) = card m * card n * finrank R M

Tactic:
simp [finrank]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem head?_range (n : Nat) : (range n).head? = if n = 0 then none else some 0

Proof state:
n : Nat
⊢ (range n).head? = if n = 0 then none else some 0

Tactic:
induction n with
| zero => simp
| succ n ih =>
  simp only [range_succ, head?_append, ih]
  split <;> simp_all

Result:
no goals

Proof state:
case succ
n : Nat
ih : (range n).head? = if n = 0 then none else some 0
⊢ (range (n + 1)).head? = if n + 1 = 0 then none else some 0

Tactic:
simp only [range_succ, head?_append, ih]

Result:
case succ
n : Nat
ih : (range n).head? = if n = 0 then none else some 0
⊢ (if n = 0 then none else some 0).or [n].head? = if n + 1 = 0 then none else some 0

Proof state:
case zero

⊢ (range 0).head? = if 0 = 0 then none else some 0

Tactic:
simp

Result:
no goals

Proof state:
case succ
n : Nat
ih : (range n).head? = if n = 0 then none else some 0
⊢ (if n = 0 then none else some 0).or [n].head? = if n + 1 = 0 then none else some 0

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem inv_le_iff_inv_le : a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Proof state:
a b : ℝ≥0∞
⊢ a⁻¹ ≤ b ↔ b⁻¹ ≤ a

Tactic:
simpa only [inv_inv] using @ENNReal.inv_le_inv a b⁻¹

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem isEmpty_eq (l : AssocList α β) : isEmpty l = l.toList.isEmpty

Proof state:
α : Type u_1
β : Type u_2
l : AssocList α β
⊢ l.isEmpty = l.toList.isEmpty

Tactic:
cases l <;> simp [*, isEmpty, List.isEmpty]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Asymptotics.lean
theorem LocallyIntegrableOn.integrableOn_of_isBigO_atTop [IsMeasurablyGenerated (atTop (α := α))]
    (hf : LocallyIntegrableOn f (Ici a) μ) (ho : f =O[atTop] g)
    (hg : IntegrableAtFilter g atTop μ) : IntegrableOn f (Ici a) μ

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
inst✝² : LinearOrder α
inst✝¹ : CompactIccSpace α
inst✝ : atTop.IsMeasurablyGenerated
hf : LocallyIntegrableOn f (Ici a) μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ StronglyMeasurableAtFilter f atTop μ

Tactic:
exact ⟨Ici a, Ici_mem_atTop a, hf.aestronglyMeasurable⟩

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
inst✝² : LinearOrder α
inst✝¹ : CompactIccSpace α
inst✝ : atTop.IsMeasurablyGenerated
hf : LocallyIntegrableOn f (Ici a) μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ IntegrableOn f (Ici a) μ

Tactic:
refine integrableOn_Ici_iff_integrableAtFilter_atTop.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : NormedAddCommGroup E
f : α → E
g : α → F
a : α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : SecondCountableTopology α
inst✝⁴ : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F
inst✝² : LinearOrder α
inst✝¹ : CompactIccSpace α
inst✝ : atTop.IsMeasurablyGenerated
hf : LocallyIntegrableOn f (Ici a) μ
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
⊢ StronglyMeasurableAtFilter f atTop μ
-- Mathlib/Order/Filter/Map.lean
theorem map_eq_map_iff_of_injOn {f g : Filter α} {m : α → β} {s : Set α} (hsf : s ∈ f) (hsg : s ∈ g)
    (hm : InjOn m s) : map m f = map m g ↔ f = g

Proof state:
α : Type u_1
β : Type u_2
f g : Filter α
m : α → β
s : Set α
hsf : s ∈ f
hsg : s ∈ g
hm : InjOn m s
⊢ map m f = map m g ↔ f = g

Tactic:
simp only [le_antisymm_iff, map_le_map_iff_of_injOn hsf hsg hm,
  map_le_map_iff_of_injOn hsg hsf hm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem compl_mem_cofinite : sᶜ ∈ μ.cofinite ↔ μ s < ∞

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ sᶜ ∈ μ.cofinite ↔ μ s < ⊤

Tactic:
rw [mem_cofinite, compl_compl]

Result:
no goals
-- Mathlib/Algebra/Star/Subalgebra.lean
theorem inf_toSubalgebra (S T : StarSubalgebra R A) :
    (S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S T : StarSubalgebra R A
⊢ (S ⊓ T).toSubalgebra = S.toSubalgebra ⊓ T.toSubalgebra

Tactic:
ext

Result:
case h
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S T : StarSubalgebra R A
x✝ : A
⊢ x✝ ∈ (S ⊓ T).toSubalgebra ↔ x✝ ∈ S.toSubalgebra ⊓ T.toSubalgebra

Proof state:
case h
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
S T : StarSubalgebra R A
x✝ : A
⊢ x✝ ∈ (S ⊓ T).toSubalgebra ↔ x✝ ∈ S.toSubalgebra ⊓ T.toSubalgebra

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/LinearMap.lean
theorem LinearIsometryEquiv.inner_map_eq_flip (f : E ≃ₗᵢ[𝕜] E') (x : E) (y : E') :
    ⟪f x, y⟫_𝕜 = ⟪x, f.symm y⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : SeminormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
E' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
x : E
y : E'
⊢ ⟪f x, y⟫_𝕜 = ⟪x, f.symm y⟫_𝕜

Tactic:
conv_lhs => rw [← f.apply_symm_apply y, f.inner_map_map]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Catalan.lean
theorem coe_treesOfNumNodesEq (n : ℕ) :
    ↑(treesOfNumNodesEq n) = { x : Tree Unit | x.numNodes = n } :=
  Set.ext (by simp)

Proof state:
n : ℕ
⊢ ∀ (x : Tree Unit), x ∈ ↑(treesOfNumNodesEq n) ↔ x ∈ {x | x.numNodes = n}

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
    (h : m.WF) {hc : k ∈ Const.alter m k f} :
    haveI h' : (f (Const.get? m k)).isSome := mem_alter_self h |>.mp hc
    Const.get (Const.alter m k f) k hc = (f (Const.get? m k)).get h'

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : Option β → Option β
h : m.WF
hc✝ : k ∈ alter m k f
hc : (alter m k f).contains k = true
⊢ get (alter m k f) k hc✝ = (f (get? m k)).get ⋯

Tactic:
revert hc

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : Option β → Option β
h : m.WF
hc : k ∈ alter m k f
⊢ (alter m k f).contains k = true → get (alter m k f) k hc = (f (get? m k)).get ⋯

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : Option β → Option β
h : m.WF
hc : k ∈ alter m k f
⊢ (alter m k f).contains k = true → get (alter m k f) k hc = (f (get? m k)).get ⋯

Tactic:
simp [get_alter h]

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : Option β → Option β
h : m.WF
hc : k ∈ alter m k f
⊢ get (alter m k f) k hc = (f (get? m k)).get ⋯

Tactic:
simp only [mem_iff_contains] at hc

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : Option β → Option β
h : m.WF
hc✝ : k ∈ alter m k f
hc : (alter m k f).contains k = true
⊢ get (alter m k f) k hc✝ = (f (get? m k)).get ⋯
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem map_prod_left_eq_zip {l : List α} (f : α → β) :
    (l.map fun x => (x, f x)) = l.zip (l.map f)

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → β
⊢ (map (fun x => x) l).zip (map f l) = l.zip (map f l)

Tactic:
congr

Result:
case e_a
α : Type u_1
β : Type u_2
l : List α
f : α → β
⊢ map (fun x => x) l = l

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → β
⊢ map (fun x => (x, f x)) l = l.zip (map f l)

Tactic:
rw [← zip_map']

Result:
α : Type u_1
β : Type u_2
l : List α
f : α → β
⊢ (map (fun x => x) l).zip (map f l) = l.zip (map f l)

Proof state:
case e_a
α : Type u_1
β : Type u_2
l : List α
f : α → β
⊢ map (fun x => x) l = l

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Final/ParallelPair.lean
lemma parallelPair_initial_mk {X Y : C} (f g : X ⟶ Y)
    (h₁ : ∀ Z, Nonempty (X ⟶ Z))
    (h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ (a : Y ⟶ Z), i = f ≫ a ∧ j = g ≫ a) :
    (parallelPair f g).Initial :=
  parallelPair_initial_mk' f g h₁ (fun Z i j => by
    obtain ⟨a, rfl, rfl⟩ := h₂ i j
    let f₁ : (mk (Y := zero) (f ≫ a) : CostructuredArrow (parallelPair f g) Z) ⟶ mk (Y := one) a :=
      homMk left
    let f₂ : (mk (Y := zero) (g ≫ a) : CostructuredArrow (parallelPair f g) Z) ⟶ mk (Y := one) a :=
      homMk right
    exact Zigzag.of_hom_inv f₁ f₂)

Proof state:
case intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ a, i = f ≫ a ∧ j = g ≫ a
Z : C
a : Y ⟶ Z
f₁ : mk (f ≫ a) ⟶ mk a := homMk left ⋯
f₂ : mk (g ≫ a) ⟶ mk a := homMk right ⋯
⊢ Zigzag (mk (f ≫ a)) (mk (g ≫ a))

Tactic:
exact Zigzag.of_hom_inv f₁ f₂

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ a, i = f ≫ a ∧ j = g ≫ a
Z : C
i j : X ⟶ Z
⊢ Zigzag (mk i) (mk j)

Tactic:
obtain ⟨a, rfl, rfl⟩ := h₂ i j

Result:
case intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ a, i = f ≫ a ∧ j = g ≫ a
Z : C
a : Y ⟶ Z
⊢ Zigzag (mk (f ≫ a)) (mk (g ≫ a))

Proof state:
case intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ a, i = f ≫ a ∧ j = g ≫ a
Z : C
a : Y ⟶ Z
f₁ : mk (f ≫ a) ⟶ mk a := homMk left ⋯
⊢ Zigzag (mk (f ≫ a)) (mk (g ≫ a))

Tactic:
let f₂ : (mk (Y := zero) (g ≫ a) : CostructuredArrow (parallelPair f g) Z) ⟶ mk (Y := one) a :=
  homMk right

Result:
case intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ a, i = f ≫ a ∧ j = g ≫ a
Z : C
a : Y ⟶ Z
f₁ : mk (f ≫ a) ⟶ mk a := homMk left ⋯
f₂ : mk (g ≫ a) ⟶ mk a := homMk right ⋯
⊢ Zigzag (mk (f ≫ a)) (mk (g ≫ a))

Proof state:
case intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ a, i = f ≫ a ∧ j = g ≫ a
Z : C
a : Y ⟶ Z
⊢ Zigzag (mk (f ≫ a)) (mk (g ≫ a))

Tactic:
let f₁ : (mk (Y := zero) (f ≫ a) : CostructuredArrow (parallelPair f g) Z) ⟶ mk (Y := one) a :=
  homMk left

Result:
case intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X Y : C
f g : X ⟶ Y
h₁ : ∀ (Z : C), Nonempty (X ⟶ Z)
h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ a, i = f ≫ a ∧ j = g ≫ a
Z : C
a : Y ⟶ Z
f₁ : mk (f ≫ a) ⟶ mk a := homMk left ⋯
⊢ Zigzag (mk (f ≫ a)) (mk (g ≫ a))
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
@[simp]
lemma polyCharpoly_map_eq_charpoly (x : L) :
    (polyCharpoly φ b).map (MvPolynomial.eval (b.repr x)) = (φ x).charpoly

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup L
inst✝⁶ : Module R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
φ : L →ₗ[R] End R M
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
x : L
⊢ Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpoly b) = charpoly (φ x)

Tactic:
rw [polyCharpoly, polyCharpolyAux_map_eq_charpoly]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/GroupWithZero/List.lean
lemma prod_nonneg {s : List R} (h : ∀ a ∈ s, 0 ≤ a) : 0 ≤ s.prod

Proof state:
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
s : List R
h : ∀ (a : R), a ∈ s → 0 ≤ a
⊢ 0 ≤ s.prod

Tactic:
induction s with
| nil => simp
| cons head tail hind =>
  simp only [prod_cons]
  simp only [mem_cons, forall_eq_or_imp] at h
  exact mul_nonneg h.1 (hind h.2)

Result:
no goals

Proof state:
case cons
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
head : R
tail : List R
hind : (∀ (a : R), a ∈ tail → 0 ≤ a) → 0 ≤ tail.prod
h : 0 ≤ head ∧ ∀ (a : R), a ∈ tail → 0 ≤ a
⊢ 0 ≤ head * tail.prod

Tactic:
exact mul_nonneg h.1 (hind h.2)

Result:
no goals

Proof state:
case cons
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
head : R
tail : List R
hind : (∀ (a : R), a ∈ tail → 0 ≤ a) → 0 ≤ tail.prod
h : ∀ (a : R), a ∈ head :: tail → 0 ≤ a
⊢ 0 ≤ (head :: tail).prod

Tactic:
simp only [prod_cons]

Result:
case cons
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
head : R
tail : List R
hind : (∀ (a : R), a ∈ tail → 0 ≤ a) → 0 ≤ tail.prod
h : ∀ (a : R), a ∈ head :: tail → 0 ≤ a
⊢ 0 ≤ head * tail.prod

Proof state:
case cons
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
head : R
tail : List R
hind : (∀ (a : R), a ∈ tail → 0 ≤ a) → 0 ≤ tail.prod
h : ∀ (a : R), a ∈ head :: tail → 0 ≤ a
⊢ 0 ≤ head * tail.prod

Tactic:
simp only [mem_cons, forall_eq_or_imp] at h

Result:
case cons
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
head : R
tail : List R
hind : (∀ (a : R), a ∈ tail → 0 ≤ a) → 0 ≤ tail.prod
h : 0 ≤ head ∧ ∀ (a : R), a ∈ tail → 0 ≤ a
⊢ 0 ≤ head * tail.prod

Proof state:
case nil
R : Type u_1
inst✝³ : CommMonoidWithZero R
inst✝² : PartialOrder R
inst✝¹ : ZeroLEOneClass R
inst✝ : PosMulMono R
h : ∀ (a : R), a ∈ [] → 0 ≤ a
⊢ 0 ≤ [].prod

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Endofunctor/Algebra.lean
theorem left_inv : strInv h ≫ A.str = 𝟙 _

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ strInv h ≫ A.str = 𝟙 (F.obj A.V)

Tactic:
rw [strInv, ← (h.from ⟨F.obj A.V, F.map A.str⟩).h, ← F.map_id, ← F.map_comp]

Result:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ F.map (A.str ≫ (h.from { V := F.obj A.V, str := F.map A.str }).f) = F.map (𝟙 A.V)

Proof state:
case e_a
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ A.str ≫ (h.from { V := F.obj A.V, str := F.map A.str }).f = 𝟙 A.V

Tactic:
exact right_inv h

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ F.map (A.str ≫ (h.from { V := F.obj A.V, str := F.map A.str }).f) = F.map (𝟙 A.V)

Tactic:
congr

Result:
case e_a
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A : Coalgebra F
h : Limits.IsTerminal A
⊢ A.str ≫ (h.from { V := F.obj A.V, str := F.map A.str }).f = 𝟙 A.V
-- Mathlib/Analysis/Convex/Side.lean
theorem wOppSide_of_left_mem {s : AffineSubspace R P} {x : P} (y : P) (hx : x ∈ s) :
    s.WOppSide x y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
⊢ SameRay R 0 (x -ᵥ y)

Tactic:
apply SameRay.zero_left

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
⊢ SameRay R (x -ᵥ x) (x -ᵥ y)

Tactic:
rw [vsub_self]

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
⊢ SameRay R 0 (x -ᵥ y)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
⊢ s.WOppSide x y

Tactic:
refine ⟨x, hx, x, hx, ?_⟩

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
hx : x ∈ s
⊢ SameRay R (x -ᵥ x) (x -ᵥ y)
-- Mathlib/CategoryTheory/Limits/Preserves/Finite.lean
/-- If we reflect limits of some arbitrary size, then we reflect all finite limits. -/
lemma ReflectsLimitsOfSize.reflectsFiniteLimits
    (F : C ⥤ D) [ReflectsLimitsOfSize.{w, w₂} F] : ReflectsFiniteLimits F where
  reflects J (sJ : SmallCategory J) fJ

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ReflectsLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ ReflectsLimitsOfShape J F

Tactic:
haveI := reflectsSmallestLimits_of_reflectsLimits F

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ReflectsLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : ReflectsLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ ReflectsLimitsOfShape J F

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ReflectsLimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : ReflectsLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ ReflectsLimitsOfShape J F

Tactic:
exact reflectsLimitsOfShape_of_equiv (FinCategory.equivAsType J) F

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem mul_meas_ge_le_lintegral₀ {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) (ε : ℝ≥0∞) :
    ε * μ { x | ε ≤ f x } ≤ ∫⁻ a, f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
ε : ℝ≥0∞
⊢ ε * μ {x | ε ≤ f x} ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
simpa only [lintegral_zero, zero_add] using
  lintegral_add_mul_meas_add_le_le_lintegral (ae_of_all _ fun x => zero_le (f x)) hf ε

Result:
no goals