harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/RootSystem/Hom.lean
@[simp]
lemma weightEquiv_comp_toLin {P : RootPairing ι R M N} (x y : RootPairing.Equiv P P) :
    weightEquiv P P (Equiv.comp x y) = weightEquiv P P y ≪≫ₗ weightEquiv P P x

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x y : P.Equiv P
⊢ weightEquiv P P (x.comp y) = weightEquiv P P y ≪≫ₗ weightEquiv P P x

Tactic:
ext

Result:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x y : P.Equiv P
x✝ : M
⊢ (weightEquiv P P (x.comp y)) x✝ = (weightEquiv P P y ≪≫ₗ weightEquiv P P x) x✝

Proof state:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x y : P.Equiv P
x✝ : M
⊢ (weightEquiv P P (x.comp y)) x✝ = (weightEquiv P P y ≪≫ₗ weightEquiv P P x) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Completion.lean
theorem lim_neg (f : CauSeq β abv) : lim (-f) = -lim f :=
  lim_eq_of_equiv_const
    (show LimZero (-f - const abv (-lim f)) by
      rw [const_neg, sub_neg_eq_add, add_comm, ← sub_eq_add_neg]
      exact Setoid.symm (equiv_lim f))

Proof state:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
⊢ (const abv f.lim - f).LimZero

Tactic:
exact Setoid.symm (equiv_lim f)

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
⊢ (-f - const abv (-f.lim)).LimZero

Tactic:
rw [const_neg, sub_neg_eq_add, add_comm, ← sub_eq_add_neg]

Result:
α : Type u_1
inst✝³ : LinearOrderedField α
β : Type u_2
inst✝² : Ring β
abv : β → α
inst✝¹ : IsAbsoluteValue abv
inst✝ : IsComplete β abv
f : CauSeq β abv
⊢ (const abv f.lim - f).LimZero
-- Mathlib/CategoryTheory/Galois/Topology.lean
/-- The image of `Aut F` in `∀ X, Aut (F.obj X)` are precisely the compatible families of
automorphisms. -/
lemma autEmbedding_range :
    Set.range (autEmbedding F) =
      ⋂ (f : Arrow C), { a | F.map f.hom ≫ (a f.right).hom = (a f.left).hom ≫ F.map f.hom }

Proof state:
case h
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
a : (X : C) → Aut (F.obj X)
h : ∀ (i : Arrow C), F.map i.hom ≫ (a i.right).hom = (a i.left).hom ≫ F.map i.hom
⊢ ∃ y, (autEmbedding F) y = a

Tactic:
use NatIso.ofComponents a (fun {X Y} f ↦ h ⟨X, Y, f⟩)

Result:
case h
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
a : (X : C) → Aut (F.obj X)
h : ∀ (i : Arrow C), F.map i.hom ≫ (a i.right).hom = (a i.left).hom ≫ F.map i.hom
⊢ (autEmbedding F) (NatIso.ofComponents a ⋯) = a

Proof state:
case h
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
a : (X : C) → Aut (F.obj X)
⊢ (∃ y, (autEmbedding F) y = a) ↔ ∀ (i : Arrow C), F.map i.hom ≫ (a i.right).hom = (a i.left).hom ≫ F.map i.hom

Tactic:
refine ⟨fun ⟨σ, h⟩ i ↦ h.symm ▸ σ.hom.naturality i.hom, fun h ↦ ?_⟩

Result:
case h
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
a : (X : C) → Aut (F.obj X)
h : ∀ (i : Arrow C), F.map i.hom ≫ (a i.right).hom = (a i.left).hom ≫ F.map i.hom
⊢ ∃ y, (autEmbedding F) y = a

Proof state:
case h
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
a : (X : C) → Aut (F.obj X)
⊢ a ∈ Set.range ⇑(autEmbedding F) ↔ a ∈ ⋂ f, {a | F.map f.hom ≫ (a f.right).hom = (a f.left).hom ≫ F.map f.hom}

Tactic:
simp only [Set.mem_range, id_obj, Set.mem_iInter, Set.mem_setOf_eq]

Result:
case h
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
a : (X : C) → Aut (F.obj X)
⊢ (∃ y, (autEmbedding F) y = a) ↔ ∀ (i : Arrow C), F.map i.hom ≫ (a i.right).hom = (a i.left).hom ≫ F.map i.hom

