harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
@[simp]
lemma inner_op_smul_left {a : A} {x y : E} : ⟪x <• a, y⟫ = star a * ⟪x, y⟫

Proof state:
A : Type u_1
E : Type u_2
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℂ A
inst✝⁵ : Module ℂ E
inst✝⁴ : PartialOrder A
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm A
inst✝¹ : Norm E
inst✝ : CStarModule A E
a : A
x y : E
⊢ inner (x <• a) y = star a * inner x y

Tactic:
rw [← star_inner]

Result:
A : Type u_1
E : Type u_2
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℂ A
inst✝⁵ : Module ℂ E
inst✝⁴ : PartialOrder A
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm A
inst✝¹ : Norm E
inst✝ : CStarModule A E
a : A
x y : E
⊢ star (inner y (x <• a)) = star a * inner x y

Proof state:
A : Type u_1
E : Type u_2
inst✝⁹ : NonUnitalRing A
inst✝⁸ : StarRing A
inst✝⁷ : AddCommGroup E
inst✝⁶ : Module ℂ A
inst✝⁵ : Module ℂ E
inst✝⁴ : PartialOrder A
inst✝³ : SMul Aᵐᵒᵖ E
inst✝² : Norm A
inst✝¹ : Norm E
inst✝ : CStarModule A E
a : A
x y : E
⊢ star (inner y (x <• a)) = star a * inner x y

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
lemma bitwise_eq_binaryRec (f : Bool → Bool → Bool) :
    bitwise f =
    binaryRec (fun n => cond (f false true) n 0) fun a m Ia =>
      binaryRec (cond (f true false) (bit a m) 0) fun b n _ => bit (f a b) (Ia n)

