harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/MorphismProperty/Comma.lean
@[ext]
lemma Under.Hom.ext {A B : P.Under Q X} {f g : A ⟶ B} (h : f.right = g.right) : f = g

Proof state:
case h.h₁
T : Type u_1
inst✝¹ : Category.{u_2, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Under Q X
f g : A ⟶ B
h : f.right = g.right
⊢ (Comma.Hom.hom f).left = (Comma.Hom.hom g).left

Tactic:
simp

Result:
no goals

Proof state:
T : Type u_1
inst✝¹ : Category.{u_2, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Under Q X
f g : A ⟶ B
h : f.right = g.right
⊢ f = g

Tactic:
ext

Result:
case h.h₁
T : Type u_1
inst✝¹ : Category.{u_2, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Under Q X
f g : A ⟶ B
h : f.right = g.right
⊢ (Comma.Hom.hom f).left = (Comma.Hom.hom g).left

case h.h₂
T : Type u_1
inst✝¹ : Category.{u_2, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Under Q X
f g : A ⟶ B
h : f.right = g.right
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right

Proof state:
case h.h₂
T : Type u_1
inst✝¹ : Category.{u_2, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Under Q X
f g : A ⟶ B
h : f.right = g.right
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right

Tactic:
exact h

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem braiding_naturality {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :
    (f ⊗ g) ≫ (braiding Y Y').hom = (braiding X X').hom ≫ (g ⊗ f)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (f ⊗ g) ≫ (β_ Y Y').hom = (β_ X X').hom ≫ (g ⊗ f)

Tactic:
rw [tensorHom_def' f g, tensorHom_def g f]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (X ◁ g ≫ f ▷ Y') ≫ (β_ Y Y').hom = (β_ X X').hom ≫ g ▷ X ≫ Y' ◁ f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ (X ◁ g ≫ f ▷ Y') ≫ (β_ Y Y').hom = (β_ X X').hom ≫ g ▷ X ≫ Y' ◁ f

Tactic:
simp_rw [Category.assoc, braiding_naturality_left, braiding_naturality_right_assoc]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Supported.lean
theorem supported_eq_range_rename (s : Set σ) : supported R s = (rename ((↑) : s → σ)).range

Proof state:
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
⊢ (aeval fun x => X ↑x).range = (aeval (X ∘ Subtype.val)).range

Tactic:
congr

Result:
no goals

Proof state:
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
⊢ supported R s = (rename Subtype.val).range

Tactic:
rw [supported, Set.image_eq_range, adjoin_range_eq_range_aeval, rename]

Result:
σ : Type u_1
R : Type u
inst✝ : CommSemiring R
s : Set σ
⊢ (aeval fun x => X ↑x).range = (aeval (X ∘ Subtype.val)).range
-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem epi_iff_surjective : Epi f ↔ Function.Surjective f

Proof state:
A B : CommGrp
f : A ⟶ B
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
rw [epi_iff_range_eq_top, MonoidHom.range_eq_top]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
lemma AddSubgroup.zmultiples_one_eq_top : zmultiples (1 : ℤ) = ⊤

Proof state:
⊢ zmultiples 1 = ⊤

Tactic:
rw [zmultiples_eq_closure, closure_singleton_int_one_eq_top]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma coindep_iff_closure_compl_eq_ground (hK : X ⊆ M.E

Proof state:
α : Type u_2
M : Matroid α
X : Set α
hK : autoParam (X ⊆ M.E) _auto✝
⊢ M.Coindep X ↔ M.closure (M.E \ X) = M.E

Tactic:
rw [coindep_iff_compl_spanning, spanning_iff_closure_eq]

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem core_comp (s : Rel β γ) (t : Set γ) : core (r • s) t = core r (core s t)

Proof state:
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
x : α
⊢ (∀ (y : γ) (x_1 : β), r x x_1 → s x_1 y → y ∈ t) → ∀ (y : β), r x y → ∀ (y_1 : γ), s y y_1 → y_1 ∈ t

Tactic:
exact fun h y rxy z => h z y rxy

Result:
no goals

Proof state:
case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
x : α
⊢ (∀ (y : β), r x y → ∀ (y_1 : γ), s y y_1 → y_1 ∈ t) → ∀ (y : γ) (x_1 : β), r x x_1 → s x_1 y → y ∈ t

Tactic:
exact fun h z y rzy => h y rzy z

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
x : α
⊢ (∀ (y : γ) (x_1 : β), r x x_1 → s x_1 y → y ∈ t) ↔ ∀ (y : β), r x y → ∀ (y_1 : γ), s y y_1 → y_1 ∈ t

Tactic:
constructor

Result:
case h.mp
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
x : α
⊢ (∀ (y : γ) (x_1 : β), r x x_1 → s x_1 y → y ∈ t) → ∀ (y : β), r x y → ∀ (y_1 : γ), s y y_1 → y_1 ∈ t

case h.mpr
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
x : α
⊢ (∀ (y : β), r x y → ∀ (y_1 : γ), s y y_1 → y_1 ∈ t) → ∀ (y : γ) (x_1 : β), r x x_1 → s x_1 y → y ∈ t

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
⊢ (r • s).core t = r.core (s.core t)

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
x : α
⊢ x ∈ (r • s).core t ↔ x ∈ r.core (s.core t)

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
x : α
⊢ x ∈ (r • s).core t ↔ x ∈ r.core (s.core t)

Tactic:
simp only [core, comp, forall_exists_index, and_imp, Set.mem_setOf_eq]

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
r : Rel α β
s : Rel β γ
t : Set γ
x : α
⊢ (∀ (y : γ) (x_1 : β), r x x_1 → s x_1 y → y ∈ t) ↔ ∀ (y : β), r x y → ∀ (y_1 : γ), s y y_1 → y_1 ∈ t
-- Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean
lemma minSmoothness_monotone : Monotone (minSmoothness 𝕜)

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
hmn : m ≤ n
⊢ (if IsRCLikeNormedField 𝕜 then m else ω) ≤ if IsRCLikeNormedField 𝕜 then n else ω

Tactic:
split_ifs <;> simp [hmn]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
hmn : m ≤ n
⊢ minSmoothness 𝕜 m ≤ minSmoothness 𝕜 n

Tactic:
simp only [minSmoothness]

Result:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
hmn : m ≤ n
⊢ (if IsRCLikeNormedField 𝕜 then m else ω) ≤ if IsRCLikeNormedField 𝕜 then n else ω

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
⊢ Monotone (minSmoothness 𝕜)

Tactic:
intro m n hmn

Result:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
m n : WithTop ℕ∞
hmn : m ≤ n
⊢ minSmoothness 𝕜 m ≤ minSmoothness 𝕜 n
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
theorem iteratedDeriv_comp_const_smul {n : ℕ} {f : 𝕜 → F} (h : ContDiff 𝕜 n f) (c : 𝕜) :
    iteratedDeriv n (fun x => f (c * x)) = fun x => c ^ n • iteratedDeriv n f (c * x)

Proof state:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
h : ContDiff 𝕜 (↑n) f
c x : 𝕜
⊢ iteratedDeriv n (fun x => f (c * x)) x = c ^ n • iteratedDeriv n f (c * x)

Tactic:
simpa only [iteratedDerivWithin_univ] using
  iteratedDerivWithin_comp_const_smul (Set.mem_univ x) uniqueDiffOn_univ (contDiffOn_univ.mpr h)
    c (Set.mapsTo_univ _ _)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
h : ContDiff 𝕜 (↑n) f
c : 𝕜
⊢ (iteratedDeriv n fun x => f (c * x)) = fun x => c ^ n • iteratedDeriv n f (c * x)

Tactic:
funext x

Result:
case h
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
h : ContDiff 𝕜 (↑n) f
c x : 𝕜
⊢ iteratedDeriv n (fun x => f (c * x)) x = c ^ n • iteratedDeriv n f (c * x)
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem cos_eq_iff_quadratic {z w : ℂ} :
    cos z = w ↔ exp (z * I) ^ 2 - 2 * w * exp (z * I) + 1 = 0

Proof state:
z w : ℂ
⊢ cos z - w = 0 ↔ cexp (z * I) ^ 2 - 2 * w * cexp (z * I) + 1 = 0

Tactic:
field_simp [cos, exp_neg, exp_ne_zero]

Result:
z w : ℂ
⊢ cexp (z * I) * cexp (z * I) + 1 - cexp (z * I) * 2 * w = 0 ↔ cexp (z * I) ^ 2 - 2 * w * cexp (z * I) + 1 = 0

Proof state:
z w : ℂ
⊢ cexp (z * I) * cexp (z * I) + 1 - cexp (z * I) * 2 * w = 0 ↔ cexp (z * I) ^ 2 - 2 * w * cexp (z * I) + 1 = 0

Tactic:
refine Eq.congr ?_ rfl

Result:
z w : ℂ
⊢ cexp (z * I) * cexp (z * I) + 1 - cexp (z * I) * 2 * w = cexp (z * I) ^ 2 - 2 * w * cexp (z * I) + 1

Proof state:
z w : ℂ
⊢ cexp (z * I) * cexp (z * I) + 1 - cexp (z * I) * 2 * w = cexp (z * I) ^ 2 - 2 * w * cexp (z * I) + 1

Tactic:
ring

Result:
no goals

Proof state:
z w : ℂ
⊢ cos z = w ↔ cexp (z * I) ^ 2 - 2 * w * cexp (z * I) + 1 = 0

Tactic:
rw [← sub_eq_zero]

Result:
z w : ℂ
⊢ cos z - w = 0 ↔ cexp (z * I) ^ 2 - 2 * w * cexp (z * I) + 1 = 0
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_sub_zsmul' (a b : α) (m : ℤ) :
    toIocDiv hp (a - m • p) b = toIocDiv hp a b + m

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp (a - m • p) b = toIocDiv hp a b + m

Tactic:
rw [sub_eq_add_neg, ← neg_smul, toIocDiv_add_zsmul', sub_neg_eq_add]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive]
lemma image_pow_of_ne_zero [MulHomClass F α β] :
    ∀ {n}, n ≠ 0 → ∀ (f : F) (s : Set α), f '' (s ^ n) = (f '' s) ^ n
  | 1, _ => by simp
  | n + 2, _ => by simp [image_mul, pow_succ _ n.succ, image_pow_of_ne_zero]

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
x✝ : 1 ≠ 0
⊢ ∀ (f : F) (s : Set α), ⇑f '' (s ^ 1) = (⇑f '' s) ^ 1

Tactic:
simp

Result:
no goals

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ∀ (f : F) (s : Set α), ⇑f '' (s ^ (n + 2)) = (⇑f '' s) ^ (n + 2)

Tactic:
simp [image_mul, pow_succ _ n.succ, image_pow_of_ne_zero]

Result:
no goals
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem LinearOrderedAddCommGroup.tendsto_nhds {x : Filter β} {a : α} :
    Tendsto f x (𝓝 a) ↔ ∀ ε > (0 : α), ∀ᶠ b in x, |f b - a| < ε

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : OrderTopology α
f : β → α
x : Filter β
a : α
⊢ Tendsto f x (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ (b : β) in x, |f b - a| < ε

Tactic:
simp [nhds_eq_iInf_abs_sub, abs_sub_comm a]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem HasMFDerivWithinAt.mul (hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p')
    (hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q') :
    HasMFDerivWithinAt I 𝓘(𝕜, F') (p * q) s z (p z • q' + q z • p' : E →L[𝕜] F')

Proof state:
case h.e'_24.h.e'_6.h
𝕜 : 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
s : Set M
z : M
F' : Type u_21
inst✝¹ : NormedCommRing F'
inst✝ : NormedAlgebra 𝕜 F'
p q : M → F'
p' q' : TangentSpace I z →L[𝕜] F'
hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'
hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q'
x✝ : TangentSpace I z
⊢ (q z • p') x✝ = (p'.smulRight (q z)) x✝

Tactic:
apply mul_comm

Result:
no goals

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
s : Set M
z : M
F' : Type u_21
inst✝¹ : NormedCommRing F'
inst✝ : NormedAlgebra 𝕜 F'
p q : M → F'
p' q' : TangentSpace I z →L[𝕜] F'
hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'
hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q'
⊢ HasMFDerivWithinAt I 𝓘(𝕜, F') (p * q) s z (p z • q' + q z • p')

Tactic:
convert hp.mul' hq

Result:
case h.e'_24.h.e'_6
𝕜 : 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
s : Set M
z : M
F' : Type u_21
inst✝¹ : NormedCommRing F'
inst✝ : NormedAlgebra 𝕜 F'
p q : M → F'
p' q' : TangentSpace I z →L[𝕜] F'
hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'
hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q'
⊢ q z • p' = p'.smulRight (q z)

Proof state:
case h.e'_24.h.e'_6
𝕜 : 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
s : Set M
z : M
F' : Type u_21
inst✝¹ : NormedCommRing F'
inst✝ : NormedAlgebra 𝕜 F'
p q : M → F'
p' q' : TangentSpace I z →L[𝕜] F'
hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'
hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q'
⊢ q z • p' = p'.smulRight (q z)

Tactic:
ext _

Result:
case h.e'_24.h.e'_6.h
𝕜 : 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
s : Set M
z : M
F' : Type u_21
inst✝¹ : NormedCommRing F'
inst✝ : NormedAlgebra 𝕜 F'
p q : M → F'
p' q' : TangentSpace I z →L[𝕜] F'
hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'
hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q'
x✝ : TangentSpace I z
⊢ (q z • p') x✝ = (p'.smulRight (q z)) x✝
-- Mathlib/Data/Set/Image.lean
theorem subset_image_compl {f : α → β} {s : Set α} (H : Surjective f) : (f '' s)ᶜ ⊆ f '' sᶜ :=
  compl_subset_iff_union.2 <| by
    rw [← image_union]
    simp [image_univ_of_surjective H]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
H : Surjective f
⊢ f '' (s ∪ sᶜ) = univ

Tactic:
simp [image_univ_of_surjective H]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
H : Surjective f
⊢ f '' s ∪ f '' sᶜ = univ

Tactic:
rw [← image_union]

Result:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
H : Surjective f
⊢ f '' (s ∪ sᶜ) = univ
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem braiding_inv_tensorUnit_right (X : C) : (β_ X (𝟙_ C)).inv = (λ_ X).hom ≫ (ρ_ X).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((ρ_ X).hom ≫ (λ_ X).inv) ≫ (λ_ X).hom ≫ (ρ_ X).inv = 𝟙 (X ⊗ 𝟙_ C)

Tactic:
monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ X (𝟙_ C)).hom ≫ (λ_ X).hom ≫ (ρ_ X).inv = 𝟙 (X ⊗ 𝟙_ C)

Tactic:
rw [braiding_tensorUnit_right]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((ρ_ X).hom ≫ (λ_ X).inv) ≫ (λ_ X).hom ≫ (ρ_ X).inv = 𝟙 (X ⊗ 𝟙_ C)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ X (𝟙_ C)).inv = (λ_ X).hom ≫ (ρ_ X).inv

Tactic:
rw [Iso.inv_ext]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ X (𝟙_ C)).hom ≫ (λ_ X).hom ≫ (ρ_ X).inv = 𝟙 (X ⊗ 𝟙_ C)
-- Mathlib/Algebra/Algebra/Operations.lean
theorem smul_induction_on' {x : M} (hx : x ∈ I • N) {p : ∀ x, x ∈ I • N → Prop}
    (smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) (smul_mem_smul hr hn))
    (add : ∀ x hx y hy, p x hx → p y hy → p (x + y) (add_mem ‹_› ‹_›)) : p x hx

Proof state:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
I : Submodule R A
N : Submodule R M
x : M
hx : x ∈ I • N
p : (x : M) → x ∈ I • N → Prop
smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯
add : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯
⊢ ∃ (x_1 : x ∈ I • N), p x x_1

Tactic:
exact smul_induction_on hx (fun a ha x hx ↦ ⟨_, smul _ ha _ hx⟩)
  fun x y ⟨_, hx⟩ ⟨_, hy⟩ ↦ ⟨_, add _ _ _ _ hx hy⟩

Result:
no goals

Proof state:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
I : Submodule R A
N : Submodule R M
x : M
hx : x ∈ I • N
p : (x : M) → x ∈ I • N → Prop
smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯
add : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯
⊢ p x hx

Tactic:
refine Exists.elim ?_ fun (h : x ∈ I • N) (H : p x h) ↦ H

Result:
R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
I : Submodule R A
N : Submodule R M
x : M
hx : x ∈ I • N
p : (x : M) → x ∈ I • N → Prop
smul : ∀ (r : A) (hr : r ∈ I) (n : M) (hn : n ∈ N), p (r • n) ⋯
add : ∀ (x : M) (hx : x ∈ I • N) (y : M) (hy : y ∈ I • N), p x hx → p y hy → p (x + y) ⋯
⊢ ∃ (x_1 : x ∈ I • N), p x x_1
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem coeff_multiset_prod_of_natDegree_le (n : ℕ) (hl : ∀ p ∈ t, natDegree p ≤ n) :
    coeff t.prod ((Multiset.card t) * n) = (t.map fun p => coeff p n).prod

Proof state:
case h
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
n : ℕ
a✝ : List R[X]
hl : ∀ p ∈ ⟦a✝⟧, p.natDegree ≤ n
⊢ (prod ⟦a✝⟧).coeff (Multiset.card ⟦a✝⟧ * n) = (Multiset.map (fun p => p.coeff n) ⟦a✝⟧).prod

Tactic:
simpa using coeff_list_prod_of_natDegree_le _ _ hl

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
n : ℕ
hl : ∀ p ∈ t, p.natDegree ≤ n
⊢ t.prod.coeff (t.card * n) = (Multiset.map (fun p => p.coeff n) t).prod

Tactic:
induction t using Quotient.inductionOn

Result:
case h
R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
n : ℕ
a✝ : List R[X]
hl : ∀ p ∈ ⟦a✝⟧, p.natDegree ≤ n
⊢ (prod ⟦a✝⟧).coeff (Multiset.card ⟦a✝⟧ * n) = (Multiset.map (fun p => p.coeff n) ⟦a✝⟧).prod
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem getElem_zero_filter (p : α → Bool) (l : Vector α n) (h) :
    (l.filter p)[0] =
      (l.find? p).get (by cases l; simpa [← Array.countP_eq_size_filter] using h)

Proof state:
case mk
α : Type
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : 0 < (Array.filter p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray).size
⊢ (find? p { toArray := toArray✝, size_toArray := size_toArray✝ }).isSome = true

Tactic:
simpa [← Array.countP_eq_size_filter] using h

Result:
no goals

Proof state:
α : Type
n : Nat
p : α → Bool
l : Vector α n
h : 0 < (Array.filter p l.toArray).size
⊢ (Array.filter p l.toArray)[0] = (find? p l).get ⋯

Tactic:
cases l

Result:
case mk
α : Type
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : 0 < (Array.filter p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray).size
⊢ (Array.filter p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray)[0] =
    (find? p { toArray := toArray✝, size_toArray := size_toArray✝ }).get ⋯

Proof state:
α : Type
n : Nat
p : α → Bool
l : Vector α n
h : 0 < (Array.filter p l.toArray).size
⊢ (find? p l).isSome = true

Tactic:
cases l

Result:
case mk
α : Type
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : 0 < (Array.filter p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray).size
⊢ (find? p { toArray := toArray✝, size_toArray := size_toArray✝ }).isSome = true

Proof state:
case mk
α : Type
n : Nat
p : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
h : 0 < (Array.filter p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray).size
⊢ (Array.filter p { toArray := toArray✝, size_toArray := size_toArray✝ }.toArray)[0] =
    (find? p { toArray := toArray✝, size_toArray := size_toArray✝ }).get ⋯

Tactic:
simp [List.getElem_zero_eq_head]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem listTransvecRow_getElem {i : ℕ} (h : i < (listTransvecRow M).length) :
    (listTransvecRow M)[i] =
      letI i' : Fin r := ⟨i, length_listTransvecRow M ▸ h⟩
      transvection (inr unit) (inl i') <| -M (inr unit) (inl i') / M (inr unit) (inr unit)

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : ℕ
h : i < (listTransvecRow M).length
⊢ (listTransvecRow M)[i] = transvection (inr ()) (inl ⟨i, ⋯⟩) (-M (inr ()) (inl ⟨i, ⋯⟩) / M (inr ()) (inr ()))

Tactic:
simp [listTransvecRow, Fin.cast]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Induced.lean
@[simp]
lemma shiftFunctorAdd_hom_app_obj_of_induced (a b : A) (X : C) :
    letI := HasShift.induced F A s i
    (shiftFunctorAdd D a b).hom.app (F.obj X) =
      (i (a + b)).hom.app X ≫
        F.map ((shiftFunctorAdd C a b).hom.app X) ≫
        (i b).inv.app ((shiftFunctor C a).obj X) ≫
        (s b).map ((i a).inv.app X)

Proof state:
C : Type u_4
D : Type u_2
inst✝⁵ : Category.{u_5, u_4} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
a b : A
X : C
this : HasShift D A := HasShift.induced F A s i
⊢ (shiftFunctorAdd D a b).hom.app (F.obj X) =
    (i (a + b)).hom.app X ≫
      F.map ((shiftFunctorAdd C a b).hom.app X) ≫ (i b).inv.app ((shiftFunctor C a).obj X) ≫ (s b).map ((i a).inv.app X)

Tactic:
simp only [ShiftMkCore.shiftFunctorAdd_eq, HasShift.Induced.add_hom_app_obj]

Result:
no goals

Proof state:
C : Type u_4
D : Type u_2
inst✝⁵ : Category.{u_5, u_4} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
a b : A
X : C
⊢ (shiftFunctorAdd D a b).hom.app (F.obj X) =
    (i (a + b)).hom.app X ≫
      F.map ((shiftFunctorAdd C a b).hom.app X) ≫ (i b).inv.app ((shiftFunctor C a).obj X) ≫ (s b).map ((i a).inv.app X)

Tactic:
letI := HasShift.induced F A s i

Result:
C : Type u_4
D : Type u_2
inst✝⁵ : Category.{u_5, u_4} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
a b : A
X : C
this : HasShift D A := HasShift.induced F A s i
⊢ (shiftFunctorAdd D a b).hom.app (F.obj X) =
    (i (a + b)).hom.app X ≫
      F.map ((shiftFunctorAdd C a b).hom.app X) ≫ (i b).inv.app ((shiftFunctor C a).obj X) ≫ (s b).map ((i a).inv.app X)
-- Mathlib/Order/Interval/Set/ProjIcc.lean
theorem strictMonoOn_projIci : StrictMonoOn (projIci a) (Ici a) := fun x hx y hy hxy => by
  simpa only [projIci_of_mem, hx, hy]

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a x : α
hx : x ∈ Ici a
y : α
hy : y ∈ Ici a
hxy : x < y
⊢ projIci a x < projIci a y

Tactic:
simpa only [projIci_of_mem, hx, hy]

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem mem_map {f : α → β} {y : β} {o : Option α} : y ∈ o.map f ↔ ∃ x ∈ o, f x = y

Proof state:
α : Type u_1
β : Type u_2
f : α → β
y : β
o : Option α
⊢ y ∈ Option.map f o ↔ ∃ x, x ∈ o ∧ f x = y

Tactic:
simp

Result:
no goals