harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Alter.lean
theorem Ordered.ins : ∀ {path : Path α} {t : RBNode α},
    t.Ordered cmp → path.Ordered cmp → t.All (path.RootOrdered cmp) → (path.ins t).Ordered cmp
  | .root, _, ht, _, _ => Ordered.setBlack.2 ht
  | .left red parent x b, a, ha, ⟨hp, xb, xp, bp, hb⟩, H => by
    unfold Path.ins
    have ⟨ax, ap⟩ := All_and.1 H
    exact hp.ins ⟨ax, xb, ha, hb⟩ ⟨xp, ap, bp⟩
  | .right red a x parent, b, hb, ⟨hp, ax, xp, ap, ha⟩, H => by
    unfold Path.ins
    have ⟨xb, bp⟩ := All_and.1 H
    exact hp.ins ⟨ax, xb, ha, hb⟩ ⟨xp, ap, bp⟩
  | .left black parent x b, a, ha, ⟨hp, xb, xp, bp, hb⟩, H => by
    unfold Path.ins
    have ⟨ax, ap⟩ := All_and.1 H
    exact hp.ins (ha.balance1 ax xb hb) (balance1_All.2 ⟨xp, ap, bp⟩)
  | .right black a x parent, b, hb, ⟨hp, ax, xp, ap, ha⟩, H => by
    unfold Path.ins
    have ⟨xb, bp⟩ := All_and.1 H
    exact hp.ins (ha.balance2 ax xb hb) (balance2_All.2 ⟨xp, ap, bp⟩)

Proof state:
α : Type u_1
cmp : α → α → Ordering
parent : Path α
x : α
b a : RBNode α
ha : RBNode.Ordered cmp a
hp : Ordered cmp parent
xb : All (fun x_1 => cmpLT cmp x x_1) b
xp : RootOrdered cmp parent x
bp : All (RootOrdered cmp parent) b
hb : RBNode.Ordered cmp b
H : All (RootOrdered cmp (left red parent x b)) a
⊢ RBNode.Ordered cmp ((left red parent x b).ins a)

Tactic:
unfold Path.ins

Result:
α : Type u_1
cmp : α → α → Ordering
parent : Path α
x : α
b a : RBNode α
ha : RBNode.Ordered cmp a
hp : Ordered cmp parent
xb : All (fun x_1 => cmpLT cmp x x_1) b
xp : RootOrdered cmp parent x
bp : All (RootOrdered cmp parent) b
hb : RBNode.Ordered cmp b
H : All (RootOrdered cmp (left red parent x b)) a
⊢ RBNode.Ordered cmp (parent.ins (node red a x b))

Proof state:
α : Type u_1
cmp : α → α → Ordering
a : RBNode α
x : α
parent : Path α
b : RBNode α
hb : RBNode.Ordered cmp b
hp : Ordered cmp parent
ax : All (fun x_1 => cmpLT cmp x_1 x) a
xp : RootOrdered cmp parent x
ap : All (RootOrdered cmp parent) a
ha : RBNode.Ordered cmp a
H : All (RootOrdered cmp (right red a x parent)) b
⊢ RBNode.Ordered cmp ((right red a x parent).ins b)

Tactic:
unfold Path.ins

Result:
α : Type u_1
cmp : α → α → Ordering
a : RBNode α
x : α
parent : Path α
b : RBNode α
hb : RBNode.Ordered cmp b
hp : Ordered cmp parent
ax : All (fun x_1 => cmpLT cmp x_1 x) a
xp : RootOrdered cmp parent x
ap : All (RootOrdered cmp parent) a
ha : RBNode.Ordered cmp a
H : All (RootOrdered cmp (right red a x parent)) b
⊢ RBNode.Ordered cmp (parent.ins (node red a x b))

