harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_sub_const_Icc : (fun x => x - a) ⁻¹' Icc b c = Icc (b + a) (c + a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b c : α
⊢ (fun x => x - a) ⁻¹' Icc b c = Icc (b + a) (c + a)

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/Data/List/Map2.lean
theorem zipRight_eq_zipRight' : zipRight as bs = (zipRight' as bs).fst

Proof state:
α : Type u
β : Type v
as : List α
bs : List β
⊢ as.zipRight bs = (as.zipRight' bs).fst

Tactic:
induction as generalizing bs <;> cases bs <;> simp [*]

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_ex : θ.ex.Realize v xs ↔ ∃ a : M, θ.Realize v (Fin.snoc xs a)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
θ : L.BoundedFormula α l.succ
v : α → M
xs : Fin l → M
⊢ (∃'θ).Realize v xs ↔ ∃ a, θ.Realize v (snoc xs a)

Tactic:
rw [BoundedFormula.ex, realize_not, realize_all, not_forall]

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
θ : L.BoundedFormula α l.succ
v : α → M
xs : Fin l → M
⊢ (∃ x, ¬(∼θ).Realize v (snoc xs x)) ↔ ∃ a, θ.Realize v (snoc xs a)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
l : ℕ
θ : L.BoundedFormula α l.succ
v : α → M
xs : Fin l → M
⊢ (∃ x, ¬(∼θ).Realize v (snoc xs x)) ↔ ∃ a, θ.Realize v (snoc xs a)

Tactic:
simp_rw [realize_not, Classical.not_not]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem ext_iff' (v w : VectorMeasure α M) : v = w ↔ ∀ i : Set α, v i = w i

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : TopologicalSpace M
v w : VectorMeasure α M
⊢ v = w ↔ ∀ (i : Set α), ↑v i = ↑w i

Tactic:
rw [← coe_injective.eq_iff, funext_iff]

Result:
no goals
-- Mathlib/Data/Sign.lean
private lemma le_trans (a b c : SignType) (_ : a ≤ b) (_ : b ≤ c) : a ≤ c

Proof state:
a b c : SignType
x✝¹ : a ≤ b
x✝ : b ≤ c
⊢ a ≤ c

Tactic:
cases a <;> cases b <;> cases c <;> tauto

Result:
no goals
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalarsSum_of_subsingleton [Subsingleton E] {x : E} : ofScalarsSum c x = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
c : ℕ → 𝕜
inst✝ : Subsingleton E
x : E
⊢ ofScalarsSum c x = 0

Tactic:
simp [Subsingleton.eq_zero x, Subsingleton.eq_zero (1 : E)]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem rightUnitor_tensor_inv (X Y : C) :
    (ρ_ (X ⊗ Y)).inv = X ◁ (ρ_ Y).inv ≫ (α_ X Y (𝟙_ C)).inv

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (ρ_ (X ⊗ Y)).inv = X ◁ (ρ_ Y).inv ≫ (α_ X Y (𝟙_ C)).inv

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Basic.lean
theorem Convex.affinity (hs : Convex 𝕜 s) (z : E) (c : 𝕜) :
    Convex 𝕜 ((fun x => z + c • x) '' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedCommSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z : E
c : 𝕜
⊢ Convex 𝕜 ((fun x => z + c • x) '' s)

Tactic:
simpa only [← image_smul, ← image_vadd, image_image] using (hs.smul c).vadd z

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Chain.lean
@[simp] lemma chainBotCoeff_neg : chainBotCoeff (-α) β = chainTopCoeff α β

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
⊢ chainBotCoeff (-α) β = chainTopCoeff α β

Tactic:
rw [← chainTopCoeff_neg, neg_neg]

Result:
no goals
-- Mathlib/Data/Part.lean
theorem bind_some (a : α) (f : α → Part β) : (some a).bind f = f a :=
  ext <| by simp

Proof state:
α : Type u_1
β : Type u_2
a : α
f : α → Part β
⊢ ∀ (a_1 : β), a_1 ∈ (some a).bind f ↔ a_1 ∈ f a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iInter_iInter_eq' {f : ι → α} {g : α → Set β} :
    ⋂ (x) (y) (_ : f y = x), g x = ⋂ y, g (f y)

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → α
g : α → Set β
⊢ ⋂ x, ⋂ y, ⋂ (_ : f y = x), g x = ⋂ y, g (f y)

Tactic:
simpa using biInter_range

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem not_anisotropic_iff_exists (Q : QuadraticMap R M N) :
    ¬Anisotropic Q ↔ ∃ x, x ≠ 0 ∧ Q x = 0

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
⊢ ¬Q.Anisotropic ↔ ∃ x, x ≠ 0 ∧ Q x = 0

Tactic:
simp only [Anisotropic, not_forall, exists_prop, and_comm]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[simp]
lemma mul_le_iff_le_one_left [MulPosMono α] [MulPosReflectLE α] (b0 : 0 < b) : a * b ≤ b ↔ a ≤ 1 :=
  Iff.trans (by rw [one_mul]) (mul_le_mul_right b0)

Proof state:
α : Type u_3
a b : α
inst✝⁴ : MulOneClass α
inst✝³ : Zero α
inst✝² : Preorder α
inst✝¹ : MulPosMono α
inst✝ : MulPosReflectLE α
b0 : 0 < b
⊢ a * b ≤ b ↔ a * b ≤ 1 * b

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
@[simp]
lemma postcomp_uniq_symm : solution'.postcomp (uniq h h').symm.toLinearMap = 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
N : Type v'
inst✝¹ : AddCommGroup N
inst✝ : Module A N
solution' : relations.Solution N
h' : solution'.IsPresentation
⊢ solution'.postcomp ↑(h.uniq h').symm = solution

Tactic:
simp [uniq]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem pi_inter_distrib : (s.pi fun i => t i ∩ t₁ i) = s.pi t ∩ s.pi t₁ :=
  ext fun x => by simp only [forall_and, mem_pi, mem_inter_iff]

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t t₁ : (i : ι) → Set (α i)
x : (i : ι) → α i
⊢ (x ∈ s.pi fun i => t i ∩ t₁ i) ↔ x ∈ s.pi t ∩ s.pi t₁

Tactic:
simp only [forall_and, mem_pi, mem_inter_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
theorem map_id {f : StructuredArrow S T} : (map (𝟙 S)).obj f = f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
f : StructuredArrow S T
⊢ (map (𝟙 S)).obj (mk f.hom) = mk f.hom

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
f : StructuredArrow S T
⊢ (map (𝟙 S)).obj f = f

Tactic:
rw [eq_mk f]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
f : StructuredArrow S T
⊢ (map (𝟙 S)).obj (mk f.hom) = mk f.hom
-- Mathlib/Order/Basic.lean
theorem const_le_const : const β a ≤ const β b ↔ a ≤ b

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Nonempty β
a b : α
⊢ const β a ≤ const β b ↔ a ≤ b

Tactic:
simp [Pi.le_def]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem imageSubobject_le {A B : C} {X : Subobject B} (f : A ⟶ B) [HasImage f] (h : A ⟶ X)
    (w : h ≫ X.arrow = f) : imageSubobject f ≤ X :=
  Subobject.le_of_comm
    ((imageSubobjectIso f).hom ≫
      image.lift
        { I := (X : C)
          e := h
          m := X.arrow })
    (by rw [assoc, image.lift_fac, imageSubobject_arrow])

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
A B : C
X : Subobject B
f : A ⟶ B
inst✝ : HasImage f
h : A ⟶ underlying.obj X
w : h ≫ X.arrow = f
⊢ ((imageSubobjectIso f).hom ≫ image.lift (MonoFactorisation.mk (underlying.obj X) X.arrow h ⋯)) ≫ X.arrow =
    (imageSubobject f).arrow

Tactic:
rw [assoc, image.lift_fac, imageSubobject_arrow]

Result:
no goals
-- Mathlib/RingTheory/HopfAlgebra/MonoidAlgebra.lean
theorem antipode_C_mul_T (a : A) (n : ℤ) :
    HopfAlgebra.antipode (R := R) (C a * T n) = C (HopfAlgebra.antipode (R := R) a) * T (-n)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : HopfAlgebra R A
a : A
n : ℤ
⊢ antipode (C a * T n) = C (antipode a) * T (-n)

Tactic:
simp [← single_eq_C_mul_T]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem cardinalMk_adjoin_le {E : Type u} [Field E] [Algebra F E] (s : Set E) :
    #(adjoin F s) ≤ #F ⊔ #s ⊔ ℵ₀

Proof state:
F : Type u
inst✝² : Field F
E : Type u
inst✝¹ : Field E
inst✝ : Algebra F E
s : Set E
⊢ #↥(adjoin F s) ≤ #F ⊔ #↑s ⊔ ℵ₀

Tactic:
simpa using lift_cardinalMk_adjoin_le F s

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
@[simp] lemma shadow_iterate_empty (k : ℕ) : ∂^[k] (∅ : Finset (Finset α)) = ∅

Proof state:
α : Type u_1
inst✝ : DecidableEq α
k : ℕ
⊢ ∂ ^[k] ∅ = ∅

Tactic:
induction k <;> simp [*, shadow_empty]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_eq_self : a / b = a ↔ b = 1

Proof state:
G : Type u_3
inst✝ : Group G
a b : G
⊢ a / b = a ↔ b = 1

Tactic:
rw [div_eq_mul_inv, mul_right_eq_self, inv_eq_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/OfFn.lean
theorem getLast_ofFn {n} (f : Fin n → α) (h : ofFn f ≠ []) :
    (ofFn f).getLast h = f ⟨n - 1, Nat.sub_one_lt (mt ofFn_eq_nil_iff.2 h)⟩

Proof state:
α : Type u_1
n : Nat
f : Fin n → α
h : ofFn f ≠ []
⊢ (ofFn f).getLast h = f ⟨n - 1, ⋯⟩

Tactic:
simp [getLast_eq_getElem, length_ofFn, List.getElem_ofFn]

Result:
no goals
-- Mathlib/Data/Multiset/Fintype.lean
theorem map_univ {β : Type*} (m : Multiset α) (f : α → β) :
    ((Finset.univ : Finset m).val.map fun (x : m) ↦ f (x : α)) = m.map f

Proof state:
α : Type u_1
inst✝ : DecidableEq α
β : Type u_3
m : Multiset α
f : α → β
⊢ map (fun x => f x.fst) Finset.univ.val = map f m

Tactic:
erw [← Multiset.map_map, Multiset.map_univ_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem all_reverse {l : List α} : l.reverse.all f = l.all f

Proof state:
α : Type u_1
f : α → Bool
l : List α
⊢ l.reverse.all f = l.all f

Tactic:
induction l <;> simp_all [Bool.and_comm]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigO_iff_isBigOWith : f =O[l] g ↔ ∃ c : ℝ, IsBigOWith c l f g

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
⊢ f =O[l] g ↔ ∃ c, IsBigOWith c l f g

Tactic:
rw [IsBigO_def]

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem subtype_map (p : α → Prop) [DecidablePred p] {s : Finset α} :
    (s.subtype p).map (Embedding.subtype _) = s.filter p

Proof state:
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
⊢ map (Embedding.subtype p) (Finset.subtype p s) = filter p s

Tactic:
ext x

Result:
case h
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
x : α
⊢ x ∈ map (Embedding.subtype p) (Finset.subtype p s) ↔ x ∈ filter p s

Proof state:
case h
α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
s : Finset α
x : α
⊢ x ∈ map (Embedding.subtype p) (Finset.subtype p s) ↔ x ∈ filter p s

Tactic:
simp [@and_comm _ (_ = _), @and_left_comm _ (_ = _), @and_comm (p x) (x ∈ s)]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Field.lean
/-- If `r` is a negative constant, `fun x ↦ f x / r` tends to negative infinity along a filter `l`
if and only if `f` tends to infinity along `l`. -/
lemma tendsto_div_const_atBot_of_neg (hr : r < 0) :
    Tendsto (fun x ↦ f x / r) l atBot ↔ Tendsto f l atTop

Proof state:
α : Type u_1
β : Type u_2
inst✝ : LinearOrderedField α
l : Filter β
f : β → α
r : α
hr : r < 0
⊢ Tendsto (fun x => f x / r) l atBot ↔ Tendsto f l atTop

Tactic:
simp [div_eq_mul_inv, tendsto_mul_const_atBot_of_neg, hr]

Result:
no goals
-- Mathlib/Algebra/Order/Rearrangement.lean
theorem MonovaryOn.sum_comp_perm_smul_lt_sum_smul_iff (hfg : MonovaryOn f g s)
    (hσ : {x | σ x ≠ x} ⊆ s) :
    ∑ i ∈ s, f (σ i) • g i < ∑ i ∈ s, f i • g i ↔ ¬MonovaryOn (f ∘ σ) g s

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : MonovaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f (σ i) • g i < ∑ i ∈ s, f i • g i ↔ ¬MonovaryOn (f ∘ ⇑σ) g ↑s

Tactic:
simp [← hfg.sum_comp_perm_smul_eq_sum_smul_iff hσ, lt_iff_le_and_ne,
  hfg.sum_comp_perm_smul_le_sum_smul hσ]

Result:
no goals
-- Mathlib/Tactic/Abel.lean
lemma subst_into_smul {α} [AddCommMonoid α]
    (l r tl tr t) (prl : l = tl) (prr : r = tr)
    (prt : @smul α _ tl tr = t) : smul l r = t

Proof state:
α : Type u_1
inst✝ : AddCommMonoid α
l : ℕ
r : α
tl : ℕ
tr t : α
prl : l = tl
prr : r = tr
prt : smul tl tr = t
⊢ smul l r = t

Tactic:
simp [prl, prr, prt]

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem add_rat_iff : LiouvilleWith p (x + r) ↔ LiouvilleWith p x :=
  ⟨fun h => by simpa using h.add_rat (-r), fun h => h.add_rat r⟩

Proof state:
p x : ℝ
r : ℚ
h : LiouvilleWith p (x + ↑r)
⊢ LiouvilleWith p x

Tactic:
simpa using h.add_rat (-r)

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
@[simp]
protected lemma map_single [Zero S] (f : ZeroHom R S) : (single a r).map f = single a (f r)

Proof state:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a : Γ
r : R
inst✝ : Zero S
f : ZeroHom R S
⊢ ((single a) r).map f = (single a) (f r)

Tactic:
ext g

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a : Γ
r : R
inst✝ : Zero S
f : ZeroHom R S
g : Γ
⊢ (((single a) r).map f).coeff g = ((single a) (f r)).coeff g

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a : Γ
r : R
inst✝ : Zero S
f : ZeroHom R S
g : Γ
⊢ (((single a) r).map f).coeff g = ((single a) (f r)).coeff g

Tactic:
by_cases h : g = a <;> simp [h]

Result:
no goals
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem l_iSup₂ (gc : GaloisConnection l u) {f : ∀ i, κ i → α} :
    l (⨆ (i) (j), f i j) = ⨆ (i) (j), l (f i j)

Proof state:
α : Type u
β : Type v
ι : Sort x
κ : ι → Sort u_1
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
f : (i : ι) → κ i → α
⊢ l (⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, l (f i j)

Tactic:
simp_rw [gc.l_iSup]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem utf8Len_reverseAux (cs₁ cs₂) :
    utf8Len (cs₁.reverseAux cs₂) = utf8Len cs₁ + utf8Len cs₂

Proof state:
cs₁ cs₂ : List Char
⊢ utf8Len (cs₁.reverseAux cs₂) = utf8Len cs₁ + utf8Len cs₂

Tactic:
induction cs₁ generalizing cs₂ <;> simp_all [← Nat.add_assoc, Nat.add_right_comm]

Result:
no goals
-- Mathlib/Combinatorics/Additive/ErdosGinzburgZiv.lean
theorem ZMod.erdos_ginzburg_ziv (a : ι → ZMod n) (hs : 2 * n - 1 ≤ #s) :
    ∃ t ⊆ s, #t = n ∧ ∑ i ∈ t, a i = 0

Proof state:
ι : Type u_1
n : ℕ
s : Finset ι
a : ι → ZMod n
hs : 2 * n - 1 ≤ #s
⊢ ∃ t ⊆ s, #t = n ∧ ∑ i ∈ t, a i = 0

Tactic:
simpa [← ZMod.intCast_zmod_eq_zero_iff_dvd] using Int.erdos_ginzburg_ziv (ZMod.cast ∘ a) hs

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Lemmas.lean
theorem size_set! (a : Array α) (i v) : (a.set! i v).size = a.size

Proof state:
α : Type u_1
a : Array α
i : Nat
v : α
⊢ (a.set! i v).size = a.size

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem id_tensor_associator_naturality {X Y Z Z' : C} (h : Z ⟶ Z') :
    (𝟙 (X ⊗ Y) ⊗ h) ≫ (α_ X Y Z').hom = (α_ X Y Z).hom ≫ (𝟙 X ⊗ 𝟙 Y ⊗ h)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
h : Z ⟶ Z'
⊢ (𝟙 (X ⊗ Y) ⊗ h) ≫ (α_ X Y Z').hom = (α_ X Y Z).hom ≫ (𝟙 X ⊗ 𝟙 Y ⊗ h)

Tactic:
rw [← tensor_id, associator_naturality]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem getLast?_enum (l : List α) :
    l.enum.getLast? = l.getLast?.map fun a => (l.length - 1, a)

Proof state:
α : Type u_1
l : List α
⊢ l.enum.getLast? = Option.map (fun a => (l.length - 1, a)) l.getLast?

Tactic:
simp [getLast?_eq_getElem?]

Result:
no goals
-- Mathlib/Analysis/Convex/Basic.lean
theorem Convex.sub (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) : Convex 𝕜 (s - t)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 (s + -t)

Tactic:
exact hs.add ht.neg

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 (s - t)

Tactic:
rw [sub_eq_add_neg]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 (s + -t)
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma uIcc_injective_left (a : α) : Injective (uIcc a)

Proof state:
α : Type u_1
inst✝ : DistribLattice α
a : α
⊢ Injective (uIcc a)

Tactic:
simpa only [uIcc_comm] using uIcc_injective_right a

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem biUnion_preimage_singleton (f : α → β) (s : Set β) : ⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ ⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' s

Tactic:
rw [← preimage_iUnion₂, biUnion_of_singleton]

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
protected lemma eq_sub_of_add_eq (hstu : s + t = u) : s = u - t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
hstu : s + t = u
⊢ s = u - t

Tactic:
rw [← hstu, Multiset.add_sub_cancel_right]

Result:
no goals
-- Mathlib/FieldTheory/Fixed.lean
theorem rank_le_card : Module.rank (FixedPoints.subfield G F) F ≤ Fintype.card G :=
  rank_le fun s hs => by
    simpa only [rank_fun', Cardinal.mk_coe_finset, Finset.coe_sort_coe, Cardinal.lift_natCast,
      Nat.cast_le] using
      (linearIndependent_smul_of_linearIndependent G F hs).cardinal_lift_le_rank

Proof state:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
s : Finset F
hs : LinearIndependent ↥(subfield G F) fun i => ↑i
⊢ #s ≤ Fintype.card G

Tactic:
simpa only [rank_fun', Cardinal.mk_coe_finset, Finset.coe_sort_coe, Cardinal.lift_natCast,
  Nat.cast_le] using
  (linearIndependent_smul_of_linearIndependent G F hs).cardinal_lift_le_rank

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem aeval_S [Algebra R R'] (x : R') (n : ℤ) : aeval x (S R n) = (S R' n).eval x

Proof state:
R : Type u_1
R' : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing R'
inst✝ : Algebra R R'
x : R'
n : ℤ
⊢ (aeval x) (S R n) = eval x (S R' n)

Tactic:
rw [aeval_def, eval₂_eq_eval_map, map_S]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem Module.finrank_fin_fun {n : ℕ} : finrank R (Fin n → R) = n

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
n : ℕ
⊢ finrank R (Fin n → R) = n

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem mk'_add (x y : B) (hx : IsIntegral R x) (hy : IsIntegral R y) :
    mk' A (x + y) (hx.add hy) = mk' A x hx + mk' A y hy :=
  algebraMap_injective A R B <| by simp only [algebraMap_mk', RingHom.map_add]

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsIntegralClosure A R B
x y : B
hx : IsIntegral R x
hy : IsIntegral R y
⊢ (algebraMap A B) (mk' A (x + y) ⋯) = (algebraMap A B) (mk' A x hx + mk' A y hy)

Tactic:
simp only [algebraMap_mk', RingHom.map_add]

Result:
no goals
-- Mathlib/NumberTheory/PrimeCounting.lean
@[simp]
lemma primeCounting'_eq_zero_iff {n : ℕ} : n.primeCounting' = 0 ↔ n ≤ 2

Proof state:
n : ℕ
⊢ π' n = 0 ↔ n ≤ 2

Tactic:
rw [primeCounting', Nat.count_eq_zero ⟨_, Nat.prime_two⟩, Nat.nth_prime_zero_eq_two]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Swap.lean
lemma mul_swap_of_ne {i j b : n} {a : m} (hbi : b ≠ i) (hbj : b ≠ j) (g : Matrix m n R) :
    (g * swap R i j) a b = g a b

Proof state:
R : Type u_1
n : Type u_2
m : Type u_3
inst✝² : Semiring R
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j b : n
a : m
hbi : b ≠ i
hbj : b ≠ j
g : Matrix m n R
⊢ (g * swap R i j) a b = g a b

Tactic:
simp [swap, PEquiv.mul_toMatrix_toPEquiv, Equiv.swap_apply_of_ne_of_ne hbi hbj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem find?_range_eq_none {n : Nat} {p : Nat → Bool} :
    (range n).find? p = none ↔ ∀ i, i < n → !p i

Proof state:
n : Nat
p : Nat → Bool
⊢ find? p (range n) = none ↔ ∀ (i : Nat), i < n → (!p i) = true

Tactic:
simp [range_eq_range']

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma changeLevel_toUnitHom {m : ℕ} (hm : n ∣ m) :
    (changeLevel hm χ).toUnitHom = χ.toUnitHom.comp (ZMod.unitsMap hm)

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
m : ℕ
hm : n ∣ m
⊢ toUnitHom ((changeLevel hm) χ) = (toUnitHom χ).comp (ZMod.unitsMap hm)

Tactic:
simp [changeLevel]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_hom₂_nonempty {l : List ι} (f : M → N → P)
    (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d) (f₁ : ι → M) (f₂ : ι → N) (hl : l ≠ []) :
    (l.map fun i => f (f₁ i) (f₂ i)).prod = f (l.map f₁).prod (l.map f₂).prod

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl✝ : l ≠ []
x : ι
xs : List ι
hl : x :: xs ≠ []
⊢ (map (fun i => f (f₁ i) (f₂ i)) (x :: xs)).prod = f (map f₁ (x :: xs)).prod (map f₂ (x :: xs)).prod

Tactic:
induction xs generalizing x <;> aesop

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l : List ι
f : M → N → P
hf : ∀ (a b : M) (c d : N), f (a * b) (c * d) = f a c * f b d
f₁ : ι → M
f₂ : ι → N
hl : l ≠ []
⊢ (map (fun i => f (f₁ i) (f₂ i)) l).prod = f (map f₁ l).prod (map f₂ l).prod

Tactic:
match l, hl with | x :: xs, hl => induction xs generalizing x <;> aesop

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean
/-- A zero functor preserves colimits. -/
lemma preservesColimitsOfShape_of_isZero : PreservesColimitsOfShape J G where
  preservesColimit {K} := ⟨fun _ => ⟨by
    rw [Functor.isZero_iff] at hG
    exact IsColimit.ofIsZero _ ((K ⋙ G).isZero (fun X ↦ hG _)) (hG _)⟩⟩

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
hG : ∀ (X : C), IsZero (G.obj X)
J : Type u_1
inst✝ : Category.{u_2, u_1} J
K : J ⥤ C
c✝ : Cocone K
x✝ : IsColimit c✝
⊢ IsColimit (G.mapCocone c✝)

Tactic:
exact IsColimit.ofIsZero _ ((K ⋙ G).isZero (fun X ↦ hG _)) (hG _)

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
hG : IsZero G
J : Type u_1
inst✝ : Category.{u_2, u_1} J
K : J ⥤ C
c✝ : Cocone K
x✝ : IsColimit c✝
⊢ IsColimit (G.mapCocone c✝)

Tactic:
rw [Functor.isZero_iff] at hG

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
hG : ∀ (X : C), IsZero (G.obj X)
J : Type u_1
inst✝ : Category.{u_2, u_1} J
K : J ⥤ C
c✝ : Cocone K
x✝ : IsColimit c✝
⊢ IsColimit (G.mapCocone c✝)
-- Mathlib/AlgebraicGeometry/EllipticCurve/ModelsWithJ.lean
lemma ofJ_0_of_three_eq_zero (h3 : (3 : F) = 0) : ofJ 0 = ofJ1728 F

Proof state:
F : Type u_2
inst✝¹ : Field F
inst✝ : DecidableEq F
h3 : 3 = 0
⊢ ofJ 0 = ofJ1728 F

Tactic:
rw [ofJ, if_pos rfl, if_pos h3]

Result:
no goals
-- Mathlib/Algebra/CharP/Two.lean
theorem neg_eq (x : R) : -x = x

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R 2
x : R
⊢ -x = x

Tactic:
rw [neg_eq_iff_add_eq_zero, add_self_eq_zero]

Result:
no goals