harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean
@[reassoc (attr := simp)]
lemma π_reflexiveCoequalizerIsoCoequalizer_inv :
    coequalizer.π _ _ ≫ (reflexiveCoequalizerIsoCoequalizer F).inv = colimit.ι F _

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
inst✝ : HasCoequalizer (F.map left) (F.map right)
⊢ coequalizer.π (F.map left) (F.map right) ≫
      (((ReflexiveCofork.isColimitEquiv F (colimit.cocone F)).symm (colimit.isColimit F)).coconePointUniqueUpToIso
          (colimit.isColimit (parallelPair (F.map left) (F.map right)))).inv =
    colimit.ι F zero

Tactic:
simp only [colimit.comp_coconePointUniqueUpToIso_inv, Cofork.ofπ_pt, colimit.cocone_x,
  Cofork.ofπ_ι_app, colimit.cocone_ι]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
inst✝ : HasCoequalizer (F.map left) (F.map right)
⊢ coequalizer.π (F.map left) (F.map right) ≫ (reflexiveCoequalizerIsoCoequalizer F).inv = colimit.ι F zero

Tactic:
rw [reflexiveCoequalizerIsoCoequalizer]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
F : WalkingReflexivePair ⥤ C
inst✝ : HasCoequalizer (F.map left) (F.map right)
⊢ coequalizer.π (F.map left) (F.map right) ≫
      (((ReflexiveCofork.isColimitEquiv F (colimit.cocone F)).symm (colimit.isColimit F)).coconePointUniqueUpToIso
          (colimit.isColimit (parallelPair (F.map left) (F.map right)))).inv =
    colimit.ι F zero
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean
theorem norm_condExpIndL1Fin_le (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : G) :
    ‖condExpIndL1Fin hm hs hμs x‖ ≤ (μ s).toReal * ‖x‖

Proof state:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
⊢ ‖condExpIndL1Fin hm hs hμs x‖ ≤ (μ s).toReal * ‖x‖

Tactic:
rw [L1.norm_eq_integral_norm, ← ENNReal.toReal_ofReal (norm_nonneg x), ← ENNReal.toReal_mul,
  ← ENNReal.ofReal_le_iff_le_toReal (ENNReal.mul_ne_top hμs ENNReal.ofReal_ne_top),
  ofReal_integral_norm_eq_lintegral_enorm]

Result:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
⊢ ∫⁻ (x_1 : α), ‖↑↑(condExpIndL1Fin hm hs hμs x) x_1‖ₑ ∂μ ≤ μ s * ENNReal.ofReal ‖x‖

α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
⊢ Integrable (↑↑(condExpIndL1Fin hm hs hμs x)) μ

Proof state:
α : Type u_1
G : Type u_4
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
⊢ MemLp (↑↑(condExpIndL1Fin hm hs hμs x)) 1 μ

Tactic:
exact Lp.memLp _

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
theorem mem_lpMeasSubgroup_toLp_of_trim (hm : m ≤ m0) (f : Lp F p (μ.trim hm)) :
    (memLp_of_memLp_trim hm (Lp.memLp f)).toLp f ∈ lpMeasSubgroup F m p μ

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
hf_mem_ℒp : MemLp (↑↑f) p μ := memLp_of_memLp_trim hm (Lp.memLp f)
⊢ AEStronglyMeasurable (↑↑(MemLp.toLp ↑↑f ⋯)) μ

Tactic:
refine AEStronglyMeasurable'.congr ?_ (MemLp.coeFn_toLp hf_mem_ℒp).symm

Result:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
hf_mem_ℒp : MemLp (↑↑f) p μ := memLp_of_memLp_trim hm (Lp.memLp f)
⊢ AEStronglyMeasurable (↑↑f) μ

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
hf_mem_ℒp : MemLp (↑↑f) p μ := memLp_of_memLp_trim hm (Lp.memLp f)
⊢ MemLp.toLp ↑↑f ⋯ ∈ lpMeasSubgroup F m p μ