Proof state:
α : Type u_1
cmp : α → α → Ordering
parent : Path α
x : α
b a : RBNode α
ha : RBNode.Ordered cmp a
hp : Ordered cmp parent
xb : All (fun x_1 => cmpLT cmp x x_1) b
xp : RootOrdered cmp parent x
bp : All (RootOrdered cmp parent) b
hb : RBNode.Ordered cmp b
H : All (RootOrdered cmp (left red parent x b)) a
ax : All (fun a => cmpLT cmp a x) a
ap : All (RootOrdered cmp parent) a
⊢ RBNode.Ordered cmp (parent.ins (node red a x b))

Tactic:
exact hp.ins ⟨ax, xb, ha, hb⟩ ⟨xp, ap, bp⟩

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Prorepresentability.lean
@[simp]
lemma autMulEquivAutGalois_symm_app (x : AutGalois F) (A : C) [IsGalois A] (a : F.obj A) :
    ((autMulEquivAutGalois F).symm ⟨x⟩).hom.app A a =
      F.map (AutGalois.π F ⟨A, a, inferInstance⟩ x).hom a

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
x : AutGalois F
A : C
inst✝ : IsGalois A
a : (F.obj A).carrier
⊢ ((autMulEquivAutGalois F).symm { unop' := x }).hom.app A a =
    F.map ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) x).hom a

Tactic:
rw [← autMulEquivAutGalois_π, MulEquiv.apply_symm_apply]

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
x : AutGalois F
A : C
inst✝ : IsGalois A
a : (F.obj A).carrier
⊢ F.map ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) (MulOpposite.unop { unop' := x })).hom a =
    F.map ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) x).hom a

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
x : AutGalois F
A : C
inst✝ : IsGalois A
a : (F.obj A).carrier
⊢ F.map ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) (MulOpposite.unop { unop' := x })).hom a =
    F.map ((AutGalois.π F { obj := A, pt := a, isGalois := ⋯ }) x).hom a

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem toMeasureOfZeroLE_toSignedMeasure (hs : 0 ≤[Set.univ] s) :
    (s.toMeasureOfZeroLE Set.univ MeasurableSet.univ hs).toSignedMeasure = s

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
hs : 0 ≤[univ] s
⊢ (s.toMeasureOfZeroLE univ ⋯ hs).toSignedMeasure = s

Tactic:
ext i hi

Result:
case h
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
hs : 0 ≤[univ] s
i : Set α
hi : MeasurableSet i
⊢ ↑(s.toMeasureOfZeroLE univ ⋯ hs).toSignedMeasure i = ↑s i

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
hs : 0 ≤[univ] s
i : Set α
hi : MeasurableSet i
⊢ ↑(s.toMeasureOfZeroLE univ ⋯ hs).toSignedMeasure i = ↑s i

Tactic:
simp [hi, toMeasureOfZeroLE_apply _ _ _ hi]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem isAlgebraic_iSup {ι : Type*} {t : ι → IntermediateField K L}
    (h : ∀ i, Algebra.IsAlgebraic K (t i)) :
    Algebra.IsAlgebraic K (⨆ i, t i : IntermediateField K L)

Proof state:
case isAlgebraic
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)
⊢ ∀ (x : ↥(⨆ i, t i)), IsAlgebraic K x

Tactic:
rintro ⟨x, hx⟩

Result:
case isAlgebraic.mk
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)
x : L
hx : x ∈ ⨆ i, t i
⊢ IsAlgebraic K ⟨x, hx⟩

Proof state:
case isAlgebraic.mk
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)
x : L
hx : x ∈ ⨆ i, t i
⊢ IsAlgebraic K ⟨x, hx⟩

Tactic:
obtain ⟨s, hx⟩ := exists_finset_of_mem_supr' hx

Result:
case isAlgebraic.mk.intro
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)
x : L
hx✝ : x ∈ ⨆ i, t i
s : Finset ((i : ι) × ↥(t i))
hx : x ∈ ⨆ i ∈ s, K⟮↑i.snd⟯
⊢ IsAlgebraic K ⟨x, hx✝⟩

Proof state:
case isAlgebraic.mk.intro
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)
x : L
hx✝ : x ∈ ⨆ i, t i
s : Finset ((i : ι) × ↥(t i))
hx : x ∈ ⨆ i ∈ s, K⟮↑i.snd⟯
⊢ IsAlgebraic K ⟨x, hx⟩

