harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Logic/Function/Basic.lean
lemma factorsThrough_iff (g : α → γ) [Nonempty γ] : g.FactorsThrough f ↔ ∃ (e : β → γ), g = e ∘ f :=
  ⟨fun hf => ⟨extend f g (const β (Classical.arbitrary γ)),
      funext (fun x => by simp only [comp_apply, hf.extend_apply])⟩,
  fun h _ _ hf => by rw [Classical.choose_spec h, comp_apply, comp_apply, hf]⟩

Proof state:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst✝ : Nonempty γ
hf : FactorsThrough g f
x : α
⊢ g x = (extend f g (const β (Classical.arbitrary γ)) ∘ f) x

Tactic:
simp only [comp_apply, hf.extend_apply]

Result:
no goals

Proof state:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
g : α → γ
inst✝ : Nonempty γ
h : ∃ e, g = e ∘ f
x✝¹ x✝ : α
hf : f x✝¹ = f x✝
⊢ g x✝¹ = g x✝

Tactic:
rw [Classical.choose_spec h, comp_apply, comp_apply, hf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_alter_eq_self_of_not_mem (h : m.1.WF) {k : α} {f : Option β → Option β}
    (h₁ : m.contains k = false) (h₂ : (f (Const.get? m k)).isNone) :
    (Const.alter m k f).1.size = m.1.size

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k : α
f : Option β → Option β
h₁ : m.contains k = false
h₂ : (f (get? m k)).isNone = true
⊢ (alter m k f).val.size = m.val.size

Tactic:
simp [size_alter, h, h₁, h₂]

Result:
no goals
-- Mathlib/RingTheory/Derivation/ToSquareZero.lean
theorem liftOfDerivationToSquareZero_mk_apply [IsScalarTower R A B] (d : Derivation R A I) (x : A) :
    Ideal.Quotient.mk I (liftOfDerivationToSquareZero I hI d x) = algebraMap A (B ⧸ I) x

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
d : Derivation R A ↥I
x : A
⊢ (Ideal.Quotient.mk I) ((liftOfDerivationToSquareZero I hI d) x) = (algebraMap A (B ⧸ I)) x

Tactic:
rw [liftOfDerivationToSquareZero_apply, map_add, Ideal.Quotient.eq_zero_iff_mem.mpr (d x).prop,
  zero_add]

Result:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
d : Derivation R A ↥I
x : A
⊢ (Ideal.Quotient.mk I) ((algebraMap A B) x) = (algebraMap A (B ⧸ I)) x

Proof state:
R : Type u
A : Type v
B : Type w
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra R B
I : Ideal B
inst✝¹ : Algebra A B
hI : I ^ 2 = ⊥
inst✝ : IsScalarTower R A B
d : Derivation R A ↥I
x : A
⊢ (Ideal.Quotient.mk I) ((algebraMap A B) x) = (algebraMap A (B ⧸ I)) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Ab.lean
lemma abCyclesIso_inv_apply_iCycles (x : AddMonoidHom.ker S.g.hom) :
    S.iCycles (S.abCyclesIso.inv x) = x

Proof state:
S : ShortComplex Ab
x : ↥(AddCommGrp.Hom.hom S.g).ker
⊢ (ConcreteCategory.hom S.iCycles) ((ConcreteCategory.hom S.abLeftHomologyData.cyclesIso.inv) x) = ↑x

Tactic:
rw [← ConcreteCategory.comp_apply, S.abLeftHomologyData.cyclesIso_inv_comp_iCycles]

Result:
S : ShortComplex Ab
x : ↥(AddCommGrp.Hom.hom S.g).ker
⊢ (ConcreteCategory.hom S.abLeftHomologyData.i) x = ↑x

Proof state:
S : ShortComplex Ab
x : ↥(AddCommGrp.Hom.hom S.g).ker
⊢ (ConcreteCategory.hom S.abLeftHomologyData.i) x = ↑x

Tactic:
rfl

Result:
no goals

Proof state:
S : ShortComplex Ab
x : ↥(AddCommGrp.Hom.hom S.g).ker
⊢ (ConcreteCategory.hom S.iCycles) ((ConcreteCategory.hom S.abCyclesIso.inv) x) = ↑x

Tactic:
dsimp only [abCyclesIso]

Result:
S : ShortComplex Ab
x : ↥(AddCommGrp.Hom.hom S.g).ker
⊢ (ConcreteCategory.hom S.iCycles) ((ConcreteCategory.hom S.abLeftHomologyData.cyclesIso.inv) x) = ↑x
-- Mathlib/Topology/Algebra/InfiniteSum/Order.lean
theorem isLUB_hasProd' (hf : HasProd f a) : IsLUB (Set.range fun s ↦ ∏ i ∈ s, f i) a

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : OrderedCommMonoid α
inst✝² : CanonicallyOrderedMul α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a : α
hf : HasProd f a
⊢ IsLUB (Set.range fun s => ∏ i ∈ s, f i) a

Tactic:
classical
exact isLUB_of_tendsto_atTop (Finset.prod_mono_set' f) hf

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : OrderedCommMonoid α
inst✝² : CanonicallyOrderedMul α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a : α
hf : HasProd f a
⊢ IsLUB (Set.range fun s => ∏ i ∈ s, f i) a

Tactic:
exact isLUB_of_tendsto_atTop (Finset.prod_mono_set' f) hf

Result:
no goals
-- Mathlib/Order/Monotone/Basic.lean
/-- A function between linear orders which is neither monotone nor antitone makes a dent upright or
downright. -/
lemma not_monotone_not_antitone_iff_exists_le_le :
    ¬ Monotone f ∧ ¬ Antitone f ↔
      ∃ a b c, a ≤ b ∧ b ≤ c ∧ ((f a < f b ∧ f c < f b) ∨ (f b < f a ∧ f b < f c))

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
obtain hfdb | hfbd := le_or_lt (f d) (f b)

Result:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfdb : f d ≤ f b
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inl.inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hac : a ≤ c
hfbd : f b < f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Proof state:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
obtain hfca | hfac := lt_or_le (f c) (f a)

Result:
case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inl
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfca : f c < f a
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

case refine_2.intro.intro.intro.intro.intro.intro.intro.inr.inr.inr.inr
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hab : a ≤ b
hfba : f b < f a
c d : α
hcd : c ≤ d
hfcd : f c < f d
had : a ≤ d
hca : c ≤ a
hfbd : f b < f d
hfac : f a ≤ f c
⊢ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Proof state:
case refine_1.intro.intro.intro.intro.intro.inl.intro
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfab : f a < f b
hfcb : f c < f b
⊢ (∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1

case refine_1.intro.intro.intro.intro.intro.inr.intro
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfba : f b < f a
hfbc : f b < f c
⊢ (∃ x x_1 h, f x_1 < f x) ∧ ∃ x x_1 h, f x < f x_1

Tactic:
exacts [⟨⟨_, _, hbc, hfcb⟩, _, _, hab, hfab⟩, ⟨⟨_, _, hab, hfba⟩, _, _, hbc, hfbc⟩]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/CoverLifting.lean
@[reassoc (attr := simp)]
lemma fac (i : S.Arrow) : lift hF hR s ≫ R.map i.f.op = s.ι i

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
i : S.Arrow
⊢ lift hF hR s ≫ R.map i.f.op = s.ι i

Tactic:
apply (hR (op i.Y)).hom_ext

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
i : S.Arrow
⊢ ∀ (j : StructuredArrow (op i.Y) G.op),
    (lift hF hR s ≫ R.map i.f.op) ≫ ((Functor.RightExtension.mk R α).coneAt (op i.Y)).π.app j =
      s.ι i ≫ ((Functor.RightExtension.mk R α).coneAt (op i.Y)).π.app j

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_3, u_2} D
G : C ⥤ D
A : Type w
inst✝¹ : Category.{w', w} A
J : GrothendieckTopology C
K : GrothendieckTopology D
inst✝ : G.IsCocontinuous J K
F : Cᵒᵖ ⥤ A
hF : Presheaf.IsSheaf J F
R : Dᵒᵖ ⥤ A
α : G.op ⋙ R ⟶ F
hR : (Functor.RightExtension.mk R α).IsPointwiseRightKanExtension
X : D
S : K.Cover X
s : Multifork (S.index R)
i : S.Arrow
j : StructuredArrow (op i.Y) G.op
eq : lift hF hR s ≫ R.map i.f.op ≫ R.map j.hom ≫ α.app j.right = liftAux hF α s (j.hom.unop ≫ i.f)
⊢ liftAux hF α s (j.hom.unop ≫ i.f) = s.ι i ≫ R.map j.hom ≫ α.app j.right

Tactic:
simpa using liftAux_map hF α s (j.hom.unop ≫ i.f) (𝟙 _) i j.hom.unop (by simp)

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
theorem exists_Solution_multiplicity_lt :
    ∃ S₁ : Solution hζ, S₁.multiplicity < S.multiplicity

Proof state:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
S' : Solution hζ
hS' : S'.multiplicity = S.Solution'_descent.multiplicity
⊢ ∃ S₁, S₁.multiplicity < S.multiplicity

Tactic:
exact ⟨S', hS' ▸ Solution'_descent_multiplicity_lt S⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ ∃ S₁, S₁.multiplicity < S.multiplicity

Tactic:
classical
obtain ⟨S', hS'⟩ := exists_Solution_of_Solution' (Solution'_descent S)
exact ⟨S', hS' ▸ Solution'_descent_multiplicity_lt S⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ ∃ S₁, S₁.multiplicity < S.multiplicity

Tactic:
obtain ⟨S', hS'⟩ := exists_Solution_of_Solution' (Solution'_descent S)

Result:
case intro
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
S' : Solution hζ
hS' : S'.multiplicity = S.Solution'_descent.multiplicity
⊢ ∃ S₁, S₁.multiplicity < S.multiplicity
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem le_degrees_add_left (h : Disjoint p.degrees q.degrees) : p.degrees ≤ (p + q).degrees

Proof state:
case a.inr.intro
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ a ∈ p.degrees, ∃ b ∈ q.degrees, a = b

Tactic:
refine ⟨j, ?_, j, ?_, rfl⟩

Result:
case a.inr.intro.refine_1
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ j ∈ p.degrees

case a.inr.intro.refine_2
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ j ∈ q.degrees

Proof state:
case a.inl
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
hd : 0 ∈ p.support
⊢ 0 ≤ (p + q).degrees

Tactic:
apply Multiset.zero_le

Result:
no goals
-- Mathlib/Data/Set/Constructions.lean
theorem mk₂ (h: ∀ ⦃s⦄, s ∈ S → ∀ ⦃t⦄, t ∈ S → s ∩ t ∈ S) :
    FiniteInter (insert (univ : Set α) S) where
  univ_mem := Set.mem_insert Set.univ S
  inter_mem s hs t ht

Proof state:
α : Type u_1
S : Set (Set α)
h : ∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S
s : Set α
hs : s ∈ insert univ S
t : Set α
ht : t ∈ insert univ S
⊢ s ∩ t ∈ insert univ S

Tactic:
aesop

Result:
no goals
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem isPrimitiveClassified_of_coprime (hc : Int.gcd x y = 1) : h.IsPrimitiveClassified

Proof state:
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : ¬0 < z
h' : PythagoreanTriple x y (-z)
⊢ 0 < -z

Tactic:
apply lt_of_le_of_ne _ (h'.ne_zero_of_coprime hc).symm

Result:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : ¬0 < z
h' : PythagoreanTriple x y (-z)
⊢ 0 ≤ -z

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ h.IsPrimitiveClassified

Tactic:
by_cases hz : 0 < z

Result:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : 0 < z
⊢ h.IsPrimitiveClassified

case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : ¬0 < z
⊢ h.IsPrimitiveClassified

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : ¬0 < z
h' : PythagoreanTriple x y (-z)
⊢ 0 ≤ -z

Tactic:
exact le_neg.mp (not_lt.mp hz)

Result:
no goals

Proof state:
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : ¬0 < z
⊢ h.IsPrimitiveClassified

Tactic:
have h' : PythagoreanTriple x y (-z) := by simpa [PythagoreanTriple, neg_mul_neg] using h.eq

Result:
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : ¬0 < z
h' : PythagoreanTriple x y (-z)
⊢ h.IsPrimitiveClassified

Proof state:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : 0 < z
⊢ h.IsPrimitiveClassified

Tactic:
exact h.isPrimitiveClassified_of_coprime_of_pos hc hz

Result:
no goals

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : ¬0 < z
⊢ PythagoreanTriple x y (-z)

Tactic:
simpa [PythagoreanTriple, neg_mul_neg] using h.eq

Result:
no goals

Proof state:
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : ¬0 < z
h' : PythagoreanTriple x y (-z)
⊢ h.IsPrimitiveClassified

Tactic:
apply h'.isPrimitiveClassified_of_coprime_of_pos hc

Result:
case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : ¬0 < z
h' : PythagoreanTriple x y (-z)
⊢ 0 < -z
-- Mathlib/CategoryTheory/Limits/Final.lean
theorem zigzag_of_eqvGen_quot_rel {F : C ⥤ D} {d : D} {f₁ f₂ : ΣX, d ⟶ F.obj X}
    (t : Relation.EqvGen (Types.Quot.Rel.{v, v} (F ⋙ coyoneda.obj (op d))) f₁ f₂) :
    Zigzag (StructuredArrow.mk f₁.2) (StructuredArrow.mk f₂.2)

Proof state:
case trans.hab
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y z : (X : C) × (d ⟶ F.obj X)
a✝¹ : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) x y
a✝ : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) y z
ih₁ : Zigzag (StructuredArrow.mk x.snd) (StructuredArrow.mk y.snd)
ih₂ : Zigzag (StructuredArrow.mk y.snd) (StructuredArrow.mk z.snd)
⊢ Relation.ReflTransGen Zag (StructuredArrow.mk x.snd) ?trans.b

Tactic:
exact ih₁

Result:
no goals

Proof state:
case rel.intro.a
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (F ⋙ coyoneda.obj (op d)).map f x.snd
⊢ Zag (StructuredArrow.mk x.snd) (StructuredArrow.mk y.snd)

Tactic:
left

Result:
case rel.intro.a.h
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (F ⋙ coyoneda.obj (op d)).map f x.snd
⊢ Nonempty (StructuredArrow.mk x.snd ⟶ StructuredArrow.mk y.snd)

Proof state:
case trans.hbc
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y z : (X : C) × (d ⟶ F.obj X)
a✝¹ : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) x y
a✝ : Relation.EqvGen (Types.Quot.Rel (F ⋙ coyoneda.obj (op d))) y z
ih₁ : Zigzag (StructuredArrow.mk x.snd) (StructuredArrow.mk y.snd)
ih₂ : Zigzag (StructuredArrow.mk y.snd) (StructuredArrow.mk z.snd)
⊢ Relation.ReflTransGen Zag (StructuredArrow.mk y.snd) (StructuredArrow.mk z.snd)

