harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_mono_measure {f : α → ℝ} {ν} (hle : μ ≤ ν) (hf : 0 ≤ᵐ[ν] f)
    (hfi : Integrable f ν) : ∫ a, f a ∂μ ≤ ∫ a, f a ∂ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
hfi' : Integrable f μ
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν

Tactic:
have hf' : 0 ≤ᵐ[μ] f := hle.absolutelyContinuous hf

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
hfi' : Integrable f μ
hf' : 0 ≤ᶠ[ae μ] f
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
hfi' : Integrable f μ
hf' : 0 ≤ᶠ[ae μ] f
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν

Tactic:
rw [integral_eq_lintegral_of_nonneg_ae hf' hfi'.1, integral_eq_lintegral_of_nonneg_ae hf hfi.1]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
hfi' : Integrable f μ
hf' : 0 ≤ᶠ[ae μ] f
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂ν).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
hfi' : Integrable f μ
hf' : 0 ≤ᶠ[ae μ] f
⊢ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal ≤ (∫⁻ (a : α), ENNReal.ofReal (f a) ∂ν).toReal

Tactic:
refine ENNReal.toReal_mono ?_ (lintegral_mono' hle le_rfl)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
hfi' : Integrable f μ
hf' : 0 ≤ᶠ[ae μ] f
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂ν ≠ ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν

Tactic:
have hfi' : Integrable f μ := hfi.mono_measure hle

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
hfi' : Integrable f μ
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), f a ∂ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
hle : μ ≤ ν
hf : 0 ≤ᶠ[ae ν] f
hfi : Integrable f ν
hfi' : Integrable f μ
hf' : 0 ≤ᶠ[ae μ] f
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂ν ≠ ⊤

Tactic:
exact ((hasFiniteIntegral_iff_ofReal hf).1 hfi.2).ne

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Ring.lean
theorem hasSum_const_div_iff (h : a₂ ≠ 0) :
    HasSum (fun i ↦ a₂ / f i) (a₂ * a₁) ↔ HasSum (1/ f) a₁

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalSemiring α
f : ι → α
a₁ a₂ : α
h : a₂ ≠ 0
⊢ HasSum (fun i => a₂ / f i) (a₂ * a₁) ↔ HasSum (1 / f) a₁

Tactic:
simpa only [div_eq_mul_inv, one_mul] using hasSum_mul_left_iff h

Result:
no goals
-- Mathlib/Algebra/Star/Pointwise.lean
theorem star_mul [Mul α] [StarMul α] (s t : Set α) : (s * t)⋆ = t⋆ * s⋆

Proof state:
α : Type u_1
inst✝¹ : Mul α
inst✝ : StarMul α
s t : Set α
⊢ (s * t)⋆ = t⋆ * s⋆

Tactic:
simp_rw [← image_star, ← image2_mul, image_image2, image2_image_left, image2_image_right,
  star_mul, image2_swap _ s t]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/AddCircle.lean
theorem norm_eq_of_zero {x : ℝ} : ‖(x : AddCircle (0 : ℝ))‖ = |x|

Proof state:
x : ℝ
⊢ ‖↑x‖ = |x|

Tactic:
suffices { y : ℝ | (y : AddCircle (0 : ℝ)) = (x : AddCircle (0 : ℝ)) } = {x} by
  rw [quotient_norm_eq, this, image_singleton, Real.norm_eq_abs, csInf_singleton]

Result:
x : ℝ
⊢ {y | ↑y = ↑x} = {x}

Proof state:
case h
x y : ℝ
⊢ y ∈ {y | ↑y = ↑x} ↔ y ∈ {x}

Tactic:
simp [QuotientAddGroup.eq_iff_sub_mem, mem_zmultiples_iff, sub_eq_zero]

Result:
no goals

Proof state:
x : ℝ
this : {y | ↑y = ↑x} = {x}
⊢ ‖↑x‖ = |x|

Tactic:
rw [quotient_norm_eq, this, image_singleton, Real.norm_eq_abs, csInf_singleton]

Result:
no goals

