harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Testing/Plausible/Functions.lean
theorem List.applyId_cons [DecidableEq α] (xs : List (α × α)) (x y z : α) :
    List.applyId ((y, z)::xs) x = if y = x then z else List.applyId xs x

Proof state:
α : Type u
inst✝ : DecidableEq α
xs : List (α × α)
x y z : α
⊢ (if h : y = x then some z else dlookup x (map Prod.toSigma xs)).getD x =
    if y = x then z else (dlookup x (map Prod.toSigma xs)).getD x

Tactic:
split_ifs <;> rfl

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
xs : List (α × α)
x y z : α
⊢ applyId ((y, z) :: xs) x = if y = x then z else applyId xs x

Tactic:
simp only [List.applyId, List.dlookup, eq_rec_constant, Prod.toSigma, List.map]

Result:
α : Type u
inst✝ : DecidableEq α
xs : List (α × α)
x y z : α
⊢ (if h : y = x then some z else dlookup x (map Prod.toSigma xs)).getD x =
    if y = x then z else (dlookup x (map Prod.toSigma xs)).getD x
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem minpoly_eq [IsDomain R] [IsDomain S] [NoZeroSMulDivisors R S] [IsIntegrallyClosed R]
    (h : IsAdjoinRootMonic S f) (hirr : Irreducible f) : minpoly R h.root = f :=
  let ⟨q, hq⟩ := minpoly.isIntegrallyClosed_dvd h.isIntegral_root h.aeval_root
  symm <|
    eq_of_monic_of_associated h.Monic (minpoly.monic h.isIntegral_root) <| by
      convert
        Associated.mul_left (minpoly R h.root) <|
          associated_one_iff_isUnit.2 <|
            (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root
      rw [mul_one]

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
h : IsAdjoinRootMonic S f
hirr : Irreducible f
q : R[X]
hq : f = minpoly R h.root * q
⊢ Associated f (minpoly R h.root)

Tactic:
convert
  Associated.mul_left (minpoly R h.root) <|
    associated_one_iff_isUnit.2 <|
      (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root

Result:
case h.e'_4
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
h : IsAdjoinRootMonic S f
hirr : Irreducible f
q : R[X]
hq : f = minpoly R h.root * q
⊢ minpoly R h.root = minpoly R h.root * 1

Proof state:
case h.e'_4
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
inst✝³ : IsDomain R
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
h : IsAdjoinRootMonic S f
hirr : Irreducible f
q : R[X]
hq : f = minpoly R h.root * q
⊢ minpoly R h.root = minpoly R h.root * 1

Tactic:
rw [mul_one]

Result:
no goals
-- Mathlib/MeasureTheory/Function/EssSup.lean
theorem meas_essSup_lt
    (hf : IsBoundedUnder (· ≤ ·) (ae μ) f

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) f) _auto✝
⊢ μ {y | ¬f y ≤ essSup f μ} = 0

Tactic:
exact ae_le_essSup hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) f) _auto✝
⊢ μ {y | essSup f μ < f y} = 0

Tactic:
simp_rw [← not_le]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝³ : ConditionallyCompleteLinearOrder β
f : α → β
inst✝² : TopologicalSpace β
inst✝¹ : FirstCountableTopology β
inst✝ : OrderTopology β
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) f) _auto✝
⊢ μ {y | ¬f y ≤ essSup f μ} = 0
-- Mathlib/FieldTheory/RatFunc/AsPolynomial.lean
theorem valuation_X_eq_neg_one :
    (idealX K).valuation (RatFunc K) RatFunc.X = Multiplicative.ofAdd (-1 : ℤ)

Proof state:
K : Type u_1
inst✝ : Field K
⊢ (valuation (RatFunc K) (idealX K)) RatFunc.X = ↑(Multiplicative.ofAdd (-1))

Tactic:
rw [← RatFunc.algebraMap_X, valuation_of_algebraMap, intValuation_singleton]

Result:
case hr
K : Type u_1
inst✝ : Field K
⊢ X ≠ 0

