harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/PImage.lean
theorem mem_pimage : b ∈ s.pimage f ↔ ∃ a ∈ s, b ∈ f a

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α →. β
inst✝ : (x : α) → Decidable (f x).Dom
s : Finset α
b : β
⊢ b ∈ pimage f s ↔ ∃ a ∈ s, b ∈ f a

Tactic:
simp [pimage]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Prod.lean
theorem dirac_prod_dirac {x : α} {y : β} : (dirac x).prod (dirac y) = dirac (x, y)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
x : α
y : β
⊢ (dirac x).prod (dirac y) = dirac (x, y)

Tactic:
rw [prod_dirac, map_dirac measurable_prod_mk_right]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_add_const_Iio : (fun x => x + a) '' Iio b = Iio (b + a)

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ (fun x => x + a) '' Iio b = Iio (b + a)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Localization/AtPrime.lean
theorem AtPrime.map_eq_maximalIdeal :
    Ideal.map (algebraMap R (Localization.AtPrime I)) I =
      IsLocalRing.maximalIdeal (Localization I.primeCompl)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
⊢ Ideal.map (algebraMap R (Localization.AtPrime I)) I = IsLocalRing.maximalIdeal (Localization I.primeCompl)

Tactic:
convert congr_arg (Ideal.map (algebraMap R (Localization.AtPrime I)))
(AtPrime.comap_maximalIdeal (hI := hI)).symm

Result:
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
⊢ IsLocalRing.maximalIdeal (Localization I.primeCompl) =
    Ideal.map (algebraMap R (Localization.AtPrime I))
      (Ideal.comap (algebraMap R (Localization.AtPrime I)) (IsLocalRing.maximalIdeal (Localization I.primeCompl)))

Proof state:
case h.e'_3
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
⊢ IsLocalRing.maximalIdeal (Localization I.primeCompl) =
    Ideal.map (algebraMap R (Localization.AtPrime I))
      (Ideal.comap (algebraMap R (Localization.AtPrime I)) (IsLocalRing.maximalIdeal (Localization I.primeCompl)))

Tactic:
rw [map_comap I.primeCompl]

Result:
no goals
-- Mathlib/Combinatorics/HalesJewett.lean
theorem horizontal_apply {α ι ι'} (l : Line α ι) (v : ι' → α) (x : α) :
    l.horizontal v x = Sum.elim (l x) v

Proof state:
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
v : ι' → α
x : α
⊢ ↑(l.horizontal v) x = Sum.elim (↑l x) v

Tactic:
funext i

Result:
case h
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
v : ι' → α
x : α
i : ι ⊕ ι'
⊢ ↑(l.horizontal v) x i = Sum.elim (↑l x) v i

Proof state:
case h
α : Type u_5
ι : Type u_6
ι' : Type u_7
l : Line α ι
v : ι' → α
x : α
i : ι ⊕ ι'
⊢ ↑(l.horizontal v) x i = Sum.elim (↑l x) v i

Tactic:
cases i <;> rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
@[simp]
lemma φ_one : W.φ 1 = C X

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.φ 1 = C X

