harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Order/Minimal.lean
theorem image_setOf_minimal (f : α ≃o β) (P : α → Prop) :
    f '' {x | Minimal P x} = {x | Minimal (fun x ↦ P (f.symm x)) x}

Proof state:
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ≃o β
P : α → Prop
⊢ ∀ ⦃x y : α⦄, ?m.86119 x → ?m.86119 y → (f x ≤ f y ↔ x ≤ y)

Tactic:
simp [f.le_iff_le]

Result:
no goals

Proof state:
case h.e'_3.h.e'_2.h.h.e'_3.h.a
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ≃o β
P : α → Prop
x✝¹ x✝ : β
⊢ P (f.symm x✝) ↔ ∃ x₀, P x₀ ∧ f x₀ = x✝

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ≃o β
P : α → Prop
⊢ ⇑f '' {x | Minimal P x} = {x | Minimal (fun x => P (f.symm x)) x}

Tactic:
convert _root_.image_monotone_setOf_minimal (f := f) (by simp [f.le_iff_le])

Result:
case h.e'_3.h.e'_2.h.h.e'_3.h.a
α : Type u_1
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
f : α ≃o β
P : α → Prop
x✝¹ x✝ : β
⊢ P (f.symm x✝) ↔ ∃ x₀, P x₀ ∧ f x₀ = x✝
-- Mathlib/Combinatorics/SimpleGraph/Basic.lean
theorem iSup_adj {f : ι → SimpleGraph V} : (⨆ i, f i).Adj a b ↔ ∃ i, (f i).Adj a b

Proof state:
ι : Sort u_1
V : Type u
a b : V
f : ι → SimpleGraph V
⊢ (⨆ i, f i).Adj a b ↔ ∃ i, (f i).Adj a b

Tactic:
simp [iSup]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem tsub_nonpos : a - b ≤ 0 ↔ a ≤ b

Proof state:
α : Type u_1
inst✝³ : Preorder α
inst✝² : AddCommMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
⊢ a - b ≤ 0 ↔ a ≤ b

