harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_map_of_stronglyMeasurable {β} [MeasurableSpace β] {φ : α → β} (hφ : Measurable φ)
    {f : β → G} (hfm : StronglyMeasurable f) : ∫ y, f y ∂Measure.map φ μ = ∫ x, f (φ x) ∂μ

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : CompleteSpace G
⊢ ∫ (y : β), f y ∂Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ

case neg
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : ¬CompleteSpace G
⊢ ∫ (y : β), f y ∂Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ

Tactic:
swap

Result:
case neg
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : ¬CompleteSpace G
⊢ ∫ (y : β), f y ∂Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ

case pos
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : CompleteSpace G
⊢ ∫ (y : β), f y ∂Measure.map φ μ = ∫ (x : α), f (φ x) ∂μ

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : CompleteSpace G
hfi : Integrable f (Measure.map φ μ)
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(range f ∪ {0})
⊢ Tendsto (fun n => SimpleFunc.integral (Measure.map φ μ) (approxOn f ⋯ (range f ∪ {0}) 0 ⋯ n)) atTop
    (𝓝 (∫ (x : α), f (φ x) ∂μ))

Tactic:
convert tendsto_integral_approxOn_of_measurable_of_range_subset (hfm.measurable.comp hφ)
  ((integrable_map_measure hfm.aestronglyMeasurable hφ.aemeasurable).1 hfi) (range f ∪ {0})
  (union_subset_union_left {0} (range_comp_subset_range φ f)) using 1

Result:
case h.e'_3
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hG : CompleteSpace G
hfi : Integrable f (Measure.map φ μ)
this✝¹ : MeasurableSpace G := borel G
this✝ : BorelSpace G
this : SeparableSpace ↑(range f ∪ {0})
⊢ (fun n => SimpleFunc.integral (Measure.map φ μ) (approxOn f ⋯ (range f ∪ {0}) 0 ⋯ n)) = fun n =>
    SimpleFunc.integral μ (approxOn (f ∘ φ) ⋯ (range f ∪ {0}) 0 ⋯ n)
-- Mathlib/Topology/DiscreteSubset.lean
/-- If a set is codiscrete within `U`, then it is codiscrete within any subset of `U`. -/
lemma Filter.codiscreteWithin.mono {U₁ U : Set X} (hU : U₁ ⊆ U) :
   codiscreteWithin U₁ ≤ codiscreteWithin U

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
s : Set X
x : X
hx : x ∈ U₁
hs : (U \ s)ᶜ ∈ 𝓝[≠] x
⊢ U₁ \ s ⊆ U \ s

Tactic:
exact diff_subset_diff_left hU

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
s : Set X
hs : ∀ x ∈ U, (U \ s)ᶜ ∈ 𝓝[≠] x
x : X
hx : x ∈ U₁
⊢ (U₁ \ s)ᶜ ∈ 𝓝[≠] x

Tactic:
specialize hs x (hU hx)

Result:
X : Type u_1
inst✝ : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
s : Set X
x : X
hx : x ∈ U₁
hs : (U \ s)ᶜ ∈ 𝓝[≠] x
⊢ (U₁ \ s)ᶜ ∈ 𝓝[≠] x

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
s : Set X
hs : ∀ x ∈ U, (U \ s)ᶜ ∈ 𝓝[≠] x
⊢ ∀ x ∈ U₁, (U₁ \ s)ᶜ ∈ 𝓝[≠] x

Tactic:
intro x hx

Result:
X : Type u_1
inst✝ : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
s : Set X
hs : ∀ x ∈ U, (U \ s)ᶜ ∈ 𝓝[≠] x
x : X
hx : x ∈ U₁
⊢ (U₁ \ s)ᶜ ∈ 𝓝[≠] x

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
s : Set X
x : X
hx : x ∈ U₁
hs : (U \ s)ᶜ ∈ 𝓝[≠] x
⊢ (U \ s)ᶜ ⊆ (U₁ \ s)ᶜ

Tactic:
rw [Set.compl_subset_compl]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
s : Set X
x : X
hx : x ∈ U₁
hs : (U \ s)ᶜ ∈ 𝓝[≠] x
⊢ U₁ \ s ⊆ U \ s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
s : Set X
x : X
hx : x ∈ U₁
hs : (U \ s)ᶜ ∈ 𝓝[≠] x
⊢ (U₁ \ s)ᶜ ∈ 𝓝[≠] x

Tactic:
apply mem_of_superset hs

