harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean
theorem cyclotomic_eq_minpoly_rat {n : ℕ} {K : Type*} [Field K] {μ : K} (h : IsPrimitiveRoot μ n)
    (hpos : 0 < n) [CharZero K] : cyclotomic n ℚ = minpoly ℚ μ

Proof state:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ map (Int.castRingHom ℚ) (minpoly ℤ μ) = minpoly ℚ μ

Tactic:
exact (minpoly.isIntegrallyClosed_eq_field_fractions' _ (IsPrimitiveRoot.isIntegral h hpos)).symm

Result:
no goals

Proof state:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ cyclotomic n ℚ = minpoly ℚ μ

Tactic:
rw [← map_cyclotomic_int, cyclotomic_eq_minpoly h hpos]

Result:
n : ℕ
K : Type u_2
inst✝¹ : Field K
μ : K
h : IsPrimitiveRoot μ n
hpos : 0 < n
inst✝ : CharZero K
⊢ map (Int.castRingHom ℚ) (minpoly ℤ μ) = minpoly ℚ μ
-- Mathlib/RingTheory/MatrixAlgebra.lean
theorem invFun_zero : invFun n R A 0 = 0

Proof state:
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ invFun n R A 0 = 0

Tactic:
simp [invFun]

Result:
no goals
-- Mathlib/Analysis/Analytic/Polynomial.lean
theorem AnalyticAt.aeval_polynomial (hf : AnalyticAt 𝕜 f z) (p : A[X]) :
    AnalyticAt 𝕜 (fun x ↦ aeval (f x) p) z

Proof state:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
f : E → B
hf : AnalyticAt 𝕜 f z
p : A[X]
⊢ AnalyticAt 𝕜 (fun x => (aeval (f x)) p) z

Tactic:
rw [← analyticWithinAt_univ] at hf ⊢

Result:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f Set.univ z
p : A[X]
⊢ AnalyticWithinAt 𝕜 (fun x => (aeval (f x)) p) Set.univ z

Proof state:
𝕜 : Type u_1
E : Type u_2
A : Type u_3
B : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : CommSemiring A
z : E
inst✝² : NormedRing B
inst✝¹ : NormedAlgebra 𝕜 B
inst✝ : Algebra A B
f : E → B
hf : AnalyticWithinAt 𝕜 f Set.univ z
p : A[X]
⊢ AnalyticWithinAt 𝕜 (fun x => (aeval (f x)) p) Set.univ z

Tactic:
exact hf.aeval_polynomial p

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem FiniteMultiplicity.not_of_one_left (b : α) : ¬ FiniteMultiplicity 1 b

Proof state:
α : Type u_1
inst✝ : Monoid α
b : α
⊢ ¬FiniteMultiplicity 1 b

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
theorem coe_genWeightSpaceOf_zero (x : L) :
    ↑(genWeightSpaceOf M (0 : R) x) = ⨆ k, LinearMap.ker (toEnd R L M x ^ k)

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
x : L
⊢ ↑(genWeightSpaceOf M 0 x) = ⨆ k, LinearMap.ker ((toEnd R L M) x ^ k)

Tactic:
simp [genWeightSpaceOf, ← Module.End.iSup_genEigenspace_eq]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem union_product [DecidableEq α] [DecidableEq β] : (s ∪ s') ×ˢ t = s ×ˢ t ∪ s' ×ˢ t

Proof state:
α : Type u_1
β : Type u_2
s s' : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (s ∪ s') ×ˢ t = s ×ˢ t ∪ s' ×ˢ t

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
s s' : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ (s ∪ s') ×ˢ t ↔ (x, y) ∈ s ×ˢ t ∪ s' ×ˢ t

Proof state:
case h.mk
α : Type u_1
β : Type u_2
s s' : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ (s ∪ s') ×ˢ t ↔ (x, y) ∈ s ×ˢ t ∪ s' ×ˢ t

Tactic:
simp only [or_and_right, mem_union, mem_product]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem orderOf_cycleOf_dvd_orderOf (f : Perm α) (x : α) : orderOf (cycleOf f x) ∣ orderOf f

Proof state:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ orderOf (f.cycleOf x) ∈ f.cycleType

Tactic:
rw [cycleType, Multiset.mem_map]

