harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Ring/Units.lean
theorem map_neg {F : Type*} [Ring β] [FunLike F α β] [RingHomClass F α β]
    (f : F) (u : αˣ) : map (f : α →* β) (-u) = -map (f : α →* β) u :=
  ext (by simp only [coe_map, Units.val_neg, MonoidHom.coe_coe, map_neg])

Proof state:
α : Type u
β : Type v
inst✝³ : Ring α
F : Type u_1
inst✝² : Ring β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
u : αˣ
⊢ ↑((map ↑f) (-u)) = ↑(-(map ↑f) u)

Tactic:
simp only [coe_map, Units.val_neg, MonoidHom.coe_coe, map_neg]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem inv_cpow (x : ℂ) (n : ℂ) (hx : x.arg ≠ π) : x⁻¹ ^ n = (x ^ n)⁻¹

Proof state:
x n : ℂ
hx : x.arg ≠ π
⊢ x⁻¹ ^ n = (x ^ n)⁻¹

Tactic:
rw [inv_cpow_eq_ite, if_neg hx]

Result:
no goals
-- Mathlib/Algebra/Group/Int/Even.lean
@[simp] lemma not_even_one : ¬Even (1 : ℤ)

Proof state:
⊢ ¬Even 1

Tactic:
simp [even_iff]

Result:
no goals
-- Mathlib/Order/Interval/Set/Pi.lean
theorem pi_univ_Iic : (pi univ fun i ↦ Iic (x i)) = Iic x :=
  ext fun y ↦ by simp [Pi.le_def]

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → Preorder (α i)
x y : (i : ι) → α i
⊢ (y ∈ univ.pi fun i => Iic (x i)) ↔ y ∈ Iic x