Tactic:
exact ih₂

Result:
no goals

Proof state:
case rel
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
r : Types.Quot.Rel (F ⋙ coyoneda.obj (op d)) x y
⊢ Zigzag (StructuredArrow.mk x.snd) (StructuredArrow.mk y.snd)

Tactic:
obtain ⟨f, w⟩ := r

Result:
case rel.intro
C : Type v
inst✝¹ : Category.{v, v} C
D : Type u₁
inst✝ : Category.{v, u₁} D
F : C ⥤ D
d : D
f₁ f₂ x y : (X : C) × (d ⟶ F.obj X)
f : x.fst ⟶ y.fst
w : y.snd = (F ⋙ coyoneda.obj (op d)).map f x.snd
⊢ Zigzag (StructuredArrow.mk x.snd) (StructuredArrow.mk y.snd)
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem norm_le_pow_iff_le_valuation (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) :
    ‖x‖ ≤ (p : ℝ) ^ (-n : ℤ) ↔ n ≤ x.valuation

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ ‖x‖ ≤ ↑p ^ (-↑n) ↔ n ≤ x.valuation

Tactic:
rw [norm_eq_zpow_neg_valuation hx, zpow_le_zpow_iff_right₀, neg_le_neg_iff, Nat.cast_le]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ 1 < ↑p

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
hx : x ≠ 0
n : ℕ
⊢ 1 < ↑p