Tactic:
haveI : ∀ i : Σ i, t i, FiniteDimensional K K⟮(i.2 : L)⟯ := fun ⟨i, x⟩ ↦
  adjoin.finiteDimensional (isIntegral_iff.1 (Algebra.IsIntegral.isIntegral x))

Result:
case isAlgebraic.mk.intro
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)
x : L
hx✝ : x ∈ ⨆ i, t i
s : Finset ((i : ι) × ↥(t i))
hx : x ∈ ⨆ i ∈ s, K⟮↑i.snd⟯
this : ∀ (i : (i : ι) × ↥(t i)), FiniteDimensional K ↥K⟮↑i.snd⟯
⊢ IsAlgebraic K ⟨x, hx⟩

Proof state:
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)
⊢ Algebra.IsAlgebraic K ↥(⨆ i, t i)

Tactic:
constructor

Result:
case isAlgebraic
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)
⊢ ∀ (x : ↥(⨆ i, t i)), IsAlgebraic K x

Proof state:
case isAlgebraic.mk.intro
K : Type u
inst✝² : Field K
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
ι : Type u_4
t : ι → IntermediateField K L
h : ∀ (i : ι), Algebra.IsAlgebraic K ↥(t i)
x : L
hx✝ : x ∈ ⨆ i, t i
s : Finset ((i : ι) × ↥(t i))
hx : x ∈ ⨆ i ∈ s, K⟮↑i.snd⟯
this : ∀ (i : (i : ι) × ↥(t i)), FiniteDimensional K ↥K⟮↑i.snd⟯
⊢ IsAlgebraic K ⟨x, hx⟩

Tactic:
apply IsAlgebraic.of_finite

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem eq_mul_of_ediv_eq_right {a b c : Int}
    (H1 : b ∣ a) (H2 : a / b = c) : a = b * c

Proof state:
a b c : Int
H1 : b ∣ a
H2 : a / b = c
⊢ a = b * c

