harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/TypesFiltered.lean
theorem eqvGen_quot_rel_of_rel (x y : Σ j, F.obj j) :
    FilteredColimit.Rel.{v, u} F x y → Relation.EqvGen (Quot.Rel F) x y := fun ⟨k, f, g, h⟩ => by
  refine Relation.EqvGen.trans _ ⟨k, F.map f x.2⟩ _ ?_ ?_
  · exact (Relation.EqvGen.rel _ _ ⟨f, rfl⟩)
  · exact (Relation.EqvGen.symm _ _ (Relation.EqvGen.rel _ _ ⟨g, h⟩))

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
⊢ Relation.EqvGen (Quot.Rel F) x y

Tactic:
refine Relation.EqvGen.trans _ ⟨k, F.map f x.2⟩ _ ?_ ?_

Result:
case refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
⊢ Relation.EqvGen (Quot.Rel F) x ⟨k, F.map f x.snd⟩

case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
⊢ Relation.EqvGen (Quot.Rel F) ⟨k, F.map f x.snd⟩ y

Proof state:
case refine_1
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
⊢ Relation.EqvGen (Quot.Rel F) x ⟨k, F.map f x.snd⟩

Tactic:
exact (Relation.EqvGen.rel _ _ ⟨f, rfl⟩)

Result:
no goals

Proof state:
case refine_2
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
x y : (j : J) × F.obj j
x✝ : FilteredColimit.Rel F x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
h : F.map f x.snd = F.map g y.snd
⊢ Relation.EqvGen (Quot.Rel F) ⟨k, F.map f x.snd⟩ y

Tactic:
exact (Relation.EqvGen.symm _ _ (Relation.EqvGen.rel _ _ ⟨g, h⟩))

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem sup_eq_iSup (x y : α) : x ⊔ y = ⨆ b : Bool, cond b x y

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
x y : α
⊢ x ⊔ y = ⨆ b, bif b then x else y

Tactic:
rw [iSup_bool_eq, Bool.cond_true, Bool.cond_false]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem mul_eval_of_const_left (l₁ l₂ : LinearCombo) (v : Coeffs) (w : l₁.coeffs.isZero) :
    (mul l₁ l₂).eval v = l₁.eval v * l₂.eval v

