harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/Embedding/Extend.lean
@[simp]
lemma extendMap_zero : extendMap (0 : K ⟶ L) e = 0

Proof state:
case h
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
⊢ (extendMap 0 e).f i' = Hom.f 0 i'

Tactic:
by_cases hi' : ∃ i, e.f i = i'

Result:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap 0 e).f i' = Hom.f 0 i'

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap 0 e).f i' = Hom.f 0 i'

Proof state:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ (extendMap 0 e).f i' = Hom.f 0 i'

Tactic:
apply (K.isZero_extend_X e i' (fun i hi => hi' ⟨i, hi⟩)).eq_of_src

Result:
no goals

Proof state:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (extendMap 0 e).f i' = Hom.f 0 i'

Tactic:
obtain ⟨i, hi⟩ := hi'

Result:
case pos.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
i : ι
hi : e.f i = i'
⊢ (extendMap 0 e).f i' = Hom.f 0 i'

Proof state:
case pos.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
i : ι
hi : e.f i = i'
⊢ (extendMap 0 e).f i' = Hom.f 0 i'

Tactic:
simp [extendMap_f _ e hi]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
⊢ extendMap 0 e = 0

Tactic:
ext i'

Result:
case h
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{u_4, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
e : c.Embedding c'
i' : ι'
⊢ (extendMap 0 e).f i' = Hom.f 0 i'
-- Mathlib/Algebra/MvPolynomial/Monad.lean
theorem map_bind₂ (f : R →+* MvPolynomial σ S) (g : S →+* T) (φ : MvPolynomial σ R) :
    map g (bind₂ f φ) = bind₂ ((map g).comp f) φ

Proof state:
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
⊢ (map g) ((bind₂ f) φ) = (bind₂ ((map g).comp f)) φ

Tactic:
simp only [bind₂, eval₂_comp_right, coe_eval₂Hom, eval₂_map]

Result:
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
⊢ eval₂ ((map g).comp f) (⇑(map g) ∘ X) φ = eval₂ ((map g).comp f) X φ

Proof state:
case e_g.h
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
x✝ : σ
⊢ (⇑(map g) ∘ X) x✝ = X x✝

Tactic:
simp only [Function.comp_apply, map_X]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
⊢ eval₂ ((map g).comp f) (⇑(map g) ∘ X) φ = eval₂ ((map g).comp f) X φ

Tactic:
congr 1 with : 1

Result:
case e_g.h
σ : Type u_1
R : Type u_3
S : Type u_4
T : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : CommSemiring T
f : R →+* MvPolynomial σ S
g : S →+* T
φ : MvPolynomial σ R
x✝ : σ
⊢ (⇑(map g) ∘ X) x✝ = X x✝
-- Mathlib/Topology/Basic.lean
theorem Dense.interior_compl (h : Dense s) : interior sᶜ = ∅ :=
  interior_eq_empty_iff_dense_compl.2 <| by rwa [compl_compl]

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
h : Dense s
⊢ Dense sᶜᶜ

Tactic:
rwa [compl_compl]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem Splits.comp_neg_X {f : K[X]} (h : f.Splits i) : (f.comp (-X)).Splits i :=
  Splits.comp_of_degree_le_one (by simpa using degree_X_sub_C_le (0 : K)) h

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
h : Splits i f
⊢ (-X).degree ≤ 1

Tactic:
simpa using degree_X_sub_C_le (0 : K)

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[gcongr]
lemma div_lt_div₀ (hac : a < c) (hdb : d ≤ b) (hc : 0 ≤ c) (hd : 0 < d) : a / b < c / d

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : LinearOrder G₀
inst✝² : ZeroLEOneClass G₀
a b c d : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : MulPosStrictMono G₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd : 0 < d
⊢ a / b < c / d

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv]

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : LinearOrder G₀
inst✝² : ZeroLEOneClass G₀
a b c d : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : MulPosStrictMono G₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd : 0 < d
⊢ a * b⁻¹ < c * d⁻¹

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : LinearOrder G₀
inst✝² : ZeroLEOneClass G₀
a b c d : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : MulPosStrictMono G₀
hac : a < c
hdb : d ≤ b
hc : 0 ≤ c
hd : 0 < d
⊢ a * b⁻¹ < c * d⁻¹

Tactic:
exact mul_lt_mul hac ((inv_le_inv₀ (hd.trans_le hdb) hd).2 hdb) (inv_pos.2 <| hd.trans_le hdb) hc

