harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/Fixed.lean
theorem monic : (minpoly G F x).Monic

Proof state:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
⊢ ((prodXSubSMul G F x).toSubring (subfield G F).toSubring ⋯).Monic

Tactic:
rw [Polynomial.monic_toSubring]

Result:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
⊢ (prodXSubSMul G F x).Monic

Proof state:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
⊢ (minpoly G F x).Monic

Tactic:
simp only [minpoly]

Result:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
⊢ ((prodXSubSMul G F x).toSubring (subfield G F).toSubring ⋯).Monic

Proof state:
G : Type u
inst✝³ : Group G
F : Type v
inst✝² : Field F
inst✝¹ : MulSemiringAction G F
inst✝ : Fintype G
x : F
⊢ (prodXSubSMul G F x).Monic

Tactic:
exact prodXSubSMul.monic G F x

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem symmDiff_triangle : a ∆ c ≤ a ∆ b ⊔ b ∆ c

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ c

Tactic:
rw [sup_comm (c \ b), sup_sup_sup_comm, symmDiff, symmDiff]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a ∆ c ≤ a ∆ b ⊔ b ∆ c

Tactic:
refine (sup_le_sup (sdiff_triangle a b c) <| sdiff_triangle _ b _).trans_eq ?_

Result:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b c : α
⊢ a \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ c
-- Mathlib/CategoryTheory/Abelian/LeftDerived.lean
/-- A component of the natural transformation between left-derived functors can be computed
using a chosen projective resolution. -/
lemma leftDerived_app_eq
    {F G : C ⥤ D} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : ProjectiveResolution X)
    (n : ℕ) : (NatTrans.leftDerived α n).app X =
      (P.isoLeftDerivedObj F n).hom ≫
        (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
        ((NatTrans.mapHomologicalComplex α _).app P.complex) ≫
        (P.isoLeftDerivedObj G n).inv

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
n : ℕ
⊢ (NatTrans.leftDerived α n).app X =
    (P.isoLeftDerivedObj F n).hom ≫
      (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) ≫
        (P.isoLeftDerivedObj G n).inv

Tactic:
dsimp [NatTrans.leftDerived, isoLeftDerivedObj]

Result:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{u_2, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
n : ℕ
⊢ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map ((NatTrans.leftDerivedToHomotopyCategory α).app X) =
    ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) ≫
      HomologicalComplex.homologyMap ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) n ≫
        (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).inv.app
            ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫
          (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj G).inv
-- Mathlib/Algebra/Squarefree/Basic.lean
theorem squarefree_natCast {n : ℕ} : Squarefree (n : ℤ) ↔ Squarefree n

Proof state:
n : ℕ
⊢ Squarefree ↑n ↔ Squarefree n

Tactic:
rw [← squarefree_natAbs, natAbs_ofNat]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
lemma iSup_add [Nonempty ι] (f : ι → ℝ≥0∞) : (⨆ i, f i) + a = ⨆ i, f i + a

Proof state:
ι : Sort u_1
a : ℝ≥0∞
inst✝ : Nonempty ι
f : ι → ℝ≥0∞
⊢ (⨆ i, f i) + a = ⨆ i, f i + a

Tactic:
simp [add_comm, add_iSup]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem L1.norm_of_fun_eq_integral_norm {f : α → H} (hf : Integrable f μ) :
    ‖hf.toL1 f‖ = ∫ a, ‖f a‖ ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_7
inst✝ : NormedAddCommGroup H
f : α → H
hf : Integrable f μ
⊢ ∫ (a : α), ‖↑↑(Integrable.toL1 f hf) a‖ ∂μ = ∫ (a : α), ‖f a‖ ∂μ

Tactic:
exact integral_congr_ae <| hf.coeFn_toL1.fun_comp _

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_7
inst✝ : NormedAddCommGroup H
f : α → H
hf : Integrable f μ
⊢ ‖Integrable.toL1 f hf‖ = ∫ (a : α), ‖f a‖ ∂μ

Tactic:
rw [L1.norm_eq_integral_norm]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
H : Type u_7
inst✝ : NormedAddCommGroup H
f : α → H
hf : Integrable f μ
⊢ ∫ (a : α), ‖↑↑(Integrable.toL1 f hf) a‖ ∂μ = ∫ (a : α), ‖f a‖ ∂μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem eq_ofNat_of_zero_le {a : Int} (h : 0 ≤ a) : ∃ n : Nat, a = n