Tactic:
rw [mem_lpMeasSubgroup_iff_aeStronglyMeasurable]

Result:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
hf_mem_ℒp : MemLp (↑↑f) p μ := memLp_of_memLp_trim hm (Lp.memLp f)
⊢ AEStronglyMeasurable (↑↑(MemLp.toLp ↑↑f ⋯)) μ

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
⊢ MemLp.toLp ↑↑f ⋯ ∈ lpMeasSubgroup F m p μ

Tactic:
let hf_mem_ℒp := memLp_of_memLp_trim hm (Lp.memLp f)

Result:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
hf_mem_ℒp : MemLp (↑↑f) p μ := memLp_of_memLp_trim hm (Lp.memLp f)
⊢ MemLp.toLp ↑↑f ⋯ ∈ lpMeasSubgroup F m p μ

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
hf_mem_ℒp : MemLp (↑↑f) p μ := memLp_of_memLp_trim hm (Lp.memLp f)
⊢ AEStronglyMeasurable (↑↑f) μ

Tactic:
refine aeStronglyMeasurable'_of_aeStronglyMeasurable'_trim hm ?_

Result:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
hf_mem_ℒp : MemLp (↑↑f) p μ := memLp_of_memLp_trim hm (Lp.memLp f)
⊢ AEStronglyMeasurable (↑↑f) (μ.trim hm)

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp F p (μ.trim hm))
hf_mem_ℒp : MemLp (↑↑f) p μ := memLp_of_memLp_trim hm (Lp.memLp f)
⊢ AEStronglyMeasurable (↑↑f) (μ.trim hm)

Tactic:
exact Lp.aestronglyMeasurable f

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem not_isRight {x : α ⊕ β} : ¬x.isRight ↔ x.isLeft

