harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/MonoCoprod.lean
theorem mono_inl_iff {A B : C} {c₁ c₂ : BinaryCofan A B} (hc₁ : IsColimit c₁) (hc₂ : IsColimit c₂) :
    Mono c₁.inl ↔ Mono c₂.inl

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B : C
c₁✝ c₂✝ : BinaryCofan A B
hc₁✝ : IsColimit c₁✝
hc₂✝ : IsColimit c₂✝
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ Mono c₁.inl → Mono c₂.inl

Tactic:
intro

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B : C
c₁✝ c₂✝ : BinaryCofan A B
hc₁✝ : IsColimit c₁✝
hc₂✝ : IsColimit c₂✝
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
x✝ : Mono c₁.inl
⊢ Mono c₂.inl

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B : C
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ ∀ (c₁ c₂ : BinaryCofan A B), IsColimit c₁ → IsColimit c₂ → Mono c₁.inl → Mono c₂.inl

Tactic:
intro c₁ c₂ hc₁ hc₂

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B : C
c₁✝ c₂✝ : BinaryCofan A B
hc₁✝ : IsColimit c₁✝
hc₂✝ : IsColimit c₂✝
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ Mono c₁.inl → Mono c₂.inl

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B : C
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ Mono c₁.inl ↔ Mono c₂.inl

Tactic:
suffices
  ∀ (c₁ c₂ : BinaryCofan A B) (_ : IsColimit c₁) (_ : IsColimit c₂) (_ : Mono c₁.inl),
    Mono c₂.inl
  by exact ⟨fun h₁ => this _ _ hc₁ hc₂ h₁, fun h₂ => this _ _ hc₂ hc₁ h₂⟩

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B : C
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ ∀ (c₁ c₂ : BinaryCofan A B), IsColimit c₁ → IsColimit c₂ → Mono c₁.inl → Mono c₂.inl

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B : C
c₁✝ c₂✝ : BinaryCofan A B
hc₁✝ : IsColimit c₁✝
hc₂✝ : IsColimit c₂✝
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
x✝ : Mono c₁.inl
⊢ Mono c₂.inl

Tactic:
simpa only [IsColimit.comp_coconePointUniqueUpToIso_hom] using
  mono_comp c₁.inl (hc₁.coconePointUniqueUpToIso hc₂).hom

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B : C
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
this : ∀ (c₁ c₂ : BinaryCofan A B), IsColimit c₁ → IsColimit c₂ → Mono c₁.inl → Mono c₂.inl
⊢ Mono c₁.inl ↔ Mono c₂.inl

Tactic:
exact ⟨fun h₁ => this _ _ hc₁ hc₂ h₁, fun h₂ => this _ _ hc₂ hc₁ h₂⟩

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
@[to_additive]
lemma LocallyLipschitzOn.div (hf : LocallyLipschitzOn s f) (hg : LocallyLipschitzOn s g) :
    LocallyLipschitzOn s fun x ↦ f x / g x

Proof state:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
s : Set α
hf : LocallyLipschitzOn s f
hg : LocallyLipschitzOn s g
⊢ LocallyLipschitzOn s fun x => f x / g x

Tactic:
simpa only [div_eq_mul_inv] using hf.mul hg.inv

Result:
no goals
-- Mathlib/Logic/Function/Iterate.lean
theorem iterate_succ' (n : ℕ) : f^[n.succ] = f ∘ f^[n]

Proof state:
α : Type u
f : α → α
n : ℕ
⊢ f^[n.succ] = f ∘ f^[n]

