harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
@[reassoc]
lemma ofCocone_map (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ < j) :
    (ofCocone c).map (homOfLE hi : ⟨i₁, hi.trans hi₂.le⟩ ⟶ ⟨i₂, hi₂.le⟩) =
      (ofCoconeObjIso c i₁ (lt_of_le_of_lt hi hi₂)).hom ≫ F.map (homOfLE hi) ≫
        (ofCoconeObjIso c i₂ hi₂).inv

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ < j
⊢ (if h₂ : i₂ < j then (ofCocone.objIso c i₁ ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (ofCocone.objIso c i₂ h₂).inv
    else
      if h₁ : i₁ < j then (ofCocone.objIso c i₁ h₁).hom ≫ c.ι.app ⟨i₁, h₁⟩ ≫ (ofCocone.objIsoPt c).inv ≫ eqToHom ⋯
      else eqToHom ⋯) =
    (ofCocone.objIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ (ofCocone.objIso c i₂ hi₂).inv

Tactic:
rw [dif_pos hi₂]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ < j
⊢ (ofCocone c).map (homOfLE hi) = (ofCoconeObjIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ (ofCoconeObjIso c i₂ hi₂).inv

Tactic:
dsimp [ofCocone, ofCoconeObjIso, ofCocone.map]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i₁ i₂ : J
hi : i₁ ≤ i₂
hi₂ : i₂ < j
⊢ (if h₂ : i₂ < j then (ofCocone.objIso c i₁ ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (ofCocone.objIso c i₂ h₂).inv
    else
      if h₁ : i₁ < j then (ofCocone.objIso c i₁ h₁).hom ≫ c.ι.app ⟨i₁, h₁⟩ ≫ (ofCocone.objIsoPt c).inv ≫ eqToHom ⋯
      else eqToHom ⋯) =
    (ofCocone.objIso c i₁ ⋯).hom ≫ F.map (homOfLE hi) ≫ (ofCocone.objIso c i₂ hi₂).inv
-- Mathlib/Data/Finsupp/WellFounded.lean
theorem Lex.acc (hbot : ∀ ⦃n⦄, ¬s n 0) (hs : WellFounded s) (x : α →₀ N)
    (h : ∀ a ∈ x.support, Acc (rᶜ ⊓ (· ≠ ·)) a) :
    Acc (Finsupp.Lex r s) x

Proof state:
α : Type u_1
N : Type u_2
inst✝ : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) a
⊢ Acc (InvImage (DFinsupp.Lex r fun x => s) toDFinsupp) x

Tactic:
classical
  refine InvImage.accessible toDFinsupp (DFinsupp.Lex.acc (fun _ => hbot) (fun _ => hs) _ ?_)
  simpa only [toDFinsupp_support] using h

Result:
no goals

Proof state:
α : Type u_1
N : Type u_2
inst✝ : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) a
⊢ ∀ i ∈ x.toDFinsupp.support, Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) i

Tactic:
simpa only [toDFinsupp_support] using h

Result:
no goals

Proof state:
α : Type u_1
N : Type u_2
inst✝ : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) a
⊢ Acc (Finsupp.Lex r s) x

Tactic:
rw [lex_eq_invImage_dfinsupp_lex]

Result:
α : Type u_1
N : Type u_2
inst✝ : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) a
⊢ Acc (InvImage (DFinsupp.Lex r fun x => s) toDFinsupp) x

Proof state:
α : Type u_1
N : Type u_2
inst✝ : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) a
⊢ Acc (InvImage (DFinsupp.Lex r fun x => s) toDFinsupp) x

Tactic:
refine InvImage.accessible toDFinsupp (DFinsupp.Lex.acc (fun _ => hbot) (fun _ => hs) _ ?_)

Result:
α : Type u_1
N : Type u_2
inst✝ : Zero N
r : α → α → Prop
s : N → N → Prop
hbot : ∀ ⦃n : N⦄, ¬s n 0
hs : WellFounded s
x : α →₀ N
h : ∀ a ∈ x.support, Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) a
⊢ ∀ i ∈ x.toDFinsupp.support, Acc (rᶜ ⊓ fun x1 x2 => x1 ≠ x2) i
-- Mathlib/RingTheory/Polynomial/IntegralNormalization.lean
theorem integralNormalization_degree : (integralNormalization p).degree = p.degree