Proof state:
case h
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
a : (X : C) → Aut (F.obj X)
h : ∀ (i : Arrow C), F.map i.hom ≫ (a i.right).hom = (a i.left).hom ≫ F.map i.hom
⊢ (autEmbedding F) (NatIso.ofComponents a ⋯) = a

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
⊢ Set.range ⇑(autEmbedding F) = ⋂ f, {a | F.map f.hom ≫ (a f.right).hom = (a f.left).hom ≫ F.map f.hom}

Tactic:
ext a

Result:
case h
C : Type u₁
inst✝ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
a : (X : C) → Aut (F.obj X)
⊢ a ∈ Set.range ⇑(autEmbedding F) ↔ a ∈ ⋂ f, {a | F.map f.hom ≫ (a f.right).hom = (a f.left).hom ≫ F.map f.hom}
-- Mathlib/RingTheory/FinitePresentation.lean
theorem iff :
    FinitePresentation R A ↔
      ∃ (n : _) (I : Ideal (MvPolynomial (Fin n) R)) (_ : (_ ⧸ I) ≃ₐ[R] A), I.FG

Proof state:
case mp.mk.intro.intro
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ ∃ n I x, I.FG

Tactic:
exact ⟨n, RingHom.ker f.toRingHom, Ideal.quotientKerAlgEquivOfSurjective hf.1, hf.2⟩

Result:
no goals

Proof state:
case mp
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ FinitePresentation R A → ∃ n I x, I.FG

Tactic:
rintro ⟨n, f, hf⟩

Result:
case mp.mk.intro.intro
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] A
hf : Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ ∃ n I x, I.FG

Proof state:
case mpr
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (∃ n I x, I.FG) → FinitePresentation R A

Tactic:
rintro ⟨n, I, e, hfg⟩

Result:
case mpr.intro.intro.intro
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
I : Ideal (MvPolynomial (Fin n) R)
e : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A
hfg : I.FG
⊢ FinitePresentation R A

Proof state:
case mpr.intro.intro.intro
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
I : Ideal (MvPolynomial (Fin n) R)
e : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A
hfg : I.FG
this : FinitePresentation R (MvPolynomial (Fin n) R ⧸ I) := FinitePresentation.quotient hfg
⊢ FinitePresentation R A

Tactic:
exact equiv e

Result:
no goals

Proof state:
case mpr.intro.intro.intro
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
I : Ideal (MvPolynomial (Fin n) R)
e : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A
hfg : I.FG
⊢ FinitePresentation R A

Tactic:
letI := (FinitePresentation.mvPolynomial R _).quotient hfg

Result:
case mpr.intro.intro.intro
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
n : ℕ
I : Ideal (MvPolynomial (Fin n) R)
e : (MvPolynomial (Fin n) R ⧸ I) ≃ₐ[R] A
hfg : I.FG
this : FinitePresentation R (MvPolynomial (Fin n) R ⧸ I) := FinitePresentation.quotient hfg
⊢ FinitePresentation R A

Proof state:
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ FinitePresentation R A ↔ ∃ n I x, I.FG

Tactic:
constructor

Result:
case mp
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ FinitePresentation R A → ∃ n I x, I.FG

case mpr
R : Type w₁
A : Type w₂
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (∃ n I x, I.FG) → FinitePresentation R A
-- Mathlib/Analysis/Complex/Hadamard.lean
/-- A technical lemma needed in the proof. -/
private lemma fun_arg_eq {l u : ℝ} (hul : l < u) (z : ℂ) :
    (↑l + (z / (↑u - ↑l) - ↑l / (↑u - ↑l)) * (↑u - ↑l)) = z

Proof state:
l u : ℝ
hul : l < u
z : ℂ
⊢ ↑l + (1 * z - 1 * ↑l) = z

Tactic:
simp

Result:
no goals

Proof state:
l u : ℝ
hul : l < u
z : ℂ
⊢ ↑l + (z / (↑u - ↑l) - ↑l / (↑u - ↑l)) * (↑u - ↑l) = z

Tactic:
rw [sub_mul, div_mul_comm, div_self (by norm_cast; linarith),
  div_mul_comm, div_self (by norm_cast; linarith)]

Result:
l u : ℝ
hul : l < u
z : ℂ
⊢ ↑l + (1 * z - 1 * ↑l) = z

Proof state:
l u : ℝ
hul : l < u
z : ℂ
⊢ ↑u - ↑l ≠ 0