Tactic:
exact mod_cast hp.out.one_lt

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_zero : (0 : MvPolynomial σ R).totalDegree = 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ (C 0).totalDegree = 0

Tactic:
exact totalDegree_C (0 : R)

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ totalDegree 0 = 0

Tactic:
rw [← C_0]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ (C 0).totalDegree = 0
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem condExp_add (hf : Integrable f μ) (hg : Integrable g μ) (m : MeasurableSpace α) :
    μ[f + g|m] =ᵐ[μ] μ[f|m] + μ[g|m]

Proof state:
case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
⊢ μ[f + g|m] =ᶠ[ae μ] μ[f|m] + μ[g|m]

Tactic:
by_cases hμm : SigmaFinite (μ.trim hm)

Result:
case pos
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ μ[f + g|m] =ᶠ[ae μ] μ[f|m] + μ[g|m]

case neg
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ μ[f + g|m] =ᶠ[ae μ] μ[f|m] + μ[g|m]
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem isIntegral_leadingCoeff_smul [Algebra R S] (h : aeval x p = 0) :
    IsIntegral R (p.leadingCoeff • x)

Proof state:
R : Type u_1
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
p : R[X]
x : S
inst✝ : Algebra R S
h : (aeval x) p = 0
⊢ IsIntegral R (p.leadingCoeff • x)

