harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Equivalence.lean
theorem cancel_counitInv_right {X Y : D} (f f' : X ⟶ Y) :
    f ≫ e.counitInv.app Y = f' ≫ e.counitInv.app Y ↔ f = f'

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
X Y : D
f f' : X ⟶ Y
⊢ f ≫ e.counitInv.app Y = f' ≫ e.counitInv.app Y ↔ f = f'

Tactic:
simp only [cancel_mono]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Map.lean
theorem map_of_not_aemeasurable {f : α → β} {μ : Measure α} (hf : ¬AEMeasurable f μ) :
    μ.map f = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
μ : Measure α
hf : ¬AEMeasurable f μ
⊢ map f μ = 0

Tactic:
simp [map, hf]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem foldl_eq_foldr' : ∀ a l, foldl f a l = foldr (flip f) a l
  | _, [] => rfl
  | a, b :: l => by rw [foldl_eq_of_comm' hf, foldr, foldl_eq_foldr' ..]; rfl

Proof state:
α : Type u
β : Type v
f : α → β → α
hf : ∀ (a : α) (b c : β), f (f a b) c = f (f a c) b
a : α
b : β
l : List β
⊢ f (foldr (flip f) a l) b = flip f b (foldr (flip f) a l)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β → α
hf : ∀ (a : α) (b c : β), f (f a b) c = f (f a c) b
a : α
b : β
l : List β
⊢ foldl f a (b :: l) = foldr (flip f) a (b :: l)

Tactic:
rw [foldl_eq_of_comm' hf, foldr, foldl_eq_foldr' ..]

Result:
α : Type u
β : Type v
f : α → β → α
hf : ∀ (a : α) (b c : β), f (f a b) c = f (f a c) b
a : α
b : β
l : List β
⊢ f (foldr (flip f) a l) b = flip f b (foldr (flip f) a l)
-- Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
theorem eLpNorm'_add_le_of_le_one (hf : AEStronglyMeasurable f μ) (hq0 : 0 ≤ q) (hq1 : q ≤ 1) :
    eLpNorm' (f + g) q μ ≤ (2 : ℝ≥0∞) ^ (1 / q - 1) * (eLpNorm' f q μ + eLpNorm' g q μ) :=
  calc
    (∫⁻ a, (‖(f + g) a‖₊ : ℝ≥0∞) ^ q ∂μ) ^ (1 / q) ≤
        (∫⁻ a, ((fun a => (‖f a‖₊ : ℝ≥0∞)) + fun a => (‖g a‖₊ : ℝ≥0∞)) a ^ q ∂μ) ^ (1 / q)

Proof state:
case h₁.hfg.h₁
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
q : ℝ
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hq0 : 0 ≤ q
hq1 : q ≤ 1
a : α
⊢ ↑‖(f + g) a‖₊ ≤ ((fun a => ↑‖f a‖₊) + fun a => ↑‖g a‖₊) a

Tactic:
simp only [Pi.add_apply, ← ENNReal.coe_add, ENNReal.coe_le_coe, nnnorm_add_le]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
q : ℝ
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hq0 : 0 ≤ q
hq1 : q ≤ 1
⊢ (∫⁻ (a : α), ↑‖(f + g) a‖₊ ^ q ∂μ) ^ (1 / q) ≤
    (∫⁻ (a : α), ((fun a => ↑‖f a‖₊) + fun a => ↑‖g a‖₊) a ^ q ∂μ) ^ (1 / q)

Tactic:
gcongr with a

Result:
case h₁.hfg.h₁
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
q : ℝ
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hq0 : 0 ≤ q
hq1 : q ≤ 1
a : α
⊢ ↑‖(f + g) a‖₊ ≤ ((fun a => ↑‖f a‖₊) + fun a => ↑‖g a‖₊) a
-- Mathlib/Algebra/Ring/Invertible.lean
theorem invOf_neg [Monoid α] [HasDistribNeg α] (a : α) [Invertible a] [Invertible (-a)] :
    ⅟ (-a) = -⅟ a :=
  invOf_eq_right_inv (by simp)

Proof state:
α : Type u
inst✝³ : Monoid α
inst✝² : HasDistribNeg α
a : α
inst✝¹ : Invertible a
inst✝ : Invertible (-a)
⊢ -a * -⅟a = 1

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
@[simp] lemma symm_dualMap_evalEquiv :
    (evalEquiv R M).symm.dualMap = Dual.eval R (Dual R M)

Proof state:
case h.h
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
x✝¹ : Dual R M
x✝ : Dual R (Dual R M)
⊢ (↑(evalEquiv R M).symm.dualMap x✝¹) x✝ = ((Dual.eval R (Dual R M)) x✝¹) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
⊢ ↑(evalEquiv R M).symm.dualMap = Dual.eval R (Dual R M)

Tactic:
ext

Result:
case h.h
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
x✝¹ : Dual R M
x✝ : Dual R (Dual R M)
⊢ (↑(evalEquiv R M).symm.dualMap x✝¹) x✝ = ((Dual.eval R (Dual R M)) x✝¹) x✝
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_apply' (M : Matrix n n R) : M.det = ∑ σ : Perm n, ε σ * ∏ i, M (σ i) i

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
⊢ M.det = ∑ σ : Perm n, ↑↑(sign σ) * ∏ i : n, M (σ i) i

Tactic:
simp [det_apply, Units.smul_def]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean
@[reassoc, to_app]
lemma whiskerRight_mapId_hom (f : a ⟶ b) : (F.mapId a).hom ▷ F.map f =
    (F.mapComp (𝟙 a) f).inv ≫ F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv

Proof state:
B : Type u₁
inst✝¹ : Bicategory B
C : Type u₂
inst✝ : Bicategory C
F : Pseudofunctor B C
a b : B
f : a ⟶ b
⊢ (F.mapId a).hom ▷ F.map f = (F.mapComp (𝟙 a) f).inv ≫ F.map₂ (λ_ f).hom ≫ (λ_ (F.map f)).inv

Tactic:
simp [whiskerRightIso_mapId]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem length_insertIdx_le_succ (l : List α) (x : α) (n : Nat) :
    (insertIdx n x l).length ≤ l.length + 1

Proof state:
α : Type u
l : List α
x : α
n : Nat
⊢ (if n ≤ l.length then l.length + 1 else l.length) ≤ l.length + 1

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type u
l : List α
x : α
n : Nat
⊢ (insertIdx n x l).length ≤ l.length + 1

Tactic:
simp only [length_insertIdx]

Result:
α : Type u
l : List α
x : α
n : Nat
⊢ (if n ≤ l.length then l.length + 1 else l.length) ≤ l.length + 1
-- Mathlib/Probability/Process/HittingTime.lean
theorem hitting_mem_set_of_hitting_lt [WellFoundedLT ι] {m : ι} (hl : hitting u s n m ω < m) :
    u (hitting u s n m ω) ω ∈ s

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
hl : hitting u s n m ω < m
⊢ u (hitting u s n m ω) ω ∈ s

Tactic:
by_cases h : ∃ j ∈ Set.Icc n m, u j ω ∈ s

Result:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
hl : hitting u s n m ω < m
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (hitting u s n m ω) ω ∈ s

case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
hl : hitting u s n m ω < m
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (hitting u s n m ω) ω ∈ s

Proof state:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
hl : hitting u s n m ω < m
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (hitting u s n m ω) ω ∈ s

Tactic:
simp_rw [hitting, if_neg h] at hl

Result:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
hl : m < m
⊢ u (hitting u s n m ω) ω ∈ s

Proof state:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
h : ¬∃ j ∈ Set.Icc n m, u j ω ∈ s
hl : m < m
⊢ u (hitting u s n m ω) ω ∈ s

Tactic:
exact False.elim (hl.ne rfl)

Result:
no goals

Proof state:
case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
inst✝ : WellFoundedLT ι
m : ι
hl : hitting u s n m ω < m
h : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ u (hitting u s n m ω) ω ∈ s

Tactic:
exact hitting_mem_set h

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Unitor.lean
@[reassoc]
lemma mapBifunctorLeftUnitor_naturality :
    mapBifunctorMapMap F p (𝟙 _) φ ≫ (mapBifunctorLeftUnitor F X e p hp Y').hom =
      (mapBifunctorLeftUnitor F X e p hp Y).hom ≫ φ

Proof state:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{u_6, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝² : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p
⊢ mapBifunctorMapMap F p (𝟙 ((single₀ I).obj X)) φ ≫ (mapBifunctorLeftUnitor F X e p hp Y').hom =
    (mapBifunctorLeftUnitor F X e p hp Y).hom ≫ φ

Tactic:
rw [← cancel_mono (mapBifunctorLeftUnitor F X e p hp Y').inv, assoc, assoc, Iso.hom_inv_id,
  comp_id, mapBifunctorLeftUnitor_inv_naturality, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Mod_.lean
theorem assoc_flip :
    (A.X ◁ M.act) ≫ M.act = (α_ A.X A.X M.X).inv ≫ (A.mul ▷ M.X) ≫ M.act

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A : Mon_ C
M : Mod_ A
⊢ A.X ◁ M.act ≫ M.act = (α_ A.X A.X M.X).inv ≫ A.mul ▷ M.X ≫ M.act

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/SmallSets.lean
theorem smallSets_bot : (⊥ : Filter α).smallSets = pure ∅

Proof state:
α : Type u_1
⊢ ⊥.smallSets = pure ∅

Tactic:
rw [smallSets, lift'_bot, powerset_empty, principal_singleton]

Result:
α : Type u_1
⊢ Monotone powerset

Proof state:
α : Type u_1
⊢ Monotone powerset

Tactic:
exact monotone_powerset

Result:
no goals
-- Mathlib/LinearAlgebra/SModEq.lean
theorem mul {I : Ideal A} {x₁ x₂ y₁ y₂ : A} (hxy₁ : x₁ ≡ y₁ [SMOD I])
    (hxy₂ : x₂ ≡ y₂ [SMOD I]) : x₁ * x₂ ≡ y₁ * y₂ [SMOD I]

Proof state:
A : Type u_2
inst✝ : CommRing A
I : Ideal A
x₁ x₂ y₁ y₂ : A
hxy₁ : x₁ ≡ y₁ [SMOD I]
hxy₂ : x₂ ≡ y₂ [SMOD I]
⊢ x₁ * x₂ ≡ y₁ * y₂ [SMOD I]

Tactic:
simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_mul] at hxy₁ hxy₂ ⊢

Result:
A : Type u_2
inst✝ : CommRing A
I : Ideal A
x₁ x₂ y₁ y₂ : A
hxy₁ : (Ideal.Quotient.mk I) x₁ = (Ideal.Quotient.mk I) y₁
hxy₂ : (Ideal.Quotient.mk I) x₂ = (Ideal.Quotient.mk I) y₂
⊢ (Ideal.Quotient.mk I) x₁ * (Ideal.Quotient.mk I) x₂ = (Ideal.Quotient.mk I) y₁ * (Ideal.Quotient.mk I) y₂

Proof state:
A : Type u_2
inst✝ : CommRing A
I : Ideal A
x₁ x₂ y₁ y₂ : A
hxy₁ : (Ideal.Quotient.mk I) x₁ = (Ideal.Quotient.mk I) y₁
hxy₂ : (Ideal.Quotient.mk I) x₂ = (Ideal.Quotient.mk I) y₂
⊢ (Ideal.Quotient.mk I) x₁ * (Ideal.Quotient.mk I) x₂ = (Ideal.Quotient.mk I) y₁ * (Ideal.Quotient.mk I) y₂

Tactic:
rw [hxy₁, hxy₂]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsPath.of_append_left {u v w : V} {p : G.Walk u v} {q : G.Walk v w} :
    (p.append q).IsPath → p.IsPath

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.append q).IsPath → p.IsPath

Tactic:
simp only [isPath_def, support_append]

Result:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.support ++ q.support.tail).Nodup → p.support.Nodup

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ (p.support ++ q.support.tail).Nodup → p.support.Nodup

Tactic:
exact List.Nodup.of_append_left

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem _root_.IsAntichain.finite_of_partiallyWellOrderedOn (ha : IsAntichain r s)
    (hp : s.PartiallyWellOrderedOn r) : s.Finite

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
ha : IsAntichain r s
hp : s.PartiallyWellOrderedOn r
⊢ s.Finite

Tactic:
refine not_infinite.1 fun hi => ?_

Result:
α : Type u_2
r : α → α → Prop
s : Set α
ha : IsAntichain r s
hp : s.PartiallyWellOrderedOn r
hi : s.Infinite
⊢ False

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
ha : IsAntichain r s
hp : s.PartiallyWellOrderedOn r
hi : s.Infinite
⊢ False

Tactic:
obtain ⟨m, n, hmn, h⟩ := hp (fun n => hi.natEmbedding _ n) fun n => (hi.natEmbedding _ n).2

Result:
case intro.intro.intro
α : Type u_2
r : α → α → Prop
s : Set α
ha : IsAntichain r s
hp : s.PartiallyWellOrderedOn r
hi : s.Infinite
m n : ℕ
hmn : m < n
h : r ↑((Infinite.natEmbedding s hi) m) ↑((Infinite.natEmbedding s hi) n)
⊢ False

Proof state:
case intro.intro.intro
α : Type u_2
r : α → α → Prop
s : Set α
ha : IsAntichain r s
hp : s.PartiallyWellOrderedOn r
hi : s.Infinite
m n : ℕ
hmn : m < n
h : r ↑((Infinite.natEmbedding s hi) m) ↑((Infinite.natEmbedding s hi) n)
⊢ False

Tactic:
exact hmn.ne ((hi.natEmbedding _).injective <| Subtype.val_injective <|
  ha.eq (hi.natEmbedding _ m).2 (hi.natEmbedding _ n).2 h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem forall_mem_push {p : α → Prop} {xs : Array α} {a : α} :
    (∀ x, x ∈ xs.push a → p x) ↔ p a ∧ ∀ x, x ∈ xs → p x

Proof state:
α : Type u_1
p : α → Prop
xs : Array α
a : α
⊢ (∀ (x : α), x ∈ xs.push a → p x) ↔ p a ∧ ∀ (x : α), x ∈ xs → p x

Tactic:
cases xs

Result:
case mk
α : Type u_1
p : α → Prop
a : α
toList✝ : List α
⊢ (∀ (x : α), x ∈ { toList := toList✝ }.push a → p x) ↔ p a ∧ ∀ (x : α), x ∈ { toList := toList✝ } → p x

Proof state:
case mk
α : Type u_1
p : α → Prop
a : α
toList✝ : List α
⊢ (∀ (x : α), x ∈ { toList := toList✝ }.push a → p x) ↔ p a ∧ ∀ (x : α), x ∈ { toList := toList✝ } → p x

Tactic:
simp [or_comm, forall_eq_or_imp]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_pi_eq' {I : Set ι} (hI : I.Finite) (s : ∀ i, Set (π i)) (x : ∀ i, π i) :
    𝓝[pi I s] x = ⨅ i, comap (fun x => x i) (𝓝 (x i) ⊓ ⨅ (_ : i ∈ I), 𝓟 (s i))

Proof state:
ι : Type u_5
π : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (π i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (π i)
x : (i : ι) → π i
⊢ 𝓝[I.pi s] x = ⨅ i, comap (fun x => x i) (𝓝 (x i) ⊓ ⨅ (_ : i ∈ I), 𝓟 (s i))

Tactic:
simp only [nhdsWithin, nhds_pi, Filter.pi, comap_inf, comap_iInf, pi_def, comap_principal, ←
  iInf_principal_finite hI, ← iInf_inf_eq]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Representable.lean
lemma of_isIso {X Y : D} (f : X ⟶ Y) [IsIso f] : F.relativelyRepresentable f :=
  fun a g ↦ ⟨a, 𝟙 a, g ≫ CategoryTheory.inv f, IsPullback.of_vert_isIso ⟨by simp⟩⟩

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X Y : D
f : X ⟶ Y
inst✝ : IsIso f
a : C
g : F.obj a ⟶ Y
⊢ (g ≫ CategoryTheory.inv f) ≫ f = F.map (𝟙 a) ≫ g

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
lemma strictAntiOn_derivWithin (hfc : StrictConcaveOn ℝ S f) (hfd : DifferentiableOn ℝ f S) :
    StrictAntiOn (derivWithin f S) S

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
⊢ StrictAntiOn (derivWithin f S) S

Tactic:
intro x hx y hy hxy

Result:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ derivWithin f S y < derivWithin f S x

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConcaveOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ derivWithin f S y < derivWithin f S x

Tactic:
exact (hfc.derivWithin_lt_slope hx hy hxy (hfd y hy)).trans
  (hfc.slope_lt_derivWithin hx hy hxy (hfd x hx))

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
/-- See `Polynomial.self_mul_modByMonic` for the other multiplication order. This version, unlike
that one, requires commutativity. -/
@[simp]
lemma mul_self_modByMonic (hq : q.Monic) : (p * q) %ₘ q = 0

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
hq : q.Monic
⊢ q ∣ p * q

Tactic:
exact dvd_mul_left q p

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
hq : q.Monic
⊢ p * q %ₘ q = 0

Tactic:
rw [modByMonic_eq_zero_iff_dvd hq]

Result:
R : Type u
inst✝ : CommRing R
p q : R[X]
hq : q.Monic
⊢ q ∣ p * q
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem self_eq_append_right {x y : Array α} : x = x ++ y ↔ y = #[]

Proof state:
α : Type u_1
x y : Array α
⊢ x = x ++ y ↔ y = #[]

Tactic:
rw [eq_comm, append_right_eq_self]

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem map_comap_of_mem {f : Filter β} {m : α → β} (hf : range m ∈ f) : (f.comap m).map m = f

Proof state:
α : Type u_1
β : Type u_2
f : Filter β
m : α → β
hf : range m ∈ f
⊢ map m (comap m f) = f

Tactic:
rw [map_comap, inf_eq_left.2 (le_principal_iff.2 hf)]

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
lemma mgf_congr_identDistrib {Ω' : Type*} {mΩ' : MeasurableSpace Ω'} {μ' : Measure Ω'}
    {Y : Ω' → ℝ} (h : IdentDistrib X Y μ μ') :
    mgf X μ = mgf Y μ'

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
h : IdentDistrib X Y μ μ'
⊢ mgf X μ = mgf Y μ'

Tactic:
rw [← mgf_id_map h.aemeasurable_fst, ← mgf_id_map h.aemeasurable_snd, h.map_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem associator_naturality_left {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) :
    η ▷ g ▷ h ≫ (α_ f' g h).hom = (α_ f g h).hom ≫ η ▷ (g ≫ h)

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d : B
f f' : a ⟶ b
η : f ⟶ f'
g : b ⟶ c
h : c ⟶ d
⊢ η ▷ g ▷ h ≫ (α_ f' g h).hom = (α_ f g h).hom ≫ η ▷ (g ≫ h)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem ker_prodMap {G' : Type*} {N' : Type*} [Group G'] [Group N'] (f : G →* N) (g : G' →* N') :
    (prodMap f g).ker = f.ker.prod g.ker

Proof state:
G : Type u_1
inst✝³ : Group G
N : Type u_5
inst✝² : Group N
G' : Type u_8
N' : Type u_9
inst✝¹ : Group G'
inst✝ : Group N'
f : G →* N
g : G' →* N'
⊢ (f.prodMap g).ker = f.ker.prod g.ker

Tactic:
rw [← comap_bot, ← comap_bot, ← comap_bot, ← prodMap_comap_prod, bot_prod_bot]

Result:
no goals
-- Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean
theorem pluennecke_ruzsa_inequality_pow_mul (hA : A.Nonempty) (B : Finset G) (n : ℕ) :
    #(B ^ n) ≤ (#(A * B) / #A : ℚ≥0) ^ n * #A

Proof state:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
n : ℕ
⊢ ↑(#(B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)

Tactic:
simpa only [_root_.pow_zero, div_one] using pluennecke_ruzsa_inequality_pow_div_pow_mul hA _ _ 0

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue_append_of_containsKey_eq_false {β : Type v} [BEq α] {l l' : List ((_ : α) × β)}
    {a : α} {h'} (h : containsKey a l' = false) : getValue a (l ++ l') h' =
      getValue a l ((containsKey_append_of_not_contains_right h).symm.trans h')

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l l' : List ((_ : α) × β)
a : α
h' : containsKey a (l ++ l') = true
h : containsKey a l' = false
⊢ getValue a (l ++ l') h' = getValue a l ⋯

Tactic:
rw [← Option.some_inj, ← getValue?_eq_some_getValue, ← getValue?_eq_some_getValue,
  getValue?_append_of_containsKey_eq_false h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblX_of_Z_eq_zero {P : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0) :
    W'.dblX P = (P x ^ 2) ^ 2

Proof state:
case a.a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ (-3 * P x ^ 2) ^ 2 - W'.a₁ * (-3 * P x ^ 2) * 0 * (P y - -P y) - W'.a₂ * 0 ^ 2 * (P y - -P y) ^ 2 -
          2 * P x * (P y - -P y) ^ 2 +
        -8 * P x * P x ^ 3 -
      ((P x ^ 2) ^ 2 + -8 * P x * P y ^ 2) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
case a.a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.dblX P + -8 * P x * P x ^ 3 - ((P x ^ 2) ^ 2 + -8 * P x * P y ^ 2) = 0

Tactic:
rw [dblX, dblU_of_Z_eq_zero hPz, negY_of_Z_eq_zero hPz, hPz]

Result:
case a.a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ (-3 * P x ^ 2) ^ 2 - W'.a₁ * (-3 * P x ^ 2) * 0 * (P y - -P y) - W'.a₂ * 0 ^ 2 * (P y - -P y) ^ 2 -
          2 * P x * (P y - -P y) ^ 2 +
        -8 * P x * P x ^ 3 -
      ((P x ^ 2) ^ 2 + -8 * P x * P y ^ 2) =
    0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.dblX P = (P x ^ 2) ^ 2

Tactic:
linear_combination (norm := (rw [dblX, dblU_of_Z_eq_zero hPz, negY_of_Z_eq_zero hPz, hPz]; ring1))
  -8 * P x * (equation_of_Z_eq_zero hPz).mp hP

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem le_mul_of_ediv_le {a b c : Int} (H1 : 0 ≤ b) (H2 : b ∣ a) (H3 : a / b ≤ c) :
    a ≤ c * b

Proof state:
a b c : Int
H1 : 0 ≤ b
H2 : b ∣ a
H3 : a / b ≤ c
⊢ a ≤ c * b

Tactic:
rw [← Int.ediv_mul_cancel H2]

Result:
a b c : Int
H1 : 0 ≤ b
H2 : b ∣ a
H3 : a / b ≤ c
⊢ a / b * b ≤ c * b

Proof state:
a b c : Int
H1 : 0 ≤ b
H2 : b ∣ a
H3 : a / b ≤ c
⊢ a / b * b ≤ c * b

Tactic:
exact Int.mul_le_mul_of_nonneg_right H3 H1

Result:
no goals
-- Mathlib/MeasureTheory/Group/Arithmetic.lean
/-- Compositional version of `Measurable.mul` for use by `fun_prop`. -/
@[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))
"Compositional version of `Measurable.add` for use by `fun_prop`."]
lemma Measurable.mul' [MeasurableMul₂ M] {f g : α → β → M} {h : α → β} (hf : Measurable ↿f)
    (hg : Measurable ↿g) (hh : Measurable h) : Measurable fun a ↦ (f a * g a) (h a)

Proof state:
M : Type u_2
α : Type u_3
β : Type u_4
inst✝² : MeasurableSpace M
inst✝¹ : Mul M
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableMul₂ M
f g : α → β → M
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
⊢ Measurable fun a => f a (h a) * g a (h a)

Tactic:
fun_prop

Result:
no goals

Proof state:
M : Type u_2
α : Type u_3
β : Type u_4
inst✝² : MeasurableSpace M
inst✝¹ : Mul M
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableMul₂ M
f g : α → β → M
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
⊢ Measurable fun a => (f a * g a) (h a)

Tactic:
simp

Result:
M : Type u_2
α : Type u_3
β : Type u_4
inst✝² : MeasurableSpace M
inst✝¹ : Mul M
m : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableMul₂ M
f g : α → β → M
h : α → β
hf : Measurable ↿f
hg : Measurable ↿g
hh : Measurable h
⊢ Measurable fun a => f a (h a) * g a (h a)
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
@[simp]
lemma Basis.toMatrix_mulVec_repr [Finite ι'] (m : M) :
    b'.toMatrix b *ᵥ b.repr m = b'.repr m

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
b' : Basis ι' R M
inst✝¹ : Fintype ι
inst✝ : Finite ι'
m : M
⊢ b'.toMatrix ⇑b *ᵥ ⇑(b.repr m) = ⇑(b'.repr m)

Tactic:
classical
cases nonempty_fintype ι'
simp [← LinearMap.toMatrix_id_eq_basis_toMatrix, LinearMap.toMatrix_mulVec_repr]

Result:
no goals

Proof state:
case intro
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
b' : Basis ι' R M
inst✝¹ : Fintype ι
inst✝ : Finite ι'
m : M
val✝ : Fintype ι'
⊢ b'.toMatrix ⇑b *ᵥ ⇑(b.repr m) = ⇑(b'.repr m)

Tactic:
simp [← LinearMap.toMatrix_id_eq_basis_toMatrix, LinearMap.toMatrix_mulVec_repr]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
b' : Basis ι' R M
inst✝¹ : Fintype ι
inst✝ : Finite ι'
m : M
⊢ b'.toMatrix ⇑b *ᵥ ⇑(b.repr m) = ⇑(b'.repr m)

Tactic:
cases nonempty_fintype ι'

Result:
case intro
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
b : Basis ι R M
b' : Basis ι' R M
inst✝¹ : Fintype ι
inst✝ : Finite ι'
m : M
val✝ : Fintype ι'
⊢ b'.toMatrix ⇑b *ᵥ ⇑(b.repr m) = ⇑(b'.repr m)
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_sub_right_eq_neg (x y : V) :
    (o.oangle x (x - y)).sign = -(o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ (o.oangle x (x - y)).sign = -(o.oangle x y).sign

Tactic:
rw [← o.oangle_sign_smul_sub_right x y 1, one_smul]

Result:
no goals