Result:
no goals
-- Mathlib/MeasureTheory/Function/UniformIntegrable.lean
theorem unifIntegrable_const {g : α → β} (hp : 1 ≤ p) (hp_ne_top : p ≠ ∞) (hg : MemLp g p μ) :
    UnifIntegrable (fun _ : ι => g) p μ

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp : 1 ≤ p
hp_ne_top : p ≠ ⊤
hg : MemLp g p μ
⊢ UnifIntegrable (fun x => g) p μ

Tactic:
intro ε hε

Result:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp : 1 ≤ p
hp_ne_top : p ≠ ⊤
hg : MemLp g p μ
ε : ℝ
hε : 0 < ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((fun x => g) i)) p μ ≤ ENNReal.ofReal ε

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp : 1 ≤ p
hp_ne_top : p ≠ ⊤
hg : MemLp g p μ
ε : ℝ
hε : 0 < ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((fun x => g) i)) p μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨δ, hδ_pos, hgδ⟩ := hg.eLpNorm_indicator_le hp hp_ne_top hε

Result:
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp : 1 ≤ p
hp_ne_top : p ≠ ⊤
hg : MemLp g p μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hgδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((fun x => g) i)) p μ ≤ ENNReal.ofReal ε

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
p : ℝ≥0∞
g : α → β
hp : 1 ≤ p
hp_ne_top : p ≠ ⊤
hg : MemLp g p μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hgδ : ∀ (s : Set α), MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal ε
⊢ ∃ δ,
    ∃ (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s → μ s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((fun x => g) i)) p μ ≤ ENNReal.ofReal ε

Tactic:
exact ⟨δ, hδ_pos, fun _ => hgδ⟩

Result:
no goals
-- Mathlib/Data/Multiset/Interval.lean
theorem card_Icc :
    #(Finset.Icc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (t.count i + 1 - s.count i)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ #(Finset.Icc s t) = ∏ i ∈ s.toFinset ∪ t.toFinset, (count i t + 1 - count i s)

Tactic:
simp_rw [Icc_eq, Finset.card_map, DFinsupp.card_Icc, Nat.card_Icc, Multiset.toDFinsupp_apply,
  toDFinsupp_support]

Result:
no goals
-- Mathlib/Data/Matrix/Rank.lean
theorem rank_one [StrongRankCondition R] [DecidableEq n] :
    rank (1 : Matrix n n R) = Fintype.card n

Proof state:
n : Type u_3
R : Type u_5
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : StrongRankCondition R
inst✝ : DecidableEq n
⊢ rank 1 = Fintype.card n

Tactic:
rw [rank, mulVecLin_one, LinearMap.range_id, finrank_top, finrank_pi]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem circumradius_reindex {m n : ℕ} (s : Simplex ℝ P m) (e : Fin (m + 1) ≃ Fin (n + 1)) :
    (s.reindex e).circumradius = s.circumradius

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).circumradius = s.circumradius

Tactic:
simp_rw [circumradius, circumsphere_reindex]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem drop_suffix_drop_left (l : List α) {m n : Nat} (h : m ≤ n) : drop n l <:+ drop m l

Proof state:
α : Type u_1
l : List α
m n : Nat
h : m ≤ n
⊢ drop (n - m) (drop m l) <:+ drop m l

Tactic:
apply drop_suffix

Result:
no goals

Proof state:
α : Type u_1
l : List α
m n : Nat
h : m ≤ n
⊢ drop n l <:+ drop m l

Tactic:
rw [← Nat.sub_add_cancel h, Nat.add_comm, ← drop_drop]

Result:
α : Type u_1
l : List α
m n : Nat
h : m ≤ n
⊢ drop (n - m) (drop m l) <:+ drop m l
-- Mathlib/Algebra/MonoidAlgebra/MapDomain.lean
theorem mapDomain_one {α : Type*} {β : Type*} {α₂ : Type*} [Semiring β] [One α] [One α₂]
    {F : Type*} [FunLike F α α₂] [OneHomClass F α α₂] (f : F) :
    (mapDomain f (1 : MonoidAlgebra β α) : MonoidAlgebra β α₂) = (1 : MonoidAlgebra β α₂)

Proof state:
α : Type u_3
β : Type u_4
α₂ : Type u_5
inst✝⁴ : Semiring β
inst✝³ : One α
inst✝² : One α₂
F : Type u_6
inst✝¹ : FunLike F α α₂
inst✝ : OneHomClass F α α₂
f : F
⊢ mapDomain (⇑f) 1 = 1