Tactic:
rw [aeval_def] at h

Result:
R : Type u_1
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
p : R[X]
x : S
inst✝ : Algebra R S
h : eval₂ (algebraMap R S) x p = 0
⊢ IsIntegral R (p.leadingCoeff • x)

Proof state:
R : Type u_1
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
p : R[X]
x : S
inst✝ : Algebra R S
h : eval₂ (algebraMap R S) x p = 0
⊢ IsIntegral R (p.leadingCoeff • x)

Tactic:
rw [Algebra.smul_def]

Result:
R : Type u_1
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
p : R[X]
x : S
inst✝ : Algebra R S
h : eval₂ (algebraMap R S) x p = 0
⊢ IsIntegral R ((algebraMap R S) p.leadingCoeff * x)

Proof state:
R : Type u_1
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
p : R[X]
x : S
inst✝ : Algebra R S
h : eval₂ (algebraMap R S) x p = 0
⊢ IsIntegral R ((algebraMap R S) p.leadingCoeff * x)

Tactic:
exact (algebraMap R S).isIntegralElem_leadingCoeff_mul p x h

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean
theorem stream_eq_none_of_fr_eq_zero {ifp_n : IntFractPair K}
    (stream_nth_eq : IntFractPair.stream v n = some ifp_n) (nth_fr_eq_zero : ifp_n.fr = 0) :
    IntFractPair.stream v (n + 1) = none