Result:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ ∃ a ∈ f.cycleFactorsFinset.val, (Finset.card ∘ support) a = orderOf (f.cycleOf x)

Proof state:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ ∃ a ∈ f.cycleFactorsFinset.val, (Finset.card ∘ support) a = orderOf (f.cycleOf x)

Tactic:
refine ⟨f.cycleOf x, ?_, ?_⟩

Result:
case neg.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ f.cycleOf x ∈ f.cycleFactorsFinset.val

case neg.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ (Finset.card ∘ support) (f.cycleOf x) = orderOf (f.cycleOf x)

Proof state:
case neg.refine_2
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ (Finset.card ∘ support) (f.cycleOf x) = orderOf (f.cycleOf x)

Tactic:
simp [(isCycle_cycleOf _ hx).orderOf]

Result:
no goals

Proof state:
case neg.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ f.cycleOf x ∈ f.cycleFactorsFinset.val

Tactic:
rwa [← Finset.mem_def, cycleOf_mem_cycleFactorsFinset_iff, mem_support]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : f.cycleOf x = 1
⊢ orderOf (f.cycleOf x) ∣ orderOf f

Tactic:
simp [hx]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : f x = x
⊢ orderOf (f.cycleOf x) ∣ orderOf f

Tactic:
rw [← cycleOf_eq_one_iff] at hx

Result:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : f.cycleOf x = 1
⊢ orderOf (f.cycleOf x) ∣ orderOf f

Proof state:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ orderOf (f.cycleOf x) ∣ orderOf f

Tactic:
refine dvd_of_mem_cycleType ?_

Result:
case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ orderOf (f.cycleOf x) ∈ f.cycleType

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
⊢ orderOf (f.cycleOf x) ∣ orderOf f

Tactic:
by_cases hx : f x = x

Result:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : f x = x
⊢ orderOf (f.cycleOf x) ∣ orderOf f

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x : α
hx : ¬f x = x
⊢ orderOf (f.cycleOf x) ∣ orderOf f
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_pi_div_sixteen : sin (π / 16) = √(2 - √(2 + √2)) / 2

Proof state:
⊢ sin (π / 16) = √(2 - √(2 + √2)) / 2

Tactic:
trans sin (π / 2 ^ 4)

Result:
⊢ sin (π / 16) = sin (π / 2 ^ 4)


⊢ sin (π / 2 ^ 4) = √(2 - √(2 + √2)) / 2

Proof state:
case e_x.e_a

⊢ 16 = 2 ^ 4

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ sin (π / 16) = sin (π / 2 ^ 4)

Tactic:
congr

Result:
case e_x.e_a

⊢ 16 = 2 ^ 4

Proof state:
⊢ sin (π / 2 ^ 4) = √(2 - √(2 + √2)) / 2

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Ultrafilter/Defs.lean
theorem le_of_inf_neBot' (f : Ultrafilter α) {g : Filter α} (hg : NeBot (g ⊓ f)) : ↑f ≤ g :=
  f.le_of_inf_neBot <| by rwa [inf_comm]

Proof state:
α : Type u
f : Ultrafilter α
g : Filter α
hg : (g ⊓ ↑f).NeBot
⊢ (↑f ⊓ g).NeBot

Tactic:
rwa [inf_comm]

Result:
no goals
-- Mathlib/Algebra/RingQuot.lean
theorem Rel.sub_left {R : Type uR} [Ring R] {r : R → R → Prop} ⦃a b c : R⦄ (h : Rel r a b) :
    Rel r (a - c) (b - c)

Proof state:
R : Type uR
inst✝ : Ring R
r : R → R → Prop
a b c : R
h : Rel r a b
⊢ Rel r (a - c) (b - c)

Tactic:
simp only [sub_eq_add_neg, h.add_left]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem sup_dualAnnihilator_le_inf (U V : Submodule R M) :
    U.dualAnnihilator ⊔ V.dualAnnihilator ≤ (U ⊓ V).dualAnnihilator

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
U V : Submodule R M
⊢ U.dualAnnihilator ⊔ V.dualAnnihilator ≤ (U ⊓ V).dualAnnihilator

Tactic:
rw [le_dualAnnihilator_iff_le_dualCoannihilator, dualCoannihilator_sup_eq]

