harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/MorphismProperty/Composition.lean
lemma multiplicativeClosure_eq_self_iff : W.multiplicativeClosure = W ↔ W.IsMultiplicative where
  mp h

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
h : W.multiplicativeClosure = W
⊢ W.multiplicativeClosure.IsMultiplicative

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
h : W.multiplicativeClosure = W
⊢ W.IsMultiplicative

Tactic:
rw [← h]

Result:
C : Type u
inst✝ : Category.{v, u} C
W : MorphismProperty C
h : W.multiplicativeClosure = W
⊢ W.multiplicativeClosure.IsMultiplicative
-- Mathlib/Logic/Equiv/Basic.lean
theorem piCongrLeft_sumInl {ι ι' ι''} (π : ι'' → Type*) (e : ι ⊕ ι' ≃ ι'') (f : ∀ i, π (e (inl i)))
    (g : ∀ i, π (e (inr i))) (i : ι) :
    piCongrLeft π e (sumPiEquivProdPi (fun x => π (e x)) |>.symm (f, g)) (e (inl i)) = f i

Proof state:
ι : Type u_10
ι' : Type u_11
ι'' : Sort u_12
π : ι'' → Type u_9
e : ι ⊕ ι' ≃ ι''
f : (i : ι) → π (e (inl i))
g : (i : ι') → π (e (inr i))
i : ι
⊢ (piCongrLeft π e) ((sumPiEquivProdPi fun x => π (e x)).symm (f, g)) (e (inl i)) = f i

Tactic:
simp_rw [piCongrLeft_apply_eq_cast, sumPiEquivProdPi_symm_apply,
  sum_rec_congr _ _ _ (e.symm_apply_apply (inl i)), cast_cast, cast_eq]

Result:
no goals
-- Mathlib/Topology/Order/UpperLowerSetTopology.lean
lemma closure_eq_lowerClosure {s : Set α} : closure s = lowerClosure s

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ closure s ⊆ ↑(lowerClosure s)

Tactic:
apply closure_minimal subset_lowerClosure _

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ IsClosed ↑(lowerClosure s)

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ IsLowerSet ↑(lowerClosure s)

Tactic:
exact LowerSet.lower (lowerClosure s)

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ closure s = ↑(lowerClosure s)

Tactic:
rw [subset_antisymm_iff]

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ closure s ⊆ ↑(lowerClosure s) ∧ ↑(lowerClosure s) ⊆ closure s

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ IsClosed ↑(lowerClosure s)

Tactic:
rw [isClosed_iff_isLower]

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ IsLowerSet ↑(lowerClosure s)

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ closure s ⊆ ↑(lowerClosure s) ∧ ↑(lowerClosure s) ⊆ closure s

Tactic:
refine ⟨?_, lowerClosure_min subset_closure (isClosed_iff_isLower.1 isClosed_closure)⟩

Result:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ closure s ⊆ ↑(lowerClosure s)
-- Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
@[reassoc]
lemma mapRightHomologyIso_hom_naturality [S₁.HasRightHomology] [S₂.HasRightHomology]
    [F.PreservesRightHomologyOf S₁] [F.PreservesRightHomologyOf S₂] :
    rightHomologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapRightHomologyIso F).hom =
      (S₁.mapRightHomologyIso F).hom ≫ F.map (rightHomologyMap φ)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Category.{u_4, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ rightHomologyMap' (F.mapShortComplex.map φ) (F.mapShortComplex.obj S₁).rightHomologyData
        (F.mapShortComplex.obj S₂).rightHomologyData ≫
      rightHomologyMap' (𝟙 (S₂.map F)) (S₂.map F).rightHomologyData (S₂.rightHomologyData.map F) =
    rightHomologyMap' (𝟙 (S₁.map F)) (S₁.map F).rightHomologyData (S₁.rightHomologyData.map F) ≫
      F.map (rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData)

Tactic:
simp only [RightHomologyData.map_rightHomologyMap', Functor.mapShortComplex_obj,
  ← rightHomologyMap'_comp, comp_id, id_comp]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Category.{u_4, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ rightHomologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapRightHomologyIso F).hom =
    (S₁.mapRightHomologyIso F).hom ≫ F.map (rightHomologyMap φ)

Tactic:
dsimp only [rightHomologyMap, mapRightHomologyIso, RightHomologyData.rightHomologyIso,
  rightHomologyMapIso', Iso.refl]

Result:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{u_3, u_1} C
inst✝⁷ : Category.{u_4, u_2} D
inst✝⁶ : HasZeroMorphisms C
inst✝⁵ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
inst✝³ : S₁.HasRightHomology
inst✝² : S₂.HasRightHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ rightHomologyMap' (F.mapShortComplex.map φ) (F.mapShortComplex.obj S₁).rightHomologyData
        (F.mapShortComplex.obj S₂).rightHomologyData ≫
      rightHomologyMap' (𝟙 (S₂.map F)) (S₂.map F).rightHomologyData (S₂.rightHomologyData.map F) =
    rightHomologyMap' (𝟙 (S₁.map F)) (S₁.map F).rightHomologyData (S₁.rightHomologyData.map F) ≫
      F.map (rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData)
-- Mathlib/Data/Multiset/DershowitzManna.lean
private lemma isDershowitzMannaLT_of_oneStep : OneStep M N → IsDershowitzMannaLT M N

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
M N X Y : Multiset α
a : α
M_def : M = X + Y
N_def : N = X + {a}
ys_lt_a : ∀ y ∈ Y, y < a
⊢ M.IsDershowitzMannaLT N

Tactic:
use X, Y, {a}, by simp, M_def, N_def

Result:
case right
α : Type u_1
inst✝ : Preorder α
M N X Y : Multiset α
a : α
M_def : M = X + Y
N_def : N = X + {a}
ys_lt_a : ∀ y ∈ Y, y < a
⊢ ∀ y ∈ Y, ∃ z ∈ {a}, y < z

Proof state:
case right
α : Type u_1
inst✝ : Preorder α
M N X Y : Multiset α
a : α
M_def : M = X + Y
N_def : N = X + {a}
ys_lt_a : ∀ y ∈ Y, y < a
⊢ ∀ y ∈ Y, ∃ z ∈ {a}, y < z

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
M N X Y : Multiset α
a : α
M_def : M = X + Y
N_def : N = X + {a}
ys_lt_a : ∀ y ∈ Y, y < a
⊢ {a} ≠ ∅

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
M N : Multiset α
⊢ Multiset.OneStep M N → M.IsDershowitzMannaLT N

Tactic:
rintro ⟨X, Y, a, M_def, N_def, ys_lt_a⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
inst✝ : Preorder α
M N X Y : Multiset α
a : α
M_def : M = X + Y
N_def : N = X + {a}
ys_lt_a : ∀ y ∈ Y, y < a
⊢ M.IsDershowitzMannaLT N
-- Mathlib/Topology/UniformSpace/Completion.lean
theorem nonempty_cauchyFilter_iff : Nonempty (CauchyFilter α) ↔ Nonempty α

Proof state:
α : Type u
inst✝ : UniformSpace α
⊢ Nonempty (CauchyFilter α) ↔ Nonempty α

Tactic:
constructor <;> rintro ⟨c⟩

Result:
case mp.intro
α : Type u
inst✝ : UniformSpace α
c : CauchyFilter α
⊢ Nonempty α

case mpr.intro
α : Type u
inst✝ : UniformSpace α
c : α
⊢ Nonempty (CauchyFilter α)

Proof state:
case mpr.intro
α : Type u
inst✝ : UniformSpace α
c : α
⊢ Nonempty (CauchyFilter α)

Tactic:
exact ⟨pureCauchy c⟩

Result:
no goals

Proof state:
case mp.intro
α : Type u
inst✝ : UniformSpace α
c : CauchyFilter α
this : c ∈ closure (range pureCauchy)
⊢ Nonempty α

Tactic:
obtain ⟨_, ⟨_, a, _⟩⟩ := mem_closure_iff.1 this _ isOpen_univ trivial

Result:
case mp.intro.intro.intro.intro
α : Type u
inst✝ : UniformSpace α
c : CauchyFilter α
this : c ∈ closure (range pureCauchy)
w✝ : CauchyFilter α
left✝ : w✝ ∈ univ
a : α
h✝ : pureCauchy a = w✝
⊢ Nonempty α

Proof state:
case mp.intro
α : Type u
inst✝ : UniformSpace α
c : CauchyFilter α
⊢ Nonempty α

Tactic:
have := eq_univ_iff_forall.1 isDenseEmbedding_pureCauchy.isDenseInducing.closure_range c

Result:
case mp.intro
α : Type u
inst✝ : UniformSpace α
c : CauchyFilter α
this : c ∈ closure (range pureCauchy)
⊢ Nonempty α

Proof state:
case mp.intro.intro.intro.intro
α : Type u
inst✝ : UniformSpace α
c : CauchyFilter α
this : c ∈ closure (range pureCauchy)
w✝ : CauchyFilter α
left✝ : w✝ ∈ univ
a : α
h✝ : pureCauchy a = w✝
⊢ Nonempty α

Tactic:
exact ⟨a⟩

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma Y_eq_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : P y * Q z = Q y * P z

Proof state:
R : Type r
inst✝ : CommRing R
P Q : Fin 3 → R
h : P ≈ Q
⊢ P y * Q z = Q y * P z

Tactic:
rcases h with ⟨u, rfl⟩

Result:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ (fun m => m • Q) u y * Q z = Q y * (fun m => m • Q) u z

Proof state:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ (fun m => m • Q) u y * Q z = Q y * (fun m => m • Q) u z

Tactic:
simp only [Units.smul_def, smul_fin3_ext]

Result:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ ↑u * Q y * Q z = Q y * (↑u * Q z)

Proof state:
case intro
R : Type r
inst✝ : CommRing R
Q : Fin 3 → R
u : Rˣ
⊢ ↑u * Q y * Q z = Q y * (↑u * Q z)

Tactic:
ring1

Result:
no goals
-- Mathlib/Computability/Halting.lean
theorem sumCasesOn {f : α → β ⊕ γ} {g : α → β →. σ} {h : α → γ →. σ} (hf : Computable f)
    (hg : Partrec₂ g) (hh : Partrec₂ h) : @Partrec _ σ _ _ fun a => Sum.casesOn (f a) (g a) (h a) :=
  option_some_iff.1 <|
    (cond (sumCasesOn hf (const true).to₂ (const false).to₂)
          (sumCasesOn_left hf (option_some_iff.2 hg).to₂ (const Option.none).to₂)
          (sumCasesOn_right hf (const Option.none).to₂ (option_some_iff.2 hh).to₂)).of_eq
      fun a => by cases f a <;> simp only [Bool.cond_true, Bool.cond_false]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
f : α → β ⊕ γ
g : α → β →. σ
h : α → γ →. σ
hf : Computable f
hg : Partrec₂ g
hh : Partrec₂ h
a : α
⊢ (bif Sum.casesOn (f a) (fun b => true) fun b => false then
      Sum.casesOn (f a) (fun b => Part.map Option.some (g (a, b).1 (a, b).2)) fun c => Part.some Option.none
    else Sum.casesOn (f a) (fun b => Part.some Option.none) fun b => Part.map Option.some (h (a, b).1 (a, b).2)) =
    Part.map Option.some (Sum.casesOn (f a) (g a) (h a))

Tactic:
cases f a <;> simp only [Bool.cond_true, Bool.cond_false]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem ext_iff_isBase {M₁ M₂ : Matroid α} :
    M₁ = M₂ ↔ M₁.E = M₂.E ∧ ∀ ⦃B⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B) :=
  ⟨fun h ↦ by simp [h], fun ⟨hE, h⟩ ↦ ext_isBase hE h⟩

Proof state:
α : Type u_1
M₁ M₂ : Matroid α
h : M₁ = M₂
⊢ M₁.E = M₂.E ∧ ∀ ⦃B : Set α⦄, B ⊆ M₁.E → (M₁.IsBase B ↔ M₂.IsBase B)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
lemma measure_Iic_of_tendsto_atBot_atBot (hf : Tendsto f atBot atBot) (x : ℝ) :
    f.measure (Iic x) = ∞

Proof state:
f : StieltjesFunction
hf : Tendsto (↑f) atBot atBot
x : ℝ
r : ℝ≥0
⊢ ↑r ≤ f.measure (Iic x)

Tactic:
obtain ⟨N, hN⟩ := eventually_atBot.mp (tendsto_atBot.mp hf (f x - r))

Result:
case intro
f : StieltjesFunction
hf : Tendsto (↑f) atBot atBot
x : ℝ
r : ℝ≥0
N : ℝ
hN : ∀ b ≤ N, ↑f b ≤ ↑f x - ↑r
⊢ ↑r ≤ f.measure (Iic x)

Proof state:
f : StieltjesFunction
hf : Tendsto (↑f) atBot atBot
x : ℝ
⊢ f.measure (Iic x) = ⊤

Tactic:
refine ENNReal.eq_top_of_forall_nnreal_le fun r ↦ ?_

Result:
f : StieltjesFunction
hf : Tendsto (↑f) atBot atBot
x : ℝ
r : ℝ≥0
⊢ ↑r ≤ f.measure (Iic x)

Proof state:
case intro
f : StieltjesFunction
hf : Tendsto (↑f) atBot atBot
x : ℝ
r : ℝ≥0
N : ℝ
hN : ∀ b ≤ N, ↑f b ≤ ↑f x - ↑r
⊢ ↑r ≤ f.measure (Iic x)

Tactic:
exact (f.measure_Ioc (min x N) x ▸ ENNReal.coe_nnreal_eq r ▸ (ENNReal.ofReal_le_ofReal <|
  le_sub_comm.mp <| hN _ (min_le_right x N))).trans (measure_mono Ioc_subset_Iic_self)

Result:
no goals
-- Mathlib/Data/Set/Finite/Lattice.lean
theorem Finite.bddAbove_biUnion {I : Set β} {S : β → Set α} (H : I.Finite) :
    BddAbove (⋃ i ∈ I, S i) ↔ ∀ i ∈ I, BddAbove (S i) :=
  Finite.induction_on _ H (by simp only [biUnion_empty, bddAbove_empty, forall_mem_empty])
    fun _ _ hs => by simp only [biUnion_insert, forall_mem_insert, bddAbove_union, hs]

Proof state:
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : Nonempty α
I : Set β
S : β → Set α
H : I.Finite
a✝ : β
s✝ : Set β
x✝¹ : a✝ ∉ s✝
x✝ : s✝.Finite
hs : BddAbove (⋃ i ∈ s✝, S i) ↔ ∀ i ∈ s✝, BddAbove (S i)
⊢ BddAbove (⋃ i ∈ insert a✝ s✝, S i) ↔ ∀ i ∈ insert a✝ s✝, BddAbove (S i)

Tactic:
simp only [biUnion_insert, forall_mem_insert, bddAbove_union, hs]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : Nonempty α
I : Set β
S : β → Set α
H : I.Finite
⊢ BddAbove (⋃ i ∈ ∅, S i) ↔ ∀ i ∈ ∅, BddAbove (S i)

Tactic:
simp only [biUnion_empty, bddAbove_empty, forall_mem_empty]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem irreducible_mul_leadingCoeff_inv {p : K[X]} :
    Irreducible (p * C (leadingCoeff p)⁻¹) ↔ Irreducible p

Proof state:
case neg
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp0 : ¬p = 0
⊢ Irreducible (p * C p.leadingCoeff⁻¹) ↔ Irreducible p

Tactic:
exact irreducible_mul_isUnit
  (isUnit_C.mpr (IsUnit.mk0 _ (inv_ne_zero (leadingCoeff_ne_zero.mpr hp0))))

Result:
no goals

Proof state:
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
⊢ Irreducible (p * C p.leadingCoeff⁻¹) ↔ Irreducible p

Tactic:
by_cases hp0 : p = 0

Result:
case pos
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp0 : p = 0
⊢ Irreducible (p * C p.leadingCoeff⁻¹) ↔ Irreducible p

case neg
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp0 : ¬p = 0
⊢ Irreducible (p * C p.leadingCoeff⁻¹) ↔ Irreducible p

Proof state:
case pos
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp0 : p = 0
⊢ Irreducible (p * C p.leadingCoeff⁻¹) ↔ Irreducible p

Tactic:
simp [hp0]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
theorem separating_of_generateFrom (S : Set (Set α))
    [h : @SeparatesPoints α (generateFrom S)] :
    ∀ x y : α, (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y

Proof state:
α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
x y : α
hxy : ∀ s ∈ S, x ∈ s ↔ y ∈ s
⊢ x = y

Tactic:
rw [← forall_generateFrom_mem_iff_mem_iff] at hxy

Result:
α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
x y : α
hxy : ∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)
⊢ x = y

Proof state:
α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
⊢ ∀ (x y : α), (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y

Tactic:
intros x y hxy

Result:
α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
x y : α
hxy : ∀ s ∈ S, x ∈ s ↔ y ∈ s
⊢ x = y

Proof state:
α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
⊢ ∀ (x y : α), (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y

Tactic:
letI := generateFrom S

Result:
α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
⊢ ∀ (x y : α), (∀ s ∈ S, x ∈ s ↔ y ∈ s) → x = y

Proof state:
α : Type u_1
S : Set (Set α)
h : SeparatesPoints α
this : MeasurableSpace α := generateFrom S
x y : α
hxy : ∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)
⊢ x = y

Tactic:
exact separatesPoints_def <| fun _ hs ↦ (hxy _ hs).mp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/End.lean
theorem obj_ε_app (n : M) (X : C) [F.Monoidal]:
    (F.obj n).map ((ε F).app X) = (F.map (λ_ n).inv).app X ≫ (δ F (𝟙_ M) n).app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj n).map ((ε F).app X) = (F.map (λ_ n).inv).app X ≫ (δ F (𝟙_ M) n).app X

Tactic:
rw [map_leftUnitor_inv]

Result:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj n).map ((ε F).app X) = ((λ_ (F.obj n)).inv ≫ ε F ▷ F.obj n ≫ μ F (𝟙_ M) n).app X ≫ (δ F (𝟙_ M) n).app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj n).map ((ε F).app X) =
    (𝟙 ((F.obj n).obj X) ≫ (F.obj n).map ((ε F).app X) ≫ (μ F (𝟙_ M) n).app X) ≫ (δ F (𝟙_ M) n).app X

