harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Density.lean
theorem quasiMeasurePreserving_hasPDF (hg : QuasiMeasurePreserving g μ ν)
    (hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν) : HasPDF (g ∘ X) ℙ ν

Proof state:
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ μ
g : E → F
hg : QuasiMeasurePreserving g μ ν
hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν
hgm : AEMeasurable g (map X ℙ)
⊢ AEMeasurable (g ∘ X) ℙ ∧ (map g (map X ℙ)).HaveLebesgueDecomposition ν ∧ map g (map X ℙ) ≪ ν

Tactic:
refine ⟨hg.measurable.comp_aemeasurable (HasPDF.aemeasurable _ _ μ), hmap, ?_⟩

Result:
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ μ
g : E → F
hg : QuasiMeasurePreserving g μ ν
hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν
hgm : AEMeasurable g (map X ℙ)
⊢ map g (map X ℙ) ≪ ν

Proof state:
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ μ
g : E → F
hg : QuasiMeasurePreserving g μ ν
hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν
⊢ HasPDF (g ∘ X) ℙ ν

Tactic:
have hgm : AEMeasurable g (map X ℙ) := hg.aemeasurable.mono_ac HasPDF.absolutelyContinuous

Result:
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ μ
g : E → F
hg : QuasiMeasurePreserving g μ ν
hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν
hgm : AEMeasurable g (map X ℙ)
⊢ HasPDF (g ∘ X) ℙ ν

Proof state:
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ μ
g : E → F
hg : QuasiMeasurePreserving g μ ν
hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν
hgm : AEMeasurable g (map X ℙ)
⊢ HasPDF (g ∘ X) ℙ ν

Tactic:
rw [hasPDF_iff, ← AEMeasurable.map_map_of_aemeasurable hgm (HasPDF.aemeasurable X ℙ μ)]

Result:
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ μ
g : E → F
hg : QuasiMeasurePreserving g μ ν
hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν
hgm : AEMeasurable g (map X ℙ)
⊢ AEMeasurable (g ∘ X) ℙ ∧ (map g (map X ℙ)).HaveLebesgueDecomposition ν ∧ map g (map X ℙ) ≪ ν

Proof state:
Ω : Type u_1
E : Type u_2
inst✝² : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
F : Type u_3
inst✝¹ : MeasurableSpace F
ν : Measure F
X : Ω → E
inst✝ : HasPDF X ℙ μ
g : E → F
hg : QuasiMeasurePreserving g μ ν
hmap : (map g (map X ℙ)).HaveLebesgueDecomposition ν
hgm : AEMeasurable g (map X ℙ)
⊢ map g (map X ℙ) ≪ ν

Tactic:
exact (HasPDF.absolutelyContinuous.map hg.1).trans hg.2

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem Fintype.card_setUniv [Fintype α] {h : Fintype (Set.univ : Set α)} :
    Fintype.card (Set.univ : Set α) = Fintype.card α

Proof state:
α : Type u_1
inst✝ : Fintype α
h : Fintype ↑Set.univ
⊢ card ↑Set.univ = card α

Tactic:
apply Fintype.card_of_finset'

Result:
case H
α : Type u_1
inst✝ : Fintype α
h : Fintype ↑Set.univ
⊢ ∀ (x : α), x ∈ univ ↔ x ∈ Set.univ

Proof state:
case H
α : Type u_1
inst✝ : Fintype α
h : Fintype ↑Set.univ
⊢ ∀ (x : α), x ∈ univ ↔ x ∈ Set.univ

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem LinearMap.toMatrix_basis_equiv [Fintype l] [DecidableEq l] (b : Basis l R M₁)
    (b' : Basis l R M₂) :
    LinearMap.toMatrix b' b (b'.equiv b (Equiv.refl l) : M₂ →ₗ[R] M₁) = 1

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
l : Type u_2
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Fintype l
inst✝ : DecidableEq l
b : Basis l R M₁
b' : Basis l R M₂
⊢ (toMatrix b' b) ↑(b'.equiv b (Equiv.refl l)) = 1