Proof state:
x : ℝ
⊢ {y | ↑y = ↑x} = {x}

Tactic:
ext y

Result:
case h
x y : ℝ
⊢ y ∈ {y | ↑y = ↑x} ↔ y ∈ {x}
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem eLpNorm_one_le_of_le' {r : ℝ} (hfint : Integrable f μ) (hfint' : 0 ≤ ∫ x, f x ∂μ)
    (hf : ∀ᵐ ω ∂μ, f ω ≤ r) : eLpNorm f 1 μ ≤ 2 * μ Set.univ * ENNReal.ofReal r

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ r
⊢ eLpNorm f 1 μ ≤ 2 * μ univ * ENNReal.ofReal r

Tactic:
refine eLpNorm_one_le_of_le hfint hfint' ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ r
⊢ ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r.toNNReal

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ r
⊢ ∀ᵐ (ω : α) ∂μ, f ω ≤ r ∨ f ω ≤ 0

Tactic:
filter_upwards [hf] with ω hω using Or.inl hω

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ r
⊢ ∀ᵐ (ω : α) ∂μ, f ω ≤ ↑r.toNNReal

Tactic:
simp only [Real.coe_toNNReal', le_max_iff]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
r : ℝ
hfint : Integrable f μ
hfint' : 0 ≤ ∫ (x : α), f x ∂μ
hf : ∀ᵐ (ω : α) ∂μ, f ω ≤ r
⊢ ∀ᵐ (ω : α) ∂μ, f ω ≤ r ∨ f ω ≤ 0
-- Mathlib/Analysis/Matrix.lean
theorem mul_unitOf (a : α) : a * unitOf a = algebraMap _ _ (‖a‖₊ : ℝ)

Proof state:
case neg
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
h : ¬a = 0
⊢ a * ‖a‖ • a⁻¹ = (algebraMap ℝ α) ‖a‖

Tactic:
rw [mul_smul_comm, mul_inv_cancel₀ h, Algebra.algebraMap_eq_smul_one]

Result:
no goals

Proof state:
case pos
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
h : a = 0
⊢ a * 1 = (algebraMap ℝ α) ‖a‖

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
⊢ (a * if a = 0 then 1 else ‖a‖ • a⁻¹) = (algebraMap ℝ α) ‖a‖

Tactic:
split_ifs with h

Result:
case pos
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
h : a = 0
⊢ a * 1 = (algebraMap ℝ α) ‖a‖

case neg
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
h : ¬a = 0
⊢ a * ‖a‖ • a⁻¹ = (algebraMap ℝ α) ‖a‖

Proof state:
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
⊢ a * Matrix.unitOf a = (algebraMap ℝ α) ↑‖a‖₊

Tactic:
simp only [unitOf, coe_nnnorm]

Result:
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
⊢ (a * if a = 0 then 1 else ‖a‖ • a⁻¹) = (algebraMap ℝ α) ‖a‖
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem primitiveRoots_zero : primitiveRoots 0 R = ∅

Proof state:
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ primitiveRoots 0 R = ∅

Tactic:
rw [primitiveRoots, nthRoots_zero, Multiset.toFinset_zero, Finset.filter_empty]

Result:
no goals

Proof state:
R : Type u_4
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ primitiveRoots 0 R = ∅

Tactic:
classical
rw [primitiveRoots, nthRoots_zero, Multiset.toFinset_zero, Finset.filter_empty]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean
theorem involute_eq_of_mem_odd {x : CliffordAlgebra Q} (h : x ∈ evenOdd Q 1) : involute x = -x

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
h : x ∈ evenOdd Q 1
⊢ involute x = -x

Tactic:
induction x, h using odd_induction with
| ι m => exact involute_ι _
| add x y _hx _hy ihx ihy =>
  rw [map_add, ihx, ihy, neg_add]
| ι_mul_ι_mul m₁ m₂ x _hx ihx =>
  rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg, mul_neg]

Result:
no goals

Proof state:
case ι
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
m : M
⊢ involute ((ι Q) m) = -(ι Q) m