Tactic:
simp only [Category.id_comp, Category.assoc, μ_δ_app, endofunctorMonoidalCategory_tensorObj_obj,
  Category.comp_id]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj n).map ((ε F).app X) = ((λ_ (F.obj n)).inv ≫ ε F ▷ F.obj n ≫ μ F (𝟙_ M) n).app X ≫ (δ F (𝟙_ M) n).app X

Tactic:
dsimp

Result:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
n : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj n).map ((ε F).app X) =
    (𝟙 ((F.obj n).obj X) ≫ (F.obj n).map ((ε F).app X) ≫ (μ F (𝟙_ M) n).app X) ≫ (δ F (𝟙_ M) n).app X
-- Mathlib/RingTheory/TensorProduct/MvPolynomial.lean
@[simp]
lemma coeff_rTensorAlgHom_tmul
    (p : MvPolynomial σ S) (n : N) (d : σ →₀ ℕ) :
    coeff d (rTensorAlgHom (p ⊗ₜ[R] n)) = (coeff d p) ⊗ₜ[R] n

Proof state:
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ 1 ⊗ₜ[R] n * coeff d ((mapAlgHom Algebra.TensorProduct.includeLeft) p) = coeff d p ⊗ₜ[R] n

Tactic:
simp [mapAlgHom, coeff_map]