Proof state:
a : Int
h : 0 ≤ a
t : ∃ n, a - 0 = ↑n
⊢ ∃ n, a = ↑n

Tactic:
rwa [Int.sub_zero] at t

Result:
no goals

Proof state:
a : Int
h : 0 ≤ a
⊢ ∃ n, a = ↑n

Tactic:
have t := le.dest_sub h

Result:
a : Int
h : 0 ≤ a
t : ∃ n, a - 0 = ↑n
⊢ ∃ n, a = ↑n
-- Mathlib/Data/List/Rotate.lean
theorem rotate_eq_self_iff_eq_replicate [hα : Nonempty α] :
    ∀ {l : List α}, (∀ n, l.rotate n = l) ↔ ∃ a, l = replicate l.length a
  | [] => by simp
  | a :: l => ⟨fun h => ⟨a, ext_getElem (length_replicate _ _).symm fun n h₁ h₂ => by
      rw [getElem_replicate, ← Option.some_inj, ← getElem?_eq_getElem, ← head?_rotate h₁, h,
        head?_cons]⟩,
    fun ⟨b, hb⟩ n => by rw [hb, rotate_replicate]⟩

Proof state:
α : Type u
hα : Nonempty α
a : α
l : List α
h : ∀ (n : ℕ), (a :: l).rotate n = a :: l
n : ℕ
h₁ : n < (a :: l).length
h₂ : n < (replicate (a :: l).length a).length
⊢ (a :: l)[n] = (replicate (a :: l).length a)[n]

Tactic:
rw [getElem_replicate, ← Option.some_inj, ← getElem?_eq_getElem, ← head?_rotate h₁, h,
  head?_cons]

Result:
no goals

Proof state:
α : Type u
hα : Nonempty α
a : α
l : List α
x✝ : ∃ a_1, a :: l = replicate (a :: l).length a_1
n : ℕ
b : α
hb : a :: l = replicate (a :: l).length b
⊢ (a :: l).rotate n = a :: l

Tactic:
rw [hb, rotate_replicate]

Result:
no goals

Proof state:
α : Type u
hα : Nonempty α
⊢ (∀ (n : ℕ), [].rotate n = []) ↔ ∃ a, [] = replicate [].length a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/Interval.lean
theorem uIcc_eq :
    uIcc s t =
      (uIcc (toDFinsupp s) (toDFinsupp t)).map Multiset.equivDFinsupp.toEquiv.symm.toEmbedding :=
  (Icc_eq _ _).trans <| by simp [uIcc]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ Finset.map equivDFinsupp.symm.toEmbedding (Finset.Icc (toDFinsupp (s ⊓ t)) (toDFinsupp (s ⊔ t))) =
    Finset.map equivDFinsupp.symm.toEmbedding (uIcc (toDFinsupp s) (toDFinsupp t))

Tactic:
simp [uIcc]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_le_one_iff_val_nonneg (x : ℚ_[p]) : ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation

Tactic:
by_cases hx : x = 0

Result:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x = 0
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation

case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬x = 0
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬x = 0
⊢ 1 < ↑p