Tactic:
exact involute_ι _

Result:
no goals

Proof state:
case ι_mul_ι_mul
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ : CliffordAlgebra Q
m₁ m₂ : M
x : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 1
ihx : involute x = -x
⊢ involute ((ι Q) m₁ * (ι Q) m₂ * x) = -((ι Q) m₁ * (ι Q) m₂ * x)

Tactic:
rw [map_mul, map_mul, involute_ι, involute_ι, ihx, neg_mul_neg, mul_neg]

Result:
no goals

Proof state:
case add
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x✝ x y : CliffordAlgebra Q
_hx : x ∈ evenOdd Q 1
_hy : y ∈ evenOdd Q 1
ihx : involute x = -x
ihy : involute y = -y
⊢ involute (x + y) = -(x + y)

Tactic:
rw [map_add, ihx, ihy, neg_add]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem LipschitzOnWith.comp_eVariationOn_le {f : E → F} {C : ℝ≥0} {t : Set E}
    (h : LipschitzOnWith C f t) {g : α → E} {s : Set α} (hg : MapsTo g s t) :
    eVariationOn (f ∘ g) s ≤ C * eVariationOn g s

Proof state:
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
F : Type u_3
inst✝ : PseudoEMetricSpace F
f : E → F
C : ℝ≥0
t : Set E
h : LipschitzOnWith C f t
g : α → E
s : Set α
hg : MapsTo g s t
⊢ ∀ (i : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }),
    ∑ i_1 ∈ Finset.range i.1, edist ((f ∘ g) (↑i.2 (i_1 + 1))) ((f ∘ g) (↑i.2 i_1)) ≤ ↑C * eVariationOn g s

Tactic:
rintro ⟨n, ⟨u, hu, us⟩⟩

Result:
case mk.mk.intro
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
F : Type u_3
inst✝ : PseudoEMetricSpace F
f : E → F
C : ℝ≥0
t : Set E
h : LipschitzOnWith C f t
g : α → E
s : Set α
hg : MapsTo g s t
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
⊢ ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist ((f ∘ g) (↑(n, ⟨u, ⋯⟩).2 (i + 1))) ((f ∘ g) (↑(n, ⟨u, ⋯⟩).2 i)) ≤
    ↑C * eVariationOn g s

Proof state:
case mk.mk.intro
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
F : Type u_3
inst✝ : PseudoEMetricSpace F
f : E → F
C : ℝ≥0
t : Set E
h : LipschitzOnWith C f t
g : α → E
s : Set α
hg : MapsTo g s t
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
⊢ ∑ i ∈ Finset.range (n, ⟨u, ⋯⟩).1, edist ((f ∘ g) (↑(n, ⟨u, ⋯⟩).2 (i + 1))) ((f ∘ g) (↑(n, ⟨u, ⋯⟩).2 i)) ≤
    ↑C * eVariationOn g s

Tactic:
calc
  (∑ i ∈ Finset.range n, edist (f (g (u (i + 1)))) (f (g (u i)))) ≤
      ∑ i ∈ Finset.range n, C * edist (g (u (i + 1))) (g (u i)) :=
    Finset.sum_le_sum fun i _ => h (hg (us _)) (hg (us _))
  _ = C * ∑ i ∈ Finset.range n, edist (g (u (i + 1))) (g (u i)) := by rw [Finset.mul_sum]
  _ ≤ C * eVariationOn g s := mul_le_mul_left' (eVariationOn.sum_le _ _ hu us) _

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
F : Type u_3
inst✝ : PseudoEMetricSpace F
f : E → F
C : ℝ≥0
t : Set E
h : LipschitzOnWith C f t
g : α → E
s : Set α
hg : MapsTo g s t
n : ℕ
u : ℕ → α
hu : Monotone u
us : ∀ (i : ℕ), u i ∈ s
⊢ ∑ i ∈ Finset.range n, ↑C * edist (g (u (i + 1))) (g (u i)) =
    ↑C * ∑ i ∈ Finset.range n, edist (g (u (i + 1))) (g (u i))

