harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Tactic/CategoryTheory/Monoidal/PureCoherence.lean
theorem naturality_whiskerRight {p f g h pf pfh : C} {η : f ≅ g}
    (η_f : p ⊗ f ≅ pf) (η_g : p ⊗ g ≅ pf) (η_fh : (pf ⊗ h) ≅ pfh)
    (ih_η : p ◁ η ≪≫ η_g = η_f) :
    p ◁ (η ▷ h) ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp η_f η_fh

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfh : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
η_fh : pf ⊗ h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp η_f η_fh

Tactic:
rw [← ih_η]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfh : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
η_fh : pf ⊗ h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh

Proof state:
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfh : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
η_fh : pf ⊗ h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
⊢ (p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh).hom = (normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh).hom

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfh : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
η_fh : pf ⊗ h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
⊢ p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh = normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh

Tactic:
apply Iso.ext

Result:
case w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
p f g h pf pfh : C
η : f ≅ g
η_f : p ⊗ f ≅ pf
η_g : p ⊗ g ≅ pf
η_fh : pf ⊗ h ≅ pfh
ih_η : p ◁ η ≪≫ η_g = η_f
⊢ (p ◁ η ▷ h ≪≫ normalizeIsoComp η_g η_fh).hom = (normalizeIsoComp (p ◁ η ≪≫ η_g) η_fh).hom
-- Mathlib/LinearAlgebra/BilinearForm/Basic.lean
theorem flip_flip :
    flipHom.trans flipHom = LinearEquiv.refl R (BilinForm R M)

Proof state:
case h.H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : BilinForm R M
x✝ y✝ : M
⊢ (((flipHom ≪≫ₗ flipHom) A) x✝) y✝ = (((LinearEquiv.refl R (BilinForm R M)) A) x✝) y✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ flipHom ≪≫ₗ flipHom = LinearEquiv.refl R (BilinForm R M)

Tactic:
ext A

Result:
case h.H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : BilinForm R M
x✝ y✝ : M
⊢ (((flipHom ≪≫ₗ flipHom) A) x✝) y✝ = (((LinearEquiv.refl R (BilinForm R M)) A) x✝) y✝
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem union_ae_eq_right : (s ∪ t : Set α) =ᵐ[μ] t ↔ μ (s \ t) = 0

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ s ∪ t =ᶠ[ae μ] t ↔ μ (s \ t) = 0

Tactic:
simp [eventuallyLE_antisymm_iff, ae_le_set, union_diff_right,
  diff_eq_empty.2 Set.subset_union_right]

Result:
no goals
-- Mathlib/Data/Nat/Prime/Defs.lean
theorem prime_three : Prime 3

Proof state:
⊢ Prime 3

Tactic:
decide

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Grothendieck.lean
lemma Hom.congr {a b : ∫ F} {f g : a ⟶ b} (h : f = g) :
    f.fiber = g.fiber ≫ eqToHom (h ▸ rfl)

Proof state:
𝒮 : Type u₁
inst✝ : Category.{v₁, u₁} 𝒮
F : Pseudofunctor (LocallyDiscrete 𝒮ᵒᵖ) Cat
a b : ∫ F
f g : a ⟶ b
h : f = g
⊢ f.fiber = g.fiber ≫ eqToHom ⋯

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_sub (a b : α) : toIocMod hp a (b - p) = toIocMod hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a (b - p) = toIocMod hp a b