Tactic:
exact Nat.one_lt_cast.2 (Nat.Prime.one_lt' p).1

Result:
no goals

Proof state:
case pos
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : x = 0
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation

Tactic:
simp only [hx, norm_zero, valuation_zero, zero_le_one, le_refl]

Result:
no goals

Proof state:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬x = 0
⊢ ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation

Tactic:
rw [norm_eq_zpow_neg_valuation hx, ← zpow_zero (p : ℝ), zpow_le_zpow_iff_right₀, neg_nonpos]

Result:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
x : ℚ_[p]
hx : ¬x = 0
⊢ 1 < ↑p
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_le_succ_sub (a i : Nat) : a - i ≤ a.succ - i

Proof state:
case zero
a : Nat
⊢ a - 0 ≤ a.succ - 0

Tactic:
apply Nat.le_of_lt

Result:
case zero.a
a : Nat
⊢ a - 0 < a.succ - 0

Proof state:
case succ
a i : Nat
⊢ (a - i).pred ≤ a - i

Tactic:
apply Nat.pred_le

Result:
no goals

Proof state:
case zero.a
a : Nat
⊢ a - 0 < a.succ - 0

Tactic:
apply Nat.lt_succ_self

Result:
no goals

Proof state:
case succ
a i : Nat
⊢ a - (i + 1) ≤ a.succ - (i + 1)

Tactic:
rw [Nat.sub_succ, Nat.succ_sub_succ]

Result:
case succ
a i : Nat
⊢ (a - i).pred ≤ a - i

Proof state:
a i : Nat
⊢ a - i ≤ a.succ - i

Tactic:
cases i with
| zero => apply Nat.le_of_lt; apply Nat.lt_succ_self
| succ i => rw [Nat.sub_succ, Nat.succ_sub_succ]; apply Nat.pred_le

Result:
no goals
-- Mathlib/Algebra/BigOperators/Module.lean
theorem sum_range_by_parts :
    ∑ i ∈ range n, f i • g i =
      f (n - 1) • G n - ∑ i ∈ range (n - 1), (f (i + 1) - f i) • G (i + 1)

Proof state:
case neg
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : ¬n = 0
⊢ ∑ i ∈ range n, f i • g i =
    f (n - 1) • ∑ i ∈ range n, g i - ∑ i ∈ range (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Tactic:
rw [range_eq_Ico, sum_Ico_by_parts f g (Nat.pos_of_ne_zero hn), sum_range_zero, smul_zero,
  sub_zero, range_eq_Ico]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
⊢ ∑ i ∈ range n, f i • g i =
    f (n - 1) • ∑ i ∈ range n, g i - ∑ i ∈ range (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Tactic:
by_cases hn : n = 0

Result:
case pos
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : n = 0
⊢ ∑ i ∈ range n, f i • g i =
    f (n - 1) • ∑ i ∈ range n, g i - ∑ i ∈ range (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

case neg
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : ¬n = 0
⊢ ∑ i ∈ range n, f i • g i =
    f (n - 1) • ∑ i ∈ range n, g i - ∑ i ∈ range (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Proof state:
case pos
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ℕ → R
g : ℕ → M
n : ℕ
hn : n = 0
⊢ ∑ i ∈ range n, f i • g i =
    f (n - 1) • ∑ i ∈ range n, g i - ∑ i ∈ range (n - 1), (f (i + 1) - f i) • ∑ i ∈ range (i + 1), g i

Tactic:
simp [hn]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean
theorem superpolynomialDecay_zero (l : Filter α) (k : α → β) : SuperpolynomialDecay l k 0 :=
  fun z => by simpa only [Pi.zero_apply, mul_zero] using tendsto_const_nhds

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
l : Filter α
k : α → β
z : ℕ
⊢ Tendsto (fun a => k a ^ z * 0 a) l (𝓝 0)

Tactic:
simpa only [Pi.zero_apply, mul_zero] using tendsto_const_nhds

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem bne_false : ∀(b : Bool), (b != false) =  b

Proof state:
⊢ ∀ (b : Bool), (b != false) = b

Tactic:
decide

Result:
no goals
-- Mathlib/Probability/Density.lean
theorem measurable_pdf {m : MeasurableSpace Ω} (X : Ω → E) (ℙ : Measure Ω)
    (μ : Measure E

Proof state:
Ω : Type u_1
E : Type u_2
inst✝ : MeasurableSpace E
m : MeasurableSpace Ω
X : Ω → E
ℙ : Measure Ω
μ : autoParam (Measure E) _auto✝
⊢ Measurable (pdf X ℙ μ)

Tactic:
exact measurable_rnDeriv _ _

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem coe_det [DecidableEq M] :
    ⇑(LinearMap.det : (M →ₗ[A] M) →* A) =
      if H : ∃ s : Finset M, Nonempty (Basis s A M) then
        LinearMap.detAux (Trunc.mk H.choose_spec.some)
      else 1

Proof state:
case neg
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
x✝ : M →ₗ[A] M
h✝ : ¬∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ 1 x✝ = 1 x✝

Tactic:
rfl

Result:
no goals

Proof state:
case pos
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
x✝ : M →ₗ[A] M
h✝ : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ (detAux (Trunc.mk ⋯.some)) x✝ = (detAux (Trunc.mk ⋯.some)) x✝

Tactic:
congr

Result:
no goals

Proof state:
case h
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
x✝ : M →ₗ[A] M
⊢ LinearMap.det x✝ = (if H : ∃ s, Nonempty (Basis { x // x ∈ s } A M) then detAux (Trunc.mk ⋯.some) else 1) x✝

Tactic:
rw [LinearMap.det_def]

Result:
case h
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
x✝ : M →ₗ[A] M
⊢ (if H : ∃ s, Nonempty (Basis { x // x ∈ s } A M) then detAux (Trunc.mk ⋯.some) else 1) x✝ =
    (if H : ∃ s, Nonempty (Basis { x // x ∈ s } A M) then detAux (Trunc.mk ⋯.some) else 1) x✝

Proof state:
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
⊢ ⇑LinearMap.det = ⇑(if H : ∃ s, Nonempty (Basis { x // x ∈ s } A M) then detAux (Trunc.mk ⋯.some) else 1)

Tactic:
ext

Result:
case h
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
x✝ : M →ₗ[A] M
⊢ LinearMap.det x✝ = (if H : ∃ s, Nonempty (Basis { x // x ∈ s } A M) then detAux (Trunc.mk ⋯.some) else 1) x✝

Proof state:
case h
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
x✝ : M →ₗ[A] M
⊢ (if H : ∃ s, Nonempty (Basis { x // x ∈ s } A M) then detAux (Trunc.mk ⋯.some) else 1) x✝ =
    (if H : ∃ s, Nonempty (Basis { x // x ∈ s } A M) then detAux (Trunc.mk ⋯.some) else 1) x✝

Tactic:
split_ifs

Result:
case pos
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
x✝ : M →ₗ[A] M
h✝ : ∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ (detAux (Trunc.mk ⋯.some)) x✝ = (detAux (Trunc.mk ⋯.some)) x✝

case neg
M : Type u_2
inst✝³ : AddCommGroup M
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : DecidableEq M
x✝ : M →ₗ[A] M
h✝ : ¬∃ s, Nonempty (Basis { x // x ∈ s } A M)
⊢ 1 x✝ = 1 x✝
-- Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
@[reassoc]
lemma extendScalars_comp_id :
    (extendScalarsComp f₁₂ (RingHom.id R₂)).hom ≫ whiskerLeft _ (extendScalarsId R₂).hom ≫
      (Functor.rightUnitor _).hom = 𝟙 _

Proof state:
case w.h.h
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ (Hom.hom ((extendScalarsId R₂).hom.app ((extendScalars f₁₂).obj M)))
      ((Hom.hom ((extendScalarsComp f₁₂ (RingHom.id R₂)).hom.app M)) (1 ⊗ₜ[R₁] m)) =
    LinearMap.id (1 ⊗ₜ[R₁] m)

Tactic:
erw [extendScalarsComp_hom_app_one_tmul f₁₂ (RingHom.id R₂) M m,
  extendScalarsId_hom_app_one_tmul]

Result:
case w.h.h
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ 1 ⊗ₜ[R₁] m = LinearMap.id (1 ⊗ₜ[R₁] m)

Proof state:
case w.h.h
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ (ConcreteCategory.hom
        (((extendScalarsComp f₁₂ (RingHom.id R₂)).hom ≫
              whiskerLeft (extendScalars f₁₂) (extendScalarsId R₂).hom ≫ (extendScalars f₁₂).rightUnitor.hom).app
          M))
      (1 ⊗ₜ[R₁] m) =
    (ConcreteCategory.hom ((𝟙 (extendScalars ((RingHom.id R₂).comp f₁₂))).app M)) (1 ⊗ₜ[R₁] m)

Tactic:
dsimp

Result:
case w.h.h
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ (Hom.hom ((extendScalarsId R₂).hom.app ((extendScalars f₁₂).obj M)))
      ((Hom.hom ((extendScalarsComp f₁₂ (RingHom.id R₂)).hom.app M)) (1 ⊗ₜ[R₁] m)) =
    LinearMap.id (1 ⊗ₜ[R₁] m)

Proof state:
case w.h.h
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ 1 ⊗ₜ[R₁] m = LinearMap.id (1 ⊗ₜ[R₁] m)

Tactic:
rfl

Result:
no goals

Proof state:
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
⊢ (extendScalarsComp f₁₂ (RingHom.id R₂)).hom ≫
      whiskerLeft (extendScalars f₁₂) (extendScalarsId R₂).hom ≫ (extendScalars f₁₂).rightUnitor.hom =
    𝟙 (extendScalars ((RingHom.id R₂).comp f₁₂))

Tactic:
ext M m

Result:
case w.h.h
R₁ R₂ : Type u₁
inst✝¹ : CommRing R₁
inst✝ : CommRing R₂
f₁₂ : R₁ →+* R₂
M : ModuleCat R₁
m : ↑M
⊢ (ConcreteCategory.hom
        (((extendScalarsComp f₁₂ (RingHom.id R₂)).hom ≫
              whiskerLeft (extendScalars f₁₂) (extendScalarsId R₂).hom ≫ (extendScalars f₁₂).rightUnitor.hom).app
          M))
      (1 ⊗ₜ[R₁] m) =
    (ConcreteCategory.hom ((𝟙 (extendScalars ((RingHom.id R₂).comp f₁₂))).app M)) (1 ⊗ₜ[R₁] m)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mul_mod_left (m n : Nat) : (m * n) % n = 0

Proof state:
m n : Nat
⊢ m * n % n = 0

Tactic:
rw [Nat.mul_comm, mul_mod_right]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem zpow_add_of_nonneg {A : M} {m n : ℤ} (hm : 0 ≤ m) (hn : 0 ≤ n) :
    A ^ (m + n) = A ^ m * A ^ n

Proof state:
case intro.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
k : ℕ
hm : 0 ≤ ↑k
l : ℕ
hn : 0 ≤ ↑l
⊢ A ^ (↑k + ↑l) = A ^ ↑k * A ^ ↑l

Tactic:
rw [← Int.ofNat_add, zpow_natCast, zpow_natCast, zpow_natCast, pow_add]

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
m n : ℤ
hm : 0 ≤ m
hn : 0 ≤ n
⊢ A ^ (m + n) = A ^ m * A ^ n

Tactic:
obtain ⟨k, rfl⟩ := eq_ofNat_of_zero_le hm

Result:
case intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
hn : 0 ≤ n
k : ℕ
hm : 0 ≤ ↑k
⊢ A ^ (↑k + n) = A ^ ↑k * A ^ n

Proof state:
case intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
n : ℤ
hn : 0 ≤ n
k : ℕ
hm : 0 ≤ ↑k
⊢ A ^ (↑k + n) = A ^ ↑k * A ^ n

Tactic:
obtain ⟨l, rfl⟩ := eq_ofNat_of_zero_le hn

Result:
case intro.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
k : ℕ
hm : 0 ≤ ↑k
l : ℕ
hn : 0 ≤ ↑l
⊢ A ^ (↑k + ↑l) = A ^ ↑k * A ^ ↑l
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_iSup_le_lift_iSup {ι : Type v} {ι' : Type v'} {f : ι → Cardinal.{w}}
    {f' : ι' → Cardinal.{w'}} (hf : BddAbove (range f)) (hf' : BddAbove (range f')) {g : ι → ι'}
    (h : ∀ i, lift.{w'} (f i) ≤ lift.{w} (f' (g i))) : lift.{w'} (iSup f) ≤ lift.{w} (iSup f')

Proof state:
ι : Type v
ι' : Type v'
f : ι → Cardinal.{w}
f' : ι' → Cardinal.{w'}
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift.{w', w} (f i) ≤ lift.{w, w'} (f' (g i))
⊢ lift.{w', w} (iSup f) ≤ lift.{w, w'} (iSup f')

Tactic:
rw [lift_iSup hf, lift_iSup hf']

Result:
ι : Type v
ι' : Type v'
f : ι → Cardinal.{w}
f' : ι' → Cardinal.{w'}
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift.{w', w} (f i) ≤ lift.{w, w'} (f' (g i))
⊢ ⨆ i, lift.{w', w} (f i) ≤ ⨆ i, lift.{w, w'} (f' i)

Proof state:
ι : Type v
ι' : Type v'
f : ι → Cardinal.{w}
f' : ι' → Cardinal.{w'}
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift.{w', w} (f i) ≤ lift.{w, w'} (f' (g i))
⊢ ⨆ i, lift.{w', w} (f i) ≤ ⨆ i, lift.{w, w'} (f' i)

Tactic:
exact ciSup_mono' (bddAbove_range_comp.{_,_,w} hf' _) fun i => ⟨_, h i⟩

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem rightCoset_one : op (1 : α) • s = s :=
  Set.ext <| by simp [← image_smul]

Proof state:
α : Type u_1
inst✝ : Monoid α
s : Set α
⊢ ∀ (x : α), x ∈ op 1 • s ↔ x ∈ s

Tactic:
simp [← image_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem merge_perm_append : ∀ {xs ys : List α}, merge xs ys le ~ xs ++ ys
  | [], ys => by simp [merge]
  | xs, [] => by simp [merge]
  | x :: xs, y :: ys => by
    simp only [merge]
    split
    · exact merge_perm_append.cons x
    · exact (merge_perm_append.cons y).trans
        ((Perm.swap x y _).trans (perm_middle.symm.cons x))

Proof state:
α : Type u_1
le : α → α → Bool
x : α
xs : List α
y : α
ys : List α
⊢ (x :: xs).merge (y :: ys) le ~ x :: xs ++ y :: ys

Tactic:
simp only [merge]

Result:
α : Type u_1
le : α → α → Bool
x : α
xs : List α
y : α
ys : List α
⊢ (if le x y = true then x :: xs.merge (y :: ys) le else y :: (x :: xs).merge ys le) ~ x :: xs ++ y :: ys

Proof state:
case isFalse
α : Type u_1
le : α → α → Bool
x : α
xs : List α
y : α
ys : List α
h✝ : ¬le x y = true
⊢ y :: (x :: xs).merge ys le ~ x :: xs ++ y :: ys

Tactic:
exact (merge_perm_append.cons y).trans
  ((Perm.swap x y _).trans (perm_middle.symm.cons x))

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
ys : List α
⊢ [].merge ys le ~ [] ++ ys

Tactic:
simp [merge]

Result:
no goals

Proof state:
case isTrue
α : Type u_1
le : α → α → Bool
x : α
xs : List α
y : α
ys : List α
h✝ : le x y = true
⊢ x :: xs.merge (y :: ys) le ~ x :: xs ++ y :: ys

Tactic:
exact merge_perm_append.cons x

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
x : α
xs : List α
y : α
ys : List α
⊢ (if le x y = true then x :: xs.merge (y :: ys) le else y :: (x :: xs).merge ys le) ~ x :: xs ++ y :: ys

Tactic:
split

Result:
case isTrue
α : Type u_1
le : α → α → Bool
x : α
xs : List α
y : α
ys : List α
h✝ : le x y = true
⊢ x :: xs.merge (y :: ys) le ~ x :: xs ++ y :: ys

case isFalse
α : Type u_1
le : α → α → Bool
x : α
xs : List α
y : α
ys : List α
h✝ : ¬le x y = true
⊢ y :: (x :: xs).merge ys le ~ x :: xs ++ y :: ys

Proof state:
α : Type u_1
le : α → α → Bool
xs : List α
⊢ xs.merge [] le ~ xs ++ []

Tactic:
simp [merge]

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEMeasurableSequence.lean
theorem fun_prop_of_mem_aeSeqSet (hf : ∀ i, AEMeasurable (f i) μ) {x : α} (hx : x ∈ aeSeqSet hf p) :
    p x fun n => f n x

Proof state:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
h_eq : (fun n => f n x) = fun n => aeSeq hf p n x
⊢ p x fun n => aeSeq hf p n x

Tactic:
exact prop_of_mem_aeSeqSet hf hx

Result:
no goals

Proof state:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
h_eq : (fun n => f n x) = fun n => aeSeq hf p n x
⊢ p x fun n => f n x

Tactic:
rw [h_eq]

Result:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
h_eq : (fun n => f n x) = fun n => aeSeq hf p n x
⊢ p x fun n => aeSeq hf p n x

Proof state:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
⊢ p x fun n => f n x

Tactic:
have h_eq : (fun n => f n x) = fun n => aeSeq hf p n x :=
  funext fun n => (aeSeq_eq_fun_of_mem_aeSeqSet hf hx n).symm

Result:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
h_eq : (fun n => f n x) = fun n => aeSeq hf p n x
⊢ p x fun n => f n x
-- Mathlib/RingTheory/Algebraic/Integral.lean
protected lemma neg : IsAlgebraic R (-a) :=
  have ⟨p, h, eval0⟩ := ha
  ⟨algEquivAevalNegX p, EmbeddingLike.map_ne_zero_iff.mpr h, by simpa [← comp_eq_aeval, aeval_comp]⟩

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
a : S
ha : IsAlgebraic R a
p : R[X]
h : p ≠ 0
eval0 : (aeval a) p = 0
⊢ (aeval (-a)) (algEquivAevalNegX p) = 0

Tactic:
simpa [← comp_eq_aeval, aeval_comp]

Result:
no goals