Tactic:
simp [Pi.le_def]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_comp_star (hf : ContinuousOn f (star '' (σₙ R a))

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : Nontrivial R
inst✝¹⁰ : StarRing R
inst✝⁹ : MetricSpace R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
instCFCₙ : NonUnitalContinuousFunctionalCalculus R p
f : R → R
a : A
inst✝ : UniqueHom R A
hf : autoParam (ContinuousOn f (star '' σₙ R a)) _auto✝
hf0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfcₙ (fun x => f (star x)) a = cfcₙ f (star a)

Tactic:
rw [cfcₙ_comp' f star a, cfcₙ_star_id a]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem liminf_bot (f : β → α) : liminf f ⊥ = ⊤

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
⊢ liminf f ⊥ = ⊤

Tactic:
simp [liminf]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Blocks.lean
/-- A singleton is a block. -/
@[to_additive "A singleton is a block."]
lemma IsBlock.singleton : IsBlock G ({a} : Set X)

Proof state:
G : Type u_1
X : Type u_2
inst✝ : SMul G X
a : X
⊢ IsBlock G {a}

Tactic:
simp [IsBlock]

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem sSameSide_vadd_right_iff {s : AffineSubspace R P} {x y : P} {v : V} (hv : v ∈ s.direction) :
    s.SSameSide x (v +ᵥ y) ↔ s.SSameSide x y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y : P
v : V
hv : v ∈ s.direction
⊢ s.SSameSide x (v +ᵥ y) ↔ s.SSameSide x y

Tactic:
rw [sSameSide_comm, sSameSide_vadd_left_iff hv, sSameSide_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem hasStrictDerivAt_rpow_const {x p : ℝ} (hx : x ≠ 0 ∨ 1 ≤ p) :
    HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x :=
  ContDiffAt.hasStrictDerivAt' (contDiffAt_rpow_const (by rwa [← Nat.cast_one] at hx))
    (hasDerivAt_rpow_const hx) le_rfl

Proof state:
x p : ℝ
hx : x ≠ 0 ∨ 1 ≤ p
⊢ x ≠ 0 ∨ ↑One.one ≤ p

Tactic:
rwa [← Nat.cast_one] at hx

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem deriv_mem_iff {f : 𝕜 → F} {s : Set F} {x : 𝕜} :
    deriv f x ∈ s ↔
      DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ (0 : F) ∈ s

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set F
x : 𝕜
⊢ deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s

Tactic:
by_cases hx : DifferentiableAt 𝕜 f x <;> simp [deriv_zero_of_not_differentiableAt, *]

Result:
no goals
-- Mathlib/Combinatorics/Pigeonhole.lean
theorem exists_card_fiber_le_of_card_le_nsmul (ht : t.Nonempty) (hb : #s ≤ #t • b) :
    ∃ y ∈ t, #{x ∈ s | f x = y} ≤ b

Proof state:
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝ : LinearOrderedCommSemiring M
ht : t.Nonempty
hb : ∑ x ∈ s, 1 ≤ #t • b
⊢ ∃ y ∈ t, ∑ x ∈ filter (fun x => f x = y) s, 1 ≤ b

Tactic:
refine
  exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul
    (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht hb

Result:
no goals

Proof state:
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝ : LinearOrderedCommSemiring M
ht : t.Nonempty
hb : ↑(#s) ≤ #t • b
⊢ ∃ y ∈ t, ↑(#(filter (fun x => f x = y) s)) ≤ b

Tactic:
simp_rw [cast_card] at hb ⊢

Result:
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝ : LinearOrderedCommSemiring M
ht : t.Nonempty
hb : ∑ x ∈ s, 1 ≤ #t • b
⊢ ∃ y ∈ t, ∑ x ∈ filter (fun x => f x = y) s, 1 ≤ b
-- Mathlib/Analysis/ConstantSpeed.lean
theorem HasConstantSpeedOnWith.hasLocallyBoundedVariationOn (h : HasConstantSpeedOnWith f s l) :
    LocallyBoundedVariationOn f s := fun x y hx hy => by
  simp only [BoundedVariationOn, h hx hy, Ne, ENNReal.ofReal_ne_top, not_false_iff]

Proof state:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : HasConstantSpeedOnWith f s l
x y : ℝ
hx : x ∈ s
hy : y ∈ s
⊢ BoundedVariationOn f (s ∩ Icc x y)

Tactic:
simp only [BoundedVariationOn, h hx hy, Ne, ENNReal.ofReal_ne_top, not_false_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem not_exists (p : α → Prop) : (¬∃ x, p x) = ∀ x, ¬p x

Proof state:
α : Sort u_1
p : α → Prop
⊢ (¬∃ x, p x) = ∀ (x : α), ¬p x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem le_castSucc_iff {i : Fin (n + 1)} {j : Fin n} : i ≤ j.castSucc ↔ i < j.succ

Proof state:
n : Nat
i : Fin (n + 1)
j : Fin n
⊢ i ≤ j.castSucc ↔ i < j.succ

Tactic:
simpa only [lt_def, le_def] using Nat.add_one_le_add_one_iff.symm

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem KerLift.map_smul (f : A →ₐ[R₁] B) (r : R₁) (x : A ⧸ (RingHom.ker f)) :
    f.kerLift (r • x) = r • f.kerLift x

Proof state:
case intro
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Semiring B
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
r : R₁
a : A
⊢ f.kerLift (r • (Quotient.mkₐ R₁ (ker f)) a) = r • f.kerLift ((Quotient.mkₐ R₁ (ker f)) a)

Tactic:
exact _root_.map_smul f _ _

Result:
no goals

Proof state:
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Semiring B
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
r : R₁
x : A ⧸ ker f
⊢ f.kerLift (r • x) = r • f.kerLift x

Tactic:
obtain ⟨a, rfl⟩ := Quotient.mkₐ_surjective R₁ _ x

Result:
case intro
R₁ : Type u_1
A : Type u_3
B : Type u_4
inst✝⁴ : CommSemiring R₁
inst✝³ : Ring A
inst✝² : Algebra R₁ A
inst✝¹ : Semiring B
inst✝ : Algebra R₁ B
f : A →ₐ[R₁] B
r : R₁
a : A
⊢ f.kerLift (r • (Quotient.mkₐ R₁ (ker f)) a) = r • f.kerLift ((Quotient.mkₐ R₁ (ker f)) a)
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_matrix_module' (m n : Type w) [Finite m] [Finite n] :
    Module.rank R (Matrix m n M) =
      lift.{max v} (#m * #n) * lift.{w} (Module.rank R M)

Proof state:
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : StrongRankCondition R
inst✝² : Free R M
m n : Type w
inst✝¹ : Finite m
inst✝ : Finite n
⊢ Module.rank R (Matrix m n M) = lift.{v, w} (#m * #n) * lift.{w, v} (Module.rank R M)

Tactic:
rw [rank_matrix_module, lift_mul, lift_umax.{w, v}]

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem update_eq_sub_add_single [AddGroup G] (f : α →₀ G) (a : α) (b : G) :
    f.update a b = f - single a (f a) + single a b

Proof state:
α : Type u_1
G : Type u_9
inst✝ : AddGroup G
f : α →₀ G
a : α
b : G
⊢ f.update a b = f - single a (f a) + single a b

Tactic:
rw [update_eq_erase_add_single, erase_eq_sub_single]

Result:
no goals
-- Mathlib/Algebra/Polynomial/EraseLead.lean
@[simp] lemma eraseLead_C_mul_X (r : R) : eraseLead (C r * X) = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
r : R
⊢ (C r * X).eraseLead = 0

Tactic:
simpa using eraseLead_C_mul_X_pow _ 1

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem le_add_right (a b : Ordinal) : a ≤ a + b

Proof state:
a b : Ordinal.{u_1}
⊢ a ≤ a + b

Tactic:
simpa only [add_zero] using add_le_add_left (Ordinal.zero_le b) a

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem _root_.Set.countable_infinite_iff_nonempty_denumerable {α : Type*} {s : Set α} :
    s.Countable ∧ s.Infinite ↔ Nonempty (Denumerable s)

Proof state:
α : Type u_1
s : Set α
⊢ s.Countable ∧ s.Infinite ↔ Nonempty (Denumerable ↑s)

Tactic:
rw [nonempty_denumerable_iff, ← Set.infinite_coe_iff, countable_coe_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Vandermonde.lean
theorem det_vandermonde_add {n : ℕ} (v : Fin n → R) (a : R) :
    (Matrix.vandermonde fun i ↦ v i + a).det = (Matrix.vandermonde v).det

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n → R
a : R
⊢ (vandermonde fun i => v i + a).det = (vandermonde v).det

Tactic:
simp [Matrix.det_vandermonde]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/MulOppositeLemmas.lean
theorem normal_op {H : Subgroup G} : H.op.Normal ↔ H.Normal

Proof state:
G : Type u_2
inst✝ : Group G
H : Subgroup G
⊢ H.op.Normal ↔ H.Normal

Tactic:
simp only [← normalizer_eq_top_iff, ← op_normalizer, op_eq_top]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_unitOfList
    {l : List α} {k : α} :
    get! (unitOfList l) k = ()

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
l : List α
k : α
⊢ get! (unitOfList l) k = ()

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arcsin_lt_pi_div_two {x : ℝ} : arcsin x < π / 2 ↔ x < 1 :=
  (arcsin_lt_iff_lt_sin' (right_mem_Ioc.2 <| neg_lt_self pi_div_two_pos)).trans <| by
    rw [sin_pi_div_two]

Proof state:
x : ℝ
⊢ x < sin (π / 2) ↔ x < 1

Tactic:
rw [sin_pi_div_two]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_apply_eq_zero' (hs : MeasurableSet s) : μ.restrict s t = 0 ↔ μ (t ∩ s) = 0

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ (μ.restrict s) t = 0 ↔ μ (t ∩ s) = 0

Tactic:
rw [restrict_apply' hs]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Defs.lean
theorem inner_neg_left (x y : F) : ⟪-x, y⟫ = -⟪x, y⟫

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ (starRingEnd 𝕜) (-1) * ⟪x, y⟫_𝕜 = -⟪x, y⟫_𝕜

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ ⟪-x, y⟫_𝕜 = -⟪x, y⟫_𝕜

Tactic:
rw [← neg_one_smul 𝕜 x, inner_smul_left]

Result:
𝕜 : Type u_1
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : PreInnerProductSpace.Core 𝕜 F
x y : F
⊢ (starRingEnd 𝕜) (-1) * ⟪x, y⟫_𝕜 = -⟪x, y⟫_𝕜
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem id_zero : 𝟙 (0 : C) = (0 : (0 : C) ⟶ 0)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
⊢ 𝟙 0 = 0

Tactic:
apply HasZeroObject.from_zero_ext

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ici_diff_Ici : Ici a \ Ici b = Ico a b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ici a \ Ici b = Ico a b

Tactic:
rw [diff_eq, compl_Ici, Ici_inter_Iio]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Raw.lean
theorem WF.insertIfNew [BEq α] [Hashable α] {m : Raw α β} {a : α} {b : β a} (h : m.WF) :
    (m.insertIfNew a b).WF

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
a : α
b : β a
h : m.WF
⊢ (m.insertIfNew a b).WF

Tactic:
simpa [Raw.insertIfNew, h.size_buckets_pos] using .insertIfNew₀ h

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem div_self {a : Ordinal} (h : a ≠ 0) : a / a = 1

Proof state:
a : Ordinal.{u_4}
h : a ≠ 0
⊢ a / a = 1

Tactic:
simpa only [mul_one] using mul_div_cancel 1 h

Result:
no goals
-- Mathlib/Order/MinMax.lean
theorem Antitone.map_max (hf : Antitone f) : f (max a b) = min (f a) (f b)

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b : α
hf : Antitone f
⊢ f (a ⊔ b) = f a ⊓ f b

Tactic:
rcases le_total a b with h | h <;> simp [h, hf h]

Result:
no goals
-- Mathlib/Data/Multiset/Sym.lean
theorem sym2_eq_zero_iff {m : Multiset α} : m.sym2 = 0 ↔ m = 0 :=
  m.inductionOn fun xs => by simp

Proof state:
α : Type u_1
m : Multiset α
xs : List α
⊢ Multiset.sym2 ⟦xs⟧ = 0 ↔ ⟦xs⟧ = 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem eraseP_mkArray_of_neg {n : Nat} {a : α} (h : ¬p a) :
    (mkArray n a).eraseP p = mkArray n a

Proof state:
α : Type u_1
p : α → Bool
n : Nat
a : α
h : ¬p a = true
⊢ (List.eraseP p (List.replicate n a)).toArray = (List.replicate n a).toArray

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
n : Nat
a : α
h : ¬p a = true
⊢ (mkArray n a).eraseP p = mkArray n a

Tactic:
simp only [← List.toArray_replicate, List.eraseP_toArray]

Result:
α : Type u_1
p : α → Bool
n : Nat
a : α
h : ¬p a = true
⊢ (List.eraseP p (List.replicate n a)).toArray = (List.replicate n a).toArray
-- Mathlib/Geometry/Euclidean/Inversion/Basic.lean
theorem inversion_self (c : P) (R : ℝ) : inversion c R c = c

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
⊢ inversion c R c = c

Tactic:
simp [inversion]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject.lean
@[reassoc (attr := simp)]
lemma map_inv_hom_id_eval (e : X ≅ Y) (F : C ⥤ D) (j : J) :
    F.map (e.inv j) ≫ F.map (e.hom j) = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
J : Type u_4
inst✝¹ : Category.{u_5, u_1} C
inst✝ : Category.{u_6, u_2} D
X Y : GradedObject J C
e : X ≅ Y
F : C ⥤ D
j : J
⊢ F.map (e.inv j) ≫ F.map (e.hom j) = 𝟙 (F.obj (Y j))

Tactic:
rw [← F.map_comp, ← GradedObject.categoryOfGradedObjects_comp, e.inv_hom_id,
  GradedObject.categoryOfGradedObjects_id, Functor.map_id]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean
theorem card_aux₁ (hucard : #u = m * 4 ^ #P.parts + a) :
    (4 ^ #P.parts - a) * m + a * (m + 1) = #u

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hucard : #u = m * 4 ^ #P.parts + a
⊢ (4 ^ #P.parts - a) * m + a * (m + 1) = #u

Tactic:
rw [hucard, mul_add, mul_one, ← add_assoc, ← add_mul,
  Nat.sub_add_cancel ((Nat.le_succ _).trans a_add_one_le_four_pow_parts_card), mul_comm]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem disjoint_union_right : Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
⊢ Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u

Tactic:
simp only [disjoint_right, mem_union, or_imp, forall_and]

Result:
no goals
-- Mathlib/RingTheory/Bialgebra/TensorProduct.lean
lemma comul_eq_algHom_toLinearMap :
    Coalgebra.comul (R := R) (A := A ⊗[R] B) =
      ((Algebra.TensorProduct.tensorTensorTensorComm R A A B B).toAlgHom.comp
      (Algebra.TensorProduct.map (Bialgebra.comulAlgHom R A)
      (Bialgebra.comulAlgHom R B))).toLinearMap

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Bialgebra R A
inst✝ : Bialgebra R B
⊢ CoalgebraStruct.comul =
    ((↑(Algebra.TensorProduct.tensorTensorTensorComm R A A B B)).comp
        (Algebra.TensorProduct.map (comulAlgHom R A) (comulAlgHom R B))).toLinearMap

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem range_reindex : Set.range (b.reindex e) = Set.range b

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
e : ι ≃ ι'
⊢ range ⇑(b.reindex e) = range ⇑b

Tactic:
simp [coe_reindex, range_comp]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean
theorem mem_balancedHull_iff : x ∈ balancedHull 𝕜 s ↔ ∃ r : 𝕜, ‖r‖ ≤ 1 ∧ x ∈ r • s

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s : Set E
x : E
⊢ x ∈ balancedHull 𝕜 s ↔ ∃ r, ‖r‖ ≤ 1 ∧ x ∈ r • s

Tactic:
simp [balancedHull]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Norm.lean
theorem HasStrictFDerivAt.hasStrictDerivAt_norm_smul_neg
    (ht : t < 0) (h : HasStrictFDerivAt (‖·‖) f x) :
    HasStrictFDerivAt (‖·‖) (-f) (t • x)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E →L[ℝ] ℝ
x : E
t : ℝ
ht : t < 0
h : HasStrictFDerivAt (fun x => ‖x‖) f x
⊢ HasStrictFDerivAt (fun x => ‖x‖) (-f) (t • x)

Tactic:
simpa [ht] using h.hasStrictFDerivAt_norm_smul ht.ne

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_ofBool (b : Bool) : (ofBool b).getMsbD i = (decide (i = 0) && b)

Proof state:
i : Nat
b : Bool
⊢ (ofBool b).getMsbD i = (decide (i = 0) && b)

Tactic:
cases b <;> simp [getMsbD]

Result:
no goals
-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter {n : ℕ}
    (s : Simplex ℝ P (n + 2)) {i₁ i₂ : Fin (n + 3)} (h : i₁ ≠ i₂) :
    s.mongePoint -ᵥ ({i₁, i₂}ᶜ : Finset (Fin (n + 3))).centroid ℝ s.points =
      (univ : Finset (PointsWithCircumcenterIndex (n + 2))).weightedVSub s.pointsWithCircumcenter
        (mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ s.mongePoint -ᵥ centroid ℝ {i₁, i₂}ᶜ s.points =
    (univ.weightedVSub s.pointsWithCircumcenter) (mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂)

Tactic:
simp_rw [mongePoint_eq_affineCombination_of_pointsWithCircumcenter,
  centroid_eq_affineCombination_of_pointsWithCircumcenter, affineCombination_vsub,
  mongePointVSubFaceCentroidWeightsWithCircumcenter_eq_sub h]

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem and_symm_left {α : Sort*} (a b : α) (p : Prop) : a = b ∧ p ↔ b = a ∧ p

Proof state:
α : Sort u_1
a b : α
p : Prop
⊢ a = b ∧ p ↔ b = a ∧ p

Tactic:
simp [eq_comm]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem sup_sup_distrib_right (a b c : α) : a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c)

Proof state:
α : Type u
inst✝ : SemilatticeSup α
a b c : α
⊢ a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c)

Tactic:
rw [sup_sup_sup_comm, sup_idem]

Result:
no goals
-- Mathlib/GroupTheory/Subgroup/Centralizer.lean
theorem normalizerMonoidHom_ker :
    H.normalizerMonoidHom.ker = (Subgroup.centralizer H).subgroupOf H.normalizer

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.normalizerMonoidHom.ker = (centralizer ↑H).subgroupOf H.normalizer

Tactic:
simp [Subgroup.ext_iff, DFunLike.ext_iff, Subtype.ext_iff,
  mem_subgroupOf, mem_centralizer_iff, eq_mul_inv_iff_mul_eq, eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Dvd.lean
theorem div_mul_cancel {n m : Nat} (H : n ∣ m) : m / n * n = m

Proof state:
n m : Nat
H : n ∣ m
⊢ m / n * n = m

Tactic:
rw [Nat.mul_comm, Nat.mul_div_cancel' H]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Basic.lean
@[to_additive]
lemma fst_mem_orbit_of_mem_orbit {x y : α × β} (h : x ∈ MulAction.orbit M y) :
    x.1 ∈ MulAction.orbit M y.1

Proof state:
M : Type u
inst✝² : Monoid M
α : Type v
inst✝¹ : MulAction M α
β : Type u_1
inst✝ : MulAction M β
x y : α × β
h : x ∈ orbit M y
⊢ x.1 ∈ orbit M y.1

Tactic:
rcases h with ⟨g, rfl⟩

Result:
case intro
M : Type u
inst✝² : Monoid M
α : Type v
inst✝¹ : MulAction M α
β : Type u_1
inst✝ : MulAction M β
y : α × β
g : M
⊢ ((fun m => m • y) g).1 ∈ orbit M y.1

Proof state:
case intro
M : Type u
inst✝² : Monoid M
α : Type v
inst✝¹ : MulAction M α
β : Type u_1
inst✝ : MulAction M β
y : α × β
g : M
⊢ ((fun m => m • y) g).1 ∈ orbit M y.1

Tactic:
exact mem_orbit _ _

Result:
no goals
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isSeparator_sigma_of_isSeparator {β : Type w} (f : β → C) [HasCoproduct f] (b : β)
    (hb : IsSeparator (f b)) : IsSeparator (∐ f) :=
  (isSeparator_sigma _).2 <| IsSeparating.mono hb <| by simp

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
b : β
hb : IsSeparator (f b)
⊢ {f b} ⊆ Set.range f

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem mul_tdiv_cancel' {a b : Int} (H : a ∣ b) : a * b.tdiv a = b

Proof state:
a b : Int
H : a ∣ b
⊢ a * b.tdiv a = b

Tactic:
rw [Int.mul_comm, Int.tdiv_mul_cancel H]

Result:
no goals
-- Mathlib/Algebra/Group/Equiv/Defs.lean
@[to_additive]
lemma comp_right_injective (e : M ≃* N) : Injective fun f : P →* M ↦ (e : M →* N).comp f :=
  LeftInverse.injective (g := (e.symm : N →* M).comp) fun f ↦ by simp [← MonoidHom.comp_assoc]

Proof state:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
e : M ≃* N
f : P →* M
⊢ (↑e.symm).comp ((↑e).comp f) = f

Tactic:
simp [← MonoidHom.comp_assoc]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_biUnion_closure_eq_closure_sUnion (M : Matroid α) (Xs : Set (Set α)) :
    M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃₀ Xs)

Proof state:
α : Type u_2
M : Matroid α
Xs : Set (Set α)
⊢ M.closure (⋃ X ∈ Xs, M.closure X) = M.closure (⋃₀ Xs)

Tactic:
rw [sUnion_eq_iUnion, biUnion_eq_iUnion, closure_iUnion_closure_eq_closure_iUnion]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma some_ne_zero {x y : R} (h : W'.Nonsingular x y) : Point.some h ≠ 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
h : W'.Nonsingular x y
⊢ some h ≠ 0

Tactic:
rintro (_ | _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RelabelNat.lean
theorem relabelNat'_fst_eq_relabelNat {aig : AIG α} : aig.relabelNat'.fst = aig.relabelNat

Proof state:
α : Type
inst✝¹ : DecidableEq α
inst✝ : Hashable α
aig : AIG α
⊢ aig.relabelNat'.fst = aig.relabelNat

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/TrivSqZeroExt.lean
theorem isUnit_iff_isUnit_fst {x : tsze R M} : IsUnit x ↔ IsUnit x.fst

Proof state:
R : Type u
M : Type v
inst✝⁴ : AddCommGroup M
inst✝³ : Semiring R
inst✝² : Module Rᵐᵒᵖ M
inst✝¹ : Module R M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : tsze R M
⊢ IsUnit x ↔ IsUnit x.fst

Tactic:
simp only [← nonempty_invertible_iff_isUnit, (invertibleEquivInvertibleFst x).nonempty_congr]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineCombination_affineCombinationLineMapWeights [DecidableEq ι] (p : ι → P) {i j : ι}
    (hi : i ∈ s) (hj : j ∈ s) (c : k) :
    s.affineCombination k p (affineCombinationLineMapWeights i j c) =
      AffineMap.lineMap (p i) (p j) c

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
p : ι → P
i j : ι
hi : i ∈ s
hj : j ∈ s
c : k
⊢ (affineCombination k s p) (affineCombinationLineMapWeights i j c) = (AffineMap.lineMap (p i) (p j)) c

Tactic:
rw [affineCombinationLineMapWeights, ← weightedVSub_vadd_affineCombination,
  weightedVSub_const_smul, s.affineCombination_affineCombinationSingleWeights k p hi,
  s.weightedVSub_weightedVSubVSubWeights k p hj hi, AffineMap.lineMap_apply]

Result:
no goals