Proof state:
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr }
nth_fr_eq_zero : fr = 0
⊢ IntFractPair.stream v (n + 1) = none

Tactic:
simp [IntFractPair.stream, stream_nth_eq, nth_fr_eq_zero]

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_n : IntFractPair K
stream_nth_eq : IntFractPair.stream v n = some ifp_n
nth_fr_eq_zero : ifp_n.fr = 0
⊢ IntFractPair.stream v (n + 1) = none

Tactic:
obtain ⟨_, fr⟩ := ifp_n

Result:
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr }
nth_fr_eq_zero : { b := b✝, fr := fr }.fr = 0
⊢ IntFractPair.stream v (n + 1) = none

Proof state:
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr }
nth_fr_eq_zero : { b := b✝, fr := fr }.fr = 0
⊢ IntFractPair.stream v (n + 1) = none

Tactic:
change fr = 0 at nth_fr_eq_zero

Result:
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
n : ℕ
b✝ : ℤ
fr : K
stream_nth_eq : IntFractPair.stream v n = some { b := b✝, fr := fr }
nth_fr_eq_zero : fr = 0
⊢ IntFractPair.stream v (n + 1) = none
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem length_erase [LawfulBEq α] (a : α) (l : List α) :
    length (l.erase a) = if a ∈ l then length l - 1 else length l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ (if (l.any fun x => a == x) = true then l.length - 1 else l.length) = if a ∈ l then l.length - 1 else l.length

Tactic:
split <;> split <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ (l.erase a).length = if a ∈ l then l.length - 1 else l.length

Tactic:
rw [erase_eq_eraseP, length_eraseP]

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ (if (l.any fun x => a == x) = true then l.length - 1 else l.length) = if a ∈ l then l.length - 1 else l.length