Tactic:
simpa only [one_zsmul] using toIocMod_sub_zsmul hp a b 1

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_congr_ae' (h : ∀ᵐ x ∂μ, x ∈ Ioc a b → f x = g x)
    (h' : ∀ᵐ x ∂μ, x ∈ Ioc b a → f x = g x) : ∫ x in a..b, f x ∂μ = ∫ x in a..b, g x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : Measure ℝ
h : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ioc a b → f x = g x
h' : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ioc b a → f x = g x
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
simp only [intervalIntegral, setIntegral_congr_ae measurableSet_Ioc h,
  setIntegral_congr_ae measurableSet_Ioc h']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem?_singleton (a : α) (i : Nat) : #v[a][i]? = if i = 0 then some a else none

Proof state:
α : Type u_1
a : α
i : Nat
⊢ { toArray := #[a], size_toArray := ⋯ }[i]? = if i = 0 then some a else none

Tactic:
simp [List.getElem?_singleton]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem sup_inf_right (a b c : α) : a ⊓ b ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)

Proof state:
α : Type u
inst✝ : DistribLattice α
a b c : α
⊢ a ⊓ b ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)

Tactic:
simp only [sup_inf_left, sup_comm _ c, eq_self_iff_true]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma equation_of_Z_eq_zero {P : Fin 3 → R} (hPz : P z = 0) :
    W'.Equation P ↔ P y ^ 2 = P x ^ 3

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hPz : P z = 0
⊢ W'.Equation P ↔ P y ^ 2 = P x ^ 3

Tactic:
simp only [equation_iff, hPz, add_zero, mul_zero, zero_pow <| OfNat.ofNat_ne_zero _, sub_eq_zero]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma densityProcess_le_one (hκν : fst κ ≤ ν) (n : ℕ) (a : α) (x : γ) (s : Set β) :
    densityProcess κ ν n a x s ≤ 1

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ κ.densityProcess ν n a x s ≤ 1

Tactic:
refine ENNReal.toReal_le_of_le_ofReal zero_le_one (ENNReal.div_le_of_le_mul ?_)

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ (κ a) (countablePartitionSet n x ×ˢ s) ≤ ENNReal.ofReal 1 * (ν a) (countablePartitionSet n x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ (κ a) (countablePartitionSet n x ×ˢ s) ≤ ENNReal.ofReal 1 * (ν a) (countablePartitionSet n x)

Tactic:
rw [ENNReal.ofReal_one, one_mul]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ (κ a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ (κ a) (countablePartitionSet n x ×ˢ s) ≤ (ν a) (countablePartitionSet n x)

Tactic:
exact meas_countablePartitionSet_le_of_fst_le hκν n a x s

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/DFinsupp.lean
theorem dfinsuppFamily_add (f g : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) (N p)) :
    dfinsuppFamily (f + g) = dfinsuppFamily f + dfinsuppFamily g

Proof state:
case H.h
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f g : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
x✝ : (i : ι) → Π₀ (j : κ i), M i j
i✝ : (i : ι) → κ i
⊢ ((dfinsuppFamily (f + g)) x✝) i✝ = ((dfinsuppFamily f + dfinsuppFamily g) x✝) i✝

Tactic:
simp

Result:
no goals

Proof state:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f g : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
⊢ dfinsuppFamily (f + g) = dfinsuppFamily f + dfinsuppFamily g

Tactic:
ext

Result:
case H.h
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
inst✝⁴ : Semiring R
inst✝³ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝² : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝¹ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝ : (p : (i : ι) → κ i) → Module R (N p)
f g : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
x✝ : (i : ι) → Π₀ (j : κ i), M i j
i✝ : (i : ι) → κ i
⊢ ((dfinsuppFamily (f + g)) x✝) i✝ = ((dfinsuppFamily f + dfinsuppFamily g) x✝) i✝
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma baseChange_Φ (n : ℤ) : (W.baseChange B).Φ n = ((W.baseChange A).Φ n).map f

Proof state:
R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ (W.baseChange B).Φ n = Polynomial.map (↑f) ((W.baseChange A).Φ n)

Tactic:
rw [← map_Φ, map_baseChange]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem volume_fundamentalDomain_stdBasis :
    volume (fundamentalDomain (stdBasis K)) = 1

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ volume (fundamentalDomain (stdBasis K)) = 1

Tactic:
rw [fundamentalDomain_stdBasis, volume_eq_prod, prod_prod, volume_pi, volume_pi, pi_pi, pi_pi,
  Complex.volume_preserving_equiv_pi.measure_preimage ?_, volume_pi, pi_pi, Real.volume_Ico,
  sub_zero, ENNReal.ofReal_one, prod_const_one, prod_const_one, prod_const_one, one_mul]

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ NullMeasurableSet (Set.univ.pi fun x => Set.Ico 0 1) volume

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ NullMeasurableSet (Set.univ.pi fun x => Set.Ico 0 1) volume

Tactic:
exact (MeasurableSet.pi Set.countable_univ (fun _ _ => measurableSet_Ico)).nullMeasurableSet

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_one_div_of_pos (ha : 0 < a) (hb : 0 < b) :
    ∫ x : ℝ in a..b, 1 / x = log (b / a)

Proof state:
a b : ℝ
ha : 0 < a
hb : 0 < b
⊢ ∫ (x : ℝ) in a..b, 1 / x = log (b / a)

Tactic:
simp only [one_div, integral_inv_of_pos ha hb]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToL1SCLM_congr_left (hT : DominatedFinMeasAdditive μ T C)
    (hT' : DominatedFinMeasAdditive μ T' C') (h : T = T') (f : α →₁ₛ[μ] E) :
    setToL1SCLM α E μ hT f = setToL1SCLM α E μ hT' f :=
  setToL1S_congr_left T T' (fun _ _ _ => by rw [h]) f

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : T = T'
f : ↥(simpleFunc E 1 μ)
x✝² : Set α
x✝¹ : MeasurableSet x✝²
x✝ : μ x✝² < ⊤
⊢ T x✝² = T' x✝²

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
lemma neg_negPart_le {a : A} (ha : IsSelfAdjoint a

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ -a⁻ ≤ a

Tactic:
simpa only [posPart_sub_negPart a, ← sub_eq_add_neg]
  using le_add_of_nonneg_left (a := -a⁻) (posPart_nonneg a)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem tendsto_normalize_of_tendsto {γ : Type*} {F : Filter γ} {μs : γ → FiniteMeasure Ω}
    (μs_lim : Tendsto μs F (𝓝 μ)) (nonzero : μ ≠ 0) :
    Tendsto (fun i ↦ (μs i).normalize) F (𝓝 μ.normalize)

Proof state:
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
⊢ ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun i => ((ProbabilityMeasure.toFiniteMeasure ∘ fun i => (μs i).normalize) i).testAgainstNN f) F
      (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))

Tactic:
exact fun f ↦ tendsto_normalize_testAgainstNN_of_tendsto μs_lim nonzero f

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
⊢ Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize)