Tactic:
rw [tsub_le_iff_left, add_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
theorem condExp_of_aestronglyMeasurable' (hm : m ≤ m₀) [hμm : SigmaFinite (μ.trim hm)] {f : α → E}
    (hf : AEStronglyMeasurable[m] f μ) (hfi : Integrable f μ) : μ[f|m] =ᵐ[μ] f

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hf : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ μ[f|m] =ᶠ[ae μ] f

Tactic:
refine ((condExp_congr_ae hf.ae_eq_mk).trans ?_).trans hf.ae_eq_mk.symm

Result:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hf : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ μ[AEStronglyMeasurable.mk f hf|m] =ᶠ[ae μ] AEStronglyMeasurable.mk f hf

Proof state:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hf : AEStronglyMeasurable f μ
hfi : Integrable f μ
⊢ μ[AEStronglyMeasurable.mk f hf|m] =ᶠ[ae μ] AEStronglyMeasurable.mk f hf

Tactic:
rw [condExp_of_stronglyMeasurable hm hf.stronglyMeasurable_mk
  ((integrable_congr hf.ae_eq_mk).mp hfi)]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem ofMkLE_arrow {B A : C} {f : A ⟶ B} [Mono f] {X : Subobject B} (h : mk f ≤ X) :
    ofMkLE f X h ≫ X.arrow = f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A : C
f : A ⟶ B
inst✝ : Mono f
X : Subobject B
h : mk f ≤ X
⊢ ofMkLE f X h ≫ X.arrow = f

Tactic:
simp [ofMkLE]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Multinomial.lean
theorem multinomial_zero [DecidableEq α] : multinomial (0 : Multiset α) = 1

Proof state:
α : Type u_1
inst✝ : DecidableEq α
⊢ multinomial 0 = 1

Tactic:
simp [multinomial, Finsupp.multinomial]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Pasting.lean
theorem pullbackRightPullbackFstIso_inv_snd_fst :
    (pullbackRightPullbackFstIso f g f').inv ≫ pullback.snd _ _ ≫ pullback.fst _ _ =
      pullback.fst _ _ ≫ f'

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
f' : W ⟶ X
inst✝¹ : HasPullback f g
inst✝ : HasPullback f' (pullback.fst f g)
⊢ (pullbackRightPullbackFstIso f g f').inv ≫ pullback.snd f' (pullback.fst f g) ≫ pullback.fst f g =
    pullback.fst (f' ≫ f) g ≫ f'

Tactic:
rw [← pullback.condition]

Result:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
f' : W ⟶ X
inst✝¹ : HasPullback f g
inst✝ : HasPullback f' (pullback.fst f g)
⊢ (pullbackRightPullbackFstIso f g f').inv ≫ pullback.fst f' (pullback.fst f g) ≫ f' = pullback.fst (f' ≫ f) g ≫ f'

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
f' : W ⟶ X
inst✝¹ : HasPullback f g
inst✝ : HasPullback f' (pullback.fst f g)
⊢ (pullbackRightPullbackFstIso f g f').inv ≫ pullback.fst f' (pullback.fst f g) ≫ f' = pullback.fst (f' ≫ f) g ≫ f'

Tactic:
exact pullbackRightPullbackFstIso_inv_fst_assoc f g f' _

Result:
no goals
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem isOpenEmbedding_coe : IsOpenEmbedding ((↑) : ℝ → EReal) :=
  ⟨isEmbedding_coe, by simp only [range_coe_eq_Ioo, isOpen_Ioo]⟩

Proof state:
⊢ IsOpen (range Real.toEReal)

Tactic:
simp only [range_coe_eq_Ioo, isOpen_Ioo]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem inter_nonempty_iff_exists_left : (s ∩ t).Nonempty ↔ ∃ x ∈ s, x ∈ t

Proof state:
α : Type u
s t : Set α
⊢ (s ∩ t).Nonempty ↔ ∃ x ∈ s, x ∈ t

Tactic:
simp_rw [inter_nonempty]

Result:
no goals
-- Mathlib/Order/ModularLattice.lean
theorem disjoint_sup_right_of_disjoint_sup_left [Lattice α] [OrderBot α]
    [IsModularLattice α] (h : Disjoint a b) (hsup : Disjoint (a ⊔ b) c) :
    Disjoint a (b ⊔ c)

Proof state:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ (?m.30782 ⊔ a) ⊓ (c ⊔ b) ≤ b

α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ α

Tactic:
rw [sup_comm, IsModularLattice.sup_inf_sup_assoc, hsup.eq_bot, bot_sup_eq]

Result:
no goals

Proof state:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ Disjoint a (b ⊔ c)

Tactic:
rw [disjoint_iff_inf_le, ← h.eq_bot, sup_comm]

Result:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ a ⊓ (c ⊔ b) ≤ a ⊓ b

Proof state:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ a ⊓ (c ⊔ b) ≤ a ⊓ b

Tactic:
apply le_inf inf_le_left

Result:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ a ⊓ (c ⊔ b) ≤ b

Proof state:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ a ⊓ (c ⊔ b) ≤ b

Tactic:
apply (inf_le_inf_right (c ⊔ b) le_sup_right).trans

Result:
α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ (?m.30782 ⊔ a) ⊓ (c ⊔ b) ≤ b

α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ α
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_toNat {n : Nat} {z : Int} (h : 0 ≤ z) : n ≤ z.toNat ↔ (n : Int) ≤ z

Proof state:
n : Nat
z : Int
h : 0 ≤ z
⊢ n ≤ z.toNat ↔ ↑n ≤ z

Tactic:
rw [← Int.ofNat_le, Int.toNat_of_nonneg h]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_nat_eq_natCast_descFactorial (S : Type*) [Semiring S] (a b : ℕ) :
    (ascPochhammer S b).eval (a : S) = (a + b - 1).descFactorial b

Proof state:
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ eval (↑a) (ascPochhammer S b) = ↑((a + b - 1).descFactorial b)

Tactic:
norm_cast

Result:
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(eval a (ascPochhammer ℕ b)) = ↑((a + b - 1).descFactorial b)

Proof state:
S : Type u_1
inst✝ : Semiring S
a b : ℕ
⊢ ↑(eval a (ascPochhammer ℕ b)) = ↑((a + b - 1).descFactorial b)

Tactic:
rw [ascPochhammer_nat_eq_descFactorial]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Functor.lean
theorem mapTriangleCommShiftIso_add
    [∀ (n : ℤ), (shiftFunctor C n).Additive]
    [∀ (n : ℤ), (shiftFunctor D n).Additive] (n m : ℤ) :
    F.mapTriangleCommShiftIso (n + m) =
      CommShift.isoAdd (a := n) (b := m)
        (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Category.{u_5, u_2} D
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
F : C ⥤ D
inst✝⁵ : F.CommShift ℤ
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : F.Additive
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
n m : ℤ
⊢ F.mapTriangleCommShiftIso (n + m) = CommShift.isoAdd (F.mapTriangleCommShiftIso n) (F.mapTriangleCommShiftIso m)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem swap_iInf [InfSet α] [InfSet β] (f : ι → α × β) : (iInf f).swap = ⨅ i, (f i).swap

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝¹ : InfSet α
inst✝ : InfSet β
f : ι → α × β
⊢ (iInf f).swap = ⨅ i, (f i).swap

Tactic:
simp_rw [iInf, swap_sInf, ← range_comp, comp_def]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
protected lemma add_posSemidef [AddLeftMono R]
    {A : Matrix m m R} {B : Matrix m m R}
    (hA : A.PosDef) (hB : B.PosSemidef) : (A + B).PosDef :=
  ⟨hA.isHermitian.add hB.isHermitian, fun x hx => by
    rw [add_mulVec, dotProduct_add]
    exact add_pos_of_pos_of_nonneg (hA.2 x hx) (hB.2 x)⟩

Proof state:
m : Type u_1
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : AddLeftMono R
A B : Matrix m m R
hA : A.PosDef
hB : B.PosSemidef
x : m → R
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ (A + B) *ᵥ x

Tactic:
rw [add_mulVec, dotProduct_add]

Result:
m : Type u_1
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : AddLeftMono R
A B : Matrix m m R
hA : A.PosDef
hB : B.PosSemidef
x : m → R
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ A *ᵥ x + star x ⬝ᵥ B *ᵥ x

Proof state:
m : Type u_1
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : CommRing R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : AddLeftMono R
A B : Matrix m m R
hA : A.PosDef
hB : B.PosSemidef
x : m → R
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ A *ᵥ x + star x ⬝ᵥ B *ᵥ x

Tactic:
exact add_pos_of_pos_of_nonneg (hA.2 x hx) (hB.2 x)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedLemmas.lean
theorem mkConstCached_hit_aig (aig : AIG α) {hit}
    (hcache : aig.cache.get? (.const val) = some hit) :
    (aig.mkConstCached val).aig = aig

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.const val)
hcache : aig.cache.get? (Decl.const val) = some hit
⊢ (aig.mkConstCached val).aig = aig

Tactic:
simp only [mkConstCached]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.const val)
hcache : aig.cache.get? (Decl.const val) = some hit
⊢ (match aig.cache.get? (Decl.const val) with
      | some hit =>
        { aig := { decls := aig.decls, cache := aig.cache, invariant := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
      | none =>
        {
          aig :=
            { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
              invariant := ⋯ },
          ref := { gate := aig.decls.size, hgate := ⋯ } }).aig =
    aig

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
aig : AIG α
hit : CacheHit aig.decls (Decl.const val)
hcache : aig.cache.get? (Decl.const val) = some hit
⊢ (match aig.cache.get? (Decl.const val) with
      | some hit =>
        { aig := { decls := aig.decls, cache := aig.cache, invariant := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
      | none =>
        {
          aig :=
            { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
              invariant := ⋯ },
          ref := { gate := aig.decls.size, hgate := ⋯ } }).aig =
    aig

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
theorem whiskerLeft_ι_colimitCompWhiskeringLeftIsoCompColimit_inv (F : J ⥤ K ⥤ C) (G : D ⥤ K)
    [HasColimitsOfShape J C] (j : J) :
    whiskerLeft G (colimit.ι F j) ≫ (colimitCompWhiskeringLeftIsoCompColimit F G).inv =
      colimit.ι (F ⋙ (whiskeringLeft _ _ _).obj G) j

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
F : J ⥤ K ⥤ C
G : D ⥤ K
inst✝ : HasColimitsOfShape J C
j : J
⊢ whiskerLeft G (colimit.ι F j) ≫ (colimitCompWhiskeringLeftIsoCompColimit F G).inv =
    colimit.ι (F ⋙ (whiskeringLeft D K C).obj G) j

Tactic:
simp [Iso.comp_inv_eq]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Basic.lean
theorem ext_nat [FunLike F ℕ R] [RingHomClass F ℕ R] (f g : F) : f = g :=
  ext_nat' f g <| by simp only [map_one f, map_one g]

Proof state:
R : Type u_3
F : Type u_5
inst✝² : NonAssocSemiring R
inst✝¹ : FunLike F ℕ R
inst✝ : RingHomClass F ℕ R
f g : F
⊢ f 1 = g 1

Tactic:
simp only [map_one f, map_one g]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem _root_.isometry_subsingleton [Subsingleton α] : Isometry f := fun x y => by
  rw [Subsingleton.elim x y]; simp

Proof state:
α : Type u
β : Type v
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
f : α → β
inst✝ : Subsingleton α
x y : α
⊢ edist (f y) (f y) = edist y y

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
f : α → β
inst✝ : Subsingleton α
x y : α
⊢ edist (f x) (f y) = edist x y

Tactic:
rw [Subsingleton.elim x y]

Result:
α : Type u
β : Type v
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
f : α → β
inst✝ : Subsingleton α
x y : α
⊢ edist (f y) (f y) = edist y y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Prop)
    (hs : ∀ i, p i (f as[i])) :
    ∃ eq : (as.map f).size = as.size, ∀ i h, p ⟨i, h⟩ ((as.map f)[i])

Proof state:
α : Type u_1
β : Type u_2
as : Array α
f : α → β
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), p i (f as[i])
⊢ ∃ eq, ∀ (i : Nat) (h : i < as.size), p ⟨i, h⟩ (map f as)[i]

Tactic:
simpa using map_induction as f (fun _ => True) trivial p (by simp_all)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
as : Array α
f : α → β
p : Fin as.size → β → Prop
hs : ∀ (i : Fin as.size), p i (f as[i])
⊢ ∀ (i : Fin as.size), (fun x => True) ↑i → p i (f as[i]) ∧ (fun x => True) (↑i + 1)

Tactic:
simp_all

Result:
no goals
-- Mathlib/RingTheory/WittVector/Defs.lean
theorem v2_coeff {p' R'} (x y : WittVector p' R') (i : Fin 2) :
    (![x, y] i).coeff = ![x.coeff, y.coeff] i

Proof state:
p' : ℕ
R' : Type u_2
x y : WittVector p' R'
i : Fin 2
⊢ (![x, y] i).coeff = ![x.coeff, y.coeff] i

Tactic:
fin_cases i <;> simp

Result:
no goals
-- Mathlib/Data/List/Map2.lean
theorem map₂Left_nil_right : map₂Left f as [] = as.map fun a => f a none

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
as : List α
⊢ map₂Left f as [] = map (fun a => f a none) as

Tactic:
cases as <;> rfl

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_mkPiAlgebraFin_zero : ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ = ‖(1 : A)‖

Proof state:
case refine_1
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ ≤ ‖1‖

Tactic:
refine opNorm_le_bound (norm_nonneg (1 : A)) ?_

Result:
case refine_1
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ∀ (m : Fin 0 → A), ‖(ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) m‖ ≤ ‖1‖ * ∏ i : Fin 0, ‖m i‖

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ = ‖1‖

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖ ≤ ‖1‖

case refine_2
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖1‖ ≤ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖

Proof state:
case refine_1
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ∀ (m : Fin 0 → A), ‖(ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) m‖ ≤ ‖1‖ * ∏ i : Fin 0, ‖m i‖

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖1‖ ≤ ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A‖

Tactic:
convert ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) fun _ => (1 : A)

Result:
case h.e'_3
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖1‖ = ‖(ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) fun x => 1‖ / ∏ i : Fin 0, ‖1‖

Proof state:
case h.e'_3
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
A : Type u_1
inst✝¹ : SeminormedRing A
inst✝ : NormedAlgebra 𝕜 A
⊢ ‖1‖ = ‖(ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 0 A) fun x => 1‖ / ∏ i : Fin 0, ‖1‖

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem mem_closure_iff_nhds_basis' {p : ι → Prop} {s : ι → Set X} (h : (𝓝 x).HasBasis p s) :
    x ∈ closure t ↔ ∀ i, p i → (s i ∩ t).Nonempty :=
  mem_closure_iff_clusterPt.trans <|
    (h.clusterPt_iff (hasBasis_principal _)).trans <| by simp only [exists_prop, forall_const]

Proof state:
X : Type u
ι : Sort w
x : X
t : Set X
inst✝ : TopologicalSpace X
p : ι → Prop
s : ι → Set X
h : (𝓝 x).HasBasis p s
⊢ (∀ ⦃i : ι⦄, p i → ∀ ⦃j : Unit⦄, True → (s i ∩ t).Nonempty) ↔ ∀ (i : ι), p i → (s i ∩ t).Nonempty

Tactic:
simp only [exists_prop, forall_const]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma negAddY_self (P : Fin 3 → R) : W'.negAddY P P = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * P x * P y + 3 * P x * P x ^ 2 * P y - P y ^ 2 * P y * P z + P y * P y ^ 2 * P z +
                                W'.a₁ * P x * P y ^ 2 * P z -
                              W'.a₁ * P x * P y ^ 2 * P z -
                            W'.a₂ * P x ^ 2 * P y * P z +
                          W'.a₂ * P x ^ 2 * P y * P z +
                        2 * W'.a₂ * P x * P x * P y * P z -
                      2 * W'.a₂ * P x * P x * P y * P z -
                    W'.a₃ * P y ^ 2 * P z ^ 2 +
                  W'.a₃ * P y ^ 2 * P z ^ 2 +
                W'.a₄ * P x * P y * P z ^ 2 -
              2 * W'.a₄ * P x * P y * P z * P z +
            2 * W'.a₄ * P x * P y * P z * P z -
          W'.a₄ * P x * P y * P z ^ 2 +
        3 * W'.a₆ * P y * P z * P z ^ 2 -
      3 * W'.a₆ * P y * P z ^ 2 * P z =
    0

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.negAddY P P = 0

Tactic:
rw [negAddY]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * P x * P y + 3 * P x * P x ^ 2 * P y - P y ^ 2 * P y * P z + P y * P y ^ 2 * P z +
                                W'.a₁ * P x * P y ^ 2 * P z -
                              W'.a₁ * P x * P y ^ 2 * P z -
                            W'.a₂ * P x ^ 2 * P y * P z +
                          W'.a₂ * P x ^ 2 * P y * P z +
                        2 * W'.a₂ * P x * P x * P y * P z -
                      2 * W'.a₂ * P x * P x * P y * P z -
                    W'.a₃ * P y ^ 2 * P z ^ 2 +
                  W'.a₃ * P y ^ 2 * P z ^ 2 +
                W'.a₄ * P x * P y * P z ^ 2 -
              2 * W'.a₄ * P x * P y * P z * P z +
            2 * W'.a₄ * P x * P y * P z * P z -
          W'.a₄ * P x * P y * P z ^ 2 +
        3 * W'.a₆ * P y * P z * P z ^ 2 -
      3 * W'.a₆ * P y * P z ^ 2 * P z =
    0
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
@[simp]
lemma fromRows_mul [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B : Matrix n m R) :
    fromRows A₁ A₂ * B = fromRows (A₁ * B) (A₂ * B)

Proof state:
R : Type u_1
m : Type u_2
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B : Matrix n m R
⊢ A₁.fromRows A₂ * B = (A₁ * B).fromRows (A₂ * B)

Tactic:
ext (_ | _) _ <;> simp [mul_apply]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
@[simp] lemma supClosed_singleton : SupClosed ({a} : Set α)

Proof state:
α : Type u_3
inst✝ : SemilatticeSup α
a : α
⊢ SupClosed {a}

Tactic:
simp [SupClosed]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem mul_nonpos_of_nonneg_of_nonpos [PosMulMono α] (ha : 0 ≤ a) (hb : b ≤ 0) : a * b ≤ 0

Proof state:
α : Type u_3
a b : α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulMono α
ha : 0 ≤ a
hb : b ≤ 0
⊢ a * b ≤ 0

Tactic:
simpa only [mul_zero] using mul_le_mul_of_nonneg_left hb ha

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem factorization_eq_zero_iff' (n : ℕ) : n.factorization = 0 ↔ n = 0 ∨ n = 1

Proof state:
n : ℕ
⊢ n.factorization = 0 ↔ n = 0 ∨ n = 1

Tactic:
rw [factorization_eq_primeFactorsList_multiset n]

Result:
n : ℕ
⊢ Multiset.toFinsupp ↑n.primeFactorsList = 0 ↔ n = 0 ∨ n = 1

Proof state:
n : ℕ
⊢ Multiset.toFinsupp ↑n.primeFactorsList = 0 ↔ n = 0 ∨ n = 1

Tactic:
simp [factorization, AddEquiv.map_eq_zero_iff, Multiset.coe_eq_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_lintegral_mul {β} [MeasurableSpace β] {ν : Measure β} {f : α → ℝ≥0∞}
    {g : β → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g ν) :
    ∫⁻ x, ∫⁻ y, f x * g y ∂ν ∂μ = (∫⁻ x, f x ∂μ) * ∫⁻ y, g y ∂ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_5
inst✝ : MeasurableSpace β
ν : Measure β
f : α → ℝ≥0∞
g : β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g ν
⊢ ∫⁻ (x : α), ∫⁻ (y : β), f x * g y ∂ν ∂μ = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν

Tactic:
simp [lintegral_const_mul'' _ hg, lintegral_mul_const'' _ hf]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
@[reassoc (attr := simp)]
lemma mapObj_trans {j₁ j₂ j₃ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂)
    (iter₃ : Φ.Iteration j₃) {k₁ k₂ k₃ : J} (h₁₂ : k₁ ≤ k₂) (h₂₃ : k₂ ≤ k₃)
    (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂) (h₃ : k₃ ≤ j₃) (h₁₂' : j₁ ≤ j₂) (h₂₃' : j₂ ≤ j₃) :
    mapObj iter₁ iter₂ h₁₂ h₁ h₂ h₁₂' ≫ mapObj iter₂ iter₃ h₂₃ h₂ h₃ h₂₃' =
      mapObj iter₁ iter₃ (h₁₂.trans h₂₃) h₁ h₃ (h₁₂'.trans h₂₃')

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁴ : LinearOrder J
inst✝³ : SuccOrder J
inst✝² : OrderBot J
inst✝¹ : HasIterationOfShape J C
inst✝ : WellFoundedLT J
j₁ j₂ j₃ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
iter₃ : Φ.Iteration j₃
k₁ k₂ k₃ : J
h₁₂ : k₁ ≤ k₂
h₂₃ : k₂ ≤ k₃
h₁ : k₁ ≤ j₁
h₂ : k₂ ≤ j₂
h₃ : k₃ ≤ j₃
h₁₂' : j₁ ≤ j₂
h₂₃' : j₂ ≤ j₃
⊢ iter₁.mapObj iter₂ h₁₂ h₁ h₂ h₁₂' ≫ iter₂.mapObj iter₃ h₂₃ h₂ h₃ h₂₃' = iter₁.mapObj iter₃ ⋯ h₁ h₃ ⋯

Tactic:
simp [mapObj, congr_map iter₂ iter₃ h₁₂ h₂ (h₂.trans h₂₃'), ← Functor.map_comp]

Result:
no goals