Proof state:
case h.h.f.f
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
        (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x y
yb : Bool
y : ℕ
hyb : y = 0 → yb = true
a✝ :
  bitwise f (bit xb x) y =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 =>
        bit (f xb b)
          (binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
            (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x n))
      y
⊢ bitwise f (bit xb x) (bit yb y) =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 =>
        bit (f xb b)
          (binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
            (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x n))
      (bit yb y)

Tactic:
rw [← bit_ne_zero_iff] at hyb

Result:
case h.h.f.f
f : Bool → Bool → Bool
xb : Bool
x : ℕ
hxb : bit xb x ≠ 0
ih :
  ∀ (y : ℕ),
    bitwise f x y =
      binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
        (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x y
yb : Bool
y : ℕ
hyb : bit yb y ≠ 0
a✝ :
  bitwise f (bit xb x) y =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 =>
        bit (f xb b)
          (binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
            (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x n))
      y
⊢ bitwise f (bit xb x) (bit yb y) =
    binaryRec (bif f true false then bit xb x else 0)
      (fun b n x_1 =>
        bit (f xb b)
          (binaryRec (motive := fun x => ℕ → ℕ) (fun n => bif f false true then n else 0)
            (fun a m Ia n => binaryRec (bif f true false then bit a m else 0) (fun b n x => bit (f a b) (Ia n)) n) x n))
      (bit yb y)
-- Mathlib/MeasureTheory/Function/UnifTight.lean
theorem tendsto_Lp_of_tendstoInMeasure (hp : 1 ≤ p) (hp' : p ≠ ∞)
    (hf : ∀ n, AEStronglyMeasurable (f n) μ) (hg : MemLp g p μ)
    (hui : UnifIntegrable f p μ) (hut : UnifTight f p μ)
    (hfg : TendstoInMeasure μ f atTop g) : Tendsto (fun n ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
ms : ℕ → ℕ
left✝ : StrictMono ms
hms' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns (ms i)) x) atTop (𝓝 (g x))
⊢ ∃ ms, Tendsto (fun n => eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)

Tactic:
exact ⟨ms,
  tendsto_Lp_of_tendsto_ae hp hp' (fun _ => hf _) hg
    (fun ε hε => let ⟨δ, hδ, hδ'⟩ := hui hε
      ⟨δ, hδ, fun i s hs hμs => hδ' _ s hs hμs⟩)
    (fun ε hε => let ⟨s, hμs, hfε⟩ := hut hε
      ⟨s, hμs, fun i => hfε _⟩)
    hms'⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
⊢ ∃ ms, Tendsto (fun n => eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)

Tactic:
obtain ⟨ms, _, hms'⟩ := TendstoInMeasure.exists_seq_tendsto_ae fun ε hε => (hfg ε hε).comp hns

Result:
case intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
ms : ℕ → ℕ
left✝ : StrictMono ms
hms' : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns (ms i)) x) atTop (𝓝 (g x))
⊢ ∃ ms, Tendsto (fun n => eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : TendstoInMeasure μ f atTop g
⊢ Tendsto (fun n => eLpNorm (f n - g) p μ) atTop (𝓝 0)

Tactic:
refine tendsto_of_subseq_tendsto fun ns hns => ?_

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ⊤
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
⊢ ∃ ms, Tendsto (fun n => eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)
-- Mathlib/Topology/Basic.lean
theorem TopologicalSpace.ext_iff_nhds {X} {t t' : TopologicalSpace X} :
    t = t' ↔ ∀ x, @nhds _ t x = @nhds _ t' x :=
  ⟨fun H _ ↦ congrFun (congrArg _ H) _, fun H ↦ by ext; simp_rw [@isOpen_iff_nhds _ _ _, H]⟩

Proof state:
X : Type u_3
t t' : TopologicalSpace X
H : ∀ (x : X), 𝓝 x = 𝓝 x
⊢ t = t'

Tactic:
ext

Result:
case a.h.a
X : Type u_3
t t' : TopologicalSpace X
H : ∀ (x : X), 𝓝 x = 𝓝 x
x✝ : Set X
⊢ IsOpen x✝ ↔ IsOpen x✝

Proof state:
case a.h.a
X : Type u_3
t t' : TopologicalSpace X
H : ∀ (x : X), 𝓝 x = 𝓝 x
x✝ : Set X
⊢ IsOpen x✝ ↔ IsOpen x✝

Tactic:
simp_rw [@isOpen_iff_nhds _ _ _, H]

Result:
no goals
-- Mathlib/RingTheory/Ideal/IdempotentFG.lean
theorem isIdempotentElem_iff_eq_bot_or_top {R : Type*} [CommRing R] [IsDomain R] (I : Ideal R)
    (h : I.FG) : IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : I.FG
⊢ IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : I.FG
⊢ IsIdempotentElem I → I = ⊥ ∨ I = ⊤

case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : I.FG
⊢ I = ⊥ ∨ I = ⊤ → IsIdempotentElem I

Proof state:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : I.FG
⊢ I = ⊥ ∨ I = ⊤ → IsIdempotentElem I

Tactic:
rintro (rfl | rfl) <;> simp [IsIdempotentElem]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
H : IsIdempotentElem (Submodule.span R {e})
⊢ e = 1 → span {e} = ⊤

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
he : IsIdempotentElem 1
h : FG (Submodule.span R {1})
H : IsIdempotentElem (Submodule.span R {1})
⊢ span {1} = ⊤

Proof state:
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
H : IsIdempotentElem (Submodule.span R {e})
⊢ Submodule.span R {e} = ⊥ ∨ Submodule.span R {e} = ⊤

Tactic:
simp only [Ideal.submodule_span_eq, Ideal.span_singleton_eq_bot]

Result:
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
H : IsIdempotentElem (Submodule.span R {e})
⊢ e = 0 ∨ span {e} = ⊤

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
he : IsIdempotentElem 1
h : FG (Submodule.span R {1})
H : IsIdempotentElem (Submodule.span R {1})
⊢ span {1} = ⊤

Tactic:
simp

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : I.FG
H : IsIdempotentElem I
⊢ I = ⊥ ∨ I = ⊤

Tactic:
obtain ⟨e, he, rfl⟩ := (I.isIdempotentElem_iff_of_fg h).mp H

Result:
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
H : IsIdempotentElem (Submodule.span R {e})
⊢ Submodule.span R {e} = ⊥ ∨ Submodule.span R {e} = ⊤

Proof state:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : I.FG
⊢ IsIdempotentElem I → I = ⊥ ∨ I = ⊤

Tactic:
intro H

Result:
case mp
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : I.FG
H : IsIdempotentElem I
⊢ I = ⊥ ∨ I = ⊤

Proof state:
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
H : IsIdempotentElem (Submodule.span R {e})
⊢ e = 0 ∨ span {e} = ⊤

Tactic:
apply Or.imp id _ (IsIdempotentElem.iff_eq_zero_or_one.mp he)

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
e : R
he : IsIdempotentElem e
h : FG (Submodule.span R {e})
H : IsIdempotentElem (Submodule.span R {e})
⊢ e = 1 → span {e} = ⊤
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem isClosed_iff_of_not_mem (h : ∞ ∉ s) :
    IsClosed s ↔ IsClosed ((↑) ⁻¹' s : Set X) ∧ IsCompact ((↑) ⁻¹' s : Set X)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∉ s
⊢ IsClosed s ↔ IsClosed (some ⁻¹' s) ∧ IsCompact (some ⁻¹' s)

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_of_mem (mem_compl h), ← preimage_compl, compl_compl]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
theorem incMatrix_mul_transpose_apply_of_adj (h : G.Adj a b) :
    (G.incMatrix R * (G.incMatrix R)ᵀ) a b = (1 : R)

Proof state:
case h.e'_2.h.e'_2
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ {x | x ∈ G.incidenceSet a ∩ G.incidenceSet b} = {s(a, b)}

Tactic:
exact G.incidenceSet_inter_incidenceSet_of_adj h

Result:
no goals

Proof state:
case h.e'_2.h.e'_2
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ filter (fun x => x ∈ G.incidenceSet a ∩ G.incidenceSet b) univ = {s(a, b)}

Tactic:
rw [← coe_eq_singleton, coe_filter_univ]

Result:
case h.e'_2.h.e'_2
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ {x | x ∈ G.incidenceSet a ∩ G.incidenceSet b} = {s(a, b)}

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ ↑(#(filter (fun x => x ∈ G.incidenceSet a ∩ G.incidenceSet b) univ)) = 1

Tactic:
convert @Nat.cast_one R _

Result:
case h.e'_2.h.e'_3
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ #(filter (fun x => x ∈ G.incidenceSet a ∩ G.incidenceSet b) univ) = 1

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1

Tactic:
simp_rw [Matrix.mul_apply, Matrix.transpose_apply, incMatrix_apply_mul_incMatrix_apply,
  Set.indicator_apply, Pi.one_apply, sum_boole]

Result:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ ↑(#(filter (fun x => x ∈ G.incidenceSet a ∩ G.incidenceSet b) univ)) = 1

Proof state:
case h.e'_2.h.e'_3
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ #(filter (fun x => x ∈ G.incidenceSet a ∩ G.incidenceSet b) univ) = 1

Tactic:
convert card_singleton s(a, b)

Result:
case h.e'_2.h.e'_2
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ filter (fun x => x ∈ G.incidenceSet a ∩ G.incidenceSet b) univ = {s(a, b)}

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝¹ : Fintype (Sym2 α)
inst✝ : Semiring R
a b : α
h : G.Adj a b
⊢ (incMatrix R G * (incMatrix R G)ᵀ) a b = 1

Tactic:
classical
  simp_rw [Matrix.mul_apply, Matrix.transpose_apply, incMatrix_apply_mul_incMatrix_apply,
    Set.indicator_apply, Pi.one_apply, sum_boole]
  convert @Nat.cast_one R _
  convert card_singleton s(a, b)
  rw [← coe_eq_singleton, coe_filter_univ]
  exact G.incidenceSet_inter_incidenceSet_of_adj h

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem toSignedMeasure_congr {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    (h : μ = ν) : μ.toSignedMeasure = ν.toSignedMeasure

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : μ = ν
⊢ μ.toSignedMeasure = ν.toSignedMeasure

Tactic:
congr

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem Products.evalCons {I} [LinearOrder I] {C : Set (I → Bool)} {l : List I} {a : I}
    (hla : (a::l).Chain' (· > ·)) : Products.eval C ⟨a::l,hla⟩ =
    (e C a) * Products.eval C ⟨l,List.Chain'.sublist hla (List.tail_sublist (a::l))⟩

Proof state:
I : Type u_1
inst✝ : LinearOrder I
C : Set (I → Bool)
l : List I
a : I
hla : List.Chain' (fun x1 x2 => x1 > x2) (a :: l)
⊢ eval C ⟨a :: l, hla⟩ = e C a * eval C ⟨l, ⋯⟩

Tactic:
simp only [eval.eq_1, List.map, List.prod_cons]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[simp]
lemma LeftHomologyData.homologyIso_leftHomologyData [S.HasHomology] :
    S.leftHomologyData.homologyIso = S.leftHomologyIso.symm

Proof state:
case w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData ≫
      leftHomologyMap' (𝟙 S) S.leftHomologyData S.leftHomologyData =
    leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData

Tactic:
rw [← leftHomologyMap'_comp, comp_id]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.leftHomologyData.homologyIso = S.leftHomologyIso.symm

Tactic:
ext

Result:
case w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.leftHomologyData.homologyIso.hom = S.leftHomologyIso.symm.hom

Proof state:
case w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.leftHomologyData.homologyIso.hom = S.leftHomologyIso.symm.hom

Tactic:
dsimp [homologyIso, leftHomologyIso, ShortComplex.leftHomologyIso]

Result:
case w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData ≫
      leftHomologyMap' (𝟙 S) S.leftHomologyData S.leftHomologyData =
    leftHomologyMap' (𝟙 S) S.homologyData.left S.leftHomologyData
-- Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
lemma eval_minpolyDiv_self : (minpolyDiv R x).eval x = aeval x (derivative <| minpoly R x)

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ eval x (minpolyDiv R x) = (aeval x) (derivative (minpoly R x))

Tactic:
rw [aeval_def, ← eval_map, ← derivative_map, ← minpolyDiv_spec R x]

Result:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ eval x (minpolyDiv R x) = eval x (derivative (minpolyDiv R x * (X - C x)))

Proof state:
R : Type u_2
S : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
⊢ eval x (minpolyDiv R x) = eval x (derivative (minpolyDiv R x * (X - C x)))

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Seq/Computation.lean
theorem le_stable (s : Computation α) {a m n} (h : m ≤ n) : s.1 m = some a → s.1 n = some a

Proof state:
case mk
α : Type u
a : α
m n : ℕ
h : m ≤ n
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ ↑⟨f, al⟩ m = some a → ↑⟨f, al⟩ n = some a

Tactic:
induction' h with n _ IH

Result:
case mk.refl
α : Type u
a : α
m n : ℕ
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ ↑⟨f, al⟩ m = some a → ↑⟨f, al⟩ m = some a

case mk.step
α : Type u
a : α
m n✝ : ℕ
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
n : ℕ
a✝ : m.le n
IH : ↑⟨f, al⟩ m = some a → ↑⟨f, al⟩ n = some a
⊢ ↑⟨f, al⟩ m = some a → ↑⟨f, al⟩ n.succ = some a

Proof state:
case mk.refl
α : Type u
a : α
m n : ℕ
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ ↑⟨f, al⟩ m = some a → ↑⟨f, al⟩ m = some a

case mk.step
α : Type u
a : α
m n✝ : ℕ
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
n : ℕ
a✝ : m.le n
IH : ↑⟨f, al⟩ m = some a → ↑⟨f, al⟩ n = some a
⊢ ↑⟨f, al⟩ m = some a → ↑⟨f, al⟩ n.succ = some a

Tactic:
exacts [id, fun h2 => al (IH h2)]

Result:
no goals

Proof state:
α : Type u
s : Computation α
a : α
m n : ℕ
h : m ≤ n
⊢ ↑s m = some a → ↑s n = some a

Tactic:
obtain ⟨f, al⟩ := s

Result:
case mk
α : Type u
a : α
m n : ℕ
h : m ≤ n
f : Stream' (Option α)
al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, f n = some a → f (n + 1) = some a
⊢ ↑⟨f, al⟩ m = some a → ↑⟨f, al⟩ n = some a
-- Mathlib/CategoryTheory/Limits/FinallySmall.lean
theorem FinallySmall.exists_small_weakly_terminal_set [FinallySmall.{w} J] :
    ∃ (s : Set J) (_ : Small.{w} s), ∀ i, ∃ j ∈ s, Nonempty (i ⟶ j)

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : FinallySmall J
i : J
⊢ ∃ j ∈ Set.range (fromFinalModel J).obj, Nonempty (i ⟶ j)

Tactic:
obtain ⟨f⟩ : Nonempty (StructuredArrow i (fromFinalModel J)) := IsConnected.is_nonempty

Result:
case intro
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : FinallySmall J
i : J
f : StructuredArrow i (fromFinalModel J)
⊢ ∃ j ∈ Set.range (fromFinalModel J).obj, Nonempty (i ⟶ j)

Proof state:
case intro
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : FinallySmall J
i : J
f : StructuredArrow i (fromFinalModel J)
⊢ ∃ j ∈ Set.range (fromFinalModel J).obj, Nonempty (i ⟶ j)

Tactic:
exact ⟨(fromFinalModel J).obj f.right, Set.mem_range_self _, ⟨f.hom⟩⟩

Result:
no goals

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : FinallySmall J
⊢ ∃ s, ∃ (_ : Small.{w, u} ↑s), ∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)

Tactic:
refine ⟨Set.range (fromFinalModel J).obj, inferInstance, fun i => ?_⟩

Result:
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : FinallySmall J
i : J
⊢ ∃ j ∈ Set.range (fromFinalModel J).obj, Nonempty (i ⟶ j)
-- Mathlib/Data/Matrix/Mul.lean
theorem one_mul [Fintype m] [DecidableEq m] (M : Matrix m n α) :
    (1 : Matrix m m α) * M = M

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
i✝ : m
j✝ : n
⊢ (1 * M) i✝ j✝ = M i✝ j✝

Tactic:
rw [← diagonal_one, diagonal_mul, one_mul]

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
⊢ 1 * M = M

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
i✝ : m
j✝ : n
⊢ (1 * M) i✝ j✝ = M i✝ j✝
-- Mathlib/Topology/UnitInterval.lean
theorem le_symm_comm {i j : I} : i ≤ σ j ↔ j ≤ σ i

Proof state:
i j : ↑I
⊢ i ≤ σ j ↔ j ≤ σ i

Tactic:
rw [← symm_le_symm, symm_symm]

Result:
no goals
-- Mathlib/Probability/Kernel/Basic.lean
lemma exists_ae_eq_isMarkovKernel {μ : Measure α}
    (h : ∀ᵐ a ∂μ, IsProbabilityMeasure (κ a)) (h' : μ ≠ 0) :
    ∃ (η : Kernel α β), (κ =ᵐ[μ] η) ∧ IsMarkovKernel η

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure (κ a)
h' : μ ≠ 0
a : α
ha : ¬IsProbabilityMeasure (κ a)
⊢ a ∈ toMeasurable μ {a | ¬IsProbabilityMeasure (κ a)}

Tactic:
exact subset_toMeasurable _ _ ha

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure (κ a)
h' : μ ≠ 0
s : Set α
s_meas : MeasurableSet s
μs : μ s = 0
hs : ∀ a ∉ s, IsProbabilityMeasure (κ a)
a : α
ha : a ∈ sᶜ
⊢ IsMarkovKernel (piecewise s_meas (const α (κ a)) κ)

Tactic:
refine ⟨fun b ↦ ?_⟩

Result:
case intro.intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure (κ a)
h' : μ ≠ 0
s : Set α
s_meas : MeasurableSet s
μs : μ s = 0
hs : ∀ a ∉ s, IsProbabilityMeasure (κ a)
a : α
ha : a ∈ sᶜ
b : α
⊢ IsProbabilityMeasure ((piecewise s_meas (const α (κ a)) κ) b)

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure (κ a)
h' : μ ≠ 0
s : Set α
s_meas : MeasurableSet s
μs : μ s = 0
hs : ∀ a ∉ s, IsProbabilityMeasure (κ a)
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ s
⊢ IsProbabilityMeasure ((piecewise s_meas (const α (κ a)) κ) b)

Tactic:
simpa [hb, piecewise] using hs _ ha

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure (κ a)
h' : μ ≠ 0
s : Set α
s_meas : MeasurableSet s
μs : μ s = 0
hs : ∀ a ∉ s, IsProbabilityMeasure (κ a)
a : α
ha : a ∈ sᶜ
⊢ ⇑κ =ᶠ[ae μ] ⇑(piecewise s_meas (const α (κ a)) κ)

Tactic:
filter_upwards [measure_zero_iff_ae_nmem.1 μs] with b hb

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
μ : Measure α
h : ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure (κ a)
h' : μ ≠ 0
s : Set α
s_meas : MeasurableSet s
μs : μ s = 0
hs : ∀ a ∉ s, IsProbabilityMeasure (κ a)
a : α
ha : a ∈ sᶜ
b : α
hb : b ∉ s
⊢ κ b = (piecewise s_meas (const α (κ a)) κ) b