Proof state:
l₁ l₂ : LinearCombo
v : Coeffs
w : l₁.coeffs.isZero
this : l₁.coeffs.dot v = 0
⊢ (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v

Tactic:
simp [mul, eval, this, Coeffs.sub_eq_add_neg, Coeffs.dot_distrib_left, Int.add_mul, Int.mul_add,
  Int.mul_comm]

Result:
no goals

Proof state:
l₁ l₂ : LinearCombo
v : Coeffs
w : l₁.coeffs.isZero
⊢ (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v

Tactic:
have : Coeffs.dot l₁.coeffs v = 0 := IntList.dot_of_left_zero w

Result:
l₁ l₂ : LinearCombo
v : Coeffs
w : l₁.coeffs.isZero
this : l₁.coeffs.dot v = 0
⊢ (l₁.mul l₂).eval v = l₁.eval v * l₂.eval v
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem ratUnits_insertRupUnits {n : Nat} (f : DefaultFormula n)
    (units : CNF.Clause (PosFin n)) :
    (f.insertRupUnits units).1.ratUnits = f.ratUnits

Proof state:
n : Nat
f : DefaultFormula n
units : CNF.Clause (PosFin n)
⊢ (f.insertRupUnits units).fst.ratUnits = f.ratUnits

Tactic:
rw [insertRupUnits]

Result:
no goals
-- Mathlib/Topology/StoneCech.lean
lemma preStoneCechCompat {F G : Ultrafilter α} {x : α} (hF : ↑F ≤ 𝓝 x) (hG : ↑G ≤ 𝓝 x) :
    Ultrafilter.extend g F = Ultrafilter.extend g G

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
F G : Ultrafilter α
x : α
hF : map g ↑F ≤ 𝓝 (g x)
hG : map g ↑G ≤ 𝓝 (g x)
⊢ Ultrafilter.extend g G = g x

Tactic:
rwa [ultrafilter_extend_eq_iff, G.coe_map]

Result:
no goals

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
F G : Ultrafilter α
x : α
hG : ↑G ≤ 𝓝 x
hF : map g ↑F ≤ 𝓝 (g x)
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G

Tactic:
replace hG := (map_mono hG).trans hg.continuousAt

Result:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
F G : Ultrafilter α
x : α
hF : map g ↑F ≤ 𝓝 (g x)
hG : map g ↑G ≤ 𝓝 (g x)
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
F G : Ultrafilter α
x : α
hF : map g ↑F ≤ 𝓝 (g x)
hG : map g ↑G ≤ 𝓝 (g x)
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G

Tactic:
rwa [show Ultrafilter.extend g G = g x by rwa [ultrafilter_extend_eq_iff, G.coe_map],
     ultrafilter_extend_eq_iff, F.coe_map]

Result:
no goals

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
F G : Ultrafilter α
x : α
hF : ↑F ≤ 𝓝 x
hG : ↑G ≤ 𝓝 x
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G

Tactic:
replace hF := (map_mono hF).trans hg.continuousAt

Result:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous g
F G : Ultrafilter α
x : α
hG : ↑G ≤ 𝓝 x
hF : map g ↑F ≤ 𝓝 (g x)
⊢ Ultrafilter.extend g F = Ultrafilter.extend g G
-- Mathlib/Data/List/Chain.lean
theorem Chain'.sublist [IsTrans α R] (hl : l₂.Chain' R) (h : l₁ <+ l₂) : l₁.Chain' R

Proof state:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
inst✝ : IsTrans α R
hl : Chain' R l₂
h : l₁ <+ l₂
⊢ Chain' R l₁

Tactic:
rw [chain'_iff_pairwise] at hl ⊢

Result:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
inst✝ : IsTrans α R
hl : Pairwise R l₂
h : l₁ <+ l₂
⊢ Pairwise R l₁

Proof state:
α : Type u
R : α → α → Prop
l₁ l₂ : List α
inst✝ : IsTrans α R
hl : Pairwise R l₂
h : l₁ <+ l₂
⊢ Pairwise R l₁

Tactic:
exact hl.sublist h

Result:
no goals
-- Mathlib/Data/List/Forall2.lean
theorem forall₂_map_right_iff {f : γ → β} :
    ∀ {l u}, Forall₂ R l (map f u) ↔ Forall₂ (fun a c => R a (f c)) l u
  | _, [] => by simp only [map, forall₂_nil_right_iff]
  | _, b :: u => by simp only [map, forall₂_cons_right_iff, forall₂_map_right_iff]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
x✝ : List α
⊢ Forall₂ R x✝ (map f []) ↔ Forall₂ (fun a c => R a (f c)) x✝ []

Tactic:
simp only [map, forall₂_nil_right_iff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
x✝ : List α
b : γ
u : List γ
⊢ Forall₂ R x✝ (map f (b :: u)) ↔ Forall₂ (fun a c => R a (f c)) x✝ (b :: u)

Tactic:
simp only [map, forall₂_cons_right_iff, forall₂_map_right_iff]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma IsCondKernelCDF.toKernel_Iic {hf : IsCondKernelCDF f κ ν} (p : α × β) (x : ℝ) :
    hf.toKernel f p (Iic x) = ENNReal.ofReal (f p x)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
x✝ : MeasurableSpace β
f : α × β → StieltjesFunction
κ : Kernel α (β × ℝ)
ν : Kernel α β
hf : IsCondKernelCDF f κ ν
p : α × β
x : ℝ
⊢ ENNReal.ofReal (↑(f p) x - 0) = ENNReal.ofReal (↑(f p) x)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
x✝ : MeasurableSpace β
f : α × β → StieltjesFunction
κ : Kernel α (β × ℝ)
ν : Kernel α β
hf : IsCondKernelCDF f κ ν
p : α × β
x : ℝ
⊢ ((toKernel f hf) p) (Iic x) = ENNReal.ofReal (↑(f p) x)

Tactic:
rw [IsCondKernelCDF.toKernel_apply p, (f p).measure_Iic (hf.tendsto_atBot_zero p)]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
x✝ : MeasurableSpace β
f : α × β → StieltjesFunction
κ : Kernel α (β × ℝ)
ν : Kernel α β
hf : IsCondKernelCDF f κ ν
p : α × β
x : ℝ
⊢ ENNReal.ofReal (↑(f p) x - 0) = ENNReal.ofReal (↑(f p) x)
-- Mathlib/Analysis/Analytic/Constructions.lean
theorem HasFPowerSeriesOnBall.neg (hf : HasFPowerSeriesOnBall f pf x r) :
    HasFPowerSeriesOnBall (-f) (-pf) x r :=
  { r_le

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf x r
⊢ r ≤ (-pf).radius

Tactic:
rw [pf.radius_neg]

Result:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf x r
⊢ r ≤ pf.radius

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f pf x r
⊢ r ≤ pf.radius

Tactic:
exact hf.r_le

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean
theorem IsIntegrallyClosed.degree_le_of_ne_zero {s : S} (hs : IsIntegral R s) {p : R[X]}
    (hp0 : p ≠ 0) (hp : Polynomial.aeval s p = 0) : degree (minpoly R s) ≤ degree p

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
p : R[X]
hp0 : p ≠ 0
hp : (Polynomial.aeval s) p = 0
⊢ ↑(minpoly R s).natDegree ≤ ↑p.natDegree

Tactic:
norm_cast

Result:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
p : R[X]
hp0 : p ≠ 0
hp : (Polynomial.aeval s) p = 0
⊢ (minpoly R s).natDegree ≤ p.natDegree

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
p : R[X]
hp0 : p ≠ 0
hp : (Polynomial.aeval s) p = 0
⊢ (minpoly R s).degree ≤ p.degree

Tactic:
rw [degree_eq_natDegree (minpoly.ne_zero hs), degree_eq_natDegree hp0]

Result:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
p : R[X]
hp0 : p ≠ 0
hp : (Polynomial.aeval s) p = 0
⊢ ↑(minpoly R s).natDegree ≤ ↑p.natDegree

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
s : S
hs : IsIntegral R s
p : R[X]
hp0 : p ≠ 0
hp : (Polynomial.aeval s) p = 0
⊢ (minpoly R s).natDegree ≤ p.natDegree

Tactic:
exact natDegree_le_of_dvd ((isIntegrallyClosed_dvd_iff hs _).mp hp) hp0

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_apply_of_not_and_and {f : R → R} (a : A)
    (ha : ¬ (p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)) :
    cfcₙ f a = 0

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : Nontrivial R
inst✝⁹ : StarRing R
inst✝⁸ : MetricSpace R
inst✝⁷ : IsTopologicalSemiring R
inst✝⁶ : ContinuousStar R
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
ha : ¬(p a ∧ ContinuousOn f (σₙ R a) ∧ f 0 = 0)
⊢ cfcₙ f a = 0

Tactic:
rw [cfcₙ_def, dif_neg ha]

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Algebra.lean
theorem Ideal.mk_eq_mk {m n : ℕ} (hmn : m ≤ n) (r : AdicCauchySequence I R) :
    Ideal.Quotient.mk (I ^ m) (r.val n) = Ideal.Quotient.mk (I ^ m) (r.val m)

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
h : I ^ m = I ^ m • ⊤
⊢ Submodule.Quotient.mk (↑r n) = Submodule.Quotient.mk (↑r m)

Tactic:
exact (r.property hmn).symm

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
⊢ (Ideal.Quotient.mk (I ^ m)) (↑r n) = (Ideal.Quotient.mk (I ^ m)) (↑r m)

Tactic:
have h : I ^ m = I ^ m • ⊤ := by simp

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
h : I ^ m = I ^ m • ⊤
⊢ (Ideal.Quotient.mk (I ^ m)) (↑r n) = (Ideal.Quotient.mk (I ^ m)) (↑r m)

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
h : I ^ m = I ^ m • ⊤
⊢ (Ideal.Quotient.mk (I ^ m)) (↑r n) = (Ideal.Quotient.mk (I ^ m)) (↑r m)

Tactic:
rw [← Ideal.Quotient.mk_eq_mk, ← Ideal.Quotient.mk_eq_mk, h]

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
h : I ^ m = I ^ m • ⊤
⊢ Submodule.Quotient.mk (↑r n) = Submodule.Quotient.mk (↑r m)

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
⊢ I ^ m = I ^ m • ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Canonical.lean
protected lemma mul_lt_mul_of_lt_of_lt
    [PosMulStrictMono α] {a b c d : α} (hab : a < b) (hcd : c < d) :
    a * c < b * d

Proof state:
case inr
α : Type u
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a b c d : α
hab : a < b
hcd : c < d
this : MulPosStrictMono α
hc : 0 < c
⊢ a * c < b * d

Tactic:
exact mul_lt_mul_of_pos' hab hcd hc ((zero_le _).trans_lt hab)

Result:
no goals

Proof state:
case inl
α : Type u
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a b d : α
hab : a < b
this : MulPosStrictMono α
hcd : 0 < d
⊢ 0 < b * d

Tactic:
exact mul_pos ((zero_le _).trans_lt hab) hcd

Result:
no goals

Proof state:
case inl
α : Type u
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a b d : α
hab : a < b
this : MulPosStrictMono α
hcd : 0 < d
⊢ a * 0 < b * d

Tactic:
rw [mul_zero]

Result:
case inl
α : Type u
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a b d : α
hab : a < b
this : MulPosStrictMono α
hcd : 0 < d
⊢ 0 < b * d

Proof state:
α : Type u
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a b c d : α
hab : a < b
hcd : c < d
⊢ a * c < b * d

Tactic:
have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›

Result:
α : Type u
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a b c d : α
hab : a < b
hcd : c < d
this : MulPosStrictMono α
⊢ a * c < b * d

Proof state:
α : Type u
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a b c d : α
hab : a < b
hcd : c < d
this : MulPosStrictMono α
⊢ a * c < b * d

Tactic:
obtain rfl | hc := eq_zero_or_pos c

Result:
case inl
α : Type u
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a b d : α
hab : a < b
this : MulPosStrictMono α
hcd : 0 < d
⊢ a * 0 < b * d

case inr
α : Type u
inst✝³ : CommSemiring α
inst✝² : PartialOrder α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
a b c d : α
hab : a < b
hcd : c < d
this : MulPosStrictMono α
hc : 0 < c
⊢ a * c < b * d
-- Mathlib/Algebra/Homology/Single.lean
@[ext]
lemma from_single_hom_ext {K : HomologicalComplex V c} {j : ι} {A : V}
    {f g : (single V c j).obj A ⟶ K} (hfg : f.f j = g.f j) : f = g

Proof state:
case h
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : (single V c j).obj A ⟶ K
hfg : f.f j = g.f j
i : ι
⊢ f.f i = g.f i

Tactic:
by_cases h : i = j

Result:
case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : (single V c j).obj A ⟶ K
hfg : f.f j = g.f j
i : ι
h : i = j
⊢ f.f i = g.f i

case neg
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : (single V c j).obj A ⟶ K
hfg : f.f j = g.f j
i : ι
h : ¬i = j
⊢ f.f i = g.f i

Proof state:
case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
A : V
i : ι
f g : (single V c i).obj A ⟶ K
hfg : f.f i = g.f i
⊢ f.f i = g.f i

Tactic:
exact hfg

Result:
no goals

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : (single V c j).obj A ⟶ K
hfg : f.f j = g.f j
⊢ f = g

Tactic:
ext i

Result:
case h
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : (single V c j).obj A ⟶ K
hfg : f.f j = g.f j
i : ι
⊢ f.f i = g.f i

Proof state:
case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : (single V c j).obj A ⟶ K
hfg : f.f j = g.f j
i : ι
h : i = j
⊢ f.f i = g.f i

Tactic:
subst h

Result:
case pos
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
A : V
i : ι
f g : (single V c i).obj A ⟶ K
hfg : f.f i = g.f i
⊢ f.f i = g.f i

Proof state:
case neg
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex V c
j : ι
A : V
f g : (single V c j).obj A ⟶ K
hfg : f.f j = g.f j
i : ι
h : ¬i = j
⊢ f.f i = g.f i

Tactic:
apply (isZero_single_obj_X c j A i h).eq_of_src

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem tail_reverse (l : List α) : l.reverse.tail = l.dropLast.reverse

Proof state:
case h
α : Type u_1
l : List α
i : Nat
h₁ : i < l.reverse.tail.length
h₂ : i < l.dropLast.reverse.length
⊢ l.reverse.tail[i] = l.dropLast.reverse[i]

Tactic:
simp [Nat.add_comm i, Nat.sub_add_eq]

Result:
no goals

Proof state:
case h
α : Type u_1
l : List α
⊢ ∀ (i : Nat) (h₁ : i < l.reverse.tail.length) (h₂ : i < l.dropLast.reverse.length),
    l.reverse.tail[i] = l.dropLast.reverse[i]

Tactic:
intro i h₁ h₂

Result:
case h
α : Type u_1
l : List α
i : Nat
h₁ : i < l.reverse.tail.length
h₂ : i < l.dropLast.reverse.length
⊢ l.reverse.tail[i] = l.dropLast.reverse[i]

Proof state:
case hl
α : Type u_1
l : List α
⊢ l.reverse.tail.length = l.dropLast.reverse.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ l.reverse.tail = l.dropLast.reverse

Tactic:
apply ext_getElem

Result:
case hl
α : Type u_1
l : List α
⊢ l.reverse.tail.length = l.dropLast.reverse.length

case h
α : Type u_1
l : List α
⊢ ∀ (i : Nat) (h₁ : i < l.reverse.tail.length) (h₂ : i < l.dropLast.reverse.length),
    l.reverse.tail[i] = l.dropLast.reverse[i]
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem tendsto_measure_Ioc_atBot [Preorder α] [NoMinOrder α]
    [(atBot : Filter α).IsCountablyGenerated] (μ : Measure α) (a : α) :
    Tendsto (fun x => μ (Ioc x a)) atBot (𝓝 (μ (Iic a)))

Proof state:
α : Type u_1
m0 : MeasurableSpace α
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : atBot.IsCountablyGenerated
μ : Measure α
a : α
⊢ Tendsto (fun x => μ (Ioc x a)) atBot (𝓝 (μ (⋃ a_1, Ioc a_1 a)))

Tactic:
exact tendsto_measure_iUnion_atBot (monotone_id.Ioc antitone_const)

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : atBot.IsCountablyGenerated
μ : Measure α
a : α
⊢ Tendsto (fun x => μ (Ioc x a)) atBot (𝓝 (μ (Iic a)))

Tactic:
rw [← iUnion_Ioc_left]

Result:
α : Type u_1
m0 : MeasurableSpace α
inst✝² : Preorder α
inst✝¹ : NoMinOrder α
inst✝ : atBot.IsCountablyGenerated
μ : Measure α
a : α
⊢ Tendsto (fun x => μ (Ioc x a)) atBot (𝓝 (μ (⋃ a_1, Ioc a_1 a)))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseP_of_forall_mem_not {l : Array α} (h : ∀ a, a ∈ l → ¬p a) : l.eraseP p = l

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

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
h : ∀ (a : α), a ∈ { toList := toList✝ } → ¬p a = true
⊢ { toList := toList✝ }.eraseP p = { toList := toList✝ }

Proof state:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
h : ∀ (a : α), a ∈ { toList := toList✝ } → ¬p a = true
⊢ { toList := toList✝ }.eraseP p = { toList := toList✝ }

Tactic:
simp_all [List.eraseP_of_forall_not]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem prime_of_coprime (n : ℕ) (h1 : 1 < n) (h : ∀ m < n, m ≠ 0 → n.Coprime m) : Prime n

Proof state:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
m : ℕ
mlt : m < n
mdvd : m ∣ n
⊢ m = 1

Tactic:
have hm : m ≠ 0 := by
  rintro rfl
  rw [zero_dvd_iff] at mdvd
  exact mlt.ne' mdvd

Result:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
m : ℕ
mlt : m < n
mdvd : m ∣ n
hm : m ≠ 0
⊢ m = 1

Proof state:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
m : ℕ
mlt : m < n
mdvd : m ∣ n
hm : m ≠ 0
⊢ m = 1

Tactic:
exact (h m mlt hm).symm.eq_one_of_dvd mdvd

Result:
no goals

Proof state:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
mlt : 0 < n
mdvd : 0 ∣ n
⊢ False

Tactic:
rw [zero_dvd_iff] at mdvd

Result:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
mlt : 0 < n
mdvd : n = 0
⊢ False

Proof state:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
m : ℕ
mlt : m < n
mdvd : m ∣ n
⊢ m ≠ 0

Tactic:
rintro rfl

Result:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
mlt : 0 < n
mdvd : 0 ∣ n
⊢ False

Proof state:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
mlt : 0 < n
mdvd : n = 0
⊢ False

Tactic:
exact mlt.ne' mdvd

Result:
no goals

Proof state:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
⊢ Prime n

Tactic:
refine prime_def_lt.mpr ⟨h1, fun m mlt mdvd => ?_⟩

Result:
n : ℕ
h1 : 1 < n
h : ∀ (m : ℕ), m < n → m ≠ 0 → n.Coprime m
m : ℕ
mlt : m < n
mdvd : m ∣ n
⊢ m = 1