Result:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
U V : Submodule R M
⊢ U ⊓ V ≤ U.dualAnnihilator.dualCoannihilator ⊓ V.dualAnnihilator.dualCoannihilator

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
U V : Submodule R M
⊢ U ⊓ V ≤ U.dualAnnihilator.dualCoannihilator ⊓ V.dualAnnihilator.dualCoannihilator

Tactic:
apply inf_le_inf <;> exact le_dualAnnihilator_dualCoannihilator _

Result:
no goals
-- Mathlib/Topology/Order/LeftRight.lean
lemma IsAntichain.interior_eq_empty [∀ x : α, (𝓝[<] x).NeBot] {s : Set α}
    (hs : IsAntichain (· ≤ ·) s) : interior s = ∅

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
x : α
hx : x ∈ interior s
this : ∀ᶠ (y : α) in 𝓝 x, y ∈ s
⊢ False

Tactic:
rcases this.exists_lt with ⟨y, hyx, hys⟩

Result:
case intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
x : α
hx : x ∈ interior s
this : ∀ᶠ (y : α) in 𝓝 x, y ∈ s
y : α
hyx : y < x
hys : y ∈ s
⊢ False

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
x : α
hx : x ∈ interior s
⊢ False

Tactic:
have : ∀ᶠ y in 𝓝 x, y ∈ s := mem_interior_iff_mem_nhds.1 hx

Result:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
x : α
hx : x ∈ interior s
this : ∀ᶠ (y : α) in 𝓝 x, y ∈ s
⊢ False

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
⊢ interior s = ∅

Tactic:
refine eq_empty_of_forall_not_mem fun x hx ↦ ?_

Result:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
x : α
hx : x ∈ interior s
⊢ False

Proof state:
case intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun x1 x2 => x1 ≤ x2) s
x : α
hx : x ∈ interior s
this : ∀ᶠ (y : α) in 𝓝 x, y ∈ s
y : α
hyx : y < x
hys : y ∈ s
⊢ False

Tactic:
exact hs hys (interior_subset hx) hyx.ne hyx.le

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem option_bind {f : α → Option β} {g : α → β → Option σ} (hf : Primrec f) (hg : Primrec₂ g) :
    Primrec fun a => (f a).bind (g a) :=
  (option_casesOn hf (const none) hg).of_eq fun a => by cases f a <;> rfl

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : α → Option β
g : α → β → Option σ
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ Option.casesOn (f a) none (g a) = (f a).bind (g a)

Tactic:
cases f a <;> rfl

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Radical.lean
theorem divRadical_dvd_wronskian_right (a b : k[X]) : divRadical b ∣ wronskian a b

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical b ∣ a.wronskian b

Tactic:
rw [← wronskian_neg_eq, dvd_neg]

Result:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical b ∣ b.wronskian a

Proof state:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b : k[X]
⊢ divRadical b ∣ b.wronskian a

Tactic:
exact divRadical_dvd_wronskian_left _ _

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_eq_one_iff_inv_eq' : a * b = 1 ↔ b⁻¹ = a

Proof state:
G : Type u_3
inst✝ : Group G
a b : G
⊢ a * b = 1 ↔ b⁻¹ = a

Tactic:
rw [mul_eq_one_iff_eq_inv, eq_comm]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem isLowerSet_compl : IsLowerSet sᶜ ↔ IsUpperSet s :=
  ⟨fun h => by
    convert h.compl
    rw [compl_compl], IsUpperSet.compl⟩

Proof state:
case h.e'_3
α : Type u_1
inst✝ : LE α
s : Set α
h : IsLowerSet sᶜ
⊢ s = sᶜᶜ

Tactic:
rw [compl_compl]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LE α
s : Set α
h : IsLowerSet sᶜ
⊢ IsUpperSet s

Tactic:
convert h.compl

Result:
case h.e'_3
α : Type u_1
inst✝ : LE α
s : Set α
h : IsLowerSet sᶜ
⊢ s = sᶜᶜ
-- Mathlib/Data/Rat/Cast/Defs.lean
/-- If monoid with zero homs `f` and `g` from `ℚ≥0` agree on the naturals then they are equal. -/
lemma ext_nnrat' (h : ∀ n : ℕ, f n = g n) : f = g :=
  (DFunLike.ext f g) fun r => by
    rw [← r.num_div_den, div_eq_mul_inv, map_mul, map_mul, h, eq_on_inv₀ f g]
    apply h

