harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/PFunctor/Multivariate/M.lean
theorem M.dest'_eq_dest' {α : TypeVec n} {x : P.last.M} {a₁ : P.A}
    {f₁ : P.last.B a₁ → P.last.M} (h₁ : PFunctor.M.dest x = ⟨a₁, f₁⟩) {a₂ : P.A}
    {f₂ : P.last.B a₂ → P.last.M} (h₂ : PFunctor.M.dest x = ⟨a₂, f₂⟩) (f' : M.Path P x ⟹ α) :
    M.dest' P h₁ f' = M.dest' P h₂ f'

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
x : P.last.M
a₁ : P.A
f₁ : P.last.B a₁ → P.last.M
h₁ : x.dest = ⟨a₁, f₁⟩
a₂ : P.A
f₂ : P.last.B a₂ → P.last.M
h₂ : x.dest = ⟨a₂, f₂⟩
f' : Path P x ⟹ α
⊢ dest' P h₁ f' = dest' P h₂ f'

Tactic:
cases h₁.symm.trans h₂

Result:
case refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
x : P.last.M
a₁ : P.A
f₁ : P.last.B a₁ → P.last.M
h₁ : x.dest = ⟨a₁, f₁⟩
f' : Path P x ⟹ α
h₂ : x.dest = ⟨a₁, f₁⟩
⊢ dest' P h₁ f' = dest' P h₂ f'

Proof state:
case refl
n : ℕ
P : MvPFunctor.{u} (n + 1)
α : TypeVec.{u} n
x : P.last.M
a₁ : P.A
f₁ : P.last.B a₁ → P.last.M
h₁ : x.dest = ⟨a₁, f₁⟩
f' : Path P x ⟹ α
h₂ : x.dest = ⟨a₁, f₁⟩
⊢ dest' P h₁ f' = dest' P h₂ f'

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem vectorSpan_insert_eq_vectorSpan {p : P} {ps : Set P} (h : p ∈ affineSpan k ps) :
    vectorSpan k (insert p ps) = vectorSpan k ps

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
ps : Set P
h : p ∈ affineSpan k ps
⊢ vectorSpan k (insert p ps) = vectorSpan k ps

Tactic:
simp_rw [← direction_affineSpan, affineSpan_insert_eq_affineSpan _ h]

Result:
no goals
-- Mathlib/Geometry/Manifold/Diffeomorph.lean
theorem uniqueDiffOn_image (h : E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F) (hn : 1 ≤ n) {s : Set E} :
    UniqueDiffOn 𝕜 (h '' s) ↔ UniqueDiffOn 𝕜 s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_4
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
h : E ≃ₘ^n⟮𝓘(𝕜, E), 𝓘(𝕜, F)⟯ F
hn : 1 ≤ n
s : Set E
⊢ UniqueDiffOn 𝕜 (⇑h '' s) ↔ UniqueDiffOn 𝕜 s

Tactic:
simp only [← uniqueMDiffOn_iff_uniqueDiffOn, uniqueMDiffOn_image, hn]

Result:
no goals
-- Mathlib/Data/Fin/VecNotation.lean
theorem cons_val_succ (x : α) (u : Fin m → α) (i : Fin m) : vecCons x u i.succ = u i

Proof state:
α : Type u
m : ℕ
x : α
u : Fin m → α
i : Fin m
⊢ vecCons x u i.succ = u i

Tactic:
simp [vecCons]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalHorizontalCompAux_cons {f f' g g' h i : C} {η : f ⟶ g} {ηs : f' ⟶ g'} {θ : h ⟶ i}
    {ηθ : f' ⊗ h ⟶ g' ⊗ i} {η₁ : f ⊗ (f' ⊗ h) ⟶ g ⊗ (g' ⊗ i)}
    {ηθ₁ : f ⊗ (f' ⊗ h) ⟶ (g ⊗ g') ⊗ i} {ηθ₂ : (f ⊗ f') ⊗ h ⟶ (g ⊗ g') ⊗ i}
    (e_ηθ : ηs ⊗ θ = ηθ) (e_η₁ : ((Iso.refl _).hom ≫ η ≫ (Iso.refl _).hom) ⊗ ηθ = η₁)
    (e_ηθ₁ : η₁ ≫ (α_ _ _ _).inv = ηθ₁) (e_ηθ₂ : (α_ _ _ _).hom ≫ ηθ₁ = ηθ₂) :
    (η ⊗ ηs) ⊗ θ = ηθ₂

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f f' g g' h i : C
η : f ⟶ g
ηs : f' ⟶ g'
θ : h ⟶ i
ηθ : f' ⊗ h ⟶ g' ⊗ i
η₁ : f ⊗ f' ⊗ h ⟶ g ⊗ g' ⊗ i
ηθ₁ : f ⊗ f' ⊗ h ⟶ (g ⊗ g') ⊗ i
ηθ₂ : (f ⊗ f') ⊗ h ⟶ (g ⊗ g') ⊗ i
e_ηθ : ηs ⊗ θ = ηθ
e_η₁ : (Iso.refl f).hom ≫ η ≫ (Iso.refl g).hom ⊗ ηθ = η₁
e_ηθ₁ : η₁ ≫ (α_ g g' i).inv = ηθ₁
e_ηθ₂ : (α_ f f' h).hom ≫ ηθ₁ = ηθ₂
⊢ (η ⊗ ηs) ⊗ θ = ηθ₂

Tactic:
simp_all

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean
theorem isSheaf_iff_preservesFiniteProducts_and_equalizerCondition
    [Preregular C] [FinitaryExtensive C]
    [h : ∀ {Y X : C} (f : Y ⟶ X) [EffectiveEpi f], HasPullback f f] :
    IsSheaf (coherentTopology C) F ↔ PreservesFiniteProducts F ∧
      EqualizerCondition F

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
A : Type u₃
inst✝² : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝¹ : Preregular C
inst✝ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
⊢ IsSheaf (coherentTopology C) F ↔ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
rw [isSheaf_coherent_iff_regular_and_extensive]

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
A : Type u₃
inst✝² : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝¹ : Preregular C
inst✝ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
⊢ IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F ↔ PreservesFiniteProducts F ∧ EqualizerCondition F

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
A : Type u₃
inst✝² : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝¹ : Preregular C
inst✝ : FinitaryExtensive C
h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f
⊢ IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F ↔ PreservesFiniteProducts F ∧ EqualizerCondition F

Tactic:
exact and_congr (isSheaf_iff_preservesFiniteProducts _)
  (@equalizerCondition_iff_isSheaf _ _ _ _ F _ h).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatMap_map (f : α → β) (g : β → List γ) (l : List α) :
    (map f l).flatMap g = l.flatMap (fun a => g (f a))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → List γ
l : List α
⊢ flatMap g (map f l) = flatMap (fun a => g (f a)) l

Tactic:
induction l <;> simp [flatMap_cons, *]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem ext {x y : 𝕎 R} (h : ∀ n, x.coeff n = y.coeff n) : x = y

Proof state:
case mk'.mk'
p : ℕ
R : Type u_1
coeff✝¹ coeff✝ : ℕ → R
h : ∀ (n : ℕ), coeff✝¹ n = coeff✝ n
⊢ { coeff := coeff✝¹ } = { coeff := coeff✝ }

Tactic:
simp [funext_iff, h]

Result:
no goals

Proof state:
case mk'
p : ℕ
R : Type u_1
y : 𝕎 R
coeff✝ : ℕ → R
h : ∀ (n : ℕ), { coeff := coeff✝ }.coeff n = y.coeff n
⊢ { coeff := coeff✝ } = y

Tactic:
cases y

Result:
case mk'.mk'
p : ℕ
R : Type u_1
coeff✝¹ coeff✝ : ℕ → R
h : ∀ (n : ℕ), { coeff := coeff✝¹ }.coeff n = { coeff := coeff✝ }.coeff n
⊢ { coeff := coeff✝¹ } = { coeff := coeff✝ }

Proof state:
p : ℕ
R : Type u_1
x y : 𝕎 R
h : ∀ (n : ℕ), x.coeff n = y.coeff n
⊢ x = y

Tactic:
cases x

Result:
case mk'
p : ℕ
R : Type u_1
y : 𝕎 R
coeff✝ : ℕ → R
h : ∀ (n : ℕ), { coeff := coeff✝ }.coeff n = y.coeff n
⊢ { coeff := coeff✝ } = y

Proof state:
case mk'.mk'
p : ℕ
R : Type u_1
coeff✝¹ coeff✝ : ℕ → R
h : ∀ (n : ℕ), { coeff := coeff✝¹ }.coeff n = { coeff := coeff✝ }.coeff n
⊢ { coeff := coeff✝¹ } = { coeff := coeff✝ }

Tactic:
simp only at h

Result:
case mk'.mk'
p : ℕ
R : Type u_1
coeff✝¹ coeff✝ : ℕ → R
h : ∀ (n : ℕ), coeff✝¹ n = coeff✝ n
⊢ { coeff := coeff✝¹ } = { coeff := coeff✝ }
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem areaForm_le (x y : E) : ω x y ≤ ‖x‖ * ‖y‖

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.areaForm x) y ≤ ‖x‖ * ‖y‖

Tactic:
simpa [areaForm_to_volumeForm, Fin.prod_univ_succ] using o.volumeForm_apply_le ![x, y]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem tangentMap_prod_right {p : TangentBundle I' M'} {x₀ : M} :
    tangentMap I' (I.prod I') (fun y => (x₀, y)) p = ⟨(x₀, p.1), (0, p.2)⟩

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
p : TangentBundle I' M'
x₀ : M
⊢ tangentMap I' (I.prod I') (fun y => (x₀, y)) p = { proj := (x₀, p.proj), snd := (0, p.snd) }