Tactic:
rw [← H2, Int.mul_ediv_cancel' H1]

Result:
no goals
-- Mathlib/Tactic/Positivity/Core.lean
lemma nonneg_of_isRat {n : ℤ} {d : ℕ} [LinearOrderedRing A] :
    (NormNum.IsRat e n d) → (decide (n = 0)) → (0 ≤ (e : A))
  | ⟨inv, eq⟩, h => by rw [eq, of_decide_eq_true h]; simp

Proof state:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ ↑0 * ⅟↑d

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ e

Tactic:
rw [eq, of_decide_eq_true h]

Result:
A : Type u_1
e : A
n : ℤ
d : ℕ
inst✝ : LinearOrderedRing A
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (n = 0) = true
⊢ 0 ≤ ↑0 * ⅟↑d
-- Mathlib/Dynamics/Ergodic/MeasurePreserving.lean
theorem comp_left_iff {g : α → β} {e : β ≃ᵐ γ} (h : MeasurePreserving e μb μc) :
    MeasurePreserving (e ∘ g) μa μc ↔ MeasurePreserving g μa μb

Proof state:
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : β ≃ᵐ γ
h : MeasurePreserving (⇑e) μb μc
hg : MeasurePreserving (⇑e ∘ g) μa μc
⊢ g = ⇑e.symm ∘ ⇑e ∘ g

Tactic:
simp [← Function.comp_assoc e.symm e g]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : β ≃ᵐ γ
h : MeasurePreserving (⇑e) μb μc
⊢ MeasurePreserving (⇑e ∘ g) μa μc ↔ MeasurePreserving g μa μb

Tactic:
refine ⟨fun hg => ?_, fun hg => h.comp hg⟩

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : β ≃ᵐ γ
h : MeasurePreserving (⇑e) μb μc
hg : MeasurePreserving (⇑e ∘ g) μa μc
⊢ MeasurePreserving g μa μb

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : β ≃ᵐ γ
h : MeasurePreserving (⇑e) μb μc
hg : MeasurePreserving (⇑e ∘ g) μa μc
⊢ MeasurePreserving g μa μb

Tactic:
convert (MeasurePreserving.symm e h).comp hg

Result:
case h.e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
g : α → β
e : β ≃ᵐ γ
h : MeasurePreserving (⇑e) μb μc
hg : MeasurePreserving (⇑e ∘ g) μa μc
⊢ g = ⇑e.symm ∘ ⇑e ∘ g
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_allOnes : (allOnes v).getMsbD i = decide (i < v)

Proof state:
v i : Nat
⊢ (allOnes v).getMsbD i = decide (i < v)

Tactic:
simp [allOnes]

Result:
v i : Nat
⊢ i < v → v - 1 - i < v

Proof state:
v i : Nat
⊢ i < v → v - 1 - i < v

Tactic:
omega

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem dlookup_kunion_right {a} {l₁ l₂ : List (Sigma β)} (h : a ∉ l₁.keys) :
    dlookup a (kunion l₁ l₂) = dlookup a l₂

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
head✝ : Sigma β
tail✝ : List (Sigma β)
ih : ∀ {l₂ : List (Sigma β)}, a ∉ tail✝.keys → dlookup a (tail✝.kunion l₂) = dlookup a l₂
l₂ : List (Sigma β)
h : a ∉ (head✝ :: tail✝).keys
⊢ dlookup a ((head✝ :: tail✝).kunion l₂) = dlookup a l₂

Tactic:
simp_all [not_or]

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₂ : List (Sigma β)
h : a ∉ [].keys
⊢ dlookup a ([].kunion l₂) = dlookup a l₂

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
h : a ∉ l₁.keys
⊢ dlookup a (l₁.kunion l₂) = dlookup a l₂

Tactic:
induction l₁ generalizing l₂ with
| nil => simp
| cons _ _ ih => simp_all [not_or]

Result:
no goals
-- Mathlib/Order/Category/HeytAlg.lean
lemma inv_hom_apply {X Y : HeytAlg} (e : X ≅ Y) (x : X) : e.inv (e.hom x) = x

Proof state:
X Y : HeytAlg
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_concat_length (l : List α) (a : α) : (l ++ [a])[l.length]? = some a

Proof state:
α : Type u_1
l : List α
a : α
⊢ (l ++ [a])[l.length]? = some a

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem comap_sSup {s : Set (Filter β)} {m : α → β} : comap m (sSup s) = ⨆ f ∈ s, comap m f

Proof state:
α : Type u_1
β : Type u_2
s : Set (Filter β)
m : α → β
⊢ comap m (sSup s) = ⨆ f ∈ s, comap m f

Tactic:
simp only [sSup_eq_iSup, comap_iSup, eq_self_iff_true]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Basic.lean
theorem tensor_comp {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁)
    (g₂ : Y₂ ⟶ Z₂) : tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂

Proof state:
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂

Tactic:
apply IsLimit.hom_ext (ℬ _ _).isLimit

Result:
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ ∀ (j : Discrete WalkingPair),
    tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app j =
      (tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app j

Proof state:
case mk.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ (ℬ Z₁ Z₂).isLimit.lift
        (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁ ≫ g₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂ ≫ g₂)) ≫
      BinaryFan.snd (ℬ Z₁ Z₂).cone =
    ((ℬ Y₁ Y₂).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂)) ≫
        (ℬ Z₁ Z₂).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ Y₁ Y₂).cone ≫ g₁) (BinaryFan.snd (ℬ Y₁ Y₂).cone ≫ g₂))) ≫
      BinaryFan.snd (ℬ Z₁ Z₂).cone

Tactic:
simp

Result:
no goals

Proof state:
case mk.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ tensorHom ℬ (f₁ ≫ g₁) (f₂ ≫ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.right } =
    (tensorHom ℬ f₁ f₂ ≫ tensorHom ℬ g₁ g₂) ≫ (ℬ Z₁ Z₂).cone.π.app { as := WalkingPair.right }

Tactic:
dsimp [tensorHom]