Proof state:
F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ≥0 M₀
inst✝ : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
h : ∀ (n : ℕ), f ↑n = g ↑n
r : ℚ≥0
⊢ f r = g r

Tactic:
rw [← r.num_div_den, div_eq_mul_inv, map_mul, map_mul, h, eq_on_inv₀ f g]

Result:
F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ≥0 M₀
inst✝ : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
h : ∀ (n : ℕ), f ↑n = g ↑n
r : ℚ≥0
⊢ f ↑r.den = g ↑r.den

Proof state:
F : Type u_1
M₀ : Type u_5
inst✝² : MonoidWithZero M₀
inst✝¹ : FunLike F ℚ≥0 M₀
inst✝ : MonoidWithZeroHomClass F ℚ≥0 M₀
f g : F
h : ∀ (n : ℕ), f ↑n = g ↑n
r : ℚ≥0
⊢ f ↑r.den = g ↑r.den

Tactic:
apply h

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem rightAngleRotation_trans_rightAngleRotation :
    LinearIsometryEquiv.trans J J = LinearIsometryEquiv.neg ℝ

Proof state:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x✝ : E
⊢ (o.rightAngleRotation.trans o.rightAngleRotation) x✝ = (LinearIsometryEquiv.neg ℝ) x✝

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
⊢ o.rightAngleRotation.trans o.rightAngleRotation = LinearIsometryEquiv.neg ℝ

Tactic:
ext

Result:
case h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x✝ : E
⊢ (o.rightAngleRotation.trans o.rightAngleRotation) x✝ = (LinearIsometryEquiv.neg ℝ) x✝
-- Mathlib/Computability/TuringMachine.lean
theorem addBottom_nth_succ_fst (L : ListBlank (∀ k, Option (Γ k))) (n : ℕ) :
    ((addBottom L).nth (n + 1)).1 = false

Proof state:
K : Type u_1
Γ : K → Type u_2
L : ListBlank ((k : K) → Option (Γ k))
n : ℕ
⊢ ((addBottom L).nth (n + 1)).1 = false

Tactic:
rw [ListBlank.nth_succ, addBottom, ListBlank.tail_cons, ListBlank.nth_map]

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem _root_.IsSMulRegular.skewMonoidAlgebra_iff {S : Type*} [Monoid S] [DistribMulAction S k]
    {a : S} [Nonempty G] : IsSMulRegular k a ↔ IsSMulRegular (SkewMonoidAlgebra k G) a

Proof state:
k : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid k
S : Type u_3
inst✝² : Monoid S
inst✝¹ : DistribMulAction S k
a : S
inst✝ : Nonempty G
inhabited_h : Inhabited G
⊢ IsSMulRegular k a ↔ IsSMulRegular (SkewMonoidAlgebra k G) a

Tactic:
refine ⟨IsSMulRegular.skewMonoidAlgebra, fun ha b₁ b₂ inj ↦ ?_⟩

Result:
k : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid k
S : Type u_3
inst✝² : Monoid S
inst✝¹ : DistribMulAction S k
a : S
inst✝ : Nonempty G
inhabited_h : Inhabited G
ha : IsSMulRegular (SkewMonoidAlgebra k G) a
b₁ b₂ : k
inj : (fun x => a • x) b₁ = (fun x => a • x) b₂
⊢ b₁ = b₂

Proof state:
k : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid k
S : Type u_3
inst✝² : Monoid S
inst✝¹ : DistribMulAction S k
a : S
inst✝ : Nonempty G
inhabited_h : Inhabited G
ha : IsSMulRegular (SkewMonoidAlgebra k G) a
b₁ b₂ : k
inj✝ : (fun x => a • x) b₁ = (fun x => a • x) b₂
inj : a • single ?m.408777 b₁ = a • single ?m.408777 b₂
⊢ b₁ = b₂

k : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid k
S : Type u_3
inst✝² : Monoid S
inst✝¹ : DistribMulAction S k
a : S
inst✝ : Nonempty G
inhabited_h : Inhabited G
ha : IsSMulRegular (SkewMonoidAlgebra k G) a
b₁ b₂ : k
inj : (fun x => a • x) b₁ = (fun x => a • x) b₂
⊢ Type ?u.408613