Tactic:
norm_cast

Result:
l u : ℝ
hul : l < u
z : ℂ
⊢ ¬u - l = 0

Proof state:
l u : ℝ
hul : l < u
z : ℂ
⊢ ¬u - l = 0

Tactic:
linarith

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
lemma IsTotallyUnimodular.submatrix {A : Matrix m n R} (f : m' → m) (g : n' → n)
    (hA : A.IsTotallyUnimodular) :
    (A.submatrix f g).IsTotallyUnimodular

Proof state:
m : Type u_1
m' : Type u_2
n : Type u_3
n' : Type u_4
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
f : m' → m
g : n' → n
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ ∀ (k : ℕ) (f_1 : Fin k → m') (g_1 : Fin k → n'), (A.submatrix (f ∘ f_1) (g ∘ g_1)).det ∈ Set.range SignType.cast

Tactic:
intro _ _ _

Result:
m : Type u_1
m' : Type u_2
n : Type u_3
n' : Type u_4
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
f : m' → m
g : n' → n
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
f✝ : Fin k✝ → m'
g✝ : Fin k✝ → n'
⊢ (A.submatrix (f ∘ f✝) (g ∘ g✝)).det ∈ Set.range SignType.cast

Proof state:
m : Type u_1
m' : Type u_2
n : Type u_3
n' : Type u_4
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
f : m' → m
g : n' → n
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
k✝ : ℕ
f✝ : Fin k✝ → m'
g✝ : Fin k✝ → n'
⊢ (A.submatrix (f ∘ f✝) (g ∘ g✝)).det ∈ Set.range SignType.cast

Tactic:
apply hA

Result:
no goals

Proof state:
m : Type u_1
m' : Type u_2
n : Type u_3
n' : Type u_4
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
f : m' → m
g : n' → n
hA : A.IsTotallyUnimodular
⊢ (A.submatrix f g).IsTotallyUnimodular

Tactic:
simp only [isTotallyUnimodular_iff, submatrix_submatrix] at hA ⊢

Result:
m : Type u_1
m' : Type u_2
n : Type u_3
n' : Type u_4
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
f : m' → m
g : n' → n
hA : ∀ (k : ℕ) (f : Fin k → m) (g : Fin k → n), (A.submatrix f g).det ∈ Set.range SignType.cast
⊢ ∀ (k : ℕ) (f_1 : Fin k → m') (g_1 : Fin k → n'), (A.submatrix (f ∘ f_1) (g ∘ g_1)).det ∈ Set.range SignType.cast
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
theorem sum_homogeneousComponent :
    (∑ i ∈ range (φ.totalDegree + 1), homogeneousComponent i φ) = φ

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
⊢ ∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i) φ = φ

Tactic:
ext1 d

Result:
case a
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d (∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i) φ) = coeff d φ

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d : σ →₀ ℕ
this : φ.totalDegree < d.support.sum ⇑d → 0 = coeff d φ
⊢ coeff d (∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i) φ) = coeff d φ

Tactic:
simpa [coeff_sum, coeff_homogeneousComponent]

Result:
no goals

Proof state:
case a
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff d (∑ i ∈ range (φ.totalDegree + 1), (homogeneousComponent i) φ) = coeff d φ

Tactic:
suffices φ.totalDegree < d.support.sum d → 0 = coeff d φ by
  simpa [coeff_sum, coeff_homogeneousComponent]

Result:
case a
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ φ.totalDegree < d.support.sum ⇑d → 0 = coeff d φ

Proof state:
case a
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ φ.totalDegree < d.support.sum ⇑d → 0 = coeff d φ