Tactic:
simp_rw [one_def, mapDomain_single, map_one]

Result:
no goals
-- Mathlib/RingTheory/Ideal/AssociatedPrime.lean
theorem associatedPrimes.nonempty [IsNoetherianRing R] [Nontrivial M] :
    (associatedPrimes R M).Nonempty

Proof state:
case intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
⊢ (associatedPrimes R M).Nonempty

Tactic:
obtain ⟨P, hP, _⟩ := exists_le_isAssociatedPrime_of_isNoetherianRing R x hx

Result:
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
P : Ideal R
hP : IsAssociatedPrime P M
right✝ : ker (toSpanSingleton R M x) ≤ P
⊢ (associatedPrimes R M).Nonempty

Proof state:
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
P : Ideal R
hP : IsAssociatedPrime P M
right✝ : ker (toSpanSingleton R M x) ≤ P
⊢ (associatedPrimes R M).Nonempty

Tactic:
exact ⟨P, hP⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Nontrivial M
⊢ (associatedPrimes R M).Nonempty

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : M)

Result:
case intro
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsNoetherianRing R
inst✝ : Nontrivial M
x : M
hx : x ≠ 0
⊢ (associatedPrimes R M).Nonempty
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
@[to_additive (attr := simp)]
lemma mul_subgroupClosure (hs : s.Nonempty) : s * closure s = closure s

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ ⋃ a ∈ s, a • ↑(closure s) = ↑(closure s)

Tactic:
have h a (ha : a ∈ s) : a • (closure s : Set G) = closure s :=
  smul_coe_set <| subset_closure ha

Result:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
h : ∀ a ∈ s, a • ↑(closure s) = ↑(closure s)
⊢ ⋃ a ∈ s, a • ↑(closure s) = ↑(closure s)

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ s * ↑(closure s) = ↑(closure s)

Tactic:
rw [← smul_eq_mul, ← Set.iUnion_smul_set]

Result:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ ⋃ a ∈ s, a • ↑(closure s) = ↑(closure s)

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
h : ∀ a ∈ s, a • ↑(closure s) = ↑(closure s)
⊢ ⋃ a ∈ s, a • ↑(closure s) = ↑(closure s)

Tactic:
simp +contextual [h, hs]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem rightUnitor_comp_inv (f : a ⟶ b) (g : b ⟶ c) :
    (ρ_ (f ≫ g)).inv = f ◁ (ρ_ g).inv ≫ (α_ f g (𝟙 c)).inv

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ c
⊢ (ρ_ (f ≫ g)).inv = f ◁ (ρ_ g).inv ≫ (α_ f g (𝟙 c)).inv

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/Image.lean
@[simp]
lemma range_ι (G : Subpresheaf F) : range G.ι = G

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
⊢ range G.ι = G

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem Const.getD_eq_getValueD [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α]
    {m : Raw₀ α (fun _ => β)} (hm : Raw.WFImp m.1) {a : α} {fallback : β} :
    Const.getD m a fallback = getValueD a (toListModel m.1.buckets) fallback

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
hm : Raw.WFImp m.val
a : α
fallback : β
⊢ getD m a fallback = getValueD a (toListModel m.val.buckets) fallback

Tactic:
rw [getD_eq_getDₘ, getDₘ_eq_getValueD hm]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
theorem edist_comm : G.edist u v = G.edist v u

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v = G.edist v u

Tactic:
rw [edist_eq_sInf, ← Set.image_univ, ← Set.image_univ_of_surjective Walk.reverse_surjective,
  ← Set.image_comp, Set.image_univ, Function.comp_def]

Result:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ sInf (Set.range fun x => ↑x.reverse.length) = G.edist v u

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ sInf (Set.range fun x => ↑x.reverse.length) = G.edist v u

Tactic:
simp_rw [Walk.length_reverse, ← edist_eq_sInf]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Spectrum.lean
/-- Non-unital star algebra homomorphisms between C⋆-algebras are continuous linear maps.
See note [lower instance priority] -/
lemma instContinuousLinearMapClassComplex : ContinuousLinearMapClass F ℂ A B :=
  { NonUnitalAlgHomClass.instLinearMapClass with
    map_continuous := fun φ =>
      AddMonoidHomClass.continuous_of_bound φ 1 (by simpa only [one_mul] using nnnorm_apply_le φ) }