Tactic:
exact single_injective (default) (ha inj)

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid k
S : Type u_3
inst✝² : Monoid S
inst✝¹ : DistribMulAction S k
a : S
inst✝ : Nonempty G
⊢ IsSMulRegular k a ↔ IsSMulRegular (SkewMonoidAlgebra k G) a

Tactic:
inhabit G

Result:
k : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid k
S : Type u_3
inst✝² : Monoid S
inst✝¹ : DistribMulAction S k
a : S
inst✝ : Nonempty G
inhabited_h : Inhabited G
⊢ IsSMulRegular k a ↔ IsSMulRegular (SkewMonoidAlgebra k G) a

Proof state:
k : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid k
S : Type u_3
inst✝² : Monoid S
inst✝¹ : DistribMulAction S k
a : S
inst✝ : Nonempty G
inhabited_h : Inhabited G
ha : IsSMulRegular (SkewMonoidAlgebra k G) a
b₁ b₂ : k
inj : (fun x => a • x) b₁ = (fun x => a • x) b₂
⊢ b₁ = b₂

Tactic:
rw [← (single_injective _).eq_iff, ← smul_single, ← smul_single] at inj

Result:
k : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid k
S : Type u_3
inst✝² : Monoid S
inst✝¹ : DistribMulAction S k
a : S
inst✝ : Nonempty G
inhabited_h : Inhabited G
ha : IsSMulRegular (SkewMonoidAlgebra k G) a
b₁ b₂ : k
inj✝ : (fun x => a • x) b₁ = (fun x => a • x) b₂
inj : a • single ?m.408777 b₁ = a • single ?m.408777 b₂
⊢ b₁ = b₂

k : Type u_1
G : Type u_2
inst✝³ : AddCommMonoid k
S : Type u_3
inst✝² : Monoid S
inst✝¹ : DistribMulAction S k
a : S
inst✝ : Nonempty G
inhabited_h : Inhabited G
ha : IsSMulRegular (SkewMonoidAlgebra k G) a
b₁ b₂ : k
inj : (fun x => a • x) b₁ = (fun x => a • x) b₂
⊢ Type ?u.408613
-- Mathlib/Data/List/Sigma.lean
theorem lookup_ext {l₀ l₁ : List (Sigma β)} (nd₀ : l₀.NodupKeys) (nd₁ : l₁.NodupKeys)
    (h : ∀ x y, y ∈ l₀.dlookup x ↔ y ∈ l₁.dlookup x) : l₀ ~ l₁ :=
  mem_ext nd₀.nodup nd₁.nodup fun ⟨a, b⟩ => by
    rw [← mem_dlookup_iff, ← mem_dlookup_iff, h] <;> assumption

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
l₀ l₁ : List (Sigma β)
nd₀ : l₀.NodupKeys
nd₁ : l₁.NodupKeys
h : ∀ (x : α) (y : β x), y ∈ dlookup x l₀ ↔ y ∈ dlookup x l₁
x✝ : Sigma β
a : α
b : β a
⊢ ⟨a, b⟩ ∈ l₀ ↔ ⟨a, b⟩ ∈ l₁

Tactic:
rw [← mem_dlookup_iff, ← mem_dlookup_iff, h] <;> assumption

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_inter_Icc : Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)

Proof state:
α : Type u_1
inst✝ : Lattice α
a₁ a₂ b₁ b₂ : α
⊢ Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)

Tactic:
simp only [Ici_inter_Iic.symm, Ici_inter_Ici.symm, Iic_inter_Iic.symm]

Result:
α : Type u_1
inst✝ : Lattice α
a₁ a₂ b₁ b₂ : α
⊢ Ici a₁ ∩ Iic b₁ ∩ (Ici a₂ ∩ Iic b₂) = Ici a₁ ∩ Ici a₂ ∩ (Iic b₁ ∩ Iic b₂)

Proof state:
α : Type u_1
inst✝ : Lattice α
a₁ a₂ b₁ b₂ : α
⊢ Ici a₁ ∩ Iic b₁ ∩ (Ici a₂ ∩ Iic b₂) = Ici a₁ ∩ Ici a₂ ∩ (Iic b₁ ∩ Iic b₂)