Proof state:
α : Type u_1
β : Type u_2
x : α ⊕ β
⊢ ¬x.isRight = true ↔ x.isLeft = true

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem toMatrix_update [DecidableEq ι'] (x : M) :
    e.toMatrix (Function.update v j x) = Matrix.updateCol (e.toMatrix v) j (e.repr x)

Proof state:
case a
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
⊢ e.toMatrix (update v j x) i' k = (e.toMatrix v).updateCol j (⇑(e.repr x)) i' k

Tactic:
rw [Basis.toMatrix, Matrix.updateCol_apply, e.toMatrix_apply]

Result:
case a
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
⊢ (e.repr (update v j x k)) i' = if k = j then (e.repr x) i' else (e.repr (v k)) i'

Proof state:
case a
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
⊢ (e.repr (update v j x k)) i' = if k = j then (e.repr x) i' else (e.repr (v k)) i'

Tactic:
split_ifs with h

Result:
case pos
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : k = j
⊢ (e.repr (update v j x k)) i' = (e.repr x) i'

case neg
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : ¬k = j
⊢ (e.repr (update v j x k)) i' = (e.repr (v k)) i'

Proof state:
case neg
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : ¬k = j
⊢ (e.repr (update v j x k)) i' = (e.repr (v k)) i'

Tactic:
rw [update_of_ne h]

Result:
no goals

Proof state:
case pos
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : k = j
⊢ (e.repr (update v j x k)) i' = (e.repr x) i'

Tactic:
rw [h, update_self j x v]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
⊢ e.toMatrix (update v j x) = (e.toMatrix v).updateCol j ⇑(e.repr x)

Tactic:
ext i' k

Result:
case a
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
e : Basis ι R M
v : ι' → M
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
⊢ e.toMatrix (update v j x) i' k = (e.toMatrix v).updateCol j (⇑(e.repr x)) i' k
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_eq_support_biUnion_support [DecidableEq σ] :
    p.vars = p.support.biUnion Finsupp.support

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ p.vars = p.support.biUnion Finsupp.support

Tactic:
ext i

Result:
case h
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
i : σ
⊢ i ∈ p.vars ↔ i ∈ p.support.biUnion Finsupp.support

Proof state:
case h
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
i : σ
⊢ i ∈ p.vars ↔ i ∈ p.support.biUnion Finsupp.support

Tactic:
rw [mem_vars, Finset.mem_biUnion]

Result:
no goals
-- Mathlib/Combinatorics/Additive/Dissociation.lean
@[to_additive (attr := simp)]
lemma subset_mulSpan : s ⊆ mulSpan s := fun a ha ↦
  mem_mulSpan.2 ⟨Pi.single a 1, fun b ↦ by obtain rfl | hab := eq_or_ne a b <;> simp [*], by
    simp [Pi.single, Function.update, pow_ite, ha]⟩

Proof state:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
a : α
ha : a ∈ s
b : α
⊢ Pi.single a 1 b = -1 ∨ Pi.single a 1 b = 0 ∨ Pi.single a 1 b = 1

Tactic:
obtain rfl | hab := eq_or_ne a b <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
a : α
ha : a ∈ s
⊢ ∏ a_1 ∈ s, a_1 ^ Pi.single a 1 a_1 = a

Tactic:
simp [Pi.single, Function.update, pow_ite, ha]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem getKey!_eq_getKey!ₘ [BEq α] [Hashable α] [Inhabited α] (m : Raw₀ α β) (a : α) :
    getKey! m a = getKey!ₘ m a

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : Inhabited α
m : Raw₀ α β
a : α
⊢ m.getKey! a = m.getKey!ₘ a

Tactic:
simp [getKey!, getKey!ₘ, getKey?ₘ, List.getKey!_eq_getKey?, bucket]

Result:
no goals
-- Mathlib/Algebra/Ring/Hom/Defs.lean
theorem map_ite_one_zero {F : Type*} [FunLike F α β] [RingHomClass F α β] (f : F)
    (p : Prop) [Decidable p] :
    f (ite p 1 0) = ite p 1 0

Proof state:
α : Type u_2
β : Type u_3
x✝¹ : NonAssocSemiring α
x✝ : NonAssocSemiring β
F : Type u_5
inst✝² : FunLike F α β
inst✝¹ : RingHomClass F α β
f : F
p : Prop
inst✝ : Decidable p
⊢ f (if p then 1 else 0) = if p then 1 else 0

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma isIso_g' (hS : S.Exact) (h : S.RightHomologyData) [Epi S.g] :
    IsIso h.g'

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
hS : S.Exact
h : S.RightHomologyData
inst✝ : Epi S.g
⊢ IsIso h.g'

Tactic:
have := hS.mono_g' h

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
hS : S.Exact
h : S.RightHomologyData
inst✝ : Epi S.g
this : Mono h.g'
⊢ IsIso h.g'

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
hS : S.Exact
h : S.RightHomologyData
inst✝ : Epi S.g
this : Mono h.g'
⊢ IsIso h.g'

Tactic:
have := epi_of_epi_fac h.p_g'

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
hS : S.Exact
h : S.RightHomologyData
inst✝ : Epi S.g
this✝ : Mono h.g'
this : Epi h.g'
⊢ IsIso h.g'

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
hS : S.Exact
h : S.RightHomologyData
inst✝ : Epi S.g
this✝ : Mono h.g'
this : Epi h.g'
⊢ IsIso h.g'

Tactic:
exact isIso_of_mono_of_epi h.g'

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
lemma pow_mem_range_pow_of_coprime (hmn : m.Coprime n) (a : α) :
    a ^ m ∈ Set.range (· ^ n : α → α) ↔ a ∈ Set.range (· ^ n : α → α)

Proof state:
α : Type u_1
inst✝ : CommGroupWithZero α
m n : ℕ
hmn : m.Coprime n
a : α
⊢ (a ^ m ∈ Set.range fun x => x ^ n) ↔ a ∈ Set.range fun x => x ^ n

Tactic:
simp [pow_eq_pow_iff_of_coprime hmn.symm]

Result:
α : Type u_1
inst✝ : CommGroupWithZero α
m n : ℕ
hmn : m.Coprime n
a : α
⊢ (∃ y c, y = c ^ m ∧ a = c ^ n) ↔ ∃ y, y ^ n = a

Proof state:
α : Type u_1
inst✝ : CommGroupWithZero α
m n : ℕ
hmn : m.Coprime n
a : α
⊢ (∃ y c, y = c ^ m ∧ a = c ^ n) ↔ ∃ y, y ^ n = a

Tactic:
aesop

Result:
no goals
-- Mathlib/Order/Fin/Basic.lean
@[simp]
lemma symm_castOrderIso (h : n = m) : (castOrderIso h).symm = castOrderIso h.symm

Proof state:
m n : ℕ
h : n = m
⊢ (castOrderIso h).symm = castOrderIso ⋯

Tactic:
subst h

Result:
n : ℕ
⊢ (castOrderIso ⋯).symm = castOrderIso ⋯

Proof state:
n : ℕ
⊢ (castOrderIso ⋯).symm = castOrderIso ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
theorem star_re : (star a).re = a.re

Proof state:
R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ (star a).re = a.re

Tactic:
rw [QuaternionAlgebra.re_star, zero_mul, add_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Mon_.lean
theorem Mon_tensor_one_mul (M N : Mon_ C) :
    (((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one)) ▷ (M.X ⊗ N.X)) ≫
        tensorμ M.X N.X M.X N.X ≫ (M.mul ⊗ N.mul) =
      (λ_ (M.X ⊗ N.X)).hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (λ_ (𝟙_ C)).inv ▷ (M.X ⊗ N.X) ≫ tensorμ (𝟙_ C) (𝟙_ C) M.X N.X ≫ ((λ_ M.X).hom ⊗ (λ_ N.X).hom) = (λ_ (M.X ⊗ N.X)).hom

Tactic:
symm

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (λ_ (M.X ⊗ N.X)).hom = (λ_ (𝟙_ C)).inv ▷ (M.X ⊗ N.X) ≫ tensorμ (𝟙_ C) (𝟙_ C) M.X N.X ≫ ((λ_ M.X).hom ⊗ (λ_ N.X).hom)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (λ_ (𝟙_ C)).inv ▷ (M.X ⊗ N.X) ≫ (M.one ⊗ N.one) ▷ (M.X ⊗ N.X) ≫ tensorμ M.X N.X M.X N.X ≫ (M.mul ⊗ N.mul) =
    (λ_ (M.X ⊗ N.X)).hom

Tactic:
slice_lhs 2 3 => rw [tensorμ_natural_left]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (λ_ (𝟙_ C)).inv ▷ (M.X ⊗ N.X) ≫ (tensorμ (𝟙_ C) (𝟙_ C) M.X N.X ≫ (M.one ▷ M.X ⊗ N.one ▷ N.X)) ≫ (M.mul ⊗ N.mul) =
    (λ_ (M.X ⊗ N.X)).hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ ((λ_ (𝟙_ C)).inv ≫ (M.one ⊗ N.one)) ▷ (M.X ⊗ N.X) ≫ tensorμ M.X N.X M.X N.X ≫ (M.mul ⊗ N.mul) = (λ_ (M.X ⊗ N.X)).hom

Tactic:
simp only [comp_whiskerRight_assoc]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (λ_ (𝟙_ C)).inv ▷ (M.X ⊗ N.X) ≫ (M.one ⊗ N.one) ▷ (M.X ⊗ N.X) ≫ tensorμ M.X N.X M.X N.X ≫ (M.mul ⊗ N.mul) =
    (λ_ (M.X ⊗ N.X)).hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (λ_ (𝟙_ C)).inv ▷ (M.X ⊗ N.X) ≫ (tensorμ (𝟙_ C) (𝟙_ C) M.X N.X ≫ (M.one ▷ M.X ⊗ N.one ▷ N.X)) ≫ (M.mul ⊗ N.mul) =
    (λ_ (M.X ⊗ N.X)).hom

Tactic:
slice_lhs 3 4 => rw [← tensor_comp, one_mul M, one_mul N]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (λ_ (𝟙_ C)).inv ▷ (M.X ⊗ N.X) ≫ tensorμ (𝟙_ C) (𝟙_ C) M.X N.X ≫ ((λ_ M.X).hom ⊗ (λ_ N.X).hom) = (λ_ (M.X ⊗ N.X)).hom

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
M N : Mon_ C
⊢ (λ_ (M.X ⊗ N.X)).hom = (λ_ (𝟙_ C)).inv ▷ (M.X ⊗ N.X) ≫ tensorμ (𝟙_ C) (𝟙_ C) M.X N.X ≫ ((λ_ M.X).hom ⊗ (λ_ N.X).hom)

Tactic:
exact tensor_left_unitality M.X N.X

Result:
no goals
-- Mathlib/Order/Irreducible.lean
theorem not_supIrred : ¬SupIrred a ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a

Proof state:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ ¬SupIrred a ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a

Tactic:
rw [SupIrred, not_and_or]

Result:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a) ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a

Proof state:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ ∀ (a_1 b : α), a_1 ⊔ b = a ∧ a_1 ≠ a ∧ b ≠ a ↔ a_1 ⊔ b = a ∧ a_1 < a ∧ b < a

Tactic:
simp +contextual [@eq_comm _ _ a]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a) ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a