Tactic:
rw [Finset.mul_sum]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
F : Type u_3
inst✝ : PseudoEMetricSpace F
f : E → F
C : ℝ≥0
t : Set E
h : LipschitzOnWith C f t
g : α → E
s : Set α
hg : MapsTo g s t
⊢ eVariationOn (f ∘ g) s ≤ ↑C * eVariationOn g s

Tactic:
apply iSup_le _

Result:
α : Type u_1
inst✝² : LinearOrder α
E : Type u_2
inst✝¹ : PseudoEMetricSpace E
F : Type u_3
inst✝ : PseudoEMetricSpace F
f : E → F
C : ℝ≥0
t : Set E
h : LipschitzOnWith C f t
g : α → E
s : Set α
hg : MapsTo g s t
⊢ ∀ (i : ℕ × { u // Monotone u ∧ ∀ (i : ℕ), u i ∈ s }),
    ∑ i_1 ∈ Finset.range i.1, edist ((f ∘ g) (↑i.2 (i_1 + 1))) ((f ∘ g) (↑i.2 i_1)) ≤ ↑C * eVariationOn g s
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_alter [LawfulBEq α] {k k' : α} {fallback : β k'} (h : m.1.WF)
    {f : Option (β k) → Option (β k)} :
    (m.alter k f).getD k' fallback =
      if heq : k == k' then
        f (m.get? k) |>.map (cast (congrArg β <| eq_of_beq heq)) |>.getD fallback
      else
        m.getD k' fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
k k' : α
fallback : β k'
h : m.val.WF
f : Option (β k) → Option (β k)
⊢ (m.alter k f).getD k' fallback =
    if heq : (k == k') = true then (Option.map (cast ⋯) (f (m.get? k))).getD fallback else m.getD k' fallback

Tactic:
simp_to_model [alter] using List.getValueCastD_alterKey

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
lemma ιTensorObj₄_eq (i₁ i₂ i₃ i₄ j : I) (h : i₁ + i₂ + i₃ + i₄ = j) (i₂₃₄ : I)
    (hi : i₂ + i₃ + i₄ = i₂₃₄) :
    ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h =
      (_ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ _ hi) ≫
        ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j
          (by rw [← hi, ← add_assoc, ← add_assoc, h])

Proof state:
I : Type u
inst✝⁵ : AddMonoid I
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : MonoidalCategory C
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝² : X₃.HasTensor X₄
inst✝¹ : X₂.HasTensor (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
i₂₃₄ : I
hi : i₂ + i₃ + i₄ = i₂₃₄
⊢ ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h =
    X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ i₂₃₄ hi ≫ ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ i₂₃₄ j ⋯

Tactic:
subst hi

Result:
I : Type u
inst✝⁵ : AddMonoid I
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : MonoidalCategory C
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝² : X₃.HasTensor X₄
inst✝¹ : X₂.HasTensor (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
⊢ ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h =
    X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ (i₂ + i₃ + i₄) ⋯ ≫
      ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ (i₂ + i₃ + i₄) j ⋯

Proof state:
I : Type u
inst✝⁵ : AddMonoid I
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : MonoidalCategory C
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝² : X₃.HasTensor X₄
inst✝¹ : X₂.HasTensor (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
⊢ ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h =
    X₁ i₁ ◁ ιTensorObj₃ X₂ X₃ X₄ i₂ i₃ i₄ (i₂ + i₃ + i₄) ⋯ ≫
      ιTensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) i₁ (i₂ + i₃ + i₄) j ⋯

Tactic:
rfl

Result:
no goals

Proof state:
I : Type u
inst✝⁵ : AddMonoid I
C : Type u_1
inst✝⁴ : Category.{?u.205960, u_1} C
inst✝³ : MonoidalCategory C
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝² : X₃.HasTensor X₄
inst✝¹ : X₂.HasTensor (tensorObj X₃ X₄)
inst✝ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
i₁ i₂ i₃ i₄ j : I
h : i₁ + i₂ + i₃ + i₄ = j
i₂₃₄ : I
hi : i₂ + i₃ + i₄ = i₂₃₄
⊢ i₁ + i₂₃₄ = j

Tactic:
rw [← hi, ← add_assoc, ← add_assoc, h]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem mul_apply_left (f g : MonoidAlgebra k G) (x : G) :
    (f * g) x = f.sum fun a b => b * g (a⁻¹ * x) :=
  calc
    (f * g) x = sum f fun a b => (single a b * g) x

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Group G
f g : MonoidAlgebra k G
x : G
⊢ (sum f fun a b => (single a b * g) x) = sum f fun a b => b * g (a⁻¹ * x)

Tactic:
simp only [single_mul_apply, Finsupp.sum]

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Group G
f g : MonoidAlgebra k G
x : G
⊢ (f * g) x = sum f fun a b => (single a b * g) x

Tactic:
rw [← Finsupp.sum_apply, ← Finsupp.sum_mul g f, f.sum_single]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The abscissa of (absolute) convergence of the arithmetic function `ζ` is `1`. -/
lemma abscissaOfAbsConv_zeta : abscissaOfAbsConv ↗ζ = 1

Proof state:
n✝ : ℕ
hn : n✝ ≠ 0
⊢ ↑(ζ n✝) = 1 n✝

Tactic:
simp [hn]

Result:
no goals

Proof state:
⊢ (abscissaOfAbsConv fun n => ↑(ζ n)) = 1

Tactic:
rw [abscissaOfAbsConv_congr (g := 1) fun hn ↦ by simp [hn], abscissaOfAbsConv_one]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
@[simp]
lemma krullDim_enat : krullDim ℕ∞ = ⊤

Proof state:
⊢ krullDim (WithTop ℕ) = ⊤

Tactic:
simp only [krullDim_WithTop, krullDim_nat]

Result:
⊢ ⊤ + 1 = ⊤

Proof state:
⊢ krullDim ℕ∞ = ⊤

Tactic:
show (krullDim (WithTop ℕ) = ⊤)

Result:
⊢ krullDim (WithTop ℕ) = ⊤

Proof state:
⊢ ⊤ + 1 = ⊤

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/UniqueProds/Basic.lean
theorem mulHom_image_iff [DecidableEq H] (f : G →ₙ* H) (hf : Function.Injective f) :
    UniqueMul (A.image f) (B.image f) (f a0) (f b0) ↔ UniqueMul A B a0 b0 :=
  ⟨of_mulHom_image f fun _ _ _ _ _ ↦ .imp (hf ·) (hf ·), fun h _ _ ↦ by
    simp_rw [Finset.mem_image]
    rintro ⟨a, aA, rfl⟩ ⟨b, bB, rfl⟩ ab
    simp_rw [← map_mul, hf.eq_iff] at ab ⊢
    exact h aA bB ab⟩

Proof state:
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ⇑f
h : UniqueMul A B a0 b0
x✝¹ x✝ : H
⊢ x✝¹ ∈ image (⇑f) A → x✝ ∈ image (⇑f) B → x✝¹ * x✝ = f a0 * f b0 → x✝¹ = f a0 ∧ x✝ = f b0

Tactic:
simp_rw [Finset.mem_image]

Result:
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ⇑f
h : UniqueMul A B a0 b0
x✝¹ x✝ : H
⊢ (∃ a ∈ A, f a = x✝¹) → (∃ a ∈ B, f a = x✝) → x✝¹ * x✝ = f a0 * f b0 → x✝¹ = f a0 ∧ x✝ = f b0

Proof state:
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ⇑f
h : UniqueMul A B a0 b0
x✝¹ x✝ : H
⊢ (∃ a ∈ A, f a = x✝¹) → (∃ a ∈ B, f a = x✝) → x✝¹ * x✝ = f a0 * f b0 → x✝¹ = f a0 ∧ x✝ = f b0

Tactic:
rintro ⟨a, aA, rfl⟩ ⟨b, bB, rfl⟩ ab

Result:
case intro.intro.intro.intro
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ⇑f
h : UniqueMul A B a0 b0
a : G
aA : a ∈ A
b : G
bB : b ∈ B
ab : f a * f b = f a0 * f b0
⊢ f a = f a0 ∧ f b = f b0

Proof state:
case intro.intro.intro.intro
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ⇑f
h : UniqueMul A B a0 b0
a : G
aA : a ∈ A
b : G
bB : b ∈ B
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0

Tactic:
exact h aA bB ab

Result:
no goals

Proof state:
case intro.intro.intro.intro
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ⇑f
h : UniqueMul A B a0 b0
a : G
aA : a ∈ A
b : G
bB : b ∈ B
ab : f a * f b = f a0 * f b0
⊢ f a = f a0 ∧ f b = f b0

Tactic:
simp_rw [← map_mul, hf.eq_iff] at ab ⊢

Result:
case intro.intro.intro.intro
G : Type u_1
H : Type u_2
inst✝² : Mul G
inst✝¹ : Mul H
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq H
f : G →ₙ* H
hf : Function.Injective ⇑f
h : UniqueMul A B a0 b0
a : G
aA : a ∈ A
b : G
bB : b ∈ B
ab : a * b = a0 * b0
⊢ a = a0 ∧ b = b0
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem op_eq_self_of_principal (hao : a < o) (H : IsNormal (op a))
    (ho : Principal op o) (ho' : IsLimit o) : op a o = o

Proof state:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : Principal op o
ho' : o.IsLimit
⊢ ∀ i < o, op a i ≤ o

Tactic:
exact fun b hbo => (ho hao hbo).le

Result:
no goals

Proof state:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : Principal op o
ho' : o.IsLimit
⊢ op a o ≤ o

Tactic:
rw [← IsNormal.bsup_eq.{u, u} H ho', bsup_le_iff]

Result:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : Principal op o
ho' : o.IsLimit
⊢ ∀ i < o, op a i ≤ o

Proof state:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : Principal op o
ho' : o.IsLimit
⊢ op a o = o

Tactic:
apply H.le_apply.antisymm'

Result:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : Principal op o
ho' : o.IsLimit
⊢ op a o ≤ o
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
theorem integrable_rnDeriv_smul_iff (hμν : μ ≪ ν) :
    Integrable (fun x ↦ (μ.rnDeriv ν x).toReal • f x) ν ↔ Integrable f μ

Proof state:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
⊢ Integrable (fun x => (μ.rnDeriv ν x).toReal • f x) ν ↔ Integrable f μ

Tactic:
nth_rw 2 [← withDensity_rnDeriv_eq μ ν hμν]

Result:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
⊢ Integrable (fun x => (μ.rnDeriv ν x).toReal • f x) ν ↔ Integrable f (ν.withDensity (μ.rnDeriv ν))

Proof state:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : μ.HaveLebesgueDecomposition ν
inst✝ : SigmaFinite μ
f : α → E
hμν : μ ≪ ν
⊢ Integrable (fun x => (μ.rnDeriv ν x).toReal • f x) ν ↔ Integrable f (ν.withDensity (μ.rnDeriv ν))

Tactic:
rw [← integrable_withDensity_iff_integrable_smul' (E := E)
  (measurable_rnDeriv μ ν) (rnDeriv_lt_top μ ν)]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Pasting.lean
theorem inr_inl_pushoutRightPushoutInlIso_hom :
    pushout.inl _ _ ≫ pushout.inr _ _ ≫ (pushoutRightPushoutInlIso f g f').hom =
      f' ≫ pushout.inl _ _

Proof state:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
f' : Y ⟶ W
inst✝¹ : HasPushout f g
inst✝ : HasPushout f' (pushout.inl f g)
⊢ pushout.inl f g ≫ pushout.inr f' (pushout.inl f g) ≫ (pushoutRightPushoutInlIso f g f').hom =
    f' ≫ pushout.inl (f ≫ f') g

Tactic:
rw [← Category.assoc, ← pushout.condition, Category.assoc, inl_pushoutRightPushoutInlIso_hom]

Result:
no goals