Proof state:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.degree ≤ p.integralNormalization.degree

Tactic:
rw [← degree_scaleRoots, ← integralNormalization_mul_C_leadingCoeff]

Result:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p.integralNormalization * C p.leadingCoeff).degree ≤ p.integralNormalization.degree

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.integralNormalization.degree = p.degree

Tactic:
apply le_antisymm

Result:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.integralNormalization.degree ≤ p.degree

case a
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.degree ≤ p.integralNormalization.degree

Proof state:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p.integralNormalization * C p.leadingCoeff).degree ≤ p.integralNormalization.degree

Tactic:
exact (degree_mul_le _ _).trans (add_le_of_nonpos_right degree_C_le)

Result:
no goals

Proof state:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.integralNormalization.degree ≤ p.degree

Tactic:
exact Finset.sup_mono p.support_integralNormalization_subset

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem support_C_mul_X {c : R} (h : c ≠ 0) : Polynomial.support (C c * X) = singleton 1

Proof state:
R : Type u
inst✝ : Semiring R
c : R
h : c ≠ 0
⊢ (C c * X).support = {1}

Tactic:
rw [C_mul_X_eq_monomial, support_monomial 1 h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean
theorem denote_bitblast (expr : BVLogicalExpr) (assign : BVExpr.Assignment) :
    ⟦bitblast expr, assign.toAIGAssignment⟧ = expr.eval assign

Proof state:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ ⟦assign.toAIGAssignment, (ofBoolExprCached.go empty expr BVPred.bitblast).val⟧ = eval assign expr

Tactic:
rw [bitblast.go_eval_eq_eval]

Result:
no goals

Proof state:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ ⟦assign.toAIGAssignment, ofBoolExprCached expr BVPred.bitblast⟧ = eval assign expr

Tactic:
unfold ofBoolExprCached

Result:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ ⟦assign.toAIGAssignment, (ofBoolExprCached.go empty expr BVPred.bitblast).val⟧ = eval assign expr

Proof state:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ ⟦assign.toAIGAssignment, expr.bitblast⟧ = eval assign expr

Tactic:
unfold bitblast

Result:
expr : BVLogicalExpr
assign : BVExpr.Assignment
⊢ ⟦assign.toAIGAssignment, ofBoolExprCached expr BVPred.bitblast⟧ = eval assign expr
-- Mathlib/Order/Filter/AtTopBot/Field.lean
theorem tendsto_const_mul_atBot_iff [NeBot l] :
    Tendsto (fun x => r * f x) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrderedField α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
⊢ Tendsto (fun x => r * f x) l atBot ↔ 0 < r ∧ Tendsto f l atBot ∨ r < 0 ∧ Tendsto f l atTop

Tactic:
simp only [← tendsto_neg_atTop_iff, ← mul_neg, tendsto_const_mul_atTop_iff, neg_neg]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma addX_of_Z_eq_zero_right [NoZeroDivisors R] {P Q : Fin 3 → R} (hQ : W'.Equation Q)
    (hQz : Q z = 0) : W'.addX P Q = -(Q y ^ 2 * P z) * P x

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -P x * Q y ^ 2 * P z + 0 * P y ^ 2 * 0 - 2 * P x * P y * Q y * 0 + 2 * 0 * P y * Q y * P z -
                            W'.a₁ * P x ^ 2 * Q y * 0 +
                          W'.a₁ * 0 ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * 0 * 0 -
                      W'.a₂ * P x * 0 ^ 2 * P z -
                    W'.a₃ * P x * P y * 0 ^ 2 +
                  W'.a₃ * 0 * Q y * P z ^ 2 -
                2 * W'.a₃ * P x * Q y * P z * 0 +
              2 * W'.a₃ * 0 * P y * P z * 0 +
            W'.a₄ * P x ^ 2 * 0 ^ 2 -
          W'.a₄ * 0 ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * 0 ^ 2 -
      3 * W'.a₆ * 0 * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * P x

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ W'.addX P Q = -(Q y ^ 2 * P z) * P x

Tactic:
rw [addX, hQz, X_eq_zero_of_Z_eq_zero hQ hQz]

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -P x * Q y ^ 2 * P z + 0 * P y ^ 2 * 0 - 2 * P x * P y * Q y * 0 + 2 * 0 * P y * Q y * P z -
                            W'.a₁ * P x ^ 2 * Q y * 0 +
                          W'.a₁ * 0 ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * 0 * 0 -
                      W'.a₂ * P x * 0 ^ 2 * P z -
                    W'.a₃ * P x * P y * 0 ^ 2 +
                  W'.a₃ * 0 * Q y * P z ^ 2 -
                2 * W'.a₃ * P x * Q y * P z * 0 +
              2 * W'.a₃ * 0 * P y * P z * 0 +
            W'.a₄ * P x ^ 2 * 0 ^ 2 -
          W'.a₄ * 0 ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * 0 ^ 2 -
      3 * W'.a₆ * 0 * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * P x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Lemmas.lean
theorem Bool.eq_false_of_not_eq_true {a : Bool} (h : (!a) = true) : a = false

Proof state:
a : Bool
h : (!a) = true
⊢ a = false

Tactic:
simp_all

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem LinearEquiv.det_mul_det_symm {A : Type*} [CommRing A] [Module A M] (f : M ≃ₗ[A] M) :
    LinearMap.det (f : M →ₗ[A] M) * LinearMap.det (f.symm : M →ₗ[A] M) = 1

Proof state:
M : Type u_2
inst✝² : AddCommGroup M
A : Type u_5
inst✝¹ : CommRing A
inst✝ : Module A M
f : M ≃ₗ[A] M
⊢ LinearMap.det ↑f * LinearMap.det ↑f.symm = 1

Tactic:
simp [← LinearMap.det_comp]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem add_le_add_iff_right {a b : Ordinal} : ∀ n : ℕ, a + n ≤ b + n ↔ a ≤ b
  | 0 => by simp
  | n + 1 => by
    simp only [natCast_succ, add_succ, add_succ, succ_le_succ_iff, add_le_add_iff_right]

Proof state:
a b : Ordinal.{u_4}
n : ℕ
⊢ a + ↑(n + 1) ≤ b + ↑(n + 1) ↔ a ≤ b

Tactic:
simp only [natCast_succ, add_succ, add_succ, succ_le_succ_iff, add_le_add_iff_right]

Result:
no goals

Proof state:
a b : Ordinal.{u_4}
⊢ a + ↑0 ≤ b + ↑0 ↔ a ≤ b

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem Right.mul_nonneg [MulPosMono α] (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b

Proof state:
α : Type u_3
a b : α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosMono α
ha : 0 ≤ a
hb : 0 ≤ b
⊢ 0 ≤ a * b

Tactic:
simpa only [zero_mul] using mul_le_mul_of_nonneg_right ha hb

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Canonicalize.lean
theorem Bool.eq_false (a : Bool) : ((a = true) = False) = ((!a) = true)

Proof state:
a : Bool
⊢ ((a = true) = False) = ((!a) = true)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
@[to_additive]
lemma range_eq_image_or_of_mulSupport_subset {f : α → M} {k : Set α} (h : mulSupport f ⊆ k) :
    range f = f '' k ∨ range f = insert 1 (f '' k)

Proof state:
α : Type u_1
M : Type u_5
inst✝ : One M
f : α → M
k : Set α
h : mulSupport f ⊆ k
⊢ range f ≤ insert 1 (f '' k)

Tactic:
exact (range_subset_insert_image_mulSupport f).trans (insert_subset_insert (image_subset f h))

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : One M
f : α → M
k : Set α
h : mulSupport f ⊆ k
⊢ range f = f '' k ∨ range f = insert 1 (f '' k)

Tactic:
apply (wcovBy_insert _ _).eq_or_eq (image_subset_range _ _)

Result:
α : Type u_1
M : Type u_5
inst✝ : One M
f : α → M
k : Set α
h : mulSupport f ⊆ k
⊢ range f ≤ insert 1 (f '' k)
-- Mathlib/Data/Matroid/Restrict.lean
theorem ofMatroid_le_iff {M M' : Matroid α} :
    Matroidᵣ.ofMatroid M ≤ Matroidᵣ.ofMatroid M' ↔ M ≤r M'

Proof state:
α : Type u_1
M M' : Matroid α
⊢ { toMatroid := M } ≤ { toMatroid := M' } ↔ M ≤r M'

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Complemented.lean
theorem ClosedComplemented.of_quotient_finiteDimensional [CompleteSpace 𝕜]
    [FiniteDimensional 𝕜 (E ⧸ p)] (hp : IsClosed (p : Set E)) : p.ClosedComplemented

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
p : Subspace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 (E ⧸ p)
hp : IsClosed ↑p
q : Subspace 𝕜 E
hq : IsCompl p q
this : FiniteDimensional 𝕜 ↥q
⊢ ClosedComplemented p

Tactic:
exact .of_isCompl_isClosed hq hp q.closed_of_finiteDimensional

Result:
no goals

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
p : Subspace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 (E ⧸ p)
hp : IsClosed ↑p
q : Subspace 𝕜 E
hq : IsCompl p q
⊢ ClosedComplemented p

Tactic:
haveI : FiniteDimensional 𝕜 q := (p.quotientEquivOfIsCompl q hq).finiteDimensional

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
p : Subspace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 (E ⧸ p)
hp : IsClosed ↑p
q : Subspace 𝕜 E
hq : IsCompl p q
this : FiniteDimensional 𝕜 ↥q
⊢ ClosedComplemented p

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
p : Subspace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 (E ⧸ p)
hp : IsClosed ↑p
⊢ ClosedComplemented p

Tactic:
obtain ⟨q, hq⟩ : ∃ q, IsCompl p q := p.exists_isCompl

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : CompleteSpace E
p : Subspace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
inst✝ : FiniteDimensional 𝕜 (E ⧸ p)
hp : IsClosed ↑p
q : Subspace 𝕜 E
hq : IsCompl p q
⊢ ClosedComplemented p
-- Mathlib/Data/List/Perm/Lattice.lean
theorem Perm.take_inter {xs ys : List α} (n : ℕ) (h : xs ~ ys)
    (h' : ys.Nodup) : xs.take n ~ ys.inter (xs.take n)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ take n xs ~ ys.inter (take n xs)

Tactic:
simp only [List.inter]

Result:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ take n xs ~ List.filter (fun x => elem x (take n xs)) ys

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ take n xs ~ List.filter (fun x => elem x (take n xs)) ys

Tactic:
exact Perm.trans (show xs.take n ~ xs.filter (xs.take n).elem by
    conv_lhs => rw [Nodup.take_eq_filter_mem ((Perm.nodup_iff h).2 h')])
  (Perm.filter _ h)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ take n xs ~ List.filter (fun a => elem a (take n xs)) xs

Tactic:
conv_lhs => rw [Nodup.take_eq_filter_mem ((Perm.nodup_iff h).2 h')]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean
lemma exact_iff_surjective_moduleCatToCycles :
    S.Exact ↔ Function.Surjective S.moduleCatToCycles

Proof state:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.Exact ↔ Function.Surjective ⇑S.moduleCatToCycles

Tactic:
rw [S.moduleCatLeftHomologyData.exact_iff_epi_f', moduleCatLeftHomologyData_f',
  ModuleCat.epi_iff_surjective]

Result:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (ModuleCat.ofHom S.moduleCatToCycles)) ↔
    Function.Surjective ⇑S.moduleCatToCycles

Proof state:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ Function.Surjective ⇑(ConcreteCategory.hom (ModuleCat.ofHom S.moduleCatToCycles)) ↔
    Function.Surjective ⇑S.moduleCatToCycles

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Curry.lean
theorem uncurry_curry (f : ((i : Fin n) → p i) → τ) :
    uncurry (curry f) = f

Proof state:
case h.succ
τ : Type u
n : ℕ
ih : ∀ {p : Fin n → Type u} (f : ((i : Fin n) → p i) → τ) (args : (i : Fin n) → p i), (curry f).uncurry args = f args
p : Fin (n + 1) → Type u
f : ((i : Fin (n + 1)) → p i) → τ
args : (i : Fin (n + 1)) → p i
⊢ (curry f).uncurry args = f args

Tactic:
exact Eq.trans (ih _ _) (congrArg f (Fin.cons_self_tail args))

Result:
no goals

Proof state:
n : ℕ
p : Fin n → Type u
τ : Type u
f : ((i : Fin n) → p i) → τ
⊢ (curry f).uncurry = f

Tactic:
ext args

Result:
case h
n : ℕ
p : Fin n → Type u
τ : Type u
f : ((i : Fin n) → p i) → τ
args : (i : Fin n) → p i
⊢ (curry f).uncurry args = f args

Proof state:
case h
n : ℕ
p : Fin n → Type u
τ : Type u
f : ((i : Fin n) → p i) → τ
args : (i : Fin n) → p i
⊢ (curry f).uncurry args = f args

Tactic:
induction n with
| zero => exact congrArg f (Subsingleton.allEq _ _)
| succ n ih => exact Eq.trans (ih _ _) (congrArg f (Fin.cons_self_tail args))

Result:
no goals

Proof state:
case h.zero
τ : Type u
p : Fin 0 → Type u
f : ((i : Fin 0) → p i) → τ
args : (i : Fin 0) → p i
⊢ (curry f).uncurry args = f args

Tactic:
exact congrArg f (Subsingleton.allEq _ _)

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Whiskering.lean
lemma Sheaf.isSeparated {FA : A → A → Type*} {CA : A → Type*}
    [∀ X Y, FunLike (FA X Y) (CA X) (CA Y)] [ConcreteCategory A FA] [J.HasSheafCompose (forget A)]
    (F : Sheaf J A) : Presheaf.IsSeparated J F.val

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
A : Type u₂
inst✝³ : Category.{v₂, u₂} A
J : GrothendieckTopology C
FA : A → A → Type u_1
CA : A → Type u_2
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : J.HasSheafCompose (forget A)
F : Sheaf J A
⊢ Presheaf.IsSeparated J F.val

Tactic:
rintro X S hS x y h

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
A : Type u₂
inst✝³ : Category.{v₂, u₂} A
J : GrothendieckTopology C
FA : A → A → Type u_1
CA : A → Type u_2
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : J.HasSheafCompose (forget A)
F : Sheaf J A
X : C
S : Sieve X
hS : S ∈ J X
x y : ToType (F.val.obj (Opposite.op X))
h :
  ∀ (Y : C) (f : Y ⟶ X),
    S.arrows f → (ConcreteCategory.hom (F.val.map f.op)) x = (ConcreteCategory.hom (F.val.map f.op)) y
⊢ x = y

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
A : Type u₂
inst✝³ : Category.{v₂, u₂} A
J : GrothendieckTopology C
FA : A → A → Type u_1
CA : A → Type u_2
inst✝² : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝¹ : ConcreteCategory A FA
inst✝ : J.HasSheafCompose (forget A)
F : Sheaf J A
X : C
S : Sieve X
hS : S ∈ J X
x y : ToType (F.val.obj (Opposite.op X))
h :
  ∀ (Y : C) (f : Y ⟶ X),
    S.arrows f → (ConcreteCategory.hom (F.val.map f.op)) x = (ConcreteCategory.hom (F.val.map f.op)) y
⊢ x = y

Tactic:
exact (Presieve.isSeparated_of_isSheaf _ _ ((isSheaf_iff_isSheaf_of_type _ _).1
  ((sheafCompose J (forget A)).obj F).2) S hS).ext (fun _ _ hf => h _ _ hf)

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem lt_tsub_of_add_lt_right (hc : AddLECancellable c) (h : a + c < b) : a < b - c :=
  (hc.le_tsub_of_add_le_right h.le).lt_of_ne <| by
    rintro rfl
    exact h.not_le le_tsub_add

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
hc : AddLECancellable c
h : a + c < b
⊢ a ≠ b - c

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c : α
hc : AddLECancellable c
h : b - c + c < b
⊢ False

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c : α
hc : AddLECancellable c
h : b - c + c < b
⊢ False

Tactic:
exact h.not_le le_tsub_add

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem toFinset_union (l l' : List α) : (l ∪ l').toFinset = l.toFinset ∪ l'.toFinset

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
⊢ (l ∪ l').toFinset = l.toFinset ∪ l'.toFinset

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
a✝ : α
⊢ a✝ ∈ (l ∪ l').toFinset ↔ a✝ ∈ l.toFinset ∪ l'.toFinset

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
l l' : List α
a✝ : α
⊢ a✝ ∈ (l ∪ l').toFinset ↔ a✝ ∈ l.toFinset ∪ l'.toFinset

Tactic:
simp

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem _root_.FirstOrder.Language.Formula.realize_iAlls
    [Finite β] {φ : L.Formula (α ⊕ β)} {v : α → M} : (φ.iAlls β).Realize v ↔
      ∀ (i : β → M), φ.Realize (fun a => Sum.elim v i a)

Proof state:
case refine_2.e__xs
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x : Fin (Classical.choose ⋯) → M
⊢ (fun x_1 => x (natAdd (Classical.choose ⋯) x_1)) = default

Tactic:
funext i

Result:
case refine_2.e__xs.h
L : Language
M : Type w
inst✝¹ : L.Structure M
α : Type u'
β : Type v'
inst✝ : Finite β
φ : L.Formula (α ⊕ β)
v : α → M
e : β ≃ Fin (Classical.choose ⋯) := Classical.choice ⋯
x : Fin (Classical.choose ⋯) → M
i : Fin 0
⊢ x (natAdd (Classical.choose ⋯) i) = default i
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
@[to_additive (attr := simp) existing card_mul_cast_addConst]
lemma card_mul_cast_mulConst (A B : Finset G) : (#A * σₘ[A, B] : 𝕜) = #(A * B)

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑(#A) * σₘ[A, B] = ↑(#(A * B))

Tactic:
exact card_mul_mulConst _ _

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑(#A) * ↑σₘ[A, B] = ↑(#(A * B))

Tactic:
norm_cast

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑(#A) * σₘ[A, B] = ↑(#(A * B))
-- Mathlib/Topology/Order/ExtendFrom.lean
theorem eq_lim_at_right_extendFrom_Ioo [TopologicalSpace α] [LinearOrder α] [DenselyOrdered α]
    [OrderTopology α] [TopologicalSpace β] [T2Space β] {f : α → β} {a b : α} {lb : β} (hab : a < b)
    (hb : Tendsto f (𝓝[<] b) (𝓝 lb)) : extendFrom (Ioo a b) f b = lb

Proof state:
case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
lb : β
hab : a < b
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ Tendsto f (𝓝[Ioo a b] b) (𝓝 lb)

Tactic:
simpa [hab]

Result:
no goals

Proof state:
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
lb : β
hab : a < b
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ b ∈ Icc a b

Tactic:
simp only [le_of_lt hab, left_mem_Icc, right_mem_Icc]

Result:
no goals

Proof state:
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
lb : β
hab : a < b
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ b ∈ closure (Ioo a b)

Tactic:
rw [closure_Ioo hab.ne]

Result:
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
lb : β
hab : a < b
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ b ∈ Icc a b

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
lb : β
hab : a < b
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ extendFrom (Ioo a b) f b = lb

Tactic:
apply extendFrom_eq

Result:
case hx
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
lb : β
hab : a < b
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ b ∈ closure (Ioo a b)

case hf
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
f : α → β
a b : α
lb : β
hab : a < b
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ Tendsto f (𝓝[Ioo a b] b) (𝓝 lb)