harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Group/Prod.lean
theorem measurePreserving_mul_prod_inv_right [IsMulRightInvariant μ] [IsMulRightInvariant ν] :
    MeasurePreserving (fun z : G × G => (z.1 * z.2, z.1⁻¹)) (μ.prod ν) (μ.prod ν)

Proof state:
case h.e'_5
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulRightInvariant
inst✝ : ν.IsMulRightInvariant
⊢ (fun z => (z.1 * z.2, z.1⁻¹)) = (fun z => (z.2, z.1 / z.2)) ∘ fun z => (z.2, z.1 * z.2)

Tactic:
ext1 ⟨x, y⟩

Result:
case h.e'_5.h.mk
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulRightInvariant
inst✝ : ν.IsMulRightInvariant
x y : G
⊢ ((x, y).1 * (x, y).2, (x, y).1⁻¹) = ((fun z => (z.2, z.1 / z.2)) ∘ fun z => (z.2, z.1 * z.2)) (x, y)

Proof state:
case h.e'_5.h.mk
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulRightInvariant
inst✝ : ν.IsMulRightInvariant
x y : G
⊢ ((x, y).1 * (x, y).2, (x, y).1⁻¹) = ((fun z => (z.2, z.1 / z.2)) ∘ fun z => (z.2, z.1 * z.2)) (x, y)

