harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Tactic/NormNum/Prime.lean
theorem minFacHelper_3 {n k k' : ℕ} (e : k + 2 = k') (nk : (n % k).beq 0 = false)
    (h : MinFacHelper n k) : MinFacHelper n k'

Proof state:
n k k' : ℕ
e : k + 2 = k'
nk : (n % k).beq 0 = false
h : MinFacHelper n k
⊢ MinFacHelper n k'

Tactic:
refine minFacHelper_1 e h fun h2 ↦ ?_

Result:
n k k' : ℕ
e : k + 2 = k'
nk : (n % k).beq 0 = false
h : MinFacHelper n k
h2 : n.minFac = k
⊢ False

Proof state:
n k k' : ℕ
e : k + 2 = k'
nk : (n % k).beq 0 = false
h : MinFacHelper n k
h2 : n.minFac = k
⊢ False

Tactic:
have nk := Nat.ne_of_beq_eq_false nk

Result:
n k k' : ℕ
e : k + 2 = k'
nk✝ : (n % k).beq 0 = false
h : MinFacHelper n k
h2 : n.minFac = k
nk : ¬n % k = 0
⊢ False

Proof state:
n k k' : ℕ
e : k + 2 = k'
nk✝ : (n % k).beq 0 = false
h : MinFacHelper n k
h2 : n.minFac = k
nk : ¬n % k = 0
⊢ False

Tactic:
rw [← Nat.dvd_iff_mod_eq_zero, ← h2] at nk

Result:
n k k' : ℕ
e : k + 2 = k'
nk✝ : (n % k).beq 0 = false
h : MinFacHelper n k
h2 : n.minFac = k
nk : ¬n.minFac ∣ n
⊢ False

Proof state:
n k k' : ℕ
e : k + 2 = k'
nk✝ : (n % k).beq 0 = false
h : MinFacHelper n k
h2 : n.minFac = k
nk : ¬n.minFac ∣ n
⊢ False

Tactic:
exact nk <| minFac_dvd n

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem hasZeroObject_of_hasInitial_object [HasZeroMorphisms C] [HasInitial C] :
    HasZeroObject C

Proof state:
case h.e'_7
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
f : X ⟶ ⊥_ C
⊢ 𝟙 (⊥_ C) = 0

Tactic:
subsingleton

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
⊢ ∀ (a : ⊥_ C ⟶ X), a = default

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
f : X ⟶ ⊥_ C
⊢ f ≫ 𝟙 (⊥_ C) = f ≫ 0

Tactic:
congr!

Result:
case h.e'_7
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
f : X ⟶ ⊥_ C
⊢ 𝟙 (⊥_ C) = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
f : X ⟶ ⊥_ C
⊢ f = default

Tactic:
calc
  f = f ≫ 𝟙 _ := (Category.comp_id _).symm
  _ = f ≫ 0 := by congr!; subsingleton
  _ = 0 := HasZeroMorphisms.comp_zero _ _

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
⊢ HasZeroObject C

Tactic:
refine ⟨⟨⊥_ C, fun X => ⟨⟨⟨0⟩, by aesop_cat⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩⟩

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasInitial C
X : C
f : X ⟶ ⊥_ C
⊢ f = default
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Iic_sub_one_eq_Iio_of_not_isMin (hb : ¬ IsMin b) : Iic (b - 1) = Iio b

Proof state:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : One α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
b : α
hb : ¬IsMin b
⊢ Iic (b - 1) = Iio b

Tactic:
simpa [pred_eq_sub_one] using Iic_pred_eq_Iio_of_not_isMin hb

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_lt_sqrt_iff_of_pos (hy : 0 < y) : √x < √y ↔ x < y

Proof state:
x y : ℝ
hy : 0 < y
⊢ √x < √y ↔ x < y

Tactic:
rw [Real.sqrt, Real.sqrt, NNReal.coe_lt_coe, NNReal.sqrt_lt_sqrt, toNNReal_lt_toNNReal_iff hy]

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
lemma ωScottContinuous.sSup {s : Set (α → β)} (hs : ∀ f ∈ s, ωScottContinuous f) :
    ωScottContinuous (sSup s)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α → β)
hs : ∀ f ∈ s, ωScottContinuous f
⊢ ωScottContinuous (⨆ a ∈ s, a)

Tactic:
exact ωScottContinuous.iSup fun f ↦ ωScottContinuous.iSup <| hs f

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α → β)
hs : ∀ f ∈ s, ωScottContinuous f
⊢ ωScottContinuous (SupSet.sSup s)