Tactic:
push_neg

Result:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ (IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b ≠ a ∧ c ≠ a) ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a

Proof state:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ (IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b ≠ a ∧ c ≠ a) ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a

Tactic:
rw [exists₂_congr]

Result:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ ∀ (a_1 b : α), a_1 ⊔ b = a ∧ a_1 ≠ a ∧ b ≠ a ↔ a_1 ⊔ b = a ∧ a_1 < a ∧ b < a
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem FactorSet.prod_eq_zero_iff [Nontrivial α] (p : FactorSet α) : p.prod = 0 ↔ p = ⊤

Proof state:
case coe
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ prod ↑a✝ = 0 ↔ ↑a✝ = ⊤

Tactic:
rw [prod_coe, Multiset.prod_eq_zero_iff, Multiset.mem_map, eq_false WithTop.coe_ne_top,
  iff_false, not_exists]

Result:
case coe
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ ∀ (x : { a // Irreducible a }), ¬(x ∈ a✝ ∧ ↑x = 0)

Proof state:
case coe
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ ∀ (x : { a // Irreducible a }), ¬(x ∈ a✝ ∧ ↑x = 0)

Tactic:
exact fun a => not_and_of_not_right _ a.prop.ne_zero

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Nontrivial α
p : WithTop (Multiset { a // Irreducible a })
⊢ prod p = 0 ↔ p = ⊤

Tactic:
induction p

Result:
case top
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Nontrivial α
⊢ prod ⊤ = 0 ↔ ⊤ = ⊤

case coe
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
⊢ prod ↑a✝ = 0 ↔ ↑a✝ = ⊤

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Nontrivial α
p : FactorSet α
⊢ p.prod = 0 ↔ p = ⊤

Tactic:
unfold FactorSet at p

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Nontrivial α
p : WithTop (Multiset { a // Irreducible a })
⊢ prod p = 0 ↔ p = ⊤

Proof state:
case top
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : Nontrivial α
⊢ prod ⊤ = 0 ↔ ⊤ = ⊤

Tactic:
simp only [eq_self_iff_true, Associates.prod_top]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioc_insert_left (h : a ≤ b) : insert a (Ioc a b) = Icc a b

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidableEq α
h : a ≤ b
⊢ insert a (Ioc a b) = Icc a b

Tactic:
rw [← coe_inj, coe_insert, coe_Ioc, coe_Icc, Set.insert_eq, Set.union_comm, Set.Ioc_union_left h]

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
theorem map_le_map_iff {f : α → β} (hf : Function.Injective f) {s t : Multiset α} :
    s.map f ≤ t.map f ↔ s ≤ t

Proof state:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s ≤ map f t ↔ s ≤ t

Tactic:
classical
  refine ⟨fun h => le_iff_count.mpr fun a => ?_, map_le_map⟩
  simpa [count_map_eq_count' f _ hf] using le_iff_count.mp h (f a)

Result:
no goals

Proof state:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
h : map f s ≤ map f t
a : α
⊢ count a s ≤ count a t

Tactic:
simpa [count_map_eq_count' f _ hf] using le_iff_count.mp h (f a)

Result:
no goals

Proof state:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s ≤ map f t ↔ s ≤ t

Tactic:
refine ⟨fun h => le_iff_count.mpr fun a => ?_, map_le_map⟩

Result:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
h : map f s ≤ map f t
a : α
⊢ count a s ≤ count a t
-- Mathlib/RingTheory/Discriminant.lean
theorem discr_isIntegral {b : ι → L} (h : ∀ i, IsIntegral R (b i)) : IsIntegral R (discr K b)

Proof state:
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
K : Type u
L : Type v
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Module.Finite K L
R : Type z
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
b : ι → L
h : ∀ (i : ι), IsIntegral R (b i)
⊢ IsIntegral R (traceMatrix K b).det

Tactic:
exact IsIntegral.det fun i j ↦ isIntegral_trace ((h i).mul (h j))

Result:
no goals

Proof state:
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
K : Type u
L : Type v
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Module.Finite K L
R : Type z
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
b : ι → L
h : ∀ (i : ι), IsIntegral R (b i)
⊢ IsIntegral R (discr K b)

Tactic:
classical
rw [discr_def]
exact IsIntegral.det fun i j ↦ isIntegral_trace ((h i).mul (h j))

Result:
no goals

Proof state:
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
K : Type u
L : Type v
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Module.Finite K L
R : Type z
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
b : ι → L
h : ∀ (i : ι), IsIntegral R (b i)
⊢ IsIntegral R (discr K b)

Tactic:
rw [discr_def]

Result:
ι : Type w
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
K : Type u
L : Type v
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
inst✝⁴ : Module.Finite K L
R : Type z
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
b : ι → L
h : ∀ (i : ι), IsIntegral R (b i)
⊢ IsIntegral R (traceMatrix K b).det
-- Mathlib/NumberTheory/JacobiSum/Basic.lean
theorem jacobiSum_eq_gaussSum_mul_gaussSum_div_gaussSum (h : (Fintype.card F : F') ≠ 0)
    {χ φ : MulChar F F'} (hχφ : χ * φ ≠ 1) {ψ : AddChar F F'} (hψ : ψ.IsPrimitive) :
    jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ / gaussSum (χ * φ) ψ

Proof state:
F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ↑(Fintype.card F) ≠ 0
χ φ : MulChar F F'
hχφ : χ * φ ≠ 1
ψ : AddChar F F'
hψ : ψ.IsPrimitive
⊢ jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ / gaussSum (χ * φ) ψ

Tactic:
rw [eq_div_iff <| gaussSum_ne_zero_of_nontrivial h hχφ hψ, mul_comm]

Result:
F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ↑(Fintype.card F) ≠ 0
χ φ : MulChar F F'
hχφ : χ * φ ≠ 1
ψ : AddChar F F'
hψ : ψ.IsPrimitive
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ

Proof state:
F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ↑(Fintype.card F) ≠ 0
χ φ : MulChar F F'
hχφ : χ * φ ≠ 1
ψ : AddChar F F'
hψ : ψ.IsPrimitive
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ

Tactic:
exact jacobiSum_mul_nontrivial hχφ ψ

Result:
no goals