Tactic:
rw [iterate_succ, (Commute.self_iterate f n).comp_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem pmap_isSome {p : α → Prop} {f : ∀ (a : α), p a → β} {o : Option α} {h} :
    (pmap f o h).isSome = o.isSome

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
o : Option α
h : ∀ (a : α), a ∈ o → p a
⊢ (pmap f o h).isSome = o.isSome

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Taylor.lean
theorem taylor_monomial (i : ℕ) (k : R) : taylor r (monomial i k) = C k * (X + C r) ^ i

Proof state:
R : Type u_1
inst✝ : Semiring R
r : R
i : ℕ
k : R
⊢ (taylor r) ((monomial i) k) = C k * (X + C r) ^ i

Tactic:
simp [taylor_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem eval_apply_eq_zero_iff (v : V) : (eval K V) v = 0 ↔ v = 0

Proof state:
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
v : V
⊢ (eval K V) v = 0 ↔ v = 0

Tactic:
simpa only using SetLike.ext_iff.mp (eval_ker K V) v

Result:
no goals
-- Mathlib/CategoryTheory/Functor/FunctorHom.lean
lemma congr_app {f g : HomObj F G A} (h : f = g) (X : C)
    (a : A.obj X) : f.app X a = g.app X a

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A : C ⥤ Type w
f g : F.HomObj G A
h : f = g
X : C
a : A.obj X
⊢ f.app X a = g.app X a

Tactic:
subst h

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A : C ⥤ Type w
f : F.HomObj G A
X : C
a : A.obj X
⊢ f.app X a = f.app X a

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
A : C ⥤ Type w
f : F.HomObj G A
X : C
a : A.obj X
⊢ f.app X a = f.app X a

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Commute/Defs.lean
theorem right_comm (h : Commute b c) (a : S) : a * b * c = a * c * b

Proof state:
S : Type u_3
inst✝ : Semigroup S
b c : S
h : Commute b c
a : S
⊢ a * b * c = a * c * b

Tactic:
simp only [mul_assoc, h.eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem eq_natAbs_iff_mul_eq_zero : natAbs a = n ↔ (a - n) * (a + n) = 0

Proof state:
a : Int
n : Nat
⊢ a.natAbs = n ↔ (a - ↑n) * (a + ↑n) = 0

Tactic:
rw [natAbs_eq_iff, Int.mul_eq_zero, ← Int.sub_neg, Int.sub_eq_zero, Int.sub_eq_zero]

Result:
no goals
-- Mathlib/Analysis/Fourier/FourierTransform.lean
lemma fourierIntegralInv_eq_fourierIntegral_neg (f : V → E) (w : V) :
    𝓕⁻ f w = 𝓕 f (-w)

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
w : V
⊢ 𝓕⁻ f w = 𝓕 f (-w)

Tactic:
simp [fourierIntegral_eq, fourierIntegralInv_eq]

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_sub_nsmul [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b]
    (f : F) (x : G) (n : ℕ) : f (x - n • a) = f x - n • b

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
⊢ f (x - n • a) = f x - n • b

Tactic:
conv_rhs => rw [← sub_add_cancel x (n • a), map_add_nsmul, add_sub_cancel_right]

Result:
no goals
-- Mathlib/Computability/Language.lean
theorem mul_self_kstar_comm (l : Language α) : l∗ * l = l * l∗

Proof state:
α : Type u_1
l : Language α
⊢ l∗ * l = l * l∗

Tactic:
simp only [kstar_eq_iSup_pow, mul_iSup, iSup_mul, ← pow_succ, ← pow_succ']

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem card_typein_toType_lt (c : Cardinal) (x : c.ord.toType) :
    card (typein (α := c.ord.toType) (· < ·) x) < c

Proof state:
c : Cardinal.{u_1}
x : c.ord.toType
⊢ ((typein fun x1 x2 => x1 < x2).toRelEmbedding x).card < c

Tactic:
rw [← lt_ord]

Result:
c : Cardinal.{u_1}
x : c.ord.toType
⊢ (typein fun x1 x2 => x1 < x2).toRelEmbedding x < c.ord

Proof state:
c : Cardinal.{u_1}
x : c.ord.toType
⊢ (typein fun x1 x2 => x1 < x2).toRelEmbedding x < c.ord

Tactic:
apply typein_lt_self

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem isEmpty_alter_eq_isEmpty_erase (h : m.1.WF)  {k : α} {f : Option β → Option β} :
    (Const.alter m k f).1.isEmpty = ((m.erase k).1.isEmpty && (f (Const.get? m k)).isNone)

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 β
⊢ (alter m k f).val.isEmpty = ((m.erase k).val.isEmpty && (f (get? m k)).isNone)

Tactic:
simp_to_model [Const.alter, erase] using List.Const.isEmpty_alterKey_eq_isEmpty_eraseKey

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallySurjective.lean
lemma isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective_fac
    {F₁ F₂ F₃ : Cᵒᵖ ⥤ A} {f₁ : F₁ ⟶ F₂} {f₂ : F₂ ⟶ F₃} (f₃ : F₁ ⟶ F₃) (fac : f₁ ≫ f₂ = f₃)
    [IsLocallySurjective J f₃] [IsLocallyInjective J f₂] :
    IsLocallySurjective J f₁

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
f₃ : F₁ ⟶ F₃
fac : f₁ ≫ f₂ = f₃
inst✝¹ : IsLocallySurjective J f₃
inst✝ : IsLocallyInjective J f₂
⊢ IsLocallySurjective J f₁

Tactic:
subst fac

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallyInjective J f₂
inst✝ : IsLocallySurjective J (f₁ ≫ f₂)
⊢ IsLocallySurjective J f₁

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁴ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝³ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝² : ConcreteCategory A FA
F₁ F₂ F₃ : Cᵒᵖ ⥤ A
f₁ : F₁ ⟶ F₂
f₂ : F₂ ⟶ F₃
inst✝¹ : IsLocallyInjective J f₂
inst✝ : IsLocallySurjective J (f₁ ≫ f₂)
⊢ IsLocallySurjective J f₁

Tactic:
exact isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective J f₁ f₂

Result:
no goals
-- Mathlib/Data/Multiset/Sections.lean
theorem mem_sections {s : Multiset (Multiset α)} :
    ∀ {a}, a ∈ Sections s ↔ s.Rel (fun s a => a ∈ s) a

Proof state:
case cons
α : Type u_1
a✝ : Multiset α
s✝ : Multiset (Multiset α)
ih : ∀ {a : Multiset α}, a ∈ s✝.Sections ↔ Rel (fun s a => a ∈ s) s✝ a
⊢ ∀ {a : Multiset α}, a ∈ (a✝ ::ₘ s✝).Sections ↔ Rel (fun s a => a ∈ s) (a✝ ::ₘ s✝) a

Tactic:
simp [ih, rel_cons_left, eq_comm]

Result:
no goals

Proof state:
case empty
α : Type u_1
⊢ ∀ {a : Multiset α}, a ∈ Sections 0 ↔ Rel (fun s a => a ∈ s) 0 a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s : Multiset (Multiset α)
⊢ ∀ {a : Multiset α}, a ∈ s.Sections ↔ Rel (fun s a => a ∈ s) s a

Tactic:
induction s using Multiset.induction_on with
| empty => simp
| cons _ _ ih => simp [ih, rel_cons_left, eq_comm]

Result:
no goals
-- Mathlib/Algebra/Ring/Units.lean
theorem map_neg_one {F : Type*} [Ring β] [FunLike F α β] [RingHomClass F α β]
    (f : F) : map (f : α →* β) (-1) = -1

Proof state:
α : Type u
β : Type v
inst✝³ : Ring α
F : Type u_1
inst✝² : Ring β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
⊢ (map ↑f) (-1) = -1

Tactic:
simp only [Units.map_neg, map_one]

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
lemma surjective_π : Function.Surjective solution.π

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
h : solution.IsPresentation
⊢ Function.Surjective ⇑solution.π

Tactic:
simpa only [← surjective_fromQuotient_iff_surjective_π] using h.bijective.2

Result:
no goals
-- Mathlib/Algebra/Star/Basic.lean
theorem IsRightRegular.star [Mul R] [StarMul R] {x : R} (hx : IsRightRegular x) :
    IsLeftRegular (star x) :=
  fun a b h => star_injective <| hx <| by simpa using congr_arg Star.star h

Proof state:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
hx : IsRightRegular x
a b : R
h : (fun x_1 => star x * x_1) a = (fun x_1 => star x * x_1) b
⊢ (fun x_1 => x_1 * x) (star a) = (fun x_1 => x_1 * x) (star b)

Tactic:
simpa using congr_arg Star.star h

Result:
no goals
-- Mathlib/Data/Nat/Nth.lean
theorem nth_zero : nth p 0 = sInf (setOf p)

Proof state:
p : ℕ → Prop
⊢ nth p 0 = sInf (setOf p)

Tactic:
rw [nth_eq_sInf]

Result:
p : ℕ → Prop
⊢ sInf {x | p x ∧ ∀ k < 0, nth p k < x} = sInf (setOf p)

Proof state:
p : ℕ → Prop
⊢ sInf {x | p x ∧ ∀ k < 0, nth p k < x} = sInf (setOf p)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Grothendieck.lean
theorem arrow_stable (f : Y ⟶ X) (S : Sieve X) (h : J.Covers S f) {Z : C} (g : Z ⟶ Y) :
    J.Covers S (g ≫ f)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
h : Sieve.pullback f S ∈ J Y
Z : C
g : Z ⟶ Y
⊢ Sieve.pullback (g ≫ f) S ∈ J Z

Tactic:
simp [h, Sieve.pullback_comp]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
h : J.Covers S f
Z : C
g : Z ⟶ Y
⊢ J.Covers S (g ≫ f)

Tactic:
rw [covers_iff] at h ⊢

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
J : GrothendieckTopology C
f : Y ⟶ X
S : Sieve X
h : Sieve.pullback f S ∈ J Y
Z : C
g : Z ⟶ Y
⊢ Sieve.pullback (g ≫ f) S ∈ J Z
-- Mathlib/Algebra/Group/Defs.lean
theorem negSucc_zsmul {G} [SubNegMonoid G] (a : G) (n : ℕ) :
    Int.negSucc n • a = -((n + 1) • a)

Proof state:
G : Type u_2
inst✝ : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -((n + 1) • a)

Tactic:
rw [← natCast_zsmul]

Result:
G : Type u_2
inst✝ : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -(↑(n + 1) • a)

Proof state:
G : Type u_2
inst✝ : SubNegMonoid G
a : G
n : ℕ
⊢ Int.negSucc n • a = -(↑(n + 1) • a)

Tactic:
exact SubNegMonoid.zsmul_neg' n a

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem nfp_mul_one {a : Ordinal} (ha : 0 < a) : nfp (a * ·) 1 = a ^ ω

Proof state:
a : Ordinal.{u_1}
ha : 0 < a
⊢ ⨆ n, (fun x => a * x)^[n] 1 = ⨆ n, a ^ n

Tactic:
congr

Result:
case e_s
a : Ordinal.{u_1}
ha : 0 < a
⊢ (fun n => (fun x => a * x)^[n] 1) = fun n => a ^ n

Proof state:
case e_s.h.zero
a : Ordinal.{u_1}
ha : 0 < a
⊢ (fun x => a * x)^[0] 1 = a ^ 0

Tactic:
rw [pow_zero, iterate_zero_apply]

Result:
no goals

Proof state:
case e_s
a : Ordinal.{u_1}
ha : 0 < a
⊢ (fun n => (fun x => a * x)^[n] 1) = fun n => a ^ n

Tactic:
funext n

Result:
case e_s.h
a : Ordinal.{u_1}
ha : 0 < a
n : ℕ
⊢ (fun x => a * x)^[n] 1 = a ^ n

Proof state:
case e_s.h
a : Ordinal.{u_1}
ha : 0 < a
n : ℕ
⊢ (fun x => a * x)^[n] 1 = a ^ n

Tactic:
induction' n with n hn

Result:
case e_s.h.zero
a : Ordinal.{u_1}
ha : 0 < a
⊢ (fun x => a * x)^[0] 1 = a ^ 0

case e_s.h.succ
a : Ordinal.{u_1}
ha : 0 < a
n : ℕ
hn : (fun x => a * x)^[n] 1 = a ^ n
⊢ (fun x => a * x)^[n + 1] 1 = a ^ (n + 1)

Proof state:
a : Ordinal.{u_1}
ha : 0 < a
⊢ nfp (fun x => a * x) 1 = a ^ ω

Tactic:
rw [← iSup_iterate_eq_nfp, ← iSup_pow ha]

Result:
a : Ordinal.{u_1}
ha : 0 < a
⊢ ⨆ n, (fun x => a * x)^[n] 1 = ⨆ n, a ^ n

Proof state:
case e_s.h.succ
a : Ordinal.{u_1}
ha : 0 < a
n : ℕ
hn : (fun x => a * x)^[n] 1 = a ^ n
⊢ (fun x => a * x)^[n + 1] 1 = a ^ (n + 1)

Tactic:
rw [iterate_succ_apply', Nat.add_comm, pow_add, pow_one, hn]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem isCycle_of_prime_order' {σ : Perm α} (h1 : (orderOf σ).Prime)
    (h2 : Fintype.card α < 2 * orderOf σ) : σ.IsCycle

Proof state:
α : Type u_1
inst✝ : Fintype α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : Fintype.card α < 2 * orderOf σ
⊢ σ.IsCycle

Tactic:
classical exact isCycle_of_prime_order h1 (lt_of_le_of_lt σ.support.card_le_univ h2)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Fintype α
σ : Perm α
h1 : Nat.Prime (orderOf σ)
h2 : Fintype.card α < 2 * orderOf σ
⊢ σ.IsCycle

Tactic:
exact isCycle_of_prime_order h1 (lt_of_le_of_lt σ.support.card_le_univ h2)

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean
theorem δ_comp_σ_of_gt {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.castSucc < i) :
    δ i.succ ≫ σ j.castSucc = σ j ≫ δ i

Proof state:
case h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ FreeSimplexQuiver.homRel
    (Paths.of.map (FreeSimplexQuiver.Hom.δ i.succ) ≫ Paths.of.map (FreeSimplexQuiver.Hom.σ j.castSucc))
    (Paths.of.map (FreeSimplexQuiver.Hom.σ j) ≫ Paths.of.map (FreeSimplexQuiver.Hom.δ i))

Tactic:
exact FreeSimplexQuiver.homRel.δ_comp_σ_of_gt H

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ δ i.succ ≫ σ j.castSucc = σ j ≫ δ i

Tactic:
apply CategoryTheory.Quotient.sound

Result:
case h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ FreeSimplexQuiver.homRel
    (Paths.of.map (FreeSimplexQuiver.Hom.δ i.succ) ≫ Paths.of.map (FreeSimplexQuiver.Hom.σ j.castSucc))
    (Paths.of.map (FreeSimplexQuiver.Hom.σ j) ≫ Paths.of.map (FreeSimplexQuiver.Hom.δ i))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem negSucc_mul_negOfNat (m n : Nat) : -[m+1] * negOfNat n = ofNat (succ m * n)

Proof state:
m n : Nat
⊢ -[m+1] * negOfNat n = ofNat (m.succ * n)

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem fract_eq_fract (m n : E) : fract b m = fract b n ↔ -m + n ∈ span ℤ (Set.range b)

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m n : E
⊢ fract b m = fract b n ↔ -m + n ∈ span ℤ (Set.range ⇑b)

Tactic:
rw [eq_comm, Basis.ext_elem_iff b]

Result:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m n : E
⊢ (∀ (i : ι), (b.repr (fract b n)) i = (b.repr (fract b m)) i) ↔ -m + n ∈ span ℤ (Set.range ⇑b)

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m n : E
⊢ fract b m = fract b n ↔ -m + n ∈ span ℤ (Set.range ⇑b)

Tactic:
classical
rw [eq_comm, Basis.ext_elem_iff b]
simp_rw [repr_fract_apply, Int.fract_eq_fract, eq_comm, Basis.mem_span_iff_repr_mem,
  sub_eq_neg_add, map_add, map_neg, Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply,
  Pi.neg_apply, ← eq_intCast (algebraMap ℤ K) _, Set.mem_range]

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m n : E
⊢ (∀ (i : ι), (b.repr (fract b n)) i = (b.repr (fract b m)) i) ↔ -m + n ∈ span ℤ (Set.range ⇑b)

Tactic:
simp_rw [repr_fract_apply, Int.fract_eq_fract, eq_comm, Basis.mem_span_iff_repr_mem,
  sub_eq_neg_add, map_add, map_neg, Finsupp.coe_add, Finsupp.coe_neg, Pi.add_apply,
  Pi.neg_apply, ← eq_intCast (algebraMap ℤ K) _, Set.mem_range]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem average_zero_measure (f : α → E) : ⨍ x, f x ∂(0 : Measure α) = 0

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
⊢ ⨍ (x : α), f x ∂0 = 0

Tactic:
rw [average, smul_zero, integral_zero_measure]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem mul_left_inj (a : αˣ) {b c : α} : b * a = c * a ↔ b = c :=
  ⟨fun h => by simpa only [mul_inv_cancel_right] using congr_arg (fun x : α => x * ↑(a⁻¹ : αˣ)) h,
    congr_arg (· * a.val)⟩

Proof state:
α : Type u
inst✝ : Monoid α
a : αˣ
b c : α
h : b * ↑a = c * ↑a
⊢ b = c

Tactic:
simpa only [mul_inv_cancel_right] using congr_arg (fun x : α => x * ↑(a⁻¹ : αˣ)) h

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem coe_int_sub_eq_ite {n : Nat} (u v : Fin n) :
    ((u - v : Fin n) : Int) = if v ≤ u then (u - v : Int) else (u - v : Int) + n

Proof state:
case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑⟨(n - ↑v + ↑u) % n, ⋯⟩ = ↑↑u - ↑↑v + ↑n

Tactic:
rw [ofNat_emod, Int.emod_eq_of_lt] <;> omega

Result:
no goals

Proof state:
case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑↑⟨(n - ↑v + ↑u) % n, ⋯⟩ = ↑↑u - ↑↑v

Tactic:
rw [ofNat_emod, Int.emod_eq_sub_self_emod, Int.emod_eq_of_lt] <;> omega

Result:
no goals

Proof state:
n : ℕ
u v : Fin n
⊢ ↑↑(u - v) = if v ≤ u then ↑↑u - ↑↑v else ↑↑u - ↑↑v + ↑n

Tactic:
rw [Fin.sub_def]

Result:
n : ℕ
u v : Fin n
⊢ ↑↑⟨(n - ↑v + ↑u) % n, ⋯⟩ = if v ≤ u then ↑↑u - ↑↑v else ↑↑u - ↑↑v + ↑n

Proof state:
n : ℕ
u v : Fin n
⊢ ↑↑⟨(n - ↑v + ↑u) % n, ⋯⟩ = if v ≤ u then ↑↑u - ↑↑v else ↑↑u - ↑↑v + ↑n

Tactic:
split

Result:
case isTrue
n : ℕ
u v : Fin n
h✝ : v ≤ u
⊢ ↑↑⟨(n - ↑v + ↑u) % n, ⋯⟩ = ↑↑u - ↑↑v

case isFalse
n : ℕ
u v : Fin n
h✝ : ¬v ≤ u
⊢ ↑↑⟨(n - ↑v + ↑u) % n, ⋯⟩ = ↑↑u - ↑↑v + ↑n
-- Mathlib/Data/Fin/Basic.lean
lemma succAbove_pred_of_lt (p i : Fin (n + 1)) (h : p < i)
    (hi := Fin.ne_of_gt <| Fin.lt_of_le_of_lt p.zero_le h) : succAbove p (i.pred hi) = i

Proof state:
n : ℕ
p i : Fin (n + 1)
h : p < i
hi : optParam (i ≠ 0) ⋯
⊢ p.succAbove (i.pred hi) = i

Tactic:
rw [succAbove_of_lt_succ _ _ (succ_pred _ _ ▸ h), succ_pred]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
lemma InjOn.image (h : s.InjOn f) : s.powerset.InjOn (image f) :=
  fun s₁ hs₁ s₂ hs₂ h' ↦ by rw [← h.preimage_image_inter hs₁, h', h.preimage_image_inter hs₂]

Proof state:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
s₁ : Set α
hs₁ : s₁ ∈ 𝒫 s
s₂ : Set α
hs₂ : s₂ ∈ 𝒫 s
h' : f '' s₁ = f '' s₂
⊢ s₁ = s₂

Tactic:
rw [← h.preimage_image_inter hs₁, h', h.preimage_image_inter hs₂]

Result:
no goals
-- Mathlib/Topology/Order/UpperLowerSetTopology.lean
lemma isOpen_iff_isLowerSet : IsOpen s ↔ IsLowerSet s

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
s : Set α
⊢ IsOpen s ↔ IsLowerSet s

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem gcd_insert [DecidableEq β] {b : β} :
    (insert b s : Finset β).gcd f = GCDMonoid.gcd (f b) (s.gcd f)

Proof state:
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
⊢ (insert b s).gcd f = GCDMonoid.gcd (f b) (s.gcd f)

Tactic:
by_cases h : b ∈ s

Result:
case pos
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∈ s
⊢ (insert b s).gcd f = GCDMonoid.gcd (f b) (s.gcd f)

case neg
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∉ s
⊢ (insert b s).gcd f = GCDMonoid.gcd (f b) (s.gcd f)

Proof state:
case neg
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∉ s
⊢ (insert b s).gcd f = GCDMonoid.gcd (f b) (s.gcd f)

Tactic:
apply fold_insert h

Result:
no goals

Proof state:
case pos
α : Type u_2
β : Type u_3
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
s : Finset β
f : β → α
inst✝ : DecidableEq β
b : β
h : b ∈ s
⊢ (insert b s).gcd f = GCDMonoid.gcd (f b) (s.gcd f)

Tactic:
rw [insert_eq_of_mem h,
  (gcd_eq_right_iff (f b) (s.gcd f) (Multiset.normalize_gcd (s.1.map f))).2 (gcd_dvd h)]

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
theorem add_ne_top : a + b ≠ ∞ ↔ a ≠ ∞ ∧ b ≠ ∞

Proof state:
a b : ℝ≥0∞
⊢ a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤

Tactic:
simpa only [lt_top_iff_ne_top] using add_lt_top

Result:
no goals