Result:
no goals

Proof state:
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ coeff d
      ((mapAlgHom Algebra.TensorProduct.includeLeft) p *
        ((IsScalarTower.toAlgHom R (S ⊗[R] N) (MvPolynomial σ (S ⊗[R] N))).comp Algebra.TensorProduct.includeRight) n) =
    coeff d p ⊗ₜ[R] n

Tactic:
rw [AlgHom.coe_comp, IsScalarTower.coe_toAlgHom', Function.comp_apply,
  Algebra.TensorProduct.includeRight_apply]

Result:
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ coeff d
      ((mapAlgHom Algebra.TensorProduct.includeLeft) p *
        (algebraMap (S ⊗[R] N) (MvPolynomial σ (S ⊗[R] N))) (1 ⊗ₜ[R] n)) =
    coeff d p ⊗ₜ[R] n

Proof state:
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ coeff d (rTensorAlgHom (p ⊗ₜ[R] n)) = coeff d p ⊗ₜ[R] n

Tactic:
rw [rTensorAlgHom, Algebra.TensorProduct.lift_tmul]

Result:
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ coeff d
      ((mapAlgHom Algebra.TensorProduct.includeLeft) p *
        ((IsScalarTower.toAlgHom R (S ⊗[R] N) (MvPolynomial σ (S ⊗[R] N))).comp Algebra.TensorProduct.includeRight) n) =
    coeff d p ⊗ₜ[R] n