Tactic:
rw [φ, ψ_one, one_pow, mul_one, sub_self, ψ_zero, mul_zero, sub_zero]

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean
lemma preadditiveYoneda_homologySequenceδ_singleTriangle_apply
    [HasDerivedCategory.{w'} C] {Y : C} {n₀ : ℕ} (x : Ext S.X₁ Y n₀)
    {n₁ : ℕ} (h : 1 + n₀ = n₁) :
    (preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
      ((triangleOpEquivalence _).functor.obj (op hS.singleTriangle)) n₀ n₁ (by omega) x.hom =
      (hS.extClass.comp x h).hom

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y✝ : C
inst✝ : HasDerivedCategory C
Y : C
n₀ : ℕ
x : Ext S.X₁ Y n₀
n₁ : ℕ
h : 1 + n₀ = n₁
⊢ ↑n₀ + 1 = ↑n₁

Tactic:
omega

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
Y : C
n₀ : ℕ
x : Ext S.X₁ Y n₀
n₁ : ℕ
h : 1 + n₀ = n₁
⊢ hS.singleTriangle.mor₃ ≫
      (shiftFunctor (DerivedCategory C) 1).map x.hom ≫
        (shiftFunctorAdd' (DerivedCategory C) (↑n₀) 1 ↑n₁ ⋯).inv.app ((singleFunctor C 0).obj Y) =
    hS.singleδ ≫
      (shiftFunctor (DerivedCategory C) ↑1).map x.hom ≫
        (shiftFunctorAdd' (DerivedCategory C) ↑n₀ ↑1 ↑n₁ ⋯).inv.app ((singleFunctor C 0).obj Y)

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
Y : C
n₀ : ℕ
x : Ext S.X₁ Y n₀
n₁ : ℕ
h : 1 + n₀ = n₁
⊢ (ConcreteCategory.hom
        ((preadditiveYoneda.obj ((singleFunctor C 0).obj Y)).homologySequenceδ
          ((triangleOpEquivalence (DerivedCategory C)).functor.obj (op hS.singleTriangle)) ↑n₀ ↑n₁ ⋯))
      x.hom =
    (hS.extClass.comp x h).hom

Tactic:
rw [preadditiveYoneda_homologySequenceδ_apply,
  comp_hom, hS.extClass_hom, ShiftedHom.comp]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
Y : C
n₀ : ℕ
x : Ext S.X₁ Y n₀
n₁ : ℕ
h : 1 + n₀ = n₁
⊢ hS.singleTriangle.mor₃ ≫
      (shiftFunctor (DerivedCategory C) 1).map x.hom ≫
        (shiftFunctorAdd' (DerivedCategory C) (↑n₀) 1 ↑n₁ ⋯).inv.app ((singleFunctor C 0).obj Y) =
    hS.singleδ ≫
      (shiftFunctor (DerivedCategory C) ↑1).map x.hom ≫
        (shiftFunctorAdd' (DerivedCategory C) ↑n₀ ↑1 ↑n₁ ⋯).inv.app ((singleFunctor C 0).obj Y)
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upperCrossingTime_eq_upperCrossingTime_of_lt {M : ℕ} (hNM : N ≤ M)
    (h : upperCrossingTime a b f N n ω < N) :
    upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω

Proof state:
case succ
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
n✝ : ℕ
h : upperCrossingTime a b f N (n✝ + 1) ω < N
⊢ upperCrossingTime a b f M (n✝ + 1) ω = upperCrossingTime a b f N (n✝ + 1) ω

Tactic:
exact (crossing_eq_crossing_of_upperCrossingTime_lt hNM h).1

Result:
no goals

Proof state:
case zero
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N 0 ω < N
⊢ upperCrossingTime a b f M 0 ω = upperCrossingTime a b f N 0 ω

Tactic:
simp

Result:
no goals

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N n ω < N
⊢ upperCrossingTime a b f M n ω = upperCrossingTime a b f N n ω

Tactic:
cases n

Result:
case zero
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N 0 ω < N
⊢ upperCrossingTime a b f M 0 ω = upperCrossingTime a b f N 0 ω

case succ
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
n✝ : ℕ
h : upperCrossingTime a b f N (n✝ + 1) ω < N
⊢ upperCrossingTime a b f M (n✝ + 1) ω = upperCrossingTime a b f N (n✝ + 1) ω
-- Mathlib/Algebra/Module/Presentation/Basic.lean
@[simp]
lemma uniq_symm_var (g : relations.G) : (uniq h h').symm (solution'.var g) = solution.var g

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
g : relations.G
⊢ (h.uniq h').symm (solution'.var g) = solution.var g

Tactic:
simp [uniq]

Result:
no goals
-- Mathlib/CategoryTheory/ConcreteCategory/EpiMono.lean
lemma surjective_eq_epimorphisms [(forget C).PreservesEpimorphisms] :
    MorphismProperty.surjective C = epimorphisms C

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : (forget C).PreservesEpimorphisms
⊢ (forget C).PreservesEpimorphisms

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : (forget C).PreservesEpimorphisms
⊢ MorphismProperty.surjective C = epimorphisms C

Tactic:
rw [surjective_eq_epimorphisms_iff]

Result:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : (forget C).PreservesEpimorphisms
⊢ (forget C).PreservesEpimorphisms
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem tensorTensorTensorComm_symm :
    (tensorTensorTensorComm R A B C D).symm = tensorTensorTensorComm R A C B D

Proof state:
case h
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
a✝ : (A ⊗[R] C) ⊗[R] B ⊗[R] D
⊢ (tensorTensorTensorComm R A B C D).symm a✝ = (tensorTensorTensorComm R A C B D) a✝

Tactic:
rfl

Result:
no goals

Proof state:
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
⊢ (tensorTensorTensorComm R A B C D).symm = tensorTensorTensorComm R A C B D

Tactic:
ext

Result:
case h
R : Type uR
A : Type uA
B : Type uB
C : Type uC
D : Type uD
inst✝⁸ : CommSemiring R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R B
inst✝³ : Semiring C
inst✝² : Algebra R C
inst✝¹ : Semiring D
inst✝ : Algebra R D
a✝ : (A ⊗[R] C) ⊗[R] B ⊗[R] D
⊢ (tensorTensorTensorComm R A B C D).symm a✝ = (tensorTensorTensorComm R A C B D) a✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem size_updateAllBuckets {self : Array (AssocList α β)} {f : AssocList α β → AssocList α δ} :
    (updateAllBuckets self f).size = self.size

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
self : Array (AssocList α β)
f : AssocList α β → AssocList α δ
⊢ (updateAllBuckets self f).size = self.size

Tactic:
simp [updateAllBuckets]

Result:
no goals
-- Mathlib/Data/Set/Finite/Lemmas.lean
theorem Finite.induction_to {C : Set α → Prop} {S : Set α} (h : S.Finite)
    (S0 : Set α) (hS0 : S0 ⊆ S) (H0 : C S0) (H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)) :
    C S

Proof state:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
⊢ C S

Tactic:
have : Finite S := Finite.to_subtype h

Result:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this : Finite ↑S
⊢ C S

Proof state:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C ↑⟨S0, hS0⟩
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this✝ : Finite ↑S
this : Finite { T // T ⊆ S }
s : { x // x ⊆ S }
hs : ↑s ≠ ↑⟨S, ⋯⟩
hs' : C ↑s
⊢ ∃ c > s, C ↑c

Tactic:
obtain ⟨a, ⟨ha1, ha2⟩, ha'⟩ := H1 s (ssubset_of_ne_of_subset hs s.2) hs'

Result:
case intro.intro.intro
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C ↑⟨S0, hS0⟩
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this✝ : Finite ↑S
this : Finite { T // T ⊆ S }
s : { x // x ⊆ S }
hs : ↑s ≠ ↑⟨S, ⋯⟩
hs' : C ↑s
a : α
ha' : C (insert a ↑s)
ha1 : a ∈ S
ha2 : a ∉ ↑s
⊢ ∃ c > s, C ↑c

Proof state:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C ↑⟨S0, hS0⟩
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this✝ : Finite ↑S
this : Finite { T // T ⊆ S }
⊢ C ↑⟨S, ⋯⟩

Tactic:
refine Finite.to_wellFoundedGT.wf.induction_bot' (fun s hs hs' ↦ ?_) H0

Result:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C ↑⟨S0, hS0⟩
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this✝ : Finite ↑S
this : Finite { T // T ⊆ S }
s : { x // x ⊆ S }
hs : ↑s ≠ ↑⟨S, ⋯⟩
hs' : C ↑s
⊢ ∃ c > s, C ↑c

Proof state:
case intro.intro.intro
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C ↑⟨S0, hS0⟩
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this✝ : Finite ↑S
this : Finite { T // T ⊆ S }
s : { x // x ⊆ S }
hs : ↑s ≠ ↑⟨S, ⋯⟩
hs' : C ↑s
a : α
ha' : C (insert a ↑s)
ha1 : a ∈ S
ha2 : a ∉ ↑s
⊢ ∃ c > s, C ↑c

Tactic:
exact ⟨⟨insert a s.1, insert_subset ha1 s.2⟩, Set.ssubset_insert ha2, ha'⟩

Result:
no goals

Proof state:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this : Finite ↑S
⊢ C S

Tactic:
have : Finite {T : Set α // T ⊆ S} := Finite.of_equiv (Set S) (Equiv.Set.powerset S).symm

Result:
α : Type u
C : Set α → Prop
S : Set α
h : S.Finite
S0 : Set α
hS0 : S0 ⊆ S
H0 : C S0
H1 : ∀ s ⊂ S, C s → ∃ a ∈ S \ s, C (insert a s)
this✝ : Finite ↑S
this : Finite { T // T ⊆ S }
⊢ C S
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem not_bddAbove_fp (H : IsNormal f) : ¬ BddAbove (Function.fixedPoints f)

Proof state:
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ ¬BddAbove (fixedPoints f)

Tactic:
convert not_bddAbove_fp_family fun _ : Unit => H

Result:
case h.e'_1.h.e'_3
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ fixedPoints f = ⋂ i, fixedPoints f

Proof state:
case h.e'_1.h.e'_3
f : Ordinal.{u} → Ordinal.{u}
H : IsNormal f
⊢ fixedPoints f = ⋂ i, fixedPoints f

Tactic:
exact (Set.iInter_const _).symm

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycleFactorsFinset_eq_singleton_self_iff {f : Perm α} :
    f.cycleFactorsFinset = {f} ↔ f.IsCycle

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ f.cycleFactorsFinset = {f} ↔ f.IsCycle

Tactic:
simp [cycleFactorsFinset_eq_finset]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.add [AddGroup α] [InvolutiveNeg β] (h1 : Antiperiodic f c₁)
    (h2 : Antiperiodic f c₂) : Periodic f (c₁ + c₂)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h1 : Antiperiodic f c₁
h2 : Antiperiodic f c₂
⊢ Periodic f (c₁ + c₂)

Tactic:
simp_all [← add_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem eqToIso_trans {X Y Z : C} (p : X = Y) (q : Y = Z) :
    eqToIso p ≪≫ eqToIso q = eqToIso (p.trans q)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
⊢ eqToIso p ≪≫ eqToIso q = eqToIso ⋯

Tactic:
ext

Result:
case w
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
⊢ (eqToIso p ≪≫ eqToIso q).hom = (eqToIso ⋯).hom

Proof state:
case w
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X = Y
q : Y = Z
⊢ (eqToIso p ≪≫ eqToIso q).hom = (eqToIso ⋯).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convolution.lean
theorem ConvolutionExists.add_distrib (hfg : ConvolutionExists f g L μ)
    (hfg' : ConvolutionExists f' g L μ) : (f + f') ⋆[L, μ] g = f ⋆[L, μ] g + f' ⋆[L, μ] g

Proof state:
case h
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f f' : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
hfg : ConvolutionExists f g L μ
hfg' : ConvolutionExists f' g L μ
x : G
⊢ ((f + f') ⋆[L, μ] g) x = (f ⋆[L, μ] g + f' ⋆[L, μ] g) x

Tactic:
exact (hfg x).add_distrib (hfg' x)

Result:
no goals

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f f' : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
hfg : ConvolutionExists f g L μ
hfg' : ConvolutionExists f' g L μ
⊢ (f + f') ⋆[L, μ] g = f ⋆[L, μ] g + f' ⋆[L, μ] g

Tactic:
ext x

Result:
case h
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup E'
inst✝⁷ : NormedAddCommGroup F
f f' : G → E
g : G → E'
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedSpace 𝕜 E
inst✝⁴ : NormedSpace 𝕜 E'
inst✝³ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝² : MeasurableSpace G
μ : Measure G
inst✝¹ : NormedSpace ℝ F
inst✝ : AddGroup G
hfg : ConvolutionExists f g L μ
hfg' : ConvolutionExists f' g L μ
x : G
⊢ ((f + f') ⋆[L, μ] g) x = (f ⋆[L, μ] g + f' ⋆[L, μ] g) x
-- Mathlib/NumberTheory/NumberField/EquivReindex.lean
theorem inverse_basisMatrix_mulVec_eq_repr [DecidableEq (K →+* ℂ)] (α : 𝓞 K) :
    ∀ i, ((basisMatrix K).transpose)⁻¹.mulVec (fun j =>
      canonicalEmbedding K (algebraMap (𝓞 K) K α) j) i =
      ((integralBasis K).reindex (equivReindex K).symm).repr α i := fun i => by
  rw [inv_mulVec_eq_vec (canonicalEmbedding_eq_basisMatrix_mulVec ((algebraMap (𝓞 K) K) α))]

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
⊢ ((basisMatrix K)ᵀ⁻¹ *ᵥ fun j => (canonicalEmbedding K) ((algebraMap (𝓞 K) K) α) j) i =
    ↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)

Tactic:
rw [inv_mulVec_eq_vec (canonicalEmbedding_eq_basisMatrix_mulVec ((algebraMap (𝓞 K) K) α))]

Result:
no goals
-- Mathlib/Order/Interval/Multiset.lean
theorem Ico_filter_le_of_left_le [DecidablePred (c ≤ ·)] (hac : a ≤ c) :
    ((Ico a b).filter fun x => c ≤ x) = Ico c b

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => c ≤ x
hac : a ≤ c
⊢ (Finset.Ico c b).val = Ico c b

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => c ≤ x
hac : a ≤ c
⊢ filter (fun x => c ≤ x) (Ico a b) = Ico c b

Tactic:
rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_left_le hac]

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
a b c : α
inst✝ : DecidablePred fun x => c ≤ x
hac : a ≤ c
⊢ (Finset.Ico c b).val = Ico c b
-- Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean
@[simp] lemma Int.range_castAddHom {A : Type*} [AddGroupWithOne A] :
    (Int.castAddHom A).range = AddSubgroup.zmultiples 1

Proof state:
case h
A : Type u_4
inst✝ : AddGroupWithOne A
a : A
⊢ a ∈ (castAddHom A).range ↔ a ∈ AddSubgroup.zmultiples 1

Tactic:
simp_rw [AddMonoidHom.mem_range, Int.coe_castAddHom, AddSubgroup.mem_zmultiples_iff, zsmul_one]

Result:
no goals

Proof state:
A : Type u_4
inst✝ : AddGroupWithOne A
⊢ (castAddHom A).range = AddSubgroup.zmultiples 1

Tactic:
ext a

Result:
case h
A : Type u_4
inst✝ : AddGroupWithOne A
a : A
⊢ a ∈ (castAddHom A).range ↔ a ∈ AddSubgroup.zmultiples 1
-- Mathlib/NumberTheory/MulChar/Basic.lean
/-- If `χ` is a multiplicative character on a commutative monoid `M` with finitely many units,
then `χ ^ #Mˣ = 1`. -/
protected lemma pow_card_eq_one [Fintype Mˣ] (χ : MulChar M R) : χ ^ (Fintype.card Mˣ) = 1

Proof state:
M : Type u_1
inst✝² : CommMonoid M
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : Fintype Mˣ
χ : MulChar M R
⊢ χ ^ Fintype.card Mˣ = 1

Tactic:
ext1

Result:
case h
M : Type u_1
inst✝² : CommMonoid M
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : Fintype Mˣ
χ : MulChar M R
a✝ : Mˣ
⊢ (χ ^ Fintype.card Mˣ) ↑a✝ = 1 ↑a✝

Proof state:
case h
M : Type u_1
inst✝² : CommMonoid M
R : Type u_2
inst✝¹ : CommMonoidWithZero R
inst✝ : Fintype Mˣ
χ : MulChar M R
a✝ : Mˣ
⊢ (χ ^ Fintype.card Mˣ) ↑a✝ = 1 ↑a✝

Tactic:
rw [pow_apply_coe, ← map_pow, one_apply_coe, ← Units.val_pow_eq_pow_val, pow_card_eq_one,
  Units.val_eq_one.mpr rfl, map_one]

Result:
no goals
-- Mathlib/Algebra/Free.lean
theorem length_toFreeSemigroup (x : FreeMagma α) : (toFreeSemigroup x).length = x.length :=
  FreeMagma.recOnMul x (fun _ ↦ rfl) fun x y hx hy ↦ by
    rw [map_mul, FreeSemigroup.length_mul, hx, hy]; rfl

Proof state:
α : Type u
x✝ x y : FreeMagma α
hx : (toFreeSemigroup x).length = x.length
hy : (toFreeSemigroup y).length = y.length
⊢ x.length + y.length = (x * y).length

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
x✝ x y : FreeMagma α
hx : (toFreeSemigroup x).length = x.length
hy : (toFreeSemigroup y).length = y.length
⊢ (toFreeSemigroup (x * y)).length = (x * y).length

Tactic:
rw [map_mul, FreeSemigroup.length_mul, hx, hy]

Result:
α : Type u
x✝ x y : FreeMagma α
hx : (toFreeSemigroup x).length = x.length
hy : (toFreeSemigroup y).length = y.length
⊢ x.length + y.length = (x * y).length
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem mem_nhdsGE_iff_exists_Ico_subset' {a u' : α} {s : Set α} (hu' : a < u') :
    s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s :=
  (TFAE_mem_nhdsGE hu' s).out 0 4 (by norm_num) (by norm_num)

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a u' : α
s : Set α
hu' : a < u'
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a u'] a, s ∈ 𝓝[Ico a u'] a, ∃ u ∈ Ioc a u', Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s].get? 4 =
    some (∃ u ∈ Ioi a, Ico a u ⊆ s)

Tactic:
norm_num

Result:
no goals

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a u' : α
s : Set α
hu' : a < u'
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a u'] a, s ∈ 𝓝[Ico a u'] a, ∃ u ∈ Ioc a u', Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s].get? 0 =
    some (s ∈ 𝓝[≥] a)

Tactic:
norm_num

Result:
no goals
-- Mathlib/RingTheory/Nilpotent/Basic.lean
lemma IsUnit.not_isNilpotent [Ring R] [Nontrivial R] {x : R} (hx : IsUnit x) :
    ¬ IsNilpotent x

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
x : R
hx : IsUnit x
H : IsNilpotent x
⊢ False

Tactic:
simpa using H.isUnit_add_right_of_commute hx.neg (by simp)

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
x : R
hx : IsUnit x
⊢ ¬IsNilpotent x

Tactic:
intro H

Result:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
x : R
hx : IsUnit x
H : IsNilpotent x
⊢ False

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : Nontrivial R
x : R
hx : IsUnit x
H : IsNilpotent x
⊢ Commute x (-x)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem prod_eq_biUnion_left : s ×ˢ t = ⋃ a ∈ s, (fun b => (a, b)) '' t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s ×ˢ t = ⋃ a ∈ s, (fun b => (a, b)) '' t

Tactic:
rw [iUnion_image_left, image2_mk_eq_prod]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Erase.lean
theorem getElem?_eraseIdx (l : Vector α n) (i : Nat) (h : i < n) (j : Nat) :
    (l.eraseIdx i)[j]? = if j < i then l[j]? else l[j + 1]?

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
j : Nat
⊢ (l.eraseIdx i h)[j]? = if j < i then l[j]? else l[j + 1]?

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
i j : Nat
l : Array α
h : i < l.size
⊢ ({ toArray := l, size_toArray := ⋯ }.eraseIdx i h)[j]? =
    if j < i then { toArray := l, size_toArray := ⋯ }[j]? else { toArray := l, size_toArray := ⋯ }[j + 1]?

Proof state:
case mk
α : Type u_1
i j : Nat
l : Array α
h : i < l.size
⊢ ({ toArray := l, size_toArray := ⋯ }.eraseIdx i h)[j]? =
    if j < i then { toArray := l, size_toArray := ⋯ }[j]? else { toArray := l, size_toArray := ⋯ }[j + 1]?

Tactic:
simp [Array.getElem?_eraseIdx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldl_eq_foldr_reverse (l : List α) (f : β → α → β) (b) :
    l.foldl f b = l.reverse.foldr (fun x y => f y x) b

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : β → α → β
b : β
⊢ foldl f b l = foldr (fun x y => f y x) b l.reverse

Tactic:
simp

Result:
no goals