Result:
case mk.right
C : Type u
inst✝ : Category.{v, u} C
ℬ : (X Y : C) → LimitCone (pair X Y)
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ (ℬ Z₁ Z₂).isLimit.lift
        (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁ ≫ g₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂ ≫ g₂)) ≫
      BinaryFan.snd (ℬ Z₁ Z₂).cone =
    ((ℬ Y₁ Y₂).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ X₁ X₂).cone ≫ f₁) (BinaryFan.snd (ℬ X₁ X₂).cone ≫ f₂)) ≫
        (ℬ Z₁ Z₂).isLimit.lift (BinaryFan.mk (BinaryFan.fst (ℬ Y₁ Y₂).cone ≫ g₁) (BinaryFan.snd (ℬ Y₁ Y₂).cone ≫ g₂))) ≫
      BinaryFan.snd (ℬ Z₁ Z₂).cone
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem _root_.Multiset.aestronglyMeasurable_prod (s : Multiset (α → M))
    (hs : ∀ f ∈ s, AEStronglyMeasurable f μ) :
    AEStronglyMeasurable (fun x => (s.map fun f : α → M => f x).prod) μ

Proof state:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
s : Multiset (α → M)
hs : ∀ f ∈ s, AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x => (Multiset.map (fun f => f x) s).prod) μ

Tactic:
simpa only [← Pi.multiset_prod_apply] using s.aestronglyMeasurable_prod' hs

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma castPred_succAbove (x : Fin n) (y : Fin (n + 1)) (h : castSucc x < y)
    (h' := Fin.ne_last_of_lt <| (succAbove_lt_iff_castSucc_lt ..).2 h) :
    (y.succAbove x).castPred h' = x

Proof state:
n : ℕ
x : Fin n
y : Fin (n + 1)
h : x.castSucc < y
h' : optParam (y.succAbove x ≠ last n) ⋯
⊢ (y.succAbove x).castPred h' = x

Tactic:
rw [castPred_eq_iff_eq_castSucc, succAbove_of_castSucc_lt _ _ h]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem ENNReal.tsum_geometric_add_one (r : ℝ≥0∞) : ∑' n : ℕ, r ^ (n + 1) = r * (1 - r)⁻¹

Proof state:
r : ℝ≥0∞
⊢ ∑' (n : ℕ), r ^ (n + 1) = r * (1 - r)⁻¹

Tactic:
simp only [_root_.pow_succ', ENNReal.tsum_mul_left, ENNReal.tsum_geometric]

Result:
no goals
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem limNthHom_zero : limNthHom f_compat 0 = 0

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
⊢ limNthHom f_compat 0 = 0

Tactic:
simp [limNthHom]

Result:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
⊢ ofIntSeq 0 ⋯ = 0

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
⊢ ofIntSeq 0 ⋯ = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Hom.lean
lemma of_map (f : F) [neZero : NeZero (f a)] : NeZero a :=
  ⟨fun h ↦ ne (f a) <| by rw [h]; exact ZeroHomClass.map_zero f⟩

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroHomClass F α β
a : α
f : F
neZero : NeZero (f a)
h : a = 0
⊢ f a = 0

Tactic:
rw [h]

Result:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroHomClass F α β
a : α
f : F
neZero : NeZero (f a)
h : a = 0
⊢ f 0 = 0

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Zero α
inst✝² : Zero β
inst✝¹ : FunLike F α β
inst✝ : ZeroHomClass F α β
a : α
f : F
neZero : NeZero (f a)
h : a = 0
⊢ f 0 = 0

Tactic:
exact ZeroHomClass.map_zero f

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem mfderivWithin_id (hxs : UniqueMDiffWithinAt I s x) :
    mfderivWithin I I (@id M) s x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
x : M
hxs : UniqueMDiffWithinAt I s x
⊢ mfderiv I I id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)

Tactic:
exact mfderiv_id

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
x : M
hxs : UniqueMDiffWithinAt I s x
⊢ mfderivWithin I I id s x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)