Tactic:
rw [ProbabilityMeasure.tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds,
  tendsto_iff_forall_testAgainstNN_tendsto]

Result:
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto μs F (𝓝 μ)
nonzero : μ ≠ 0
⊢ ∀ (f : Ω →ᵇ ℝ≥0),
    Tendsto (fun i => ((ProbabilityMeasure.toFiniteMeasure ∘ fun i => (μs i).normalize) i).testAgainstNN f) F
      (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))
-- Mathlib/Analysis/Convex/EGauge.lean
lemma egauge_union (s t : Set E) (x : E) : egauge 𝕜 (s ∪ t) x = egauge 𝕜 s x ⊓ egauge 𝕜 t x

Proof state:
𝕜 : Type u_1
inst✝¹ : NNNorm 𝕜
E : Type u_2
inst✝ : SMul 𝕜 E
s t : Set E
x : E
⊢ egauge 𝕜 (s ∪ t) x = egauge 𝕜 s x ⊓ egauge 𝕜 t x

Tactic:
unfold egauge

Result:
𝕜 : Type u_1
inst✝¹ : NNNorm 𝕜
E : Type u_2
inst✝ : SMul 𝕜 E
s t : Set E
x : E
⊢ ⨅ c, ⨅ (_ : x ∈ c • (s ∪ t)), ‖c‖ₑ = (⨅ c, ⨅ (_ : x ∈ c • s), ‖c‖ₑ) ⊓ ⨅ c, ⨅ (_ : x ∈ c • t), ‖c‖ₑ