Result:
X : Type u_1
inst✝ : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
s : Set X
x : X
hx : x ∈ U₁
hs : (U \ s)ᶜ ∈ 𝓝[≠] x
⊢ (U \ s)ᶜ ⊆ (U₁ \ s)ᶜ

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
⊢ codiscreteWithin U₁ ≤ codiscreteWithin U

Tactic:
intro s hs

Result:
X : Type u_1
inst✝ : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
s : Set X
hs : s ∈ codiscreteWithin U
⊢ s ∈ codiscreteWithin U₁

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
s : Set X
hs : s ∈ codiscreteWithin U
⊢ s ∈ codiscreteWithin U₁

Tactic:
simp_rw [mem_codiscreteWithin, disjoint_principal_right] at hs ⊢

Result:
X : Type u_1
inst✝ : TopologicalSpace X
U₁ U : Set X
hU : U₁ ⊆ U
s : Set X
hs : ∀ x ∈ U, (U \ s)ᶜ ∈ 𝓝[≠] x
⊢ ∀ x ∈ U₁, (U₁ \ s)ᶜ ∈ 𝓝[≠] x
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem isClosed_C1 : IsClosed (C1 C ho)

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ IsClosed (C1 C ho)

Tactic:
refine hC.inter ?_

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ IsClosed {f | f (term I ho) = true}

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun x1 x2 => x1 < x2
h : Continuous fun f => f (term I ho)
⊢ IsClosed {f | f (term I ho) = true}

Tactic:
exact IsClosed.preimage h (t := {true}) (isClosed_discrete _)

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ IsClosed {f | f (term I ho) = true}

Tactic:
have h : Continuous (fun (f : I → Bool) ↦ f (term I ho)) := continuous_apply (term I ho)

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
ho : o < Ordinal.type fun x1 x2 => x1 < x2
h : Continuous fun f => f (term I ho)
⊢ IsClosed {f | f (term I ho) = true}
-- Mathlib/Data/Nat/Init.lean
lemma add_eq_one_iff : m + n = 1 ↔ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0

Proof state:
m n : ℕ
⊢ m + n = 1 ↔ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0

Tactic:
omega

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem isRightDescent_iff {w : W} {i : B} :
    cs.IsRightDescent w i ↔ ℓ (w * s i) + 1 = ℓ w

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) < cs.length w ↔ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
constructor

Result:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) < cs.length w → cs.length (w * cs.simple i) + 1 = cs.length w

case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) + 1 = cs.length w → cs.length (w * cs.simple i) < cs.length w

Proof state:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) < cs.length w → cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
intro _

Result:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
a✝ : cs.length (w * cs.simple i) < cs.length w
⊢ cs.length (w * cs.simple i) + 1 = cs.length w

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.IsRightDescent w i ↔ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
unfold IsRightDescent

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) < cs.length w ↔ cs.length (w * cs.simple i) + 1 = cs.length w

Proof state:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
a✝ : cs.length (w * cs.simple i) < cs.length w
⊢ cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
exact (cs.length_mul_simple w i).resolve_left (by omega)

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
a✝ : cs.length (w * cs.simple i) < cs.length w
⊢ ¬cs.length (w * cs.simple i) = cs.length w + 1

Tactic:
omega

Result:
no goals

Proof state:
case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) + 1 = cs.length w → cs.length (w * cs.simple i) < cs.length w

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem forIn_pure_yield_eq_foldl [Monad m] [LawfulMonad m]
    (l : List α) (f : α → β → β) (init : β) :
    forIn l init (fun a b => pure (.yield (f a b))) =
      pure (f := m) (l.foldl (fun b a => f a b) init)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : α → β → β
init : β
⊢ ForInStep.value <$>
      List.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => pure (ForInStep.yield (f a b))
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l =
    pure (foldl (fun b a => f a b) init l)

Tactic:
induction l generalizing init <;> simp_all

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : α → β → β
init : β
⊢ (forIn l init fun a b => pure (ForInStep.yield (f a b))) = pure (foldl (fun b a => f a b) init l)

Tactic:
simp only [forIn_eq_foldlM]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
f : α → β → β
init : β
⊢ ForInStep.value <$>
      List.foldlM
        (fun b a =>
          match b with
          | ForInStep.yield b => pure (ForInStep.yield (f a b))
          | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) l =
    pure (foldl (fun b a => f a b) init l)
-- Mathlib/RingTheory/Spectrum/Prime/TensorProduct.lean
lemma PrimeSpectrum.isEmbedding_tensorProductTo_of_surjectiveOnStalks :
    IsEmbedding (tensorProductTo R S T)