Tactic:
ac_rfl

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem sublists'_eq_sublists (l : List α) : sublists' l = map reverse (sublists (reverse l))

Proof state:
α : Type u
l : List α
⊢ l.sublists' = map reverse l.reverse.sublists

Tactic:
rw [← sublists'_reverse, reverse_reverse]

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem dist_partial_sum_le_of_le_geometric (hf : ∀ n, ‖f n‖ ≤ C * r ^ n) (n : ℕ) :
    dist (∑ i ∈ range n, f i) (∑ i ∈ range (n + 1), f i) ≤ C * r ^ n

Proof state:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
n : ℕ
⊢ ‖f n‖ ≤ C * r ^ n

Tactic:
exact hf n

Result:
no goals

Proof state:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
n : ℕ
⊢ dist (∑ i ∈ Finset.range n, f i) (∑ i ∈ Finset.range (n + 1), f i) ≤ C * r ^ n

Tactic:
rw [sum_range_succ, dist_eq_norm, ← norm_neg, neg_sub, add_sub_cancel_left]

Result:
α : Type u_1
inst✝ : SeminormedAddCommGroup α
r C : ℝ
f : ℕ → α
hf : ∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n
n : ℕ
⊢ ‖f n‖ ≤ C * r ^ n
-- Mathlib/CategoryTheory/Monoidal/End.lean
theorem associativity_app (m₁ m₂ m₃ : M) (X : C) [F.LaxMonoidal] :
    (F.obj m₃).map ((μ F m₁ m₂).app X) ≫
        (μ F (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
      (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫ (μ F m₁ (m₂ ⊗ m₃)).app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.LaxMonoidal
this :
  (μ F m₁ m₂ ▷ F.obj m₃ ≫ μ F (m₁ ⊗ m₂) m₃ ≫ F.map (α_ m₁ m₂ m₃).hom).app X =
    ((α_ (F.obj m₁) (F.obj m₂) (F.obj m₃)).hom ≫ F.obj m₁ ◁ μ F m₂ m₃ ≫ μ F m₁ (m₂ ⊗ m₃)).app X
⊢ (F.obj m₃).map ((μ F m₁ m₂).app X) ≫ (μ F (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫ (μ F m₁ (m₂ ⊗ m₃)).app X

Tactic:
dsimp at this

Result:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.LaxMonoidal
this :
  (F.obj m₃).map ((μ F m₁ m₂).app X) ≫ (μ F (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    𝟙 ((F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X))) ≫
      (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫ (μ F m₁ (m₂ ⊗ m₃)).app X
⊢ (F.obj m₃).map ((μ F m₁ m₂).app X) ≫ (μ F (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫ (μ F m₁ (m₂ ⊗ m₃)).app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.LaxMonoidal
⊢ (F.obj m₃).map ((μ F m₁ m₂).app X) ≫ (μ F (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫ (μ F m₁ (m₂ ⊗ m₃)).app X

Tactic:
have := congr_app (associativity F m₁ m₂ m₃) X

Result:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.LaxMonoidal
this :
  (μ F m₁ m₂ ▷ F.obj m₃ ≫ μ F (m₁ ⊗ m₂) m₃ ≫ F.map (α_ m₁ m₂ m₃).hom).app X =
    ((α_ (F.obj m₁) (F.obj m₂) (F.obj m₃)).hom ≫ F.obj m₁ ◁ μ F m₂ m₃ ≫ μ F m₁ (m₂ ⊗ m₃)).app X
⊢ (F.obj m₃).map ((μ F m₁ m₂).app X) ≫ (μ F (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫ (μ F m₁ (m₂ ⊗ m₃)).app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.LaxMonoidal
this :
  (F.obj m₃).map ((μ F m₁ m₂).app X) ≫ (μ F (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    𝟙 ((F.obj m₃).obj ((F.obj m₂).obj ((F.obj m₁).obj X))) ≫
      (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫ (μ F m₁ (m₂ ⊗ m₃)).app X
⊢ (F.obj m₃).map ((μ F m₁ m₂).app X) ≫ (μ F (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X =
    (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫ (μ F m₁ (m₂ ⊗ m₃)).app X

Tactic:
simpa using this

Result:
no goals