Proof state:
𝕜 : Type u_1
inst✝¹ : NNNorm 𝕜
E : Type u_2
inst✝ : SMul 𝕜 E
s t : Set E
x : E
⊢ ⨅ c, ⨅ (_ : x ∈ c • (s ∪ t)), ‖c‖ₑ = (⨅ c, ⨅ (_ : x ∈ c • s), ‖c‖ₑ) ⊓ ⨅ c, ⨅ (_ : x ∈ c • t), ‖c‖ₑ

Tactic:
simp [smul_set_union, iInf_or, iInf_inf_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem pentagon_hom_hom_inv_inv_hom (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
    (α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv =
      (α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom :=
  eq_of_inv_eq_inv (by simp)

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ f (g ≫ h) i).hom ≫ f ◁ (α_ g h i).hom ≫ (α_ f g (h ≫ i)).inv) =
    inv ((α_ f g h).inv ▷ i ≫ (α_ (f ≫ g) h i).hom)

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/Jacobian.lean
lemma _root_.MeasurableEmbedding.withDensity_ofReal_comap_apply_eq_integral_abs_det_fderiv_mul
    (hs : MeasurableSet s) (hf : MeasurableEmbedding f)
    {g : E → ℝ} (hg : ∀ᵐ x ∂μ, x ∈ f '' s → 0 ≤ g x) (hg_int : IntegrableOn g (f '' s) μ)
    (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :
    (μ.withDensity (fun x ↦ ENNReal.ofReal (g x))).comap f s
      = ENNReal.ofReal (∫ x in s, |(f' x).det| * g (f x) ∂μ)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf : MeasurableEmbedding f
g : E → ℝ
hg : ∀ᵐ (x : E) ∂μ, x ∈ f '' s → 0 ≤ g x
hg_int : IntegrableOn g (f '' s) μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ (Measure.comap f (μ.withDensity fun x => ENNReal.ofReal (g x))) s =
    ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g (f x) ∂μ)

Tactic:
rw [Measure.comap_apply f hf.injective (fun t ht ↦ hf.measurableSet_image' ht) _ hs,
  withDensity_apply _ (hf.measurableSet_image' hs),
  ← ofReal_integral_eq_lintegral_ofReal hg_int
    ((ae_restrict_iff' (hf.measurableSet_image' hs)).mpr hg),
  integral_image_eq_integral_abs_det_fderiv_smul μ hs hf' hf.injective.injOn]

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf : MeasurableEmbedding f
g : E → ℝ
hg : ∀ᵐ (x : E) ∂μ, x ∈ f '' s → 0 ≤ g x
hg_int : IntegrableOn g (f '' s) μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| • g (f x) ∂μ) =
    ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g (f x) ∂μ)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : FiniteDimensional ℝ E
s : Set E
f : E → E
f' : E → E →L[ℝ] E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
hs : MeasurableSet s
hf : MeasurableEmbedding f
g : E → ℝ
hg : ∀ᵐ (x : E) ∂μ, x ∈ f '' s → 0 ≤ g x
hg_int : IntegrableOn g (f '' s) μ
hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| • g (f x) ∂μ) =
    ENNReal.ofReal (∫ (x : E) in s, |(f' x).det| * g (f x) ∂μ)

Tactic:
simp_rw [smul_eq_mul]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem cthickening_eq_iInter_thickening {δ : ℝ} (δ_nn : 0 ≤ δ) (E : Set α) :
    cthickening δ E = ⋂ (ε : ℝ) (_ : δ < ε), thickening ε E

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ cthickening δ E = ⋂ ε, ⋂ (_ : δ < ε), thickening ε E

Tactic:
apply cthickening_eq_iInter_thickening' δ_nn (Ioi δ) rfl.subset

Result:
case hs
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → (Ioi δ ∩ Ioc δ ε).Nonempty

Proof state:
case hs
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → (Ioc δ ε).Nonempty

Tactic:
exact fun _ hε => nonempty_Ioc.mpr hε

Result:
no goals

Proof state:
case hs
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → (Ioi δ ∩ Ioc δ ε).Nonempty

Tactic:
simp_rw [inter_eq_right.mpr Ioc_subset_Ioi_self]

Result:
case hs
α : Type u
inst✝ : PseudoEMetricSpace α
δ : ℝ
δ_nn : 0 ≤ δ
E : Set α
⊢ ∀ (ε : ℝ), δ < ε → (Ioc δ ε).Nonempty
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem pos_iff_ne_zero {a : Fin (n + 1)} : 0 < a ↔ a ≠ 0

Proof state:
n : Nat
a : Fin (n + 1)
⊢ 0 < a ↔ a ≠ 0

Tactic:
rw [lt_def, val_zero, Nat.pos_iff_ne_zero, ← val_ne_iff]

Result:
n : Nat
a : Fin (n + 1)
⊢ ↑a ≠ 0 ↔ ↑a ≠ ↑0

Proof state:
n : Nat
a : Fin (n + 1)
⊢ ↑a ≠ 0 ↔ ↑a ≠ ↑0

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem foldl_eq (f : δ → α → β → δ) (init l) :
    foldl f init l = l.toList.foldl (fun d (a, b) => f d a b) init

Proof state:
δ : Type u_1
α : Type u_2
β : Type u_3
f : δ → α → β → δ
init : δ
l : AssocList α β
⊢ foldl f init l =
    List.foldl
      (fun d x =>
        match x with
        | (a, b) => f d a b)
      init l.toList

Tactic:
simp [List.foldl_eq_foldlM, foldl, Id.run]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem induction_on [Semiring k] [Monoid G] {p : MonoidAlgebra k G → Prop} (f : MonoidAlgebra k G)
    (hM : ∀ g, p (of k G g)) (hadd : ∀ f g : MonoidAlgebra k G, p f → p g → p (f + g))
    (hsmul : ∀ (r : k) (f), p f → p (r • f)) : p f

Proof state:
case refine_1
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Monoid G
p : MonoidAlgebra k G → Prop
f : MonoidAlgebra k G
hM : ∀ (g : G), p ((of k G) g)
hadd : ∀ (f g : MonoidAlgebra k G), p f → p g → p (f + g)
hsmul : ∀ (r : k) (f : MonoidAlgebra k G), p f → p (r • f)
⊢ p 0

Tactic:
simpa using hsmul 0 (of k G 1) (hM 1)

Result:
no goals

Proof state:
case refine_2
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Monoid G
p : MonoidAlgebra k G → Prop
f : MonoidAlgebra k G
hM : ∀ (g : G), p ((of k G) g)
hadd : ∀ (f g : MonoidAlgebra k G), p f → p g → p (f + g)
hsmul : ∀ (r : k) (f : MonoidAlgebra k G), p f → p (r • f)
g : G
r : k
⊢ p (Finsupp.single g r)

Tactic:
convert hsmul r (of k G g) (hM g)

Result:
case h.e'_1
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Monoid G
p : MonoidAlgebra k G → Prop
f : MonoidAlgebra k G
hM : ∀ (g : G), p ((of k G) g)
hadd : ∀ (f g : MonoidAlgebra k G), p f → p g → p (f + g)
hsmul : ∀ (r : k) (f : MonoidAlgebra k G), p f → p (r • f)
g : G
r : k
⊢ Finsupp.single g r = r • (of k G) g

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Monoid G
p : MonoidAlgebra k G → Prop
f : MonoidAlgebra k G
hM : ∀ (g : G), p ((of k G) g)
hadd : ∀ (f g : MonoidAlgebra k G), p f → p g → p (f + g)
hsmul : ∀ (r : k) (f : MonoidAlgebra k G), p f → p (r • f)
⊢ p f

Tactic:
refine Finsupp.induction_linear f ?_ (fun f g hf hg => hadd f g hf hg) fun g r => ?_

Result:
case refine_1
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Monoid G
p : MonoidAlgebra k G → Prop
f : MonoidAlgebra k G
hM : ∀ (g : G), p ((of k G) g)
hadd : ∀ (f g : MonoidAlgebra k G), p f → p g → p (f + g)
hsmul : ∀ (r : k) (f : MonoidAlgebra k G), p f → p (r • f)
⊢ p 0

case refine_2
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Monoid G
p : MonoidAlgebra k G → Prop
f : MonoidAlgebra k G
hM : ∀ (g : G), p ((of k G) g)
hadd : ∀ (f g : MonoidAlgebra k G), p f → p g → p (f + g)
hsmul : ∀ (r : k) (f : MonoidAlgebra k G), p f → p (r • f)
g : G
r : k
⊢ p (Finsupp.single g r)

Proof state:
case h.e'_1
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : Monoid G
p : MonoidAlgebra k G → Prop
f : MonoidAlgebra k G
hM : ∀ (g : G), p ((of k G) g)
hadd : ∀ (f g : MonoidAlgebra k G), p f → p g → p (f + g)
hsmul : ∀ (r : k) (f : MonoidAlgebra k G), p f → p (r • f)
g : G
r : k
⊢ Finsupp.single g r = r • (of k G) g

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc]
lemma μ_comp (X Y : C) :
    LaxMonoidal.μ (F ⋙ G) X Y = LaxMonoidal.μ G _ _ ≫ G.map (LaxMonoidal.μ F X Y)

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : ChosenFiniteProducts C
D : Type u₁
inst✝⁵ : Category.{v₁, u₁} D
inst✝⁴ : ChosenFiniteProducts D
F : C ⥤ D
inst✝³ : PreservesFiniteProducts F
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : ChosenFiniteProducts E
G : D ⥤ E
inst✝ : PreservesFiniteProducts G
X Y : C
⊢ LaxMonoidal.μ (F ⋙ G) X Y ≫ (μIso (F ⋙ G) X Y).inv =
    (LaxMonoidal.μ G (F.obj X) (F.obj Y) ≫ G.map (LaxMonoidal.μ F X Y)) ≫ (μIso (F ⋙ G) X Y).inv

Tactic:
apply ChosenFiniteProducts.hom_ext <;> simp [← Functor.comp_obj, ← Functor.map_comp]

Result:
no goals

Proof state:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : ChosenFiniteProducts C
D : Type u₁
inst✝⁵ : Category.{v₁, u₁} D
inst✝⁴ : ChosenFiniteProducts D
F : C ⥤ D
inst✝³ : PreservesFiniteProducts F
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : ChosenFiniteProducts E
G : D ⥤ E
inst✝ : PreservesFiniteProducts G
X Y : C
⊢ LaxMonoidal.μ (F ⋙ G) X Y = LaxMonoidal.μ G (F.obj X) (F.obj Y) ≫ G.map (LaxMonoidal.μ F X Y)

Tactic:
apply (cancel_mono (μIso _ _ _).inv).1

Result:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : ChosenFiniteProducts C
D : Type u₁
inst✝⁵ : Category.{v₁, u₁} D
inst✝⁴ : ChosenFiniteProducts D
F : C ⥤ D
inst✝³ : PreservesFiniteProducts F
E : Type u₂
inst✝² : Category.{v₂, u₂} E
inst✝¹ : ChosenFiniteProducts E
G : D ⥤ E
inst✝ : PreservesFiniteProducts G
X Y : C
⊢ LaxMonoidal.μ (F ⋙ G) X Y ≫ (μIso (F ⋙ G) X Y).inv =
    (LaxMonoidal.μ G (F.obj X) (F.obj Y) ≫ G.map (LaxMonoidal.μ F X Y)) ≫ (μIso (F ⋙ G) X Y).inv