Tactic:
ext i j

Result:
case a
R : Type u_1
inst✝⁶ : CommSemiring R
l : Type u_2
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Fintype l
inst✝ : DecidableEq l
b : Basis l R M₁
b' : Basis l R M₂
i j : l
⊢ (toMatrix b' b) (↑(b'.equiv b (Equiv.refl l))) i j = 1 i j

Proof state:
case a
R : Type u_1
inst✝⁶ : CommSemiring R
l : Type u_2
M₁ : Type u_5
M₂ : Type u_6
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Fintype l
inst✝ : DecidableEq l
b : Basis l R M₁
b' : Basis l R M₂
i j : l
⊢ (toMatrix b' b) (↑(b'.equiv b (Equiv.refl l))) i j = 1 i j

Tactic:
simp [LinearMap.toMatrix_apply, Matrix.one_apply, Finsupp.single_apply, eq_comm]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[simp] lemma ofEpiOfIsIsoOfMono'_p : (ofEpiOfIsIsoOfMono' φ h).p = φ.τ₂ ≫ h.p

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₂.RightHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono' φ h).p = φ.τ₂ ≫ h.p

Tactic:
simp [ofEpiOfIsIsoOfMono', opMap]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Polynomial.lean
theorem polynomialFunctions.starClosure_eq_adjoin_X [StarRing R] [ContinuousStar R] (s : Set R) :
    (polynomialFunctions s).starClosure = adjoin R {toContinuousMapOnAlgHom s X}

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalSemiring R
inst✝¹ : StarRing R
inst✝ : ContinuousStar R
s : Set R
⊢ (polynomialFunctions s).starClosure = adjoin R {(toContinuousMapOnAlgHom s) X}

Tactic:
rw [polynomialFunctions.eq_adjoin_X s, adjoin_eq_starClosure_adjoin]

Result:
no goals
-- Mathlib/CategoryTheory/PathCategory/Basic.lean
/-- To prove a property on morphisms of a path category, it suffices to prove it for the identity
and prove that the property is preserved under composition on the left with length 1 paths. -/
lemma induction' (P : ∀ {a b : Paths V}, (a ⟶ b) → Prop)
    (id : ∀ {v : V}, P (𝟙 (of.obj v)))
    (comp : ∀ {u v w : V} (p : u ⟶ v) (q : of.obj v ⟶ of.obj w), P q → P (of.map p ≫ q)) :
    ∀ {a b : Paths V} (f : a ⟶ b), P f

Proof state:
V : Type u₁
inst✝ : Quiver V
P : {a b : Paths V} → (a ⟶ b) → Prop
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : of.obj v ⟶ of.obj w), P q → P (of.map p ≫ q)
b : Paths V
⊢ ∀ {a : Paths V} (f : a ⟶ b), P f

Tactic:
exact induction_fixed_target (P := fun f ↦ P f) id (fun _ _ ↦ comp _ _)

Result:
no goals

Proof state:
V : Type u₁
inst✝ : Quiver V
P : {a b : Paths V} → (a ⟶ b) → Prop
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : of.obj v ⟶ of.obj w), P q → P (of.map p ≫ q)
a b : Paths V
⊢ ∀ (f : a ⟶ b), P f

Tactic:
revert a

Result:
V : Type u₁
inst✝ : Quiver V
P : {a b : Paths V} → (a ⟶ b) → Prop
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : of.obj v ⟶ of.obj w), P q → P (of.map p ≫ q)
b : Paths V
⊢ ∀ {a : Paths V} (f : a ⟶ b), P f

Proof state:
V : Type u₁
inst✝ : Quiver V
P : {a b : Paths V} → (a ⟶ b) → Prop
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : of.obj v ⟶ of.obj w), P q → P (of.map p ≫ q)
⊢ ∀ {a b : Paths V} (f : a ⟶ b), P f

Tactic:
intro a b