Proof state:
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ coeff d
      ((mapAlgHom Algebra.TensorProduct.includeLeft) p *
        (algebraMap (S ⊗[R] N) (MvPolynomial σ (S ⊗[R] N))) (1 ⊗ₜ[R] n)) =
    coeff d p ⊗ₜ[R] n

Tactic:
rw [algebraMap_eq, mul_comm, coeff_C_mul]

Result:
R : Type u
N : Type v
inst✝⁴ : CommSemiring R
σ : Type u_1
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ 1 ⊗ₜ[R] n * coeff d ((mapAlgHom Algebra.TensorProduct.includeLeft) p) = coeff d p ⊗ₜ[R] n
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem BlockTriangular.add [AddZeroClass R] (hM : BlockTriangular M b) (hN : BlockTriangular N b) :
    BlockTriangular (M + N) b := fun i j h => by simp_rw [Matrix.add_apply, hM h, hN h, zero_add]

Proof state:
α : Type u_1
m : Type u_3
R : Type v
M N : Matrix m m R
b : m → α
inst✝¹ : LT α
inst✝ : AddZeroClass R
hM : M.BlockTriangular b
hN : N.BlockTriangular b
i j : m
h : b j < b i
⊢ (M + N) i j = 0

Tactic:
simp_rw [Matrix.add_apply, hM h, hN h, zero_add]

Result:
no goals
-- Mathlib/Order/Iterate.lean
theorem seq_le_seq (hf : Monotone f) (n : ℕ) (h₀ : x 0 ≤ y 0) (hx : ∀ k < n, x (k + 1) ≤ f (x k))
    (hy : ∀ k < n, f (y k) ≤ y (k + 1)) : x n ≤ y n

Proof state:
case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ x (n + 1) ≤ y (n + 1)

Tactic:
refine (hx _ n.lt_succ_self).trans ((hf <| ihn ?_ ?_).trans (hy _ n.lt_succ_self))

Result:
case succ.refine_1
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)

case succ.refine_2
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)

Proof state:
case zero
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
hx : ∀ (k : ℕ), k < 0 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)
⊢ x 0 ≤ y 0

Tactic:
exact h₀

Result:
no goals

Proof state:
case succ.refine_2
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)

Tactic:
exact fun k hk => hy _ (hk.trans n.lt_succ_self)

Result:
no goals

Proof state:
case succ.refine_1
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : (∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)

Tactic:
exact fun k hk => hx _ (hk.trans n.lt_succ_self)

Result:
no goals