Tactic:
simp only [tangentMap, mfderiv_prod_right, TotalSpace.mk_inj]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
p : TangentBundle I' M'
x₀ : M
⊢ (ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' p.proj)) p.snd = (0, p.snd)

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
p : TangentBundle I' M'
x₀ : M
⊢ (ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' p.proj)) p.snd = (0, p.snd)

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem measure_Ico (a b : ℝ) : f.measure (Ico a b) = ofReal (leftLim f b - leftLim f a)

Proof state:
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ 0 = ofReal (leftLim (↑f) b - leftLim (↑f) a)

Tactic:
symm

Result:
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ ofReal (leftLim (↑f) b - leftLim (↑f) a) = 0

Proof state:
f : StieltjesFunction
a b : ℝ
⊢ f.measure (Ico a b) = ofReal (leftLim (↑f) b - leftLim (↑f) a)

Tactic:
rcases le_or_lt b a with (hab | hab)

Result:
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ f.measure (Ico a b) = ofReal (leftLim (↑f) b - leftLim (↑f) a)

case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
⊢ f.measure (Ico a b) = ofReal (leftLim (↑f) b - leftLim (↑f) a)

Proof state:
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ ofReal (leftLim (↑f) b - leftLim (↑f) a) = 0

Tactic:
simp [ENNReal.ofReal_eq_zero, f.mono.leftLim hab]

Result:
no goals

Proof state:
f : StieltjesFunction
a b : ℝ
hab : a < b
⊢ Disjoint {a} (Ioo a b)

Tactic:
simp

Result:
no goals

Proof state:
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
⊢ f.measure (Ico a b) = ofReal (leftLim (↑f) b - leftLim (↑f) a)

Tactic:
have A : Disjoint {a} (Ioo a b) := by simp

Result:
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint {a} (Ioo a b)
⊢ f.measure (Ico a b) = ofReal (leftLim (↑f) b - leftLim (↑f) a)

Proof state:
case inr
f : StieltjesFunction
a b : ℝ
hab : a < b
A : Disjoint {a} (Ioo a b)
⊢ f.measure (Ico a b) = ofReal (leftLim (↑f) b - leftLim (↑f) a)

Tactic:
simp [← Icc_union_Ioo_eq_Ico le_rfl hab, -singleton_union, hab.ne, f.mono.leftLim_le,
  measure_union A measurableSet_Ioo, f.mono.le_leftLim hab, ← ENNReal.ofReal_add]

Result:
no goals

Proof state:
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ f.measure (Ico a b) = ofReal (leftLim (↑f) b - leftLim (↑f) a)

Tactic:
simp only [hab, measure_empty, Ico_eq_empty, not_lt]

Result:
case inl
f : StieltjesFunction
a b : ℝ
hab : b ≤ a
⊢ 0 = ofReal (leftLim (↑f) b - leftLim (↑f) a)
-- Mathlib/RingTheory/AdicCompletion/Functoriality.lean
theorem transitionMap_comp_reduceModIdeal (f : M →ₗ[R] N) {m n : ℕ}
    (hmn : m ≤ n) : transitionMap I N hmn ∘ₗ f.reduceModIdeal (I ^ n) =
      (f.reduceModIdeal (I ^ m) : _ →ₗ[R] _) ∘ₗ transitionMap I M hmn

Proof state:
case h.h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
m n : ℕ
hmn : m ≤ n
x : M
⊢ ((transitionMap I N hmn ∘ₗ ↑R (reduceModIdeal (I ^ n) f)) ∘ₗ (I ^ n • ⊤).mkQ) x =
    ((↑R (reduceModIdeal (I ^ m) f) ∘ₗ transitionMap I M hmn) ∘ₗ (I ^ n • ⊤).mkQ) x

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
m n : ℕ
hmn : m ≤ n
⊢ transitionMap I N hmn ∘ₗ ↑R (reduceModIdeal (I ^ n) f) = ↑R (reduceModIdeal (I ^ m) f) ∘ₗ transitionMap I M hmn

Tactic:
ext x

Result:
case h.h
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
m n : ℕ
hmn : m ≤ n
x : M
⊢ ((transitionMap I N hmn ∘ₗ ↑R (reduceModIdeal (I ^ n) f)) ∘ₗ (I ^ n • ⊤).mkQ) x =
    ((↑R (reduceModIdeal (I ^ m) f) ∘ₗ transitionMap I M hmn) ∘ₗ (I ^ n • ⊤).mkQ) x
-- Mathlib/Data/Nat/Factors.lean
theorem primeFactorsList_unique {n : ℕ} {l : List ℕ} (h₁ : prod l = n) (h₂ : ∀ p ∈ l, Prime p) :
    l ~ primeFactorsList n

Proof state:
case refine_2
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ p ∈ l, Prime p
⊢ ∀ p ∈ l, Prime p

Tactic:
exact h₂

Result:
no goals

Proof state:
case refine_1
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ p ∈ l, Prime p
⊢ l.prod = n.primeFactorsList.prod

Tactic:
rw [h₁]

Result:
case refine_1
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ p ∈ l, Prime p
⊢ n = n.primeFactorsList.prod

Proof state:
case refine_2
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ p ∈ l, Prime p
⊢ ∀ p ∈ l, _root_.Prime p

Tactic:
simp_rw [← prime_iff]

Result:
case refine_2
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ p ∈ l, Prime p
⊢ ∀ p ∈ l, Prime p

Proof state:
case refine_1
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ p ∈ l, Prime p
⊢ n = n.primeFactorsList.prod

Tactic:
refine (prod_primeFactorsList ?_).symm

Result:
case refine_1
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ p ∈ l, Prime p
⊢ n ≠ 0

Proof state:
case refine_3
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ p ∈ l, Prime p
⊢ ∀ p ∈ n.primeFactorsList, _root_.Prime p

Tactic:
simp_rw [← prime_iff]

Result:
case refine_3
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ p ∈ l, Prime p
⊢ ∀ p ∈ n.primeFactorsList, Prime p

Proof state:
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ p ∈ l, Prime p
⊢ l ~ n.primeFactorsList

Tactic:
refine perm_of_prod_eq_prod ?_ ?_ ?_

Result:
case refine_1
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ p ∈ l, Prime p
⊢ l.prod = n.primeFactorsList.prod

case refine_2
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ p ∈ l, Prime p
⊢ ∀ p ∈ l, _root_.Prime p

case refine_3
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ p ∈ l, Prime p
⊢ ∀ p ∈ n.primeFactorsList, _root_.Prime p

Proof state:
case refine_1
l : List ℕ
h₂ : ∀ p ∈ l, Prime p
h₁ : 0 ∈ l
⊢ False

Tactic:
exact Prime.ne_zero (h₂ 0 h₁) rfl

Result:
no goals

Proof state:
case refine_3
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ p ∈ l, Prime p
⊢ ∀ p ∈ n.primeFactorsList, Prime p

Tactic:
exact fun p => prime_of_mem_primeFactorsList

Result:
no goals

Proof state:
case refine_1
l : List ℕ
h₂ : ∀ p ∈ l, Prime p
h₁ : l.prod = 0
⊢ False

Tactic:
rw [prod_eq_zero_iff] at h₁

Result:
case refine_1
l : List ℕ
h₂ : ∀ p ∈ l, Prime p
h₁ : 0 ∈ l
⊢ False

Proof state:
case refine_1
n : ℕ
l : List ℕ
h₁ : l.prod = n
h₂ : ∀ p ∈ l, Prime p
⊢ n ≠ 0

Tactic:
rintro rfl

Result:
case refine_1
l : List ℕ
h₂ : ∀ p ∈ l, Prime p
h₁ : l.prod = 0
⊢ False
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
theorem IsBlock.translate (g : G) (hB : IsBlock G B) :
    IsBlock G (g • B)

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ IsBlock (↥⊤) (g • B)

Tactic:
rw [← Subgroup.map_comap_eq_self_of_surjective
        (G := G) (f := MulAut.conj g) (MulAut.conj g).surjective ⊤]

Result:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ IsBlock (↥(Subgroup.map (↑(MulAut.conj g)) (Subgroup.comap ↑(MulAut.conj g) ⊤))) (g • B)

Proof state:
case hB
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ IsBlock (↥(Subgroup.comap ↑(MulAut.conj g) ⊤)) B

Tactic:
rwa [Subgroup.comap_top]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock G B
⊢ IsBlock G (g • B)

Tactic:
rw [← isBlock_top] at hB ⊢

Result:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ IsBlock (↥⊤) (g • B)

Proof state:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ IsBlock (↥(Subgroup.map (↑(MulAut.conj g)) (Subgroup.comap ↑(MulAut.conj g) ⊤))) (g • B)

Tactic:
apply IsBlock.of_subgroup_of_conjugate

Result:
case hB
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
g : G
hB : IsBlock (↥⊤) B
⊢ IsBlock (↥(Subgroup.comap ↑(MulAut.conj g) ⊤)) B
-- Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean
theorem colimitPresheafObjIsoComponentwiseLimit_inv_ι_app (F : J ⥤ PresheafedSpace.{_, _, v} C)
    (U : Opens (Limits.colimit F).carrier) (j : J) :
    (colimitPresheafObjIsoComponentwiseLimit F U).inv ≫ (colimit.ι F j).c.app (op U) =
      limit.π _ (op j)

Proof state:
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ ((sheafIsoOfIso
                (colimit.isoColimitCocone
                    { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm).app
            (op U) ≪≫
          limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
              ((Opens.map
                      (colimit.isoColimitCocone
                              { cocone := colimitCocone F,
                                isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
                (op U)) ≪≫
            Limits.lim.mapIso (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫
      (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)

Tactic:
rw [Iso.trans_inv, Iso.trans_inv, Iso.app_inv, sheafIsoOfIso_inv, pushforwardToOfIso_app,
  congr_app (Iso.symm_inv _)]

Result:
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ (((Limits.lim.mapIso (NatIso.ofComponents (fun X => mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫
          (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
              ((Opens.map
                      (colimit.isoColimitCocone
                              { cocone := colimitCocone F,
                                isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
                (op U))).inv) ≫
        ((colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.c.app
              (op
                ((Opens.map
                      ((forget C).mapIso
                            (colimit.isoColimitCocone
                                { cocone := colimitCocone F,
                                  isColimit := colimitCoconeIsColimit F }).symm).symm.inv).obj
                  (unop (op U)))) ≫
            (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫
          (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫
      (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContinuousLinearMap.iteratedFDeriv_comp_right (g : G →L[𝕜] E) {f : E → F}
    (hf : ContDiff 𝕜 n f) (x : G) {i : ℕ} (hi : i ≤ n) :
    iteratedFDeriv 𝕜 i (f ∘ g) x =
      (iteratedFDeriv 𝕜 i f (g x)).compContinuousLinearMap fun _ => g

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
g : G →L[𝕜] E
f : E → F
hf : ContDiff 𝕜 n f
x : G
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDeriv 𝕜 i (f ∘ ⇑g) x = (iteratedFDeriv 𝕜 i f (g x)).compContinuousLinearMap fun x => g

Tactic:
simp only [← iteratedFDerivWithin_univ]

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
g : G →L[𝕜] E
f : E → F
hf : ContDiff 𝕜 n f
x : G
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) univ x = (iteratedFDerivWithin 𝕜 i f univ (g x)).compContinuousLinearMap fun x => g

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
g : G →L[𝕜] E
f : E → F
hf : ContDiff 𝕜 n f
x : G
i : ℕ
hi : ↑i ≤ n
⊢ iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) univ x = (iteratedFDerivWithin 𝕜 i f univ (g x)).compContinuousLinearMap fun x => g

Tactic:
exact g.iteratedFDerivWithin_comp_right hf.contDiffOn uniqueDiffOn_univ uniqueDiffOn_univ
    (mem_univ _) hi

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_neg {S} [Ring S] (f : R →+* S) {x : S} : (-p).eval₂ f x = -p.eval₂ f x

Proof state:
R : Type u
inst✝¹ : Ring R
p : R[X]
S : Type u_1
inst✝ : Ring S
f : R →+* S
x : S
⊢ eval₂ f x (-p) = -eval₂ f x p

Tactic:
rw [eq_neg_iff_add_eq_zero, ← eval₂_add, neg_add_cancel, eval₂_zero]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Abs.lean
lemma pow_eq_pow_iff_cases : a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n

Proof state:
R : Type u_2
inst✝ : LinearOrderedRing R
a b : R
n : ℕ
⊢ a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n

Tactic:
rcases eq_or_ne n 0 with rfl | hn <;> simp [pow_eq_pow_iff_of_ne_zero, *]

Result:
no goals