Proof state:
case intro.intro.intro.intro.intro.refine_1.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
x : PrimeSpectrum (S ⊗[R] T)
hx₁ : a ⊗ₜ[R] 1 ∉ x.asIdeal
hx₂ : 1 ⊗ₜ[R] t ∉ x.asIdeal
hx₃ : f ∈ x.asIdeal
⊢ a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∈ ↑x.asIdeal

Tactic:
rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, ← e]

Result:
case intro.intro.intro.intro.intro.refine_1.intro
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
x : PrimeSpectrum (S ⊗[R] T)
hx₁ : a ⊗ₜ[R] 1 ∉ x.asIdeal
hx₂ : 1 ⊗ₜ[R] t ∉ x.asIdeal
hx₃ : f ∈ x.asIdeal
⊢ 1 ⊗ₜ[R] (r • t) * f ∈ ↑x.asIdeal
-- Mathlib/FieldTheory/KummerPolynomial.lean
lemma root_X_pow_sub_C_ne_zero {n : ℕ} (hn : 1 < n) (a : K) :
    (AdjoinRoot.root (X ^ n - C a)) ≠ 0 :=
  mk_ne_zero_of_natDegree_lt (monic_X_pow_sub_C _ (Nat.not_eq_zero_of_lt hn))
    X_ne_zero <| by rwa [natDegree_X_pow_sub_C, natDegree_X]

Proof state:
K : Type u
inst✝ : Field K
n : ℕ
hn : 1 < n
a : K
⊢ X.natDegree < (X ^ n - C a).natDegree

Tactic:
rwa [natDegree_X_pow_sub_C, natDegree_X]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Dirac.lean
@[simp] lemma dirac_ne_zero : dirac a ≠ 0 :=
  fun h ↦ by simpa [h] using dirac_apply_of_mem (mem_univ a)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
a : α
h : dirac a = 0
⊢ False

Tactic:
simpa [h] using dirac_apply_of_mem (mem_univ a)

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
lemma mul_div_cancel_left_of_imp (h : a = 0 → b = 0) : a * b / a = b

Proof state:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b : G₀
h : a = 0 → b = 0
⊢ a * b / a = b

Tactic:
rw [mul_comm, mul_div_cancel_of_imp h]

Result:
no goals
-- Mathlib/CategoryTheory/Closed/FunctorCategory/Basic.lean
lemma homEquiv_naturality_three [∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂]
    (f : F₁ ⊗ F₂ ⟶ F₃) (f₃ : F₃ ⟶ F₃') :
    homEquiv (f ≫ f₃) = homEquiv f ≫ (ρ_ _).inv ≫ _ ◁ functorHomEquiv _ f₃ ≫
      functorEnrichedComp C F₁ F₃ F₃'

Proof state:
case w.h.h.e_a.e_a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ (ihom (F₁.obj k.right)).map (f₃.app k.right) =
    (ρ_ ((ihom (F₁.obj k.right)).obj (F₃.obj k.right))).inv ≫
      (ihom (F₁.obj k.right)).obj (F₃.obj k.right) ◁ (eHomEquiv C) (f₃.app k.right) ≫
        eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right)

Tactic:
symm

Result:
case w.h.h.e_a.e_a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ (ρ_ ((ihom (F₁.obj k.right)).obj (F₃.obj k.right))).inv ≫
      (ihom (F₁.obj k.right)).obj (F₃.obj k.right) ◁ (eHomEquiv C) (f₃.app k.right) ≫
        eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right) =
    (ihom (F₁.obj k.right)).map (f₃.app k.right)

Proof state:
case w.h.h
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ F₂.map k.hom ≫ curry (f.app k.right) ≫ (ihom (F₁.obj k.right)).map (f₃.app k.right) =
    F₂.map k.hom ≫
      curry (f.app k.right) ≫
        (ρ_ ((ihom (F₁.obj k.right)).obj (F₃.obj k.right))).inv ≫
          (ihom (F₁.obj k.right)).obj (F₃.obj k.right) ◁ (eHomEquiv C) (f₃.app k.right) ≫
            eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right)

Tactic:
congr 2