case hv
K : Type u_1
inst✝ : Field K
⊢ (idealX K).asIdeal = Ideal.span {X}

Proof state:
case hv
K : Type u_1
inst✝ : Field K
⊢ (idealX K).asIdeal = Ideal.span {X}

Tactic:
exact idealX_span K

Result:
no goals

Proof state:
case hr
K : Type u_1
inst✝ : Field K
⊢ X ≠ 0

Tactic:
exact Polynomial.X_ne_zero

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
theorem corootSpan_dualAnnihilator_le_ker_rootForm :
    P.corootSpan.dualAnnihilator.map P.toDualLeft.symm ≤ LinearMap.ker P.RootForm

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
x : M
hx : x ∈ {x | ∀ (i : ι), (P.coroot' i) x = 0}
⊢ x ∈ ↑(LinearMap.ker P.RootForm)

Tactic:
simp only [coroot', PerfectPairing.flip_apply_apply, mem_setOf_eq] at hx

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
x : M
hx : ∀ (i : ι), (P.toPerfectPairing x) (P.coroot i) = 0
⊢ x ∈ ↑(LinearMap.ker P.RootForm)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
⊢ Submodule.map P.toDualLeft.symm P.corootSpan.dualAnnihilator ≤ LinearMap.ker P.RootForm

Tactic:
rw [← SetLike.coe_subset_coe, coe_corootSpan_dualAnnihilator_map]

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
⊢ {x | ∀ (i : ι), (P.coroot' i) x = 0} ⊆ ↑(LinearMap.ker P.RootForm)

Proof state:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
x : M
hx : ∀ (i : ι), (P.toPerfectPairing x) (P.coroot i) = 0
y : M
⊢ (P.RootForm x) y = 0 y

Tactic:
simp [rootForm_apply_apply, hx]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
⊢ {x | ∀ (i : ι), (P.coroot' i) x = 0} ⊆ ↑(LinearMap.ker P.RootForm)

Tactic:
intro x hx

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
x : M
hx : x ∈ {x | ∀ (i : ι), (P.coroot' i) x = 0}
⊢ x ∈ ↑(LinearMap.ker P.RootForm)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
x : M
hx : ∀ (i : ι), (P.toPerfectPairing x) (P.coroot i) = 0
⊢ x ∈ ↑(LinearMap.ker P.RootForm)

Tactic:
ext y

Result:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
x : M
hx : ∀ (i : ι), (P.toPerfectPairing x) (P.coroot i) = 0
y : M
⊢ (P.RootForm x) y = 0 y
-- Mathlib/RingTheory/Ideal/AssociatedPrime.lean
theorem associatedPrimes.eq_empty_of_subsingleton [Subsingleton M] : associatedPrimes R M = ∅

Proof state:
case h
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
x✝ : Ideal R
⊢ x✝ ∈ associatedPrimes R M ↔ x✝ ∈ ∅

Tactic:
simp only [Set.mem_empty_iff_false, iff_false]

Result:
case h
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
x✝ : Ideal R
⊢ x✝ ∉ associatedPrimes R M

Proof state:
case h
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
x✝ : Ideal R
⊢ x✝ ∉ associatedPrimes R M

Tactic:
apply not_isAssociatedPrime_of_subsingleton

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
⊢ associatedPrimes R M = ∅

Tactic:
ext

Result:
case h
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Subsingleton M
x✝ : Ideal R
⊢ x✝ ∈ associatedPrimes R M ↔ x✝ ∈ ∅
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem c₆_of_isCharThreeJNeZeroNF_of_char_three : W.c₆ = -W.a₂ ^ 3

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ -64 * W.a₂ ^ 3 - 864 * W.a₆ = -W.a₂ ^ 3

Tactic:
linear_combination (-21 * W.a₂ ^ 3 - 288 * W.a₆) * CharP.cast_eq_zero R 3

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ W.c₆ = -W.a₂ ^ 3

Tactic:
rw [c₆_of_isCharThreeJNeZeroNF]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsCharThreeJNeZeroNF
inst✝ : CharP R 3
⊢ -64 * W.a₂ ^ 3 - 864 * W.a₆ = -W.a₂ ^ 3
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem IsOrtho.zero_left (x : M) : IsOrtho Q (0 : M) x

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
Q : QuadraticMap R M N
x : M
⊢ Q.IsOrtho 0 x

Tactic:
simp [isOrtho_def]

Result:
no goals
-- Mathlib/CategoryTheory/Simple.lean
theorem indecomposable_of_simple (X : C) [Simple X] : Indecomposable X :=
  ⟨Simple.not_isZero X, fun Y Z i => by
    refine or_iff_not_imp_left.mpr fun h => ?_
    rw [IsZero.iff_isSplitMono_eq_zero (biprod.inl : Y ⟶ Y ⊞ Z)] at h
    change biprod.inl ≠ 0 at h
    have : Simple (Y ⊞ Z) := Simple.of_iso i.symm -- Porting note: this instance is needed
    rw [← Simple.mono_isIso_iff_nonzero biprod.inl] at h
    rwa [Biprod.isIso_inl_iff_isZero] at h⟩

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : ¬IsZero Y
⊢ IsZero Z

Tactic:
rw [IsZero.iff_isSplitMono_eq_zero (biprod.inl : Y ⟶ Y ⊞ Z)] at h

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : ¬biprod.inl = 0
⊢ IsZero Z

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
⊢ IsZero Y ∨ IsZero Z

Tactic:
refine or_iff_not_imp_left.mpr fun h => ?_

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : ¬IsZero Y
⊢ IsZero Z

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : ¬biprod.inl = 0
⊢ IsZero Z

Tactic:
change biprod.inl ≠ 0 at h

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : biprod.inl ≠ 0
⊢ IsZero Z

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : biprod.inl ≠ 0
⊢ IsZero Z

Tactic:
have : Simple (Y ⊞ Z) := Simple.of_iso i.symm

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : biprod.inl ≠ 0
this : Simple (Y ⊞ Z)
⊢ IsZero Z

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : IsIso biprod.inl
this : Simple (Y ⊞ Z)
⊢ IsZero Z

Tactic:
rwa [Biprod.isIso_inl_iff_isZero] at h

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : biprod.inl ≠ 0
this : Simple (Y ⊞ Z)
⊢ IsZero Z

Tactic:
rw [← Simple.mono_isIso_iff_nonzero biprod.inl] at h

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : IsIso biprod.inl
this : Simple (Y ⊞ Z)
⊢ IsZero Z
-- Mathlib/Order/SupClosed.lean
lemma SupClosed.image [FunLike F α β] [SupHomClass F α β] (hs : SupClosed s) (f : F) :
    SupClosed (f '' s)

Proof state:
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
hs : SupClosed s
f : F
⊢ SupClosed (⇑f '' s)

Tactic:
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩

Result:
case intro.intro.intro.intro
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
hs : SupClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ f a ⊔ f b ∈ ⇑f '' s

Proof state:
case intro.intro.intro.intro
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
hs : SupClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ f a ⊔ f b ∈ ⇑f '' s

Tactic:
rw [← map_sup]

Result:
case intro.intro.intro.intro
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
hs : SupClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ f (a ⊔ b) ∈ ⇑f '' s

Proof state:
case intro.intro.intro.intro
F : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : SupHomClass F α β
hs : SupClosed s
f : F
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ f (a ⊔ b) ∈ ⇑f '' s

Tactic:
exact Set.mem_image_of_mem _ <| hs ha hb

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem reindex_tprod (e : ι ≃ ι₂) (f : Π i, s i) :
    reindex R s e (tprod R f) = tprod R fun i ↦ f (e.symm i)

Proof state:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
e : ι ≃ ι₂
f : (i : ι) → s i
⊢ (lift { toFun := ⇑(tprod R) ∘ ⇑(Equiv.piCongrLeft' s e), map_update_add' := ⋯, map_update_smul' := ⋯ })
      ((tprod R) f) =
    (tprod R) fun i => f (e.symm i)

Tactic:
exact liftAux_tprod _ f

Result:
no goals

Proof state:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
e : ι ≃ ι₂
f : (i : ι) → s i
⊢ (reindex R s e) ((tprod R) f) = (tprod R) fun i => f (e.symm i)

Tactic:
dsimp [reindex]

Result:
ι : Type u_1
ι₂ : Type u_2
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
e : ι ≃ ι₂
f : (i : ι) → s i
⊢ (lift { toFun := ⇑(tprod R) ∘ ⇑(Equiv.piCongrLeft' s e), map_update_add' := ⋯, map_update_smul' := ⋯ })
      ((tprod R) f) =
    (tprod R) fun i => f (e.symm i)
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem of_epi_eq_zero {X Y : C} (f : X ⟶ Y) [Epi f] (h : f = 0) : IsZero Y

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Epi 0
⊢ IsZero Y

Tactic:
apply of_epi_zero X Y

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : f = 0
⊢ IsZero Y

Tactic:
subst h

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Epi 0
⊢ IsZero Y
-- Mathlib/Computability/Tape.lean
theorem ListBlank.nth_zero {Γ} [Inhabited Γ] (l : ListBlank Γ) : l.nth 0 = l.head

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
l : ListBlank Γ
⊢ l.nth 0 = l.head

Tactic:
conv => lhs; rw [← ListBlank.cons_head_tail l]

Result:
Γ : Type u_1
inst✝ : Inhabited Γ
l : ListBlank Γ
⊢ (cons l.head l.tail).nth 0 = l.head

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
l : ListBlank Γ
⊢ (cons l.head l.tail).nth 0 = l.head

Tactic:
exact Quotient.inductionOn' l.tail fun l ↦ rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem dvd_of_mul_dvd_mul_left
    (kpos : 0 < k) (H : k * m ∣ k * n) : m ∣ n

Proof state:
k m n : Nat
kpos : 0 < k
H✝ : k * m ∣ k * n
l : Nat
H : k * n = k * (m * l)
⊢ m ∣ n

Tactic:
exact ⟨_, Nat.eq_of_mul_eq_mul_left kpos H⟩

Result:
no goals

Proof state:
k m n : Nat
kpos : 0 < k
H✝ : k * m ∣ k * n
l : Nat
H : k * n = k * m * l
⊢ m ∣ n

Tactic:
rw [Nat.mul_assoc] at H

Result:
k m n : Nat
kpos : 0 < k
H✝ : k * m ∣ k * n
l : Nat
H : k * n = k * (m * l)
⊢ m ∣ n

Proof state:
k m n : Nat
kpos : 0 < k
H : k * m ∣ k * n
⊢ m ∣ n

Tactic:
let ⟨l, H⟩ := H

Result:
k m n : Nat
kpos : 0 < k
H✝ : k * m ∣ k * n
l : Nat
H : k * n = k * m * l
⊢ m ∣ n
-- Mathlib/RingTheory/IsTensorProduct.lean
theorem TensorProduct.isTensorProduct : IsTensorProduct (TensorProduct.mk R M N)

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ IsTensorProduct (mk R M N)

Tactic:
delta IsTensorProduct

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ Function.Bijective ⇑(lift (mk R M N))

Proof state:
case h.e'_3.h.e'_5
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ lift (mk R M N) = LinearMap.id

Tactic:
apply TensorProduct.ext'

Result:
case h.e'_3.h.e'_5.H
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ ∀ (x : M) (y : N), (lift (mk R M N)) (x ⊗ₜ[R] y) = LinearMap.id (x ⊗ₜ[R] y)

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ Function.Bijective ⇑(lift (mk R M N))

Tactic:
convert_to Function.Bijective (LinearMap.id : M ⊗[R] N →ₗ[R] M ⊗[R] N) using 2

Result:
case h.e'_3.h.e'_5
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ lift (mk R M N) = LinearMap.id

R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ Function.Bijective ⇑LinearMap.id

Proof state:
case h.e'_3.h.e'_5.H
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ ∀ (x : M) (y : N), (lift (mk R M N)) (x ⊗ₜ[R] y) = LinearMap.id (x ⊗ₜ[R] y)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
⊢ Function.Bijective ⇑LinearMap.id

Tactic:
exact Function.bijective_id

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem getElem?_zipWith_eq_some {f : α → β → γ} {l₁ : Array α} {l₂ : Array β} {z : γ} {i : Nat} :
    (zipWith f l₁ l₂)[i]? = some z ↔
      ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
z : γ
i : Nat
toList✝¹ : List α
toList✝ : List β
⊢ (zipWith f { toList := toList✝¹ } { toList := toList✝ })[i]? = some z ↔
    ∃ x y, { toList := toList✝¹ }[i]? = some x ∧ { toList := toList✝ }[i]? = some y ∧ f x y = z

Tactic:
simp [List.getElem?_zipWith_eq_some]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₂ : Array β
z : γ
i : Nat
toList✝ : List α
⊢ (zipWith f { toList := toList✝ } l₂)[i]? = some z ↔
    ∃ x y, { toList := toList✝ }[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
z : γ
i : Nat
toList✝¹ : List α
toList✝ : List β
⊢ (zipWith f { toList := toList✝¹ } { toList := toList✝ })[i]? = some z ↔
    ∃ x y, { toList := toList✝¹ }[i]? = some x ∧ { toList := toList✝ }[i]? = some y ∧ f x y = z

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₁ : Array α
l₂ : Array β
z : γ
i : Nat
⊢ (zipWith f l₁ l₂)[i]? = some z ↔ ∃ x y, l₁[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z

Tactic:
cases l₁

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
l₂ : Array β
z : γ
i : Nat
toList✝ : List α
⊢ (zipWith f { toList := toList✝ } l₂)[i]? = some z ↔
    ∃ x y, { toList := toList✝ }[i]? = some x ∧ l₂[i]? = some y ∧ f x y = z
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem degree_mul_leadingCoeff_self_inv (p : K[X]) :
    degree (p * C (leadingCoeff p)⁻¹) = degree p

Proof state:
case neg
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp : ¬p = 0
⊢ (p * C p.leadingCoeff⁻¹).degree = p.degree

Tactic:
exact degree_mul_leadingCoeff_inv _ hp

Result:
no goals

Proof state:
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
⊢ (p * C p.leadingCoeff⁻¹).degree = p.degree

Tactic:
by_cases hp : p = 0

Result:
case pos
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp : p = 0
⊢ (p * C p.leadingCoeff⁻¹).degree = p.degree

case neg
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp : ¬p = 0
⊢ (p * C p.leadingCoeff⁻¹).degree = p.degree

Proof state:
case pos
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp : p = 0
⊢ (p * C p.leadingCoeff⁻¹).degree = p.degree

Tactic:
simp [hp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_of_forall_not {l : List α} (h : ∀ a, a ∈ l → ¬p a) : l.eraseP p = l

Proof state:
case nil
α : Type u_1
p : α → Bool
h : ∀ (a : α), a ∈ [] → ¬p a = true
⊢ eraseP p [] = []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
head✝ : α
tail✝ : List α
ih : (∀ (a : α), a ∈ tail✝ → ¬p a = true) → eraseP p tail✝ = tail✝
h : ∀ (a : α), a ∈ head✝ :: tail✝ → ¬p a = true
⊢ eraseP p (head✝ :: tail✝) = head✝ :: tail✝

Tactic:
simp [h _ (.head ..), ih (forall_mem_cons.1 h).2]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
h : ∀ (a : α), a ∈ l → ¬p a = true
⊢ eraseP p l = l

Tactic:
induction l with
| nil => rfl
| cons _ _ ih => simp [h _ (.head ..), ih (forall_mem_cons.1 h).2]

Result:
no goals