Tactic:
rw [sSup_eq_iSup]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α → β)
hs : ∀ f ∈ s, ωScottContinuous f
⊢ ωScottContinuous (⨆ a ∈ s, a)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_modify (h : m.1.WF) {k k' : α} {f : β → β} :
    Const.get? (Const.modify m k f) k' =
      if k == k' then
        (Const.get? m k).map f
      else
        Const.get? m k'

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
k k' : α
f : β → β
⊢ get? (modify m k f) k' = if (k == k') = true then Option.map f (get? m k) else get? m k'

Tactic:
simp_to_model [Const.modify] using List.Const.getValue?_modifyKey

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma tendsto_densityProcess_atTop_empty_of_antitone (κ : Kernel α (γ × β)) (ν : Kernel α γ)
    [IsFiniteKernel κ] (n : ℕ) (a : α) (x : γ)
    (seq : ℕ → Set β) (hseq : Antitone seq) (hseq_iInter : ⋂ i, seq i = ∅)
    (hseq_meas : ∀ m, MeasurableSet (seq m)) :
    Tendsto (fun m ↦ densityProcess κ ν n a x (seq m)) atTop
      (𝓝 (densityProcess κ ν n a x ∅))

Proof state:
case neg.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ ¬((κ a) (countablePartitionSet n x ×ˢ ∅) ≠ 0 ∧ (ν a) (countablePartitionSet n x) = 0 ∨
      (κ a) (countablePartitionSet n x ×ˢ ∅) = ⊤ ∧ (ν a) (countablePartitionSet n x) ≠ ⊤)

Tactic:
push_neg

Result:
case neg.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 : ¬(ν a) (countablePartitionSet n x) = 0
⊢ ((κ a) (countablePartitionSet n x ×ˢ ∅) ≠ 0 → (ν a) (countablePartitionSet n x) ≠ 0) ∧
    ((κ a) (countablePartitionSet n x ×ˢ ∅) = ⊤ → (ν a) (countablePartitionSet n x) = ⊤)
-- Mathlib/NumberTheory/Padics/Hensel.lean
theorem ncs_tendsto_const :
    Tendsto (fun i => ‖F.derivative.eval (ncs i)‖) atTop (𝓝 ‖F.derivative.eval a‖)