Result:
case w.h.h.e_a.e_a
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalClosed C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₃ F₃' : J ⥤ C
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasEnrichedHom C F₁ F₂
f : F₁ ⊗ F₂ ⟶ F₃
f₃ : F₃ ⟶ F₃'
j : J
k : Under j
⊢ (ihom (F₁.obj k.right)).map (f₃.app k.right) =
    (ρ_ ((ihom (F₁.obj k.right)).obj (F₃.obj k.right))).inv ≫
      (ihom (F₁.obj k.right)).obj (F₃.obj k.right) ◁ (eHomEquiv C) (f₃.app k.right) ≫
        eComp C (F₁.obj k.right) (F₃.obj k.right) (F₃'.obj k.right)
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem coe_restrict (f : α →ₛ β) {s : Set α} (hs : MeasurableSet s) :
    ⇑(restrict f s) = indicator s f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
⊢ ⇑(f.restrict s) = s.indicator ⇑f

Tactic:
classical
rw [restrict, dif_pos hs, coe_piecewise, coe_zero, piecewise_eq_indicator]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
⊢ ⇑(f.restrict s) = s.indicator ⇑f

Tactic:
rw [restrict, dif_pos hs, coe_piecewise, coe_zero, piecewise_eq_indicator]

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem exists_associated_pow_of_mul_eq_pow' {a b c : R} (hab : IsCoprime a b) {k : ℕ}
    (h : a * b = c ^ k) : ∃ d : R, Associated (d ^ k) a

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
a b c : R
hab : IsCoprime a b
k : ℕ
h : a * b = c ^ k
this : GCDMonoid R := IsBezout.toGCDDomain R
⊢ ∃ d, Associated (d ^ k) a

Tactic:
exact exists_associated_pow_of_mul_eq_pow ((gcd_isUnit_iff _ _).mpr hab) h

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
a b c : R
hab : IsCoprime a b
k : ℕ
h : a * b = c ^ k
⊢ ∃ d, Associated (d ^ k) a

Tactic:
classical
letI := IsBezout.toGCDDomain R
exact exists_associated_pow_of_mul_eq_pow ((gcd_isUnit_iff _ _).mpr hab) h

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
a b c : R
hab : IsCoprime a b
k : ℕ
h : a * b = c ^ k
⊢ ∃ d, Associated (d ^ k) a

Tactic:
letI := IsBezout.toGCDDomain R

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : IsDomain R
a b c : R
hab : IsCoprime a b
k : ℕ
h : a * b = c ^ k
this : GCDMonoid R := IsBezout.toGCDDomain R
⊢ ∃ d, Associated (d ^ k) a
-- Mathlib/SetTheory/Game/Basic.lean
/-- `inv' 1` has exactly the same moves as `1`. -/
lemma inv'_one : inv' 1 ≡ 1

Proof state:
case left

⊢ ∀ (z : PGame), z ∈ₗ inv' 1 ↔ z ∈ₗ 1

Tactic:
simp [memₗ_def, inv', isEmpty_subtype]

Result:
no goals

Proof state:
⊢ (∀ (z : PGame), z ∈ₗ inv' 1 ↔ z ∈ₗ 1) ∧ ∀ (z : PGame), z ∈ᵣ inv' 1 ↔ z ∈ᵣ 1

Tactic:
constructor

Result:
case left

⊢ ∀ (z : PGame), z ∈ₗ inv' 1 ↔ z ∈ₗ 1

case right

⊢ ∀ (z : PGame), z ∈ᵣ inv' 1 ↔ z ∈ᵣ 1

Proof state:
⊢ inv' 1 ≡ 1

Tactic:
rw [Identical.ext_iff]

Result:
⊢ (∀ (z : PGame), z ∈ₗ inv' 1 ↔ z ∈ₗ 1) ∧ ∀ (z : PGame), z ∈ᵣ inv' 1 ↔ z ∈ᵣ 1

Proof state:
case right

⊢ ∀ (z : PGame), z ∈ᵣ inv' 1 ↔ z ∈ᵣ 1

Tactic:
simp [memᵣ_def, inv', isEmpty_subtype]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem map_zipWith {δ : Type _} (f : α → β) (g : γ → δ → α) (l : Array γ) (l' : Array δ) :
    map f (zipWith g l l') = zipWith (fun x y => f (g x y)) l l'

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ → α
l : Array γ
l' : Array δ
⊢ map f (zipWith g l l') = zipWith (fun x y => f (g x y)) l l'

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ → α
l' : Array δ
toList✝ : List γ
⊢ map f (zipWith g { toList := toList✝ } l') = zipWith (fun x y => f (g x y)) { toList := toList✝ } l'

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ → α
toList✝¹ : List γ
toList✝ : List δ
⊢ map f (zipWith g { toList := toList✝¹ } { toList := toList✝ }) =
    zipWith (fun x y => f (g x y)) { toList := toList✝¹ } { toList := toList✝ }

Tactic:
simp [List.map_zipWith]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ → α
l' : Array δ
toList✝ : List γ
⊢ map f (zipWith g { toList := toList✝ } l') = zipWith (fun x y => f (g x y)) { toList := toList✝ } l'

Tactic:
cases l'

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ → α
toList✝¹ : List γ
toList✝ : List δ
⊢ map f (zipWith g { toList := toList✝¹ } { toList := toList✝ }) =
    zipWith (fun x y => f (g x y)) { toList := toList✝¹ } { toList := toList✝ }
-- Mathlib/NumberTheory/MulChar/Lemmas.lean
lemma apply_mem_rootsOfUnity_orderOf (χ : MulChar F R) {a : F} (ha : a ≠ 0) :
    ∃ ζ ∈ rootsOfUnity (orderOf χ) R, ζ = χ a

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
a : F
ha : a ≠ 0
hu : IsUnit (χ a)
⊢ hu.unit ∈ rootsOfUnity (orderOf χ) R

Tactic:
rw [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one,
  IsUnit.unit_spec, ← χ.pow_apply' χ.orderOf_pos.ne', pow_orderOf_eq_one,
  show a = (isUnit_iff_ne_zero.mpr ha).unit by simp only [IsUnit.unit_spec],
  MulChar.one_apply_coe]

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
a : F
ha : a ≠ 0
hu : IsUnit (χ a)
⊢ ∃ ζ ∈ rootsOfUnity (orderOf χ) R, ↑ζ = χ a

Tactic:
refine ⟨hu.unit, ?_, hu.unit_spec⟩

Result:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
a : F
ha : a ≠ 0
hu : IsUnit (χ a)
⊢ hu.unit ∈ rootsOfUnity (orderOf χ) R

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
a : F
ha : a ≠ 0
⊢ ∃ ζ ∈ rootsOfUnity (orderOf χ) R, ↑ζ = χ a

Tactic:
have hu : IsUnit (χ a) := ha.isUnit.map χ

Result:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
a : F
ha : a ≠ 0
hu : IsUnit (χ a)
⊢ ∃ ζ ∈ rootsOfUnity (orderOf χ) R, ↑ζ = χ a

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
R : Type u_2
inst✝ : CommRing R
χ : MulChar F R
a : F
ha : a ≠ 0
hu : IsUnit (χ a)
⊢ a = ↑⋯.unit

Tactic:
simp only [IsUnit.unit_spec]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mul_max_mul_left (a b c : Nat) : max (a * b) (a * c) = a * max b c

Proof state:
a b c : Nat
⊢ max (b * a) (c * a) = max b c * a

Tactic:
exact Nat.mul_max_mul_right ..

Result:
no goals

Proof state:
a b c : Nat
⊢ max (b * a) (c * a) = a * max b c

Tactic:
rw [Nat.mul_comm a]

Result:
a b c : Nat
⊢ max (b * a) (c * a) = max b c * a

Proof state:
a b c : Nat
⊢ max (a * b) (a * c) = a * max b c

Tactic:
repeat rw [Nat.mul_comm a]

Result:
a b c : Nat
⊢ max (b * a) (c * a) = max b c * a
-- Mathlib/Data/ZMod/Basic.lean
theorem castHom_injective : Function.Injective (ZMod.castHom (dvd_refl n) R)

Proof state:
case intro
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ (castHom ⋯ R) ↑k = 0 → ↑k = 0

Tactic:
rw [map_intCast, CharP.intCast_eq_zero_iff R n, CharP.intCast_eq_zero_iff (ZMod n) n]

Result:
case intro
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ ↑n ∣ k → ↑n ∣ k

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
x : ZMod n
⊢ (castHom ⋯ R) x = 0 → x = 0

Tactic:
obtain ⟨k, rfl⟩ := ZMod.intCast_surjective x

Result:
case intro
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ (castHom ⋯ R) ↑k = 0 → ↑k = 0

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
⊢ Injective ⇑(castHom ⋯ R)

Tactic:
rw [injective_iff_map_eq_zero]

Result:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
⊢ ∀ (a : ZMod n), (castHom ⋯ R) a = 0 → a = 0

Proof state:
case intro
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
k : ℤ
⊢ ↑n ∣ k → ↑n ∣ k

Tactic:
exact id

Result:
no goals

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
⊢ ∀ (a : ZMod n), (castHom ⋯ R) a = 0 → a = 0

Tactic:
intro x

Result:
n : ℕ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharP R n
x : ZMod n
⊢ (castHom ⋯ R) x = 0 → x = 0