Tactic:
exact fun h => (coeff_eq_zero_of_totalDegree_lt h).symm

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsLittleO.comp_fst : f =o[l] g → (f ∘ Prod.fst) =o[l ×ˢ l'] (g ∘ Prod.fst)

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ (∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∀ ⦃c : ℝ⦄,
      0 < c →
        ∃ pa,
          (∀ᶠ (x : α) in l, pa x) ∧
            ∃ pb,
              (∀ᶠ (y : β) in l', pb y) ∧
                ∀ {x : α}, pa x → ∀ {y : β}, pb y → ‖(f ∘ Prod.fst) (x, y)‖ ≤ c * ‖(g ∘ Prod.fst) (x, y)‖

Tactic:
exact fun h _ hc ↦ ⟨_, h hc, fun _ ↦ True, eventually_true l', fun {_} h {_} _ ↦ h⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ f =o[l] g → (f ∘ Prod.fst) =o[l ×ˢ l'] (g ∘ Prod.fst)

Tactic:
simp only [isLittleO_iff, eventually_prod_iff]

Result:
α : Type u_1
β : Type u_2
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
f : α → E
g : α → F
l : Filter α
l' : Filter β
⊢ (∀ ⦃c : ℝ⦄, 0 < c → ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖) →
    ∀ ⦃c : ℝ⦄,
      0 < c →
        ∃ pa,
          (∀ᶠ (x : α) in l, pa x) ∧
            ∃ pb,
              (∀ᶠ (y : β) in l', pb y) ∧
                ∀ {x : α}, pa x → ∀ {y : β}, pb y → ‖(f ∘ Prod.fst) (x, y)‖ ≤ c * ‖(g ∘ Prod.fst) (x, y)‖
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Pairwise.lean
theorem pairwise_of_forall_mem_list {l : List α} {r : α → α → Prop} (h : ∀ a ∈ l, ∀ b ∈ l, r a b) :
    l.Pairwise r

Proof state:
case a
α : Type u_1
l : List α
r : α → α → Prop
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b
a b : α
hab : [a, b] <+ l
⊢ b ∈ l

Tactic:
apply hab.subset

Result:
case a.a
α : Type u_1
l : List α
r : α → α → Prop
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b
a b : α
hab : [a, b] <+ l
⊢ b ∈ [a, b]

Proof state:
case a.a
α : Type u_1
l : List α
r : α → α → Prop
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b
a b : α
hab : [a, b] <+ l
⊢ b ∈ [a, b]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
r : α → α → Prop
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b
a b : α
hab : [a, b] <+ l
⊢ r a b

Tactic:
apply h <;> (apply hab.subset; simp)

Result:
no goals

Proof state:
α : Type u_1
l : List α
r : α → α → Prop
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b
⊢ Pairwise r l

Tactic:
rw [pairwise_iff_forall_sublist]

Result:
α : Type u_1
l : List α
r : α → α → Prop
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b
⊢ ∀ {a b : α}, [a, b] <+ l → r a b

Proof state:
α : Type u_1
l : List α
r : α → α → Prop
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b
⊢ ∀ {a b : α}, [a, b] <+ l → r a b

Tactic:
intro a b hab

Result:
α : Type u_1
l : List α
r : α → α → Prop
h : ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → r a b
a b : α
hab : [a, b] <+ l
⊢ r a b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Bootstrap.lean
theorem toListAppend_eq (arr : Array α) (l) : arr.toListAppend l = arr.toList ++ l

Proof state:
α : Type u_1
arr : Array α
l : List α
⊢ arr.toListAppend l = arr.toList ++ l

Tactic:
simp [toListAppend, ← foldr_toList]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem dvd_of_mem_factors' {a : α} {p : Associates α} {hp : Irreducible p} {hz : a ≠ 0}
    (h_mem : Subtype.mk p hp ∈ factors' a) : p ∣ Associates.mk a

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : ⟨p, hp⟩ ∈ factors' a
this : DecidableEq (Associates α)
⊢ p ∣ Associates.mk a

Tactic:
apply dvd_of_mem_factors

Result:
case hm
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : ⟨p, hp⟩ ∈ factors' a
this : DecidableEq (Associates α)
⊢ p ∈ (Associates.mk a).factors

Proof state:
case hm
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : ⟨p, hp⟩ ∈ factors' a
this : DecidableEq (Associates α)
⊢ p ∈ (Associates.mk a).factors

Tactic:
rw [factors_mk _ hz]

Result:
case hm
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : ⟨p, hp⟩ ∈ factors' a
this : DecidableEq (Associates α)
⊢ p ∈ ↑(factors' a)

Proof state:
case hm
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : ⟨p, hp⟩ ∈ factors' a
this : DecidableEq (Associates α)
⊢ p ∈ ↑(factors' a)

Tactic:
apply mem_factorSet_some.2 h_mem

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : ⟨p, hp⟩ ∈ factors' a
⊢ p ∣ Associates.mk a

Tactic:
haveI := Classical.decEq (Associates α)

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
p : Associates α
hp : Irreducible p
hz : a ≠ 0
h_mem : ⟨p, hp⟩ ∈ factors' a
this : DecidableEq (Associates α)
⊢ p ∣ Associates.mk a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem insertIdxTR_go_eq : ∀ n l, insertIdxTR.go a n l acc = acc.toList ++ insertIdx n a l
  | 0, l | _+1, [] => by simp [insertIdxTR.go, insertIdx]
  | n+1, a :: l => by simp [insertIdxTR.go, insertIdx, insertIdxTR_go_eq n l]

Proof state:
α✝ : Type u_1
a : α✝
acc : Array α✝
n✝ : Nat
⊢ insertIdxTR.go a (n✝ + 1) [] acc = acc.toList ++ insertIdx (n✝ + 1) a []

Tactic:
simp [insertIdxTR.go, insertIdx]

Result:
no goals

Proof state:
α✝ : Type u_1
a✝ : α✝
acc : Array α✝
n : Nat
a : α✝
l : List α✝
⊢ insertIdxTR.go a✝ (n + 1) (a :: l) acc = acc.toList ++ insertIdx (n + 1) a✝ (a :: l)

Tactic:
simp [insertIdxTR.go, insertIdx, insertIdxTR_go_eq n l]

Result:
no goals
-- Mathlib/Logic/Equiv/List.lean
theorem raise_lower' : ∀ {l n}, (∀ m ∈ l, n ≤ m) → List.Sorted (· < ·) l → raise' (lower' l n) n = l
  | [], _, _, _ => rfl
  | m :: l, n, h₁, h₂ => by
    have : n ≤ m := h₁ _ (l.mem_cons_self _)
    simp [raise', lower', Nat.sub_add_cancel this,
      raise_lower' (List.rel_of_sorted_cons h₂ : ∀ a ∈ l, m < a) h₂.of_cons]

Proof state:
m : ℕ
l : List ℕ
n : ℕ
h₁ : ∀ m_1 ∈ m :: l, n ≤ m_1
h₂ : Sorted (fun x1 x2 => x1 < x2) (m :: l)
⊢ raise' (lower' (m :: l) n) n = m :: l

Tactic:
have : n ≤ m := h₁ _ (l.mem_cons_self _)

Result:
m : ℕ
l : List ℕ
n : ℕ
h₁ : ∀ m_1 ∈ m :: l, n ≤ m_1
h₂ : Sorted (fun x1 x2 => x1 < x2) (m :: l)
this : n ≤ m
⊢ raise' (lower' (m :: l) n) n = m :: l

Proof state:
m : ℕ
l : List ℕ
n : ℕ
h₁ : ∀ m_1 ∈ m :: l, n ≤ m_1
h₂ : Sorted (fun x1 x2 => x1 < x2) (m :: l)
this : n ≤ m
⊢ raise' (lower' (m :: l) n) n = m :: l

Tactic:
simp [raise', lower', Nat.sub_add_cancel this,
  raise_lower' (List.rel_of_sorted_cons h₂ : ∀ a ∈ l, m < a) h₂.of_cons]

Result:
no goals
-- Mathlib/Data/Vector/Snoc.lean
theorem map₂_snoc {f : α → β → σ} {y : β} :
    map₂ f (xs.snoc x) (ys.snoc y) = (map₂ f xs ys).snoc (f x y)

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
n : ℕ
x : α
xs : Vector α n
ys : Vector β n
f : α → β → σ
y : β
⊢ map₂ f (xs.snoc x) (ys.snoc y) = (map₂ f xs ys).snoc (f x y)

Tactic:
induction xs, ys using Vector.inductionOn₂ <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Pointwise.lean
theorem bot_mul (S : AddSubmonoid R) : ⊥ * S = ⊥ :=
  eq_bot_iff.2 <| mul_le.2 fun m hm n _ => by
    rw [AddSubmonoid.mem_bot] at hm ⊢; rw [hm, zero_mul]

Proof state:
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m ∈ ⊥
n : R
x✝ : n ∈ S
⊢ m * n ∈ ⊥

Tactic:
rw [AddSubmonoid.mem_bot] at hm ⊢

Result:
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m = 0
n : R
x✝ : n ∈ S
⊢ m * n = 0

Proof state:
R : Type u_4
inst✝ : NonUnitalNonAssocSemiring R
S : AddSubmonoid R
m : R
hm : m = 0
n : R
x✝ : n ∈ S
⊢ m * n = 0

Tactic:
rw [hm, zero_mul]

Result:
no goals
-- Mathlib/Algebra/Module/BigOperators.lean
lemma sum_piFinset_apply (f : κ → α) (s : Finset κ) (i : ι) :
    ∑ g ∈ piFinset fun _ : ι ↦ s, f (g i) = #s ^ (card ι - 1) • ∑ b ∈ s, f b

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : AddCommMonoid α
f : κ → α
s : Finset κ
i : ι
⊢ ∑ g ∈ piFinset fun x => s, f (g i) = #s ^ (card ι - 1) • ∑ b ∈ s, f b

Tactic:
classical
rw [Finset.sum_comp]
simp only [eval_image_piFinset_const, card_filter_piFinset_const s, ite_smul, zero_smul, smul_sum,
  Finset.sum_ite_mem, inter_self]

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : AddCommMonoid α
f : κ → α
s : Finset κ
i : ι
⊢ ∑ g ∈ piFinset fun x => s, f (g i) = #s ^ (card ι - 1) • ∑ b ∈ s, f b

Tactic:
rw [Finset.sum_comp]

Result:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : AddCommMonoid α
f : κ → α
s : Finset κ
i : ι
⊢ ∑ b ∈ image (fun g => g i) (piFinset fun x => s), #(filter (fun a => a i = b) (piFinset fun x => s)) • f b =
    #s ^ (card ι - 1) • ∑ b ∈ s, f b

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : AddCommMonoid α
f : κ → α
s : Finset κ
i : ι
⊢ ∑ b ∈ image (fun g => g i) (piFinset fun x => s), #(filter (fun a => a i = b) (piFinset fun x => s)) • f b =
    #s ^ (card ι - 1) • ∑ b ∈ s, f b

Tactic:
simp only [eval_image_piFinset_const, card_filter_piFinset_const s, ite_smul, zero_smul, smul_sum,
  Finset.sum_ite_mem, inter_self]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem C_mul_X_pow_eq_monomial : ∀ {n : ℕ}, C a * X ^ n = monomial n a
  | 0 => mul_one _
  | n + 1 => by
    rw [pow_succ, ← mul_assoc, C_mul_X_pow_eq_monomial, X, monomial_mul_monomial, mul_one]

Proof state:
R : Type u
a : R
inst✝ : Semiring R
n : ℕ
⊢ C a * X ^ (n + 1) = (monomial (n + 1)) a

Tactic:
rw [pow_succ, ← mul_assoc, C_mul_X_pow_eq_monomial, X, monomial_mul_monomial, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem swap_comm (a : Vector α n) {i j : Nat} {hi hj} :
    a.swap i j hi hj = a.swap j i hj hi

Proof state:
case mk
α : Type u_1
n i j : Nat
hi : i < n
hj : j < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ toArray✝.swap i j ⋯ ⋯ = toArray✝.swap j i ⋯ ⋯

Tactic:
rw [Array.swap_comm]

Result:
no goals

Proof state:
case mk
α : Type u_1
n i j : Nat
hi : i < n
hj : j < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.swap i j hi hj =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.swap j i hj hi

Tactic:
simp only [swap_mk, mk.injEq]

Result:
case mk
α : Type u_1
n i j : Nat
hi : i < n
hj : j < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ toArray✝.swap i j ⋯ ⋯ = toArray✝.swap j i ⋯ ⋯

Proof state:
α : Type u_1
n : Nat
a : Vector α n
i j : Nat
hi : i < n
hj : j < n
⊢ a.swap i j hi hj = a.swap j i hj hi

Tactic:
cases a

Result:
case mk
α : Type u_1
n i j : Nat
hi : i < n
hj : j < n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.swap i j hi hj =
    { toArray := toArray✝, size_toArray := size_toArray✝ }.swap j i hj hi
-- Mathlib/Data/Set/Card.lean
lemma encard_preimage_of_bijective (hf : f.Bijective) (t : Set β) : (f ⁻¹' t).encard = t.encard :=
  encard_preimage_of_injective_subset_range hf.injective (by simp [hf.surjective.range_eq])

Proof state:
α : Type u_1
β : Type u_2
f : α → β
hf : Function.Bijective f
t : Set β
⊢ t ⊆ range f

Tactic:
simp [hf.surjective.range_eq]

Result:
no goals