Result:
V : Type u₁
inst✝ : Quiver V
P : {a b : Paths V} → (a ⟶ b) → Prop
id : ∀ {v : V}, P (𝟙 (of.obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : of.obj v ⟶ of.obj w), P q → P (of.map p ≫ q)
a b : Paths V
⊢ ∀ (f : a ⟶ b), P f
-- Mathlib/Topology/GDelta/Basic.lean
/-- A closed set is nowhere dense iff its interior is empty. -/
lemma IsClosed.isNowhereDense_iff {s : Set X} (hs : IsClosed s) :
    IsNowhereDense s ↔ interior s = ∅

Proof state:
X : Type u_5
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
⊢ IsNowhereDense s ↔ interior s = ∅

Tactic:
rw [IsNowhereDense, IsClosed.closure_eq hs]

Result:
no goals
-- Mathlib/Topology/Category/LightProfinite/AsLimit.lean
lemma proj_comp_transitionMap' (n : ℕ) : S.transitionMap n ∘ S.proj (n + 1) = S.proj n

Proof state:
S : LightProfinite
n : ℕ
⊢ ⇑(ConcreteCategory.hom (S.transitionMap n)) ∘ ⇑(ConcreteCategory.hom (S.proj (n + 1))) =
    ⇑(ConcreteCategory.hom (S.proj (n + 1) ≫ S.diagram.map (Opposite.op (homOfLE ⋯))))

Tactic:
rfl

Result:
no goals

Proof state:
S : LightProfinite
n : ℕ
⊢ ⇑(ConcreteCategory.hom (S.transitionMap n)) ∘ ⇑(ConcreteCategory.hom (S.proj (n + 1))) =
    ⇑(ConcreteCategory.hom (S.proj n))

Tactic:
rw [← S.proj_comp_transitionMap n]

Result:
S : LightProfinite
n : ℕ
⊢ ⇑(ConcreteCategory.hom (S.transitionMap n)) ∘ ⇑(ConcreteCategory.hom (S.proj (n + 1))) =
    ⇑(ConcreteCategory.hom (S.proj (n + 1) ≫ S.diagram.map (Opposite.op (homOfLE ⋯))))
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem isLUB_ciSup_set {f : β → α} {s : Set β} (H : BddAbove (f '' s)) (Hne : s.Nonempty) :
    IsLUB (f '' s) (⨆ i : s, f i)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : β → α
s : Set β
H : BddAbove (f '' s)
Hne : s.Nonempty
⊢ IsLUB (f '' s) (⨆ i, f ↑i)

Tactic:
rw [← sSup_image']

Result:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : β → α
s : Set β
H : BddAbove (f '' s)
Hne : s.Nonempty
⊢ IsLUB (f '' s) (sSup (f '' s))

Proof state:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : β → α
s : Set β
H : BddAbove (f '' s)
Hne : s.Nonempty
⊢ IsLUB (f '' s) (sSup (f '' s))

Tactic:
exact isLUB_csSup (Hne.image _) H

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
@[simp]
lemma map_dblXYZ (P : Fin 3 → R) : (W'.map f).toProjective.dblXYZ (f ∘ P) = f ∘ dblXYZ W' P

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
S : Type v
inst✝ : CommRing S
f : R →+* S
P : Fin 3 → R
⊢ (map W' f).toProjective.dblXYZ (⇑f ∘ P) = ⇑f ∘ W'.dblXYZ P

Tactic:
simp only [dblXYZ, map_dblX, map_dblY, map_dblZ, comp_fin3]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem nonempty_of_encard_ne_zero (h : s.encard ≠ 0) : s.Nonempty

Proof state:
α : Type u_1
s : Set α
h : s.encard ≠ 0
⊢ s.Nonempty

Tactic:
rwa [nonempty_iff_ne_empty, Ne, ← encard_eq_zero]

Result:
no goals
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem hom_ext {f g : N ⋊[φ] G →* H} (hl : f.comp inl = g.comp inl)
    (hr : f.comp inr = g.comp inr) : f = g

Proof state:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f g : N ⋊[φ] G →* H
hl : f.comp inl = g.comp inl
hr : f.comp inr = g.comp inr
⊢ f = g

Tactic:
rw [lift_unique f, lift_unique g]

Result:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f g : N ⋊[φ] G →* H
hl : f.comp inl = g.comp inl
hr : f.comp inr = g.comp inr
⊢ lift (f.comp inl) (f.comp inr) ⋯ = lift (g.comp inl) (g.comp inr) ⋯

Proof state:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f g : N ⋊[φ] G →* H
hl : f.comp inl = g.comp inl
hr : f.comp inr = g.comp inr
⊢ lift (f.comp inl) (f.comp inr) ⋯ = lift (g.comp inl) (g.comp inr) ⋯

Tactic:
simp only [*]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_mul_distrib : ∏ x ∈ s, f x * g x = (∏ x ∈ s, f x) * ∏ x ∈ s, g x :=
  Eq.trans (by rw [one_mul]; rfl) fold_op_distrib

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f g : α → β
inst✝ : CommMonoid β
⊢ ∏ x ∈ s, f x * g x = fold (fun x1 x2 => x1 * x2) 1 (fun x => f x * g x) s

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
s : Finset α
f g : α → β
inst✝ : CommMonoid β
⊢ ∏ x ∈ s, f x * g x = fold (fun x1 x2 => x1 * x2) (1 * 1) (fun x => f x * g x) s

Tactic:
rw [one_mul]

Result:
α : Type u_3
β : Type u_4
s : Finset α
f g : α → β
inst✝ : CommMonoid β
⊢ ∏ x ∈ s, f x * g x = fold (fun x1 x2 => x1 * x2) 1 (fun x => f x * g x) s
-- Mathlib/Computability/PartrecCode.lean
theorem curry_inj {c₁ c₂ n₁ n₂} (h : curry c₁ n₁ = curry c₂ n₂) : c₁ = c₂ ∧ n₁ = n₂ :=
  ⟨by injection h, by
    injection h with h₁ h₂
    injection h₂ with h₃ h₄
    exact const_inj h₃⟩

Proof state:
c₁ c₂ : Code
n₁ n₂ : ℕ
h₁ : c₁ = c₂
h₂ : (Code.const n₁).pair Code.id = (Code.const n₂).pair Code.id
⊢ n₁ = n₂

Tactic:
injection h₂ with h₃ h₄

Result:
c₁ c₂ : Code
n₁ n₂ : ℕ
h₁ : c₁ = c₂
h₃ : Code.const n₁ = Code.const n₂
h₄ : Code.id = Code.id
⊢ n₁ = n₂

Proof state:
c₁ c₂ : Code
n₁ n₂ : ℕ
h : c₁.curry n₁ = c₂.curry n₂
⊢ n₁ = n₂

Tactic:
injection h with h₁ h₂

Result:
c₁ c₂ : Code
n₁ n₂ : ℕ
h₁ : c₁ = c₂
h₂ : (Code.const n₁).pair Code.id = (Code.const n₂).pair Code.id
⊢ n₁ = n₂

Proof state:
c₁ c₂ : Code
n₁ n₂ : ℕ
h₁ : c₁ = c₂
h₃ : Code.const n₁ = Code.const n₂
h₄ : Code.id = Code.id
⊢ n₁ = n₂

Tactic:
exact const_inj h₃

Result:
no goals

Proof state:
c₁ c₂ : Code
n₁ n₂ : ℕ
h : c₁.curry n₁ = c₂.curry n₂
⊢ c₁ = c₂

Tactic:
injection h

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem inv_re (z : ℂ) : z⁻¹.re = z.re / normSq z

Proof state:
z : ℂ
⊢ z⁻¹.re = z.re / normSq z

Tactic:
simp [inv_def, division_def, ofReal]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
theorem spanNorm_top : spanNorm R (⊤ : Ideal S) = ⊤

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : IsIntegrallyClosed R
inst✝⁴ : IsIntegrallyClosed S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : Algebra.IsSeparable (FractionRing R) (FractionRing S)
⊢ spanNorm R ⊤ = ⊤

Tactic:
simp [← Ideal.span_singleton_one]

Result:
no goals
-- Mathlib/Data/Rat/Lemmas.lean
theorem isSquare_intCast_iff {z : ℤ} : IsSquare (z : ℚ) ↔ IsSquare z

Proof state:
z : ℤ
⊢ IsSquare ↑z ↔ IsSquare z

Tactic:
simp_rw [isSquare_iff, intCast_num, intCast_den, IsSquare.one, and_true]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size

Proof state:
α : Type u_1
as bs : Array α
⊢ (as ++ bs).size = as.size + bs.size

Tactic:
simp only [size, toList_append, List.length_append]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
theorem PreservesPushout.inl_iso_hom :
    pushout.inl _ _ ≫ (PreservesPushout.iso G f g).hom = G.map (pushout.inl _ _)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ pushout.inl (G.map f) (G.map g) ≫
      ((colimit.isColimit (span (G.map f) (G.map g))).coconePointUniqueUpToIso
          (isColimitOfHasPushoutOfPreservesColimit G f g)).hom =
    G.map (pushout.inl f g)

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ pushout.inl (G.map f) (G.map g) ≫ (iso G f g).hom = G.map (pushout.inl f g)

Tactic:
delta PreservesPushout.iso

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst✝² : PreservesColimit (span f g) G
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
⊢ pushout.inl (G.map f) (G.map g) ≫
      ((colimit.isColimit (span (G.map f) (G.map g))).coconePointUniqueUpToIso
          (isColimitOfHasPushoutOfPreservesColimit G f g)).hom =
    G.map (pushout.inl f g)
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma neighborSet_toSubgraph_endpoint {u v} {p : G.Walk u v}
    (hp : p.IsPath) (hnp : ¬ p.Nil) : p.toSubgraph.neighborSet v = {p.penultimate}

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ ¬p.reverse.Nil

Tactic:
rw [Walk.not_nil_iff_lt_length, Walk.length_reverse]

Result:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ 0 < p.length

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ 0 < p.length

Tactic:
exact
Walk.not_nil_iff_lt_length.mp hnp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ p.toSubgraph.neighborSet v = {p.penultimate}

Tactic:
simpa using IsPath.neighborSet_toSubgraph_startpoint hp.reverse
    (by rw [Walk.not_nil_iff_lt_length, Walk.length_reverse]; exact
      Walk.not_nil_iff_lt_length.mp hnp)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem foldr_push (f : α → β → β) (init : β) (arr : Vector α n) (a : α) :
    (arr.push a).foldr f init = arr.foldr f (f a init)

Proof state:
α : Type u_1
β : Type u_2
n : Nat
f : α → β → β
init : β
arr : Vector α n
a : α
⊢ foldr f init (arr.push a) = foldr f (f a init) arr

Tactic:
rcases arr with ⟨arr, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β → β
init : β
a : α
arr : Array α
⊢ foldr f init ({ toArray := arr, size_toArray := ⋯ }.push a) = foldr f (f a init) { toArray := arr, size_toArray := ⋯ }

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β → β
init : β
a : α
arr : Array α
⊢ foldr f init ({ toArray := arr, size_toArray := ⋯ }.push a) = foldr f (f a init) { toArray := arr, size_toArray := ⋯ }

Tactic:
simp [Array.foldr_push]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem attachWith_append {P : α → Prop} {xs ys : List α}
    {H : ∀ (a : α), a ∈ xs ++ ys → P a} :
    (xs ++ ys).attachWith P H = xs.attachWith P (fun a h => H a (mem_append_left ys h)) ++
      ys.attachWith P (fun a h => H a (mem_append_right xs h))

Proof state:
α : Type u_1
P : α → Prop
xs ys : List α
H : ∀ (a : α), a ∈ xs ++ ys → P a
⊢ (xs ++ ys).attachWith P H = xs.attachWith P ⋯ ++ ys.attachWith P ⋯

Tactic:
simp only [attachWith, attach_append, map_pmap, pmap_append]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem sub_zero (a : Int) : a - 0 = a

Proof state:
a : Int
⊢ a - 0 = a

Tactic:
simp [Int.sub_eq_add_neg]

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem cons_le_of_not_mem (hs : a ∉ s) : a ::ₘ s ≤ t ↔ a ∈ t ∧ s ≤ t

Proof state:
α : Type u_1
s t : Multiset α
a : α
hs : ¬a ∈ s
⊢ a ∈ t ∧ s ≤ t → a ::ₘ s ≤ t

Tactic:
rintro ⟨h₁, h₂⟩

Result:
case intro
α : Type u_1
s t : Multiset α
a : α
hs : ¬a ∈ s
h₁ : a ∈ t
h₂ : s ≤ t
⊢ a ::ₘ s ≤ t

Proof state:
α : Type u_1
s t : Multiset α
a : α
hs : ¬a ∈ s
⊢ a ::ₘ s ≤ t ↔ a ∈ t ∧ s ≤ t

Tactic:
apply Iff.intro (fun h ↦ ⟨subset_of_le h (mem_cons_self a s), le_trans (le_cons_self s a) h⟩)

Result:
α : Type u_1
s t : Multiset α
a : α
hs : ¬a ∈ s
⊢ a ∈ t ∧ s ≤ t → a ::ₘ s ≤ t

Proof state:
case intro
α : Type u_1
s t : Multiset α
a : α
hs : ¬a ∈ s
h₁ : a ∈ t
h₂ : s ≤ t
⊢ a ::ₘ s ≤ t

Tactic:
rcases exists_cons_of_mem h₁ with ⟨_, rfl⟩

Result:
case intro.intro
α : Type u_1
s : Multiset α
a : α
hs : ¬a ∈ s
w✝ : Multiset α
h₁ : a ∈ a ::ₘ w✝
h₂ : s ≤ a ::ₘ w✝
⊢ a ::ₘ s ≤ a ::ₘ w✝

Proof state:
case intro.intro
α : Type u_1
s : Multiset α
a : α
hs : ¬a ∈ s
w✝ : Multiset α
h₁ : a ∈ a ::ₘ w✝
h₂ : s ≤ a ::ₘ w✝
⊢ a ::ₘ s ≤ a ::ₘ w✝

Tactic:
exact cons_le_cons _ ((le_cons_of_not_mem hs).mp h₂)

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem ker_toHomUnits {M} [Monoid M] (f : G →* M) : f.toHomUnits.ker = f.ker

Proof state:
G : Type u_1
inst✝¹ : Group G
M : Type u_8
inst✝ : Monoid M
f : G →* M
⊢ f.toHomUnits.ker = f.ker

Tactic:
ext x

Result:
case h
G : Type u_1
inst✝¹ : Group G
M : Type u_8
inst✝ : Monoid M
f : G →* M
x : G
⊢ x ∈ f.toHomUnits.ker ↔ x ∈ f.ker

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
M : Type u_8
inst✝ : Monoid M
f : G →* M
x : G
⊢ x ∈ f.toHomUnits.ker ↔ x ∈ f.ker

Tactic:
simp [mem_ker, Units.ext_iff]

Result:
no goals
-- Mathlib/Topology/Filter.lean
theorem sInter_nhds (l : Filter α) : ⋂₀ { s | s ∈ 𝓝 l } = Iic l

Proof state:
α : Type u_2
l : Filter α
⊢ ⋂₀ {s | s ∈ 𝓝 l} = Iic l

Tactic:
simp_rw [nhds_eq, Function.comp_def, sInter_lift'_sets monotone_principal.Iic, Iic,
  le_principal_iff, ← setOf_forall, ← Filter.le_def]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem Filter.EventuallyEq.iteratedFDerivWithin_eq (h : f₁ =ᶠ[𝓝[s] x] f) (hx : f₁ x = f x)
    (n : ℕ) : iteratedFDerivWithin 𝕜 n f₁ s x = iteratedFDerivWithin 𝕜 n f s x :=
  have : f₁ =ᶠ[𝓝[insert x s] x] f

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f f₁ : E → F
x : E
h : f₁ =ᶠ[𝓝[s] x] f
hx : f₁ x = f x
n : ℕ
⊢ f₁ =ᶠ[𝓝[insert x s] x] f

Tactic:
simpa [EventuallyEq, hx]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Representable.lean
@[reassoc (attr := simp)]
lemma symmetry_snd [Full F] [Faithful F] : hf'.symmetry hg ≫ hg.snd f' = hf'.fst' g

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
b : C
f' : F.obj b ⟶ Y
hf' : F.relativelyRepresentable f'
a : C
g : F.obj a ⟶ Y
hg : F.relativelyRepresentable g
inst✝¹ : F.Full
inst✝ : F.Faithful
⊢ hf'.symmetry hg ≫ hg.snd f' = hf'.fst' g

Tactic:
simp [symmetry]

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
theorem xor_cancel_right (n m : ℕ) : (m ^^^ n) ^^^ n = m

Proof state:
n m : ℕ
⊢ m ^^^ n ^^^ n = m

Tactic:
rw [Nat.xor_assoc, Nat.xor_self, xor_zero]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem foldr (f) (init : α) : ∀ {s}, Valid s → s.foldr f init = s.toString.1.foldr f init
  | _, h => let ⟨_, _, _, h⟩ := h.validFor; by simp [h.foldr, h.toString]

Proof state:
α : Type u_1
f : Char → α → α
init : α
x✝ : Substring
h✝ : x✝.Valid
w✝² w✝¹ w✝ : List Char
h : ValidFor w✝² w✝¹ w✝ x✝
⊢ Substring.foldr f init x✝ = List.foldr f init x✝.toString.data

Tactic:
simp [h.foldr, h.toString]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mul_mk'_eq_mk'_of_mul (x₁ x₂) (y : S) : f.toMap x₁ * f.mk' x₂ y = f.mk' (x₁ * x₂) y

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y : ↥S
⊢ f.toMap x₁ * f.mk' x₂ y = f.mk' (x₁ * x₂) y

Tactic:
rw [← mk'_one, ← mk'_mul, one_mul]

Result:
no goals
-- Mathlib/Topology/UniformSpace/HeineCantor.lean
theorem CompactSpace.uniformContinuous_of_continuous [CompactSpace α] {f : α → β}
    (h : Continuous f) : UniformContinuous f :=
  calc map (Prod.map f f) (𝓤 α)
    = map (Prod.map f f) (𝓝ˢ (diagonal α))

Proof state:
α : Type u_1
β : Type u_2
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : CompactSpace α
f : α → β
h : Continuous f
⊢ map (Prod.map f f) (𝓤 α) = map (Prod.map f f) (𝓝ˢ (diagonal α))

Tactic:
rw [nhdsSet_diagonal_eq_uniformity]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem sInter_eq_biInter {s : Set (Set α)} : ⋂₀ s = ⋂ (i : Set α) (_ : i ∈ s), i

Proof state:
α : Type u_1
s : Set (Set α)
⊢ ⋂₀ s = ⋂ i ∈ s, i

Tactic:
rw [← sInter_image, image_id']

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem algebraicIndependent_empty_type_iff [IsEmpty ι] :
    AlgebraicIndependent R x ↔ Injective (algebraMap R A)

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : IsEmpty ι
⊢ AlgebraicIndependent R x ↔ Injective ⇑(algebraMap R A)

Tactic:
rw [algebraicIndependent_iff_injective_aeval, MvPolynomial.aeval_injective_iff_of_isEmpty]

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/Equalizer.lean
lemma mem_equalizer_iff {i : Cᵒᵖ} (x : A.toPresheaf.obj i) :
    x.1 ∈ (Subpresheaf.equalizer f g).obj i ↔ f.app i x = g.app i x

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : Cᵒᵖ ⥤ Type w
A : Subpresheaf F₁
f g : A.toPresheaf ⟶ F₂
i : Cᵒᵖ
x : A.toPresheaf.obj i
⊢ ↑x ∈ (Subpresheaf.equalizer f g).obj i ↔ f.app i x = g.app i x

Tactic:
simp

Result:
no goals