Proof state:
case h.e'_3.h
p : ℕ
inst✝ : Fact (Nat.Prime p)
ncs : CauSeq ℤ_[p] norm
F : Polynomial ℤ_[p]
a : ℤ_[p]
ncs_der_val :
  ∀ (n : ℕ), ‖Polynomial.eval (↑ncs n) (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖
x✝ : ℕ
⊢ ‖Polynomial.eval (↑ncs x✝) (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖

Tactic:
rw [ncs_der_val]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
ncs : CauSeq ℤ_[p] norm
F : Polynomial ℤ_[p]
a : ℤ_[p]
ncs_der_val :
  ∀ (n : ℕ), ‖Polynomial.eval (↑ncs n) (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖
⊢ Tendsto (fun i => ‖Polynomial.eval (↑ncs i) (Polynomial.derivative F)‖) atTop
    (𝓝 ‖Polynomial.eval a (Polynomial.derivative F)‖)

Tactic:
convert @tendsto_const_nhds ℝ ℕ _ _ _

Result:
case h.e'_3.h
p : ℕ
inst✝ : Fact (Nat.Prime p)
ncs : CauSeq ℤ_[p] norm
F : Polynomial ℤ_[p]
a : ℤ_[p]
ncs_der_val :
  ∀ (n : ℕ), ‖Polynomial.eval (↑ncs n) (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖
x✝ : ℕ
⊢ ‖Polynomial.eval (↑ncs x✝) (Polynomial.derivative F)‖ = ‖Polynomial.eval a (Polynomial.derivative F)‖
-- Mathlib/NumberTheory/NumberField/Completion.lean
theorem surjective_extensionEmbedding_of_isReal {v : InfinitePlace K} (hv : IsReal v) :
    Function.Surjective (extensionEmbeddingOfIsReal hv)

Proof state:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsReal
⊢ Function.Surjective ⇑(extensionEmbeddingOfIsReal hv)

Tactic:
rw [← RingHom.fieldRange_eq_top_iff, ← Real.subfield_eq_of_closed]

Result:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsReal
⊢ IsClosed ↑(extensionEmbeddingOfIsReal hv).fieldRange

Proof state:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsReal
⊢ IsClosed ↑(extensionEmbeddingOfIsReal hv).fieldRange

Tactic:
exact isClosed_image_extensionEmbedding_of_isReal hv

Result:
no goals
-- Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean
/-- When `Φ : LocalizerMorphism W₁ W₂`, if the composition `Φ.functor ⋙ L₂` is a
localization functor for `W₁`, then `Φ` is a localized equivalence. -/
lemma IsLocalizedEquivalence.of_isLocalization_of_isLocalization
    [(Φ.functor ⋙ L₂).IsLocalization W₁] :
    IsLocalizedEquivalence Φ

Proof state:
C₁ : Type u₁
C₂ : Type u₂
D₂ : Type u₅
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : (Φ.functor ⋙ L₂).IsLocalization W₁
this : CatCommSq Φ.functor (Φ.functor ⋙ L₂) L₂ (𝟭 D₂)
⊢ Φ.IsLocalizedEquivalence

Tactic:
exact IsLocalizedEquivalence.mk' Φ (Φ.functor ⋙ L₂) L₂ (𝟭 D₂)

Result:
no goals

Proof state:
C₁ : Type u₁
C₂ : Type u₂
D₂ : Type u₅
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : (Φ.functor ⋙ L₂).IsLocalization W₁
⊢ Φ.IsLocalizedEquivalence

Tactic:
have : CatCommSq Φ.functor (Φ.functor ⋙ L₂) L₂ (𝟭 D₂) :=
  CatCommSq.mk (Functor.rightUnitor _).symm

Result:
C₁ : Type u₁
C₂ : Type u₂
D₂ : Type u₅
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
inst✝ : (Φ.functor ⋙ L₂).IsLocalization W₁
this : CatCommSq Φ.functor (Φ.functor ⋙ L₂) L₂ (𝟭 D₂)
⊢ Φ.IsLocalizedEquivalence
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
lemma threeAPFree_sphere {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [StrictConvexSpace ℝ E] (x : E) (r : ℝ) : ThreeAPFree (sphere x r)

Proof state:
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ ThreeAPFree (sphere x r)

Tactic:
convert threeAPFree_frontier isClosed_closedBall (strictConvex_closedBall ℝ x r)

Result:
case h.e'_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ sphere x r = frontier (closedBall x r)

Proof state:
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
⊢ ThreeAPFree {x}

Tactic:
exact threeAPFree_singleton _

Result:
no goals

Proof state:
case h.e'_3
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ sphere x r = frontier (closedBall x r)

Tactic:
exact (frontier_closedBall _ hr).symm

Result:
no goals

Proof state:
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
⊢ ThreeAPFree (sphere x 0)

Tactic:
rw [sphere_zero]

Result:
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
⊢ ThreeAPFree {x}

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
r : ℝ
⊢ ThreeAPFree (sphere x r)

Tactic:
obtain rfl | hr := eq_or_ne r 0

Result:
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
⊢ ThreeAPFree (sphere x 0)

case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x : E
r : ℝ
hr : r ≠ 0
⊢ ThreeAPFree (sphere x r)
-- Mathlib/Order/WithBot.lean
@[simp]
lemma WithTop.ofDual_le_ofDual_iff {x y : WithTop αᵒᵈ} :
    WithTop.ofDual x ≤ WithTop.ofDual y ↔ y ≤ x :=  by cases x <;> cases y <;> simp

Proof state:
α : Type u_1
inst✝ : LE α
x y : WithTop αᵒᵈ
⊢ WithTop.ofDual x ≤ WithTop.ofDual y ↔ y ≤ x

Tactic:
cases x <;> cases y <;> simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/MetricSeparated.lean
theorem finite_iUnion_left_iff {ι : Type*} {I : Set ι} (hI : I.Finite) {s : ι → Set X}
    {t : Set X} : AreSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, AreSeparated (s i) t

Proof state:
X : Type u_1
inst✝ : EMetricSpace X
ι : Type u_2
I : Set ι
hI : I.Finite
s : ι → Set X
t : Set X
⊢ AreSeparated (⋃ i ∈ ∅, s i) t ↔ ∀ i ∈ ∅, AreSeparated (s i) t

Tactic:
simp

Result:
no goals

Proof state:
X : Type u_1
inst✝ : EMetricSpace X
ι : Type u_2
I✝ : Set ι
hI✝ : I✝.Finite
s : ι → Set X
t : Set X
i : ι
I : Set ι
x✝¹ : i ∉ I
x✝ : I.Finite
hI : AreSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, AreSeparated (s i) t
⊢ AreSeparated (⋃ i_1 ∈ insert i I, s i_1) t ↔ ∀ i_1 ∈ insert i I, AreSeparated (s i_1) t

Tactic:
rw [biUnion_insert, forall_mem_insert, union_left_iff, hI]

Result:
no goals

Proof state:
X : Type u_1
inst✝ : EMetricSpace X
ι : Type u_2
I : Set ι
hI : I.Finite
s : ι → Set X
t : Set X
⊢ AreSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, AreSeparated (s i) t

Tactic:
refine Finite.induction_on _ hI (by simp) @fun i I _ _ hI => ?_

Result:
X : Type u_1
inst✝ : EMetricSpace X
ι : Type u_2
I✝ : Set ι
hI✝ : I✝.Finite
s : ι → Set X
t : Set X
i : ι
I : Set ι
x✝¹ : i ∉ I
x✝ : I.Finite
hI : AreSeparated (⋃ i ∈ I, s i) t ↔ ∀ i ∈ I, AreSeparated (s i) t
⊢ AreSeparated (⋃ i_1 ∈ insert i I, s i_1) t ↔ ∀ i_1 ∈ insert i I, AreSeparated (s i_1) t
-- Mathlib/RingTheory/MvPolynomial/Tower.lean
theorem aeval_map_algebraMap (x : σ → B) (p : MvPolynomial σ R) :
    aeval x (map (algebraMap R A) p) = aeval x p

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : CommSemiring B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : σ → B
p : MvPolynomial σ R
⊢ (aeval x) ((map (algebraMap R A)) p) = (aeval x) p

Tactic:
rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/SMul.lean
theorem map_smul (r : R) : (r • p).map f = f r • p.map f

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
r : R
⊢ map f (r • p) = f r • map f p

Tactic:
rw [map, eval₂_smul, RingHom.comp_apply, C_mul']

Result:
no goals
-- Mathlib/CategoryTheory/Adhesive.lean
theorem adhesive_of_reflective [HasPullbacks D] [Adhesive C] [HasPullbacks C] [HasPushouts C]
    [H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [Mono f], HasPushout f g]
    {Gl : C ⥤ D} {Gr : D ⥤ C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful]
    [PreservesLimitsOfShape WalkingCospan Gl] :
    Adhesive D

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
inst✝⁶ : HasPullbacks D
inst✝⁵ : Adhesive C
inst✝⁴ : HasPullbacks C
inst✝³ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝² : Gr.Full
inst✝¹ : Gr.Faithful
inst✝ : PreservesLimitsOfShape WalkingCospan Gl
⊢ Adhesive D

Tactic:
have := adj.leftAdjoint_preservesColimits

Result:
C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
inst✝⁶ : HasPullbacks D
inst✝⁵ : Adhesive C
inst✝⁴ : HasPullbacks C
inst✝³ : HasPushouts C
H₂ : ∀ {X Y S : D} (f : S ⟶ X) (g : S ⟶ Y) [inst : Mono f], HasPushout f g
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝² : Gr.Full
inst✝¹ : Gr.Faithful
inst✝ : PreservesLimitsOfShape WalkingCospan Gl
this : PreservesColimitsOfSize.{?u.117986, ?u.117985, v, v'', u, u''} Gl
⊢ Adhesive D
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive]
lemma image_pow_of_ne_zero [MulHomClass F α β] :
    ∀ {n}, n ≠ 0 → ∀ (f : F) (s : Finset α), (s ^ n).image f = s.image f ^ n
  | 1, _ => by simp
  | n + 2, _ => by simp [image_mul, pow_succ _ n.succ, image_pow_of_ne_zero]

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq β
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
x✝ : 1 ≠ 0
⊢ ∀ (f : F) (s : Finset α), image (⇑f) (s ^ 1) = image (⇑f) s ^ 1

Tactic:
simp

Result:
no goals

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq β
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ∀ (f : F) (s : Finset α), image (⇑f) (s ^ (n + 2)) = image (⇑f) s ^ (n + 2)

Tactic:
simp [image_mul, pow_succ _ n.succ, image_pow_of_ne_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem getLast_attach {xs : List α} (h : xs.attach ≠ []) :
    xs.attach.getLast h = ⟨xs.getLast (by simpa using h), getLast_mem (by simpa using h)⟩

Proof state:
α : Type u_1
xs : List α
h : xs.attach ≠ []
⊢ xs.attach.getLast h = ⟨xs.getLast ⋯, ⋯⟩

Tactic:
simp only [getLast_eq_head_reverse, reverse_attach, head_map, head_attach]

Result:
no goals

Proof state:
α : Type ?u.83510
xs : List α
h : xs.attach ≠ []
⊢ xs ≠ []

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem append1_drop_last (α : TypeVec (n + 1)) : append1 (drop α) (last α) = α :=
  funext fun i => by cases i <;> rfl

Proof state:
n : ℕ
α : TypeVec.{u_1} (n + 1)
i : Fin2 (n + 1)
⊢ (α.drop ::: α.last) i = α i

Tactic:
cases i <;> rfl

Result:
no goals
-- Mathlib/CategoryTheory/Products/Bifunctor.lean
theorem map_comp_id (F : C × D ⥤ E) (X Y Z : C) (W : D) (f : X ⟶ Y) (g : Y ⟶ Z) :
    F.map ((f ≫ g, 𝟙 W) : (X, W) ⟶ (Z, W)) =
      F.map ((f, 𝟙 W) : (X, W) ⟶ (Y, W)) ≫ F.map ((g, 𝟙 W) : (Y, W) ⟶ (Z, W))

Proof state:
C : Type u₁
D : Type u₂
E : Type u₃
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Category.{v₃, u₃} E
F : C × D ⥤ E
X Y Z : C
W : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (f ≫ g, 𝟙 W) = F.map (f, 𝟙 W) ≫ F.map (g, 𝟙 W)

Tactic:
rw [← Functor.map_comp, prod_comp, Category.comp_id]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Invariants.lean
theorem le_invariants_iterate (f : α → α) (n : ℕ) :
    invariants f ≤ invariants (f^[n])

Proof state:
case succ
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
n : ℕ
ihn : invariants f ≤ invariants f^[n]
⊢ invariants f ≤ invariants f^[n + 1]

Tactic:
exact le_trans (le_inf ihn le_rfl) (inf_le_invariants_comp _ _)

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
⊢ invariants f ≤ invariants f^[0]

Tactic:
simp [invariants_le]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → α
n : ℕ
⊢ invariants f ≤ invariants f^[n]

Tactic:
induction n with
| zero => simp [invariants_le]
| succ n ihn => exact le_trans (le_inf ihn le_rfl) (inf_le_invariants_comp _ _)

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem coeffs_ofSubring {p : T[X]} : (↑(p.ofSubring T).coeffs : Set R) ⊆ T

Proof state:
case intro.intro
R : Type u
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
i : R
n : ℕ
left✝ : ¬(ofSubring T p).coeff n = 0
h'n : (ofSubring T p).coeff n = i
⊢ ↑(p.coeff n) ∈ ↑T

Tactic:
exact Subtype.mem (coeff p n : T)

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
i : R
hi : i ∈ ↑(ofSubring T p).coeffs
⊢ i ∈ ↑T

Tactic:
simp only [coeffs, Set.mem_image, mem_support_iff, Ne, Finset.mem_coe,
  (Finset.coe_image)] at hi

Result:
R : Type u
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
i : R
hi : ∃ x, ¬(ofSubring T p).coeff x = 0 ∧ (ofSubring T p).coeff x = i
⊢ i ∈ ↑T

Proof state:
R : Type u
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
⊢ ↑(ofSubring T p).coeffs ⊆ ↑T

Tactic:
intro i hi

Result:
R : Type u
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
i : R
hi : i ∈ ↑(ofSubring T p).coeffs
⊢ i ∈ ↑T

Proof state:
R : Type u
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
i : R
hi : ∃ x, ¬(ofSubring T p).coeff x = 0 ∧ (ofSubring T p).coeff x = i
⊢ i ∈ ↑T

Tactic:
rcases hi with ⟨n, _, h'n⟩

Result:
case intro.intro
R : Type u
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
i : R
n : ℕ
left✝ : ¬(ofSubring T p).coeff n = 0
h'n : (ofSubring T p).coeff n = i
⊢ i ∈ ↑T

Proof state:
R : Type u
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
⊢ ↑(ofSubring T p).coeffs ⊆ ↑T

Tactic:
classical
intro i hi
simp only [coeffs, Set.mem_image, mem_support_iff, Ne, Finset.mem_coe,
  (Finset.coe_image)] at hi
rcases hi with ⟨n, _, h'n⟩
rw [← h'n, coeff_ofSubring]
exact Subtype.mem (coeff p n : T)

Result:
no goals

Proof state:
case intro.intro
R : Type u
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
i : R
n : ℕ
left✝ : ¬(ofSubring T p).coeff n = 0
h'n : (ofSubring T p).coeff n = i
⊢ i ∈ ↑T

Tactic:
rw [← h'n, coeff_ofSubring]

Result:
case intro.intro
R : Type u
inst✝ : Ring R
T : Subring R
p : (↥T)[X]
i : R
n : ℕ
left✝ : ¬(ofSubring T p).coeff n = 0
h'n : (ofSubring T p).coeff n = i
⊢ ↑(p.coeff n) ∈ ↑T
-- Mathlib/Analysis/RCLike/Basic.lean
theorem one_im : im (1 : K) = 0

Proof state:
K : Type u_1
inst✝ : RCLike K
⊢ im 1 = 0

Tactic:
rw [← ofReal_one, ofReal_im]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Asymptotics.lean
theorem IsBigO.integrable (hfm : AEStronglyMeasurable f μ)
    (hf : f =O[⊤] g) (hg : Integrable g μ) : Integrable f μ

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
f : α → E
g : α → F
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup F
μ : Measure α
hfm : AEStronglyMeasurable f μ
hf : f =O[⊤] g
hg : Integrable g μ
⊢ Integrable f μ

Tactic:
rewrite [← integrableAtFilter_top] at *

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
f : α → E
g : α → F
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup F
μ : Measure α
hfm : AEStronglyMeasurable f μ
hf : f =O[⊤] g
hg : IntegrableAtFilter g ⊤ μ
⊢ IntegrableAtFilter f ⊤ μ

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup E
f : α → E
g : α → F
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup F
μ : Measure α
hfm : AEStronglyMeasurable f μ
hf : f =O[⊤] g
hg : IntegrableAtFilter g ⊤ μ
⊢ IntegrableAtFilter f ⊤ μ

Tactic:
exact hf.integrableAtFilter ⟨univ, univ_mem, hfm.restrict⟩ hg

Result:
no goals
-- Mathlib/Algebra/RingQuot.lean
theorem ringQuot_ext' {s : A → A → Prop} (f g : RingQuot s →ₐ[S] B)
    (w : f.comp (mkAlgHom S s) = g.comp (mkAlgHom S s)) : f = g

Proof state:
case H.intro
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f g : RingQuot s →ₐ[S] B
w : f.comp (mkAlgHom S s) = g.comp (mkAlgHom S s)
x : A
⊢ f ((mkAlgHom S s) x) = g ((mkAlgHom S s) x)

Tactic:
exact AlgHom.congr_fun w x

Result:
no goals

Proof state:
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f g : RingQuot s →ₐ[S] B
w : f.comp (mkAlgHom S s) = g.comp (mkAlgHom S s)
⊢ f = g

Tactic:
ext x

Result:
case H
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f g : RingQuot s →ₐ[S] B
w : f.comp (mkAlgHom S s) = g.comp (mkAlgHom S s)
x : RingQuot s
⊢ f x = g x

Proof state:
case H
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f g : RingQuot s →ₐ[S] B
w : f.comp (mkAlgHom S s) = g.comp (mkAlgHom S s)
x : RingQuot s
⊢ f x = g x

Tactic:
rcases mkAlgHom_surjective S s x with ⟨x, rfl⟩

Result:
case H.intro
S : Type uS
inst✝⁴ : CommSemiring S
A : Type uA
inst✝³ : Semiring A
inst✝² : Algebra S A
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f g : RingQuot s →ₐ[S] B
w : f.comp (mkAlgHom S s) = g.comp (mkAlgHom S s)
x : A
⊢ f ((mkAlgHom S s) x) = g ((mkAlgHom S s) x)
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma lift_lt_ofENat {x : Cardinal.{v}} {m : ℕ∞} : lift.{u} x < m ↔ x < m

Proof state:
x : Cardinal.{v}
m : ℕ∞
⊢ lift.{u, v} x < ↑m ↔ x < ↑m

Tactic:
rw [← lift_ofENat.{u, v}, lift_lt]

Result:
no goals