Tactic:
rw [MDifferentiable.mfderivWithin mdifferentiableAt_id hxs]

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Set M
x : M
hxs : UniqueMDiffWithinAt I s x
⊢ mfderiv I I id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem LocallyIntegrable.indicator (hf : LocallyIntegrable f μ) {s : Set X}
    (hs : MeasurableSet s) : LocallyIntegrable (s.indicator f) μ

Proof state:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
hf : LocallyIntegrable f μ
s : Set X
hs : MeasurableSet s
x : X
⊢ IntegrableAtFilter (s.indicator f) (𝓝 x) μ

Tactic:
rcases hf x with ⟨U, hU, h'U⟩

Result:
case intro.intro
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
hf : LocallyIntegrable f μ
s : Set X
hs : MeasurableSet s
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : IntegrableOn f U μ
⊢ IntegrableAtFilter (s.indicator f) (𝓝 x) μ

Proof state:
case intro.intro
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
hf : LocallyIntegrable f μ
s : Set X
hs : MeasurableSet s
x : X
U : Set X
hU : U ∈ 𝓝 x
h'U : IntegrableOn f U μ
⊢ IntegrableAtFilter (s.indicator f) (𝓝 x) μ

Tactic:
exact ⟨U, hU, h'U.indicator hs⟩

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
hf : LocallyIntegrable f μ
s : Set X
hs : MeasurableSet s
⊢ LocallyIntegrable (s.indicator f) μ

Tactic:
intro x

Result:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : NormedAddCommGroup E
f : X → E
μ : Measure X
hf : LocallyIntegrable f μ
s : Set X
hs : MeasurableSet s
x : X
⊢ IntegrableAtFilter (s.indicator f) (𝓝 x) μ
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem monic_of_natDegree_le_of_coeff_eq_one (n : ℕ) (pn : p.natDegree ≤ n) (p1 : p.coeff n = 1) :
    Monic p

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
pn : p.natDegree ≤ n
p1 : p.coeff n = 1
⊢ p.leadingCoeff = 1

Tactic:
nontriviality

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
pn : p.natDegree ≤ n
p1 : p.coeff n = 1
a✝ : Nontrivial R
⊢ p.leadingCoeff = 1

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
pn : p.natDegree ≤ n
p1 : p.coeff n = 1
a✝ : Nontrivial R
⊢ p.leadingCoeff = 1

Tactic:
refine (congr_arg _ <| natDegree_eq_of_le_of_coeff_ne_zero pn ?_).trans p1

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
pn : p.natDegree ≤ n
p1 : p.coeff n = 1
a✝ : Nontrivial R
⊢ p.coeff n ≠ 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
pn : p.natDegree ≤ n
p1 : p.coeff n = 1
a✝ : Nontrivial R
⊢ p.coeff n ≠ 0

Tactic:
exact ne_of_eq_of_ne p1 one_ne_zero

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
pn : p.natDegree ≤ n
p1 : p.coeff n = 1
⊢ p.Monic

Tactic:
unfold Monic

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
pn : p.natDegree ≤ n
p1 : p.coeff n = 1
⊢ p.leadingCoeff = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem eq_or_ne_mem_of_mem {a b : α} {l : Vector α n} (h' : a ∈ l.push b) :
    a = b ∨ (a ≠ b ∧ a ∈ l)

Proof state:
α : Type u_1
n : Nat
a b : α
l : Vector α n
h' : a ∈ l.push b
h : a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
exact .inl h

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a b : α
l : Vector α n
h : ¬a = b
h' : a ∈ l
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
exact .inr ⟨h, h'⟩

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a b : α
l : Vector α n
h' : a ∈ l.push b
h : ¬a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
simp only [mem_push, h, or_false] at h'

Result:
α : Type u_1
n : Nat
a b : α
l : Vector α n
h : ¬a = b
h' : a ∈ l
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Proof state:
α : Type u_1
n : Nat
a b : α
l : Vector α n
h' : a ∈ l.push b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
if h : a = b then
  exact .inl h
else
  simp only [mem_push, h, or_false] at h'
  exact .inr ⟨h, h'⟩

Result:
no goals