Tactic:
simp_rw [Function.comp_apply, div_mul_eq_div_div_swap, div_self', one_div]

Result:
no goals

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulRightInvariant
inst✝ : ν.IsMulRightInvariant
⊢ MeasurePreserving (fun z => (z.1 * z.2, z.1⁻¹)) (μ.prod ν) (μ.prod ν)

Tactic:
convert (measurePreserving_prod_div_swap ν μ).comp (measurePreserving_prod_mul_swap_right μ ν)
  using 1

Result:
case h.e'_5
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulRightInvariant
inst✝ : ν.IsMulRightInvariant
⊢ (fun z => (z.1 * z.2, z.1⁻¹)) = (fun z => (z.2, z.1 / z.2)) ∘ fun z => (z.2, z.1 * z.2)
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_def' (M : Matroid α) (X : Set α) (hX : X ⊆ M.E

Proof state:
α : Type u_2
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.closure X = ⋂₀ {F | M.IsFlat F ∧ X ⊆ F}

Tactic:
rw [closure, inter_eq_self_of_subset_left hX]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iInf_pair {f : β → α} {a b : β} : ⨅ x ∈ ({a, b} : Set β), f x = f a ⊓ f b

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
a b : β
⊢ ⨅ x ∈ {a, b}, f x = f a ⊓ f b

Tactic:
rw [iInf_insert, iInf_singleton]

Result:
no goals
-- Mathlib/Algebra/Homology/HasNoLoop.lean
lemma hasNoLoop_down' {α : Type*} [AddZeroClass α] [IsRightCancelAdd α] [IsLeftCancelAdd α]
    (a : α) (ha : a ≠ 0) :
    (down' a).HasNoLoop

Proof state:
α : Type u_2
inst✝² : AddZeroClass α
inst✝¹ : IsRightCancelAdd α
inst✝ : IsLeftCancelAdd α
a : α
ha : a ≠ 0
this : (up' a).HasNoLoop
⊢ (down' a).HasNoLoop

Tactic:
exact inferInstanceAs (up' a).symm.HasNoLoop

Result:
no goals

Proof state:
α : Type u_2
inst✝² : AddZeroClass α
inst✝¹ : IsRightCancelAdd α
inst✝ : IsLeftCancelAdd α
a : α
ha : a ≠ 0
⊢ (down' a).HasNoLoop

Tactic:
have := hasNoLoop_up' a ha

Result:
α : Type u_2
inst✝² : AddZeroClass α
inst✝¹ : IsRightCancelAdd α
inst✝ : IsLeftCancelAdd α
a : α
ha : a ≠ 0
this : (up' a).HasNoLoop
⊢ (down' a).HasNoLoop
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem succ_mul_succ (a b) : succ a * succ b = a * b + a + b + 1

Proof state:
a b : Nat
⊢ a.succ * b.succ = a * b + a + b + 1

Tactic:
rw [succ_mul, mul_succ]

Result:
a b : Nat
⊢ a * b + a + b.succ = a * b + a + b + 1

Proof state:
a b : Nat
⊢ a * b + a + b.succ = a * b + a + b + 1

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Vandermonde.lean
theorem det_vandermonde_eq_zero_iff [IsDomain R] {n : ℕ} {v : Fin n → R} :
    det (vandermonde v) = 0 ↔ ∃ i j : Fin n, v i = v j ∧ i ≠ j

Proof state:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ (∃ i j, v i = v j ∧ i ≠ j) → (vandermonde v).det = 0

Tactic:
simp only [Ne, forall_exists_index, and_imp]

Result:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ ∀ (x x_1 : Fin n), v x = v x_1 → ¬x = x_1 → (vandermonde v).det = 0

Proof state:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ ∀ (x : Fin n), (x ∈ univ ∧ ∃ a ∈ Ioi x, v a = v x) → ∃ i j, v i = v j ∧ i ≠ j

Tactic:
rintro i ⟨_, j, h₁, h₂⟩

Result:
case mp.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
i : Fin n
left✝ : i ∈ univ
j : Fin n
h₁ : j ∈ Ioi i
h₂ : v j = v i
⊢ ∃ i j, v i = v j ∧ i ≠ j

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ (vandermonde v).det = 0 ↔ ∃ i j, v i = v j ∧ i ≠ j

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ (vandermonde v).det = 0 → ∃ i j, v i = v j ∧ i ≠ j

case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ (∃ i j, v i = v j ∧ i ≠ j) → (vandermonde v).det = 0

Proof state:
case mp.intro.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
i : Fin n
left✝ : i ∈ univ
j : Fin n
h₁ : j ∈ Ioi i
h₂ : v j = v i
⊢ ∃ i j, v i = v j ∧ i ≠ j

Tactic:
exact ⟨j, i, h₂, (mem_Ioi.mp h₁).ne'⟩

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ (vandermonde v).det = 0 → ∃ i j, v i = v j ∧ i ≠ j

Tactic:
simp only [det_vandermonde v, Finset.prod_eq_zero_iff, sub_eq_zero, forall_exists_index]

Result:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ ∀ (x : Fin n), (x ∈ univ ∧ ∃ a ∈ Ioi x, v a = v x) → ∃ i j, v i = v j ∧ i ≠ j

Proof state:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
⊢ ∀ (x x_1 : Fin n), v x = v x_1 → ¬x = x_1 → (vandermonde v).det = 0

Tactic:
refine fun i j h₁ h₂ => Matrix.det_zero_of_row_eq h₂ (funext fun k => ?_)

Result:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
i j : Fin n
h₁ : v i = v j
h₂ : ¬i = j
k : Fin n
⊢ vandermonde v i k = vandermonde v j k

Proof state:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
v : Fin n → R
i j : Fin n
h₁ : v i = v j
h₂ : ¬i = j
k : Fin n
⊢ vandermonde v i k = vandermonde v j k

Tactic:
rw [vandermonde_apply, vandermonde_apply, h₁]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1 :=
  match n % 2, @Nat.mod_lt n 2 (by decide) with
  | 0, _ => .inl rfl
  | 1, _ => .inr rfl

Proof state:
n : Nat
⊢ 2 > 0

Tactic:
decide

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem aecover_closedBall {x : α} {r : ι → ℝ} (hr : Tendsto r l atTop) :
    AECover μ l (fun i ↦ Metric.closedBall x (r i)) where
  measurableSet _ := Metric.isClosed_closedBall.measurableSet
  ae_eventually_mem

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝¹ : PseudoMetricSpace α
inst✝ : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
⊢ ∀ᵐ (x_1 : α) ∂μ, ∀ᶠ (i : ι) in l, x_1 ∈ Metric.closedBall x (r i)

Tactic:
filter_upwards with y

Result:
case h
α : Type u_1
ι : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝¹ : PseudoMetricSpace α
inst✝ : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
y : α
⊢ ∀ᶠ (i : ι) in l, y ∈ Metric.closedBall x (r i)

Proof state:
case h
α : Type u_1
ι : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝¹ : PseudoMetricSpace α
inst✝ : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
y : α
⊢ ∀ᶠ (i : ι) in l, y ∈ Metric.closedBall x (r i)

Tactic:
filter_upwards [hr (Ici_mem_atTop (dist x y))] with a ha using by simpa [dist_comm] using ha

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : MeasurableSpace α
μ : Measure α
l : Filter ι
inst✝¹ : PseudoMetricSpace α
inst✝ : OpensMeasurableSpace α
x : α
r : ι → ℝ
hr : Tendsto r l atTop
y : α
a : ι
ha : a ∈ r ⁻¹' Ici (dist x y)
⊢ y ∈ Metric.closedBall x (r a)

Tactic:
simpa [dist_comm] using ha

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem insertMany_cons {l : List (α × β)} {k : α} {v : β} :
    (insertMany m (⟨k, v⟩ :: l)).1 = (insertMany (m.insert k v) l).1

Proof state:
case nil
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw₀ α fun x => β
k : α
v : β
⊢ insertListₘ m [(k, v)] = insertListₘ (m.insert k v) []

Tactic:
simp [insertListₘ]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw₀ α fun x => β
l : List (α × β)
k : α
v : β
⊢ (insertMany m ((k, v) :: l)).val = (insertMany (m.insert k v) l).val

Tactic:
simp only [insertMany_eq_insertListₘ]

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw₀ α fun x => β
l : List (α × β)
k : α
v : β
⊢ insertListₘ m ((k, v) :: l) = insertListₘ (m.insert k v) l

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw₀ α fun x => β
l : List (α × β)
k : α
v : β
⊢ insertListₘ m ((k, v) :: l) = insertListₘ (m.insert k v) l

Tactic:
cases l with
| nil => simp [insertListₘ]
| cons hd tl => simp [insertListₘ]

Result:
no goals

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw₀ α fun x => β
k : α
v : β
hd : α × β
tl : List (α × β)
⊢ insertListₘ m ((k, v) :: hd :: tl) = insertListₘ (m.insert k v) (hd :: tl)

Tactic:
simp [insertListₘ]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem isClosed_setOf_clusterPt {f : Filter X} : IsClosed { x | ClusterPt x f }

Proof state:
X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ IsClosed {x | ClusterPt x f}

Tactic:
simp only [ClusterPt, inf_neBot_iff_frequently_left, setOf_forall, imp_iff_not_or]

Result:
X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ IsClosed (⋂ i, {x | (¬∀ᶠ (x : X) in 𝓝 x, i x) ∨ ∃ᶠ (x : X) in f, i x})

Proof state:
X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ IsClosed (⋂ i, {x | (¬∀ᶠ (x : X) in 𝓝 x, i x) ∨ ∃ᶠ (x : X) in f, i x})

Tactic:
refine isClosed_iInter fun p => IsClosed.union ?_ ?_ <;> apply isClosed_compl_iff.2

Result:
case refine_1
X : Type u
inst✝ : TopologicalSpace X
f : Filter X
p : X → Prop
⊢ IsOpen fun x => (𝓝 x).sets {x | (fun x => p x) x}

case refine_2
X : Type u
inst✝ : TopologicalSpace X
f : Filter X
p : X → Prop
⊢ IsOpen fun x => f.sets {x | (fun x => ¬(fun x => p x) x) x}

Proof state:
case refine_1
X : Type u
inst✝ : TopologicalSpace X
f : Filter X
p : X → Prop
⊢ IsOpen fun x => (𝓝 x).sets {x | (fun x => p x) x}

case refine_2
X : Type u
inst✝ : TopologicalSpace X
f : Filter X
p : X → Prop
⊢ IsOpen fun x => f.sets {x | (fun x => ¬(fun x => p x) x) x}

Tactic:
exacts [isOpen_setOf_eventually_nhds, isOpen_const]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem SameCycle.exists_fin_pow_eq [Finite α] (h : SameCycle f x y) :
    ∃ i : Fin (orderOf f), (f ^ (i : ℕ)) x = y

Proof state:
case intro.intro
α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
h : f.SameCycle x y
i : ℕ
hi : i < orderOf f
hx : (f ^ i) x = y
⊢ ∃ i, (f ^ ↑i) x = y

Tactic:
exact ⟨⟨i, hi⟩, hx⟩

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
h : f.SameCycle x y
⊢ ∃ i, (f ^ ↑i) x = y

Tactic:
obtain ⟨i, hi, hx⟩ := SameCycle.exists_pow_eq' h

Result:
case intro.intro
α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
h : f.SameCycle x y
i : ℕ
hi : i < orderOf f
hx : (f ^ i) x = y
⊢ ∃ i, (f ^ ↑i) x = y
-- Mathlib/RingTheory/Frobenius.lean
lemma restrict_apply (x : S ⧸ Q) :
    H.restrict x = x ^ Nat.card (R ⧸ Q.under R)

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
x : S
⊢ H.restrict ((Ideal.Quotient.mk Q) x) = (Ideal.Quotient.mk Q) x ^ Nat.card (R ⧸ Ideal.under R Q)

Tactic:
exact H.mk_apply x

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
x : S ⧸ Q
⊢ H.restrict x = x ^ Nat.card (R ⧸ Ideal.under R Q)

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Result:
case intro
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
x : S
⊢ H.restrict ((Ideal.Quotient.mk Q) x) = (Ideal.Quotient.mk Q) x ^ Nat.card (R ⧸ Ideal.under R Q)
-- Mathlib/Algebra/Small/Group.lean
@[simp]
lemma equivShrink_smul {R : Type*} [SMul R α] [Small α] (r : R) (x : α) :
    equivShrink α (r • x) = r • equivShrink α x

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : SMul R α
inst✝ : Small.{u_3, u_1} α
r : R
x : α
⊢ (equivShrink α) (r • x) = (equivShrink α).symm.symm (r • (equivShrink α).symm ((equivShrink α) x))

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : SMul R α
inst✝ : Small.{u_3, u_1} α
r : R
x : α
⊢ (equivShrink α) (r • x) = r • (equivShrink α) x

Tactic:
rw [Equiv.smul_def]

Result:
α : Type u_1
R : Type u_2
inst✝¹ : SMul R α
inst✝ : Small.{u_3, u_1} α
r : R
x : α
⊢ (equivShrink α) (r • x) = (equivShrink α).symm.symm (r • (equivShrink α).symm ((equivShrink α) x))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sub_left_inj {x y : BitVec w} (z : BitVec w) : (x - z = y - z) ↔ x = y

Proof state:
w : Nat
x y z : BitVec w
⊢ x - z = y - z ↔ x = y

Tactic:
simp [sub_toAdd]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[reassoc (attr := simp)]
lemma rightHomologyIso_hom_comp_ι :
    h.rightHomologyIso.hom ≫ h.ι = S.rightHomologyι ≫ h.opcyclesIso.hom

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h : S.RightHomologyData
inst✝ : S.HasRightHomology
⊢ h.rightHomologyIso.hom ≫ h.ι = S.rightHomologyι ≫ h.opcyclesIso.hom

Tactic:
simp only [← cancel_mono h.opcyclesIso.inv, ← cancel_epi h.rightHomologyIso.inv,
  assoc, Iso.inv_hom_id_assoc, Iso.hom_inv_id, comp_id, rightHomologyIso_inv_comp_rightHomologyι]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem mem_insertMany_list [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)} {k : α} :
    k ∈ insertMany m l ↔ k ∈ m ∨ (l.map Prod.fst).contains k

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
k : α
⊢ k ∈ insertMany m l ↔ k ∈ m ∨ (List.map Prod.fst l).contains k = true

Tactic:
simp [mem_iff_contains]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Enum.lean
theorem enumOrd_def (o : Ordinal.{u}) :
    enumOrd s o = sInf (s ∩ { b | ∀ c, c < o → enumOrd s c < b })

Proof state:
s : Set Ordinal.{u}
o : Ordinal.{u}
⊢ enumOrd s o = sInf (s ∩ {b | ∀ c < o, enumOrd s c < b})

Tactic:
rw [enumOrd]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
theorem map_lift_piComparison [HasProduct f] [HasProduct fun b => G.obj (f b)] (P : C)
    (g : ∀ j, P ⟶ f j) : G.map (Pi.lift g) ≫ piComparison G f = Pi.lift fun j => G.map (g j)

Proof state:
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : β → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun b => G.obj (f b)
P : C
g : (j : β) → P ⟶ f j
⊢ G.map (Pi.lift g) ≫ piComparison G f = Pi.lift fun j => G.map (g j)

Tactic:
ext j

Result:
case h
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : β → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun b => G.obj (f b)
P : C
g : (j : β) → P ⟶ f j
j : β
⊢ (G.map (Pi.lift g) ≫ piComparison G f) ≫ Pi.π (fun b => G.obj (f b)) j =
    (Pi.lift fun j => G.map (g j)) ≫ Pi.π (fun b => G.obj (f b)) j

Proof state:
case h
β : Type w
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : β → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun b => G.obj (f b)
P : C
g : (j : β) → P ⟶ f j
j : β
⊢ (G.map (Pi.lift g) ≫ piComparison G f) ≫ Pi.π (fun b => G.obj (f b)) j =
    (Pi.lift fun j => G.map (g j)) ≫ Pi.π (fun b => G.obj (f b)) j

Tactic:
simp only [Discrete.functor_obj, Category.assoc, piComparison_comp_π, ← G.map_comp,
  limit.lift_π, Fan.mk_pt, Fan.mk_π_app]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem mulVec_zero [Fintype n] (A : Matrix m n α) : A *ᵥ 0 = 0

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
x✝ : m
⊢ (A *ᵥ 0) x✝ = 0 x✝

Tactic:
simp [mulVec]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
⊢ A *ᵥ 0 = 0

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
x✝ : m
⊢ (A *ᵥ 0) x✝ = 0 x✝
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem sinh_strictMono : StrictMono sinh :=
  strictMono_of_deriv_pos <| by rw [Real.deriv_sinh]; exact cosh_pos

Proof state:
⊢ ∀ (x : ℝ), 0 < deriv sinh x

Tactic:
rw [Real.deriv_sinh]

Result:
⊢ ∀ (x : ℝ), 0 < cosh x

Proof state:
⊢ ∀ (x : ℝ), 0 < cosh x

Tactic:
exact cosh_pos

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
lemma isBasis'_iff_isBasis_restrict_univ : M.IsBasis' I X ↔ (M ↾ univ).IsBasis I X

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
⊢ M.IsBasis' I X ↔ (M ↾ univ).IsBasis I X

Tactic:
rw [isBasis_restrict_iff', isBasis'_iff_isBasis_inter_ground, and_iff_left (subset_univ _)]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_natDegree (n : ℕ) [NoZeroDivisors S] [Nontrivial S] :
    (ascPochhammer S n).natDegree = n

Proof state:
case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
n : ℕ
hn : (ascPochhammer S n).natDegree = n
⊢ (ascPochhammer S (n + 1)).natDegree = n + 1

Tactic:
have : natDegree (X + (n : S[X])) = 1 := natDegree_X_add_C (n : S)

Result:
case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
n : ℕ
hn : (ascPochhammer S n).natDegree = n
this : (X + ↑n).natDegree = 1
⊢ (ascPochhammer S (n + 1)).natDegree = n + 1

Proof state:
S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
n : ℕ
hn : (ascPochhammer S n).natDegree = n
this : (X + ↑n).natDegree = 1
⊢ ascPochhammer S n ≠ 0

Tactic:
cases n

Result:
case zero
S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
hn : (ascPochhammer S 0).natDegree = 0
this : (X + ↑0).natDegree = 1
⊢ ascPochhammer S 0 ≠ 0

case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
n✝ : ℕ
hn : (ascPochhammer S (n✝ + 1)).natDegree = n✝ + 1
this : (X + ↑(n✝ + 1)).natDegree = 1
⊢ ascPochhammer S (n✝ + 1) ≠ 0

Proof state:
case zero
S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
⊢ (ascPochhammer S 0).natDegree = 0

Tactic:
simp

Result:
no goals

Proof state:
case zero
S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
hn : (ascPochhammer S 0).natDegree = 0
this : (X + ↑0).natDegree = 1
⊢ ascPochhammer S 0 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
S : Type u
inst✝² : Semiring S
n : ℕ
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
⊢ (ascPochhammer S n).natDegree = n

Tactic:
induction' n with n hn

Result:
case zero
S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
⊢ (ascPochhammer S 0).natDegree = 0

case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
n : ℕ
hn : (ascPochhammer S n).natDegree = n
⊢ (ascPochhammer S (n + 1)).natDegree = n + 1

Proof state:
case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
n✝ : ℕ
hn : (ascPochhammer S (n✝ + 1)).natDegree = n✝ + 1
this : (X + ↑(n✝ + 1)).natDegree = 1
⊢ ascPochhammer S (n✝ + 1) ≠ 0

Tactic:
refine ne_zero_of_natDegree_gt <| hn.symm ▸ Nat.add_one_pos _

Result:
no goals

Proof state:
case succ
S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
n : ℕ
hn : (ascPochhammer S n).natDegree = n
this : (X + ↑n).natDegree = 1
⊢ (ascPochhammer S (n + 1)).natDegree = n + 1

Tactic:
rw [ascPochhammer_succ_right,
    natDegree_mul _ (ne_zero_of_natDegree_gt <| this.symm ▸ Nat.zero_lt_one), hn, this]

Result:
S : Type u
inst✝² : Semiring S
inst✝¹ : NoZeroDivisors S
inst✝ : Nontrivial S
n : ℕ
hn : (ascPochhammer S n).natDegree = n
this : (X + ↑n).natDegree = 1
⊢ ascPochhammer S n ≠ 0
-- Mathlib/Topology/ContinuousOn.lean
theorem diff_mem_nhdsWithin_diff {x : α} {s t : Set α} (hs : s ∈ 𝓝[t] x) (t' : Set α) :
    s \ t' ∈ 𝓝[t \ t'] x

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s \ t' ∈ 𝓝[t \ t'] x

Tactic:
rw [nhdsWithin, diff_eq, diff_eq, ← inf_principal, ← inf_assoc]

Result:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s ∩ t'ᶜ ∈ 𝓝 x ⊓ 𝓟 t ⊓ 𝓟 t'ᶜ

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
x : α
s t : Set α
hs : s ∈ 𝓝[t] x
t' : Set α
⊢ s ∩ t'ᶜ ∈ 𝓝 x ⊓ 𝓟 t ⊓ 𝓟 t'ᶜ

Tactic:
exact inter_mem_inf hs (mem_principal_self _)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
lemma posPart_eq_of_eq_sub_negPart {a b : A} (hab : a = b - a⁻) (hb : 0 ≤ b

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a⁺ - a⁻ = b - a⁻
hb : autoParam (0 ≤ b) _auto✝
ha : IsSelfAdjoint a
⊢ a⁺ = b

Tactic:
simpa using hab

Result:
no goals

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a = b - a⁻
hb : autoParam (0 ≤ b) _auto✝
ha : IsSelfAdjoint a
⊢ a⁺ = b

Tactic:
nth_rw 1 [← posPart_sub_negPart a] at hab

Result:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a⁺ - a⁻ = b - a⁻
hb : autoParam (0 ≤ b) _auto✝
ha : IsSelfAdjoint a
⊢ a⁺ = b

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a = b - a⁻
hb : autoParam (0 ≤ b) _auto✝
⊢ a⁺ = b

Tactic:
have ha := hab.symm ▸ hb.isSelfAdjoint.sub (negPart_nonneg a).isSelfAdjoint

Result:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a = b - a⁻
hb : autoParam (0 ≤ b) _auto✝
ha : IsSelfAdjoint a
⊢ a⁺ = b
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_of_contains_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α}
    {v : β k} : (m.insert k v).contains a → (k == a) = false → m.contains a

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
v : β k
⊢ (m.insert k v).contains a = true → (k == a) = false → m.contains a = true

Tactic:
simp_to_model [insert] using List.containsKey_of_containsKey_insertEntry

Result:
no goals