Proof state:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : NonUnitalCStarAlgebra A
inst✝³ : NonUnitalCStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
φ : F
⊢ ∀ (x : A), ‖φ x‖ ≤ 1 * ‖x‖

Tactic:
simpa only [one_mul] using nnnorm_apply_le φ

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem finIdxOf?_toArray [BEq α] (a : α) (l : List α) :
    l.toArray.finIdxOf? a = l.finIdxOf? a

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ l.toArray.idxOfAux a 0 = findFinIdx?.go (fun x => x == a) l l 0 ⋯

Tactic:
simp [idxAuxOf_toArray]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ l.toArray.finIdxOf? a = finIdxOf? a l

Tactic:
rw [Array.finIdxOf?, finIdxOf?, findFinIdx?]

Result:
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ l.toArray.idxOfAux a 0 = findFinIdx?.go (fun x => x == a) l l 0 ⋯
-- Mathlib/Analysis/Complex/RealDeriv.lean
theorem HasDerivWithinAt.complexToReal_fderiv' {f : ℂ → E} {s : Set ℂ} {x : ℂ} {f' : E}
    (h : HasDerivWithinAt f f' s x) :
    HasFDerivWithinAt f (reCLM.smulRight f' + I • imCLM.smulRight f') s x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
s : Set ℂ
x : ℂ
f' : E
h : HasDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f (reCLM.smulRight f' + I • imCLM.smulRight f') s x

Tactic:
simpa only [Complex.restrictScalars_one_smulRight'] using
  h.hasFDerivWithinAt.restrictScalars ℝ

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/NormedSpace.lean
theorem contMDiffAt_iff_contDiffAt {f : E → E'} {x : E} :
    ContMDiffAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f x ↔ ContDiffAt 𝕜 n f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
n : WithTop ℕ∞
f : E → E'
x : E
⊢ ContMDiffAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f x ↔ ContDiffAt 𝕜 n f x

Tactic:
rw [← contMDiffWithinAt_univ, contMDiffWithinAt_iff_contDiffWithinAt, contDiffWithinAt_univ]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem mul_sub_mul_div_mul_nonpos_iff (hc : c ≠ 0) (hd : d ≠ 0) :
    (a * d - b * c) / (c * d) ≤ 0 ↔ a / c ≤ b / d

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c d : α
hc : c ≠ 0
hd : d ≠ 0
⊢ (a * d - b * c) / (c * d) ≤ 0 ↔ a / c ≤ b / d

Tactic:
rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_nonpos]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.add_of_left (hp : Monic p) (hpq : degree q < degree p) : Monic (p + q)

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
⊢ (p + q).Monic

Tactic:
rwa [Monic, add_comm, leadingCoeff_add_of_degree_lt hpq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sign_toReal {θ : Angle} (h : θ ≠ π) : SignType.sign θ.toReal = θ.sign

Proof state:
case inr.inl
θ : Angle
h : θ ≠ ↑π
ht : θ.toReal = 0
⊢ SignType.sign θ.toReal = θ.sign

Tactic:
simp [sign, ht, ← sin_toReal]

Result:
no goals

Proof state:
case inl
θ : Angle
h : θ ≠ ↑π
ht : θ.toReal < 0
⊢ SignType.sign θ.toReal = θ.sign

Tactic:
simp [ht, toReal_neg_iff_sign_neg.1 ht]

Result:
no goals

Proof state:
θ : Angle
h : θ ≠ ↑π
⊢ SignType.sign θ.toReal = θ.sign

Tactic:
rcases lt_trichotomy θ.toReal 0 with (ht | ht | ht)

Result:
case inl
θ : Angle
h : θ ≠ ↑π
ht : θ.toReal < 0
⊢ SignType.sign θ.toReal = θ.sign

case inr.inl
θ : Angle
h : θ ≠ ↑π
ht : θ.toReal = 0
⊢ SignType.sign θ.toReal = θ.sign

case inr.inr
θ : Angle
h : θ ≠ ↑π
ht : 0 < θ.toReal
⊢ SignType.sign θ.toReal = θ.sign

Proof state:
case inr.inr
θ : Angle
h : θ ≠ ↑π
ht : 0 < θ.toReal
⊢ SignType.sign θ.toReal = θ.sign

Tactic:
rw [sign, ← sin_toReal, sign_pos ht,
  sign_pos
    (sin_pos_of_pos_of_lt_pi ht ((toReal_le_pi θ).lt_of_ne (toReal_eq_pi_iff.not.2 h)))]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/WithTop.lean
theorem sub_top {a : WithTop α} : a - ⊤ = (⊥ : α)

Proof state:
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a : WithTop α
⊢ a - ⊤ = ↑⊥

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem allOnes_sub_eq_not (x : BitVec w) : allOnes w - x = ~~~x

Proof state:
w : Nat
x : BitVec w
⊢ allOnes w - x = ~~~x

Tactic:
rw [← add_not_self x, BitVec.add_comm, add_sub_cancel]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
theorem exists_measurable_superset₂ (μ ν : Measure α) (s : Set α) :
    ∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = μ s ∧ ν t = ν s

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
⊢ ∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = μ s ∧ ν t = ν s

Tactic:
simpa only [Bool.forall_bool.trans and_comm] using
  exists_measurable_superset_forall_eq (fun b => cond b μ ν) s

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_insert_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β} :
    get? (m.insert k v) k = some v

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
v : β
⊢ get? (m.insert k v) k = some v

Tactic:
simp_to_model [insert] using List.getValue?_insertEntry_self

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem mul_smul [Fintype n] [Monoid R] [DistribMulAction R α] [SMulCommClass R α α]
    (M : Matrix m n α) (a : R) (N : Matrix n l α) : M * (a • N) = a • (M * N)

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝⁵ : AddCommMonoid α
inst✝⁴ : Mul α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : SMulCommClass R α α
M : Matrix m n α
a : R
N : Matrix n l α
i✝ : m
j✝ : l
⊢ (M * a • N) i✝ j✝ = (a • (M * N)) i✝ j✝

Tactic:
apply dotProduct_smul

Result:
no goals

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝⁵ : AddCommMonoid α
inst✝⁴ : Mul α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : SMulCommClass R α α
M : Matrix m n α
a : R
N : Matrix n l α
⊢ M * a • N = a • (M * N)

Tactic:
ext

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝⁵ : AddCommMonoid α
inst✝⁴ : Mul α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : SMulCommClass R α α
M : Matrix m n α
a : R
N : Matrix n l α
i✝ : m
j✝ : l
⊢ (M * a • N) i✝ j✝ = (a • (M * N)) i✝ j✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem count_filterMap {α} [BEq β] (b : β) (f : α → Option β) (l : Array α) :
    count b (filterMap f l) = countP (fun a => f a == some b) l

Proof state:
β : Type u_1
α : Type u_2
inst✝ : BEq β
b : β
f : α → Option β
l : Array α
⊢ count b (filterMap f l) = countP (fun a => f a == some b) l

Tactic:
cases l

Result:
case mk
β : Type u_1
α : Type u_2
inst✝ : BEq β
b : β
f : α → Option β
toList✝ : List α
⊢ count b (filterMap f { toList := toList✝ }) = countP (fun a => f a == some b) { toList := toList✝ }

Proof state:
case mk
β : Type u_1
α : Type u_2
inst✝ : BEq β
b : β
f : α → Option β
toList✝ : List α
⊢ count b (filterMap f { toList := toList✝ }) = countP (fun a => f a == some b) { toList := toList✝ }

Tactic:
simp [List.count_filterMap, countP_filterMap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.add_right_eq_self (a b : BitVec w) : (a + b == a) = (b == 0#w)

Proof state:
w : Nat
a b : BitVec w
⊢ (a + b == a) = (b == 0#w)

Tactic:
rw [Bool.eq_iff_iff]

Result:
w : Nat
a b : BitVec w
⊢ (a + b == a) = true ↔ (b == 0#w) = true

Proof state:
w : Nat
a b : BitVec w
⊢ (a + b == a) = true ↔ (b == 0#w) = true

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem rightCoset_mem_rightCoset {a : α} (ha : a ∈ s) : op a • (s : Set α) = s :=
  Set.ext fun b => by simp [mem_rightCoset_iff, mul_mem_cancel_right (s.inv_mem ha)]

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
b : α
⊢ b ∈ op a • ↑s ↔ b ∈ ↑s

Tactic:
simp [mem_rightCoset_iff, mul_mem_cancel_right (s.inv_mem ha)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem _root_.List.unattach_toArray {p : α → Prop} {l : List { x // p x }} :
    l.toArray.unattach = l.unattach.toArray

Proof state:
α : Type u_1
p : α → Prop
l : List { x // p x }
⊢ l.toArray.unattach = l.unattach.toArray

Tactic:
simp only [unattach, List.map_toArray, List.unattach]

Result:
no goals