harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/Jacobian.lean
theorem aemeasurable_ofReal_abs_det_fderivWithin (hs : MeasurableSet s)
    (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :
    AEMeasurable (fun x => ENNReal.ofReal |(f' x).det|) (μ.restrict s)

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' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ AEMeasurable (fun x => ENNReal.ofReal |(f' x).det|) (μ.restrict s)

Tactic:
apply ENNReal.measurable_ofReal.comp_aemeasurable

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' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ AEMeasurable (fun x => |(f' x).det|) (μ.restrict s)

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' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ AEMeasurable (fun x => |(f' x).det|) (μ.restrict s)

Tactic:
refine continuous_abs.measurable.comp_aemeasurable ?_

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' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ AEMeasurable (fun x => (f' x).det) (μ.restrict s)

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' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ AEMeasurable f' (μ.restrict s)

Tactic:
exact aemeasurable_fderivWithin μ hs hf'

Result:
no goals

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' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ AEMeasurable (fun x => (f' x).det) (μ.restrict s)

Tactic:
refine ContinuousLinearMap.continuous_det.measurable.comp_aemeasurable ?_

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' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x
⊢ AEMeasurable f' (μ.restrict s)
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem span_idealLatticeBasis :
    (Submodule.span ℤ (Set.range (fractionalIdealLatticeBasis K I))) =
      (mixedEmbedding.idealLattice K I)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ Submodule.span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I)) = idealLattice K I

Tactic:
ext x

Result:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ x ∈ Submodule.span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I)) ↔ x ∈ idealLattice K I

Proof state:
case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ x ∈ Submodule.span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I)) ↔ x ∈ idealLattice K I

Tactic:
simp [mem_span_fractionalIdealLatticeBasis]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
theorem le_prod_of_submultiplicative (f : M → N) (h_one : f 1 = 1)
    (h_mul : ∀ x y, f (x * y) ≤ f x * f y) (s : Finset ι) (g : ι → M) :
    f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
h_one : f 1 = 1
h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y
s : Finset ι
g : ι → M
⊢ (Multiset.map (f ∘ fun i => g i) s.val).prod ≤ ∏ i ∈ s, f (g i)

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
h_one : f 1 = 1
h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y
s : Finset ι
g : ι → M
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)

Tactic:
refine le_trans (Multiset.le_prod_of_submultiplicative f h_one h_mul _) ?_

Result:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
h_one : f 1 = 1
h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y
s : Finset ι
g : ι → M
⊢ (Multiset.map f (Multiset.map (fun i => g i) s.val)).prod ≤ ∏ i ∈ s, f (g i)

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
h_one : f 1 = 1
h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y
s : Finset ι
g : ι → M
⊢ (Multiset.map f (Multiset.map (fun i => g i) s.val)).prod ≤ ∏ i ∈ s, f (g i)

Tactic:
rw [Multiset.map_map]

Result:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : CommMonoid M
inst✝ : OrderedCommMonoid N
f : M → N
h_one : f 1 = 1
h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y
s : Finset ι
g : ι → M
⊢ (Multiset.map (f ∘ fun i => g i) s.val).prod ≤ ∏ i ∈ s, f (g i)
-- Mathlib/Topology/Constructions.lean
theorem isOpenMap_inr : IsOpenMap (@inr X Y) := fun u hu => by
  simpa [isOpen_sum_iff, preimage_image_eq u Sum.inr_injective]

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
u : Set Y
hu : IsOpen u
⊢ IsOpen (inr '' u)

Tactic:
simpa [isOpen_sum_iff, preimage_image_eq u Sum.inr_injective]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Conjneg.lean
@[simp] lemma conjneg_neg' : conjneg f < 0 ↔ f < 0

Proof state:
G : Type u_1
R : Type u_2
inst✝³ : AddGroup G
inst✝² : OrderedCommRing R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
f : G → R
⊢ conjneg f < 0 ↔ f < 0

Tactic:
simp_rw [← neg_pos, ← conjneg_neg, conjneg_pos]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_singleton (a : α) : countP p #v[a] = if p a then 1 else 0

Proof state:
α : Type u_1
p : α → Bool
a : α
⊢ countP p { toArray := #[a], size_toArray := ⋯ } = if p a = true then 1 else 0

Tactic:
simp [countP_push]

Result:
no goals
-- Mathlib/Logic/Equiv/Set.lean
theorem ofLeftInverse_eq_ofInjective {α β : Type*} (f : α → β) (f_inv : Nonempty α → β → α)
    (hf : ∀ h : Nonempty α, LeftInverse (f_inv h) f) :
    ofLeftInverse f f_inv hf =
      ofInjective f ((isEmpty_or_nonempty α).elim (fun _ _ _ _ => Subsingleton.elim _ _)
        (fun h => (hf h).injective))

Proof state:
α : Type u_1
β : Type u_2
f : α → β
f_inv : Nonempty α → β → α
hf : ∀ (h : Nonempty α), LeftInverse (f_inv h) f
⊢ ofLeftInverse f f_inv hf = ofInjective f ⋯

Tactic:
ext

Result:
case H.a
α : Type u_1
β : Type u_2
f : α → β
f_inv : Nonempty α → β → α
hf : ∀ (h : Nonempty α), LeftInverse (f_inv h) f
x✝ : α
⊢ ↑((ofLeftInverse f f_inv hf) x✝) = ↑((ofInjective f ⋯) x✝)

Proof state:
case H.a
α : Type u_1
β : Type u_2
f : α → β
f_inv : Nonempty α → β → α
hf : ∀ (h : Nonempty α), LeftInverse (f_inv h) f
x✝ : α
⊢ ↑((ofLeftInverse f f_inv hf) x✝) = ↑((ofInjective f ⋯) x✝)

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean
/-- If the indicator functions of a.e.-measurable sets `Aᵢ` converge a.e. to the indicator function
of a set `A` along a nontrivial countably generated filter, then `A` is also a.e.-measurable. -/
lemma nullMeasurableSet_of_tendsto_indicator [NeBot L] {μ : Measure α}
    (As_mble : ∀ i, NullMeasurableSet (As i) μ)
    (h_lim : ∀ᵐ x ∂μ, ∀ᶠ i in L, x ∈ As i ↔ x ∈ A) :
    NullMeasurableSet A μ

Proof state:
α : Type u_3
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
inst✝ : L.NeBot
μ : Measure α
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
As_mble : ∀ (i : ι), AEMeasurable ((As i).indicator fun x => 1) μ
⊢ AEMeasurable (A.indicator fun x => 1) μ

Tactic:
apply aemeasurable_of_tendsto_metrizable_ae L As_mble

Result:
α : Type u_3
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
inst✝ : L.NeBot
μ : Measure α
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
As_mble : ∀ (i : ι), AEMeasurable ((As i).indicator fun x => 1) μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => (As n).indicator (fun x => 1) x) L (𝓝 (A.indicator (fun x => 1) x))

Proof state:
α : Type u_3
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
inst✝ : L.NeBot
μ : Measure α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
⊢ NullMeasurableSet A μ

Tactic:
simp_rw [← aemeasurable_indicator_const_iff (1 : ℝ≥0∞)] at As_mble ⊢

Result:
α : Type u_3
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
inst✝ : L.NeBot
μ : Measure α
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
As_mble : ∀ (i : ι), AEMeasurable ((As i).indicator fun x => 1) μ
⊢ AEMeasurable (A.indicator fun x => 1) μ

Proof state:
α : Type u_3
inst✝² : MeasurableSpace α
A : Set α
ι : Type u_4
L : Filter ι
inst✝¹ : L.IsCountablyGenerated
As : ι → Set α
inst✝ : L.NeBot
μ : Measure α
h_lim : ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A
As_mble : ∀ (i : ι), AEMeasurable ((As i).indicator fun x => 1) μ
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => (As n).indicator (fun x => 1) x) L (𝓝 (A.indicator (fun x => 1) x))

Tactic:
simpa [tendsto_indicator_const_apply_iff_eventually] using h_lim

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem vec2_eq {a₀ a₁ b₀ b₁ : α} (h₀ : a₀ = b₀) (h₁ : a₁ = b₁) : ![a₀, a₁] = ![b₀, b₁]

Proof state:
α : Type u
a₀ a₁ b₀ b₁ : α
h₀ : a₀ = b₀
h₁ : a₁ = b₁
⊢ ![a₀, a₁] = ![b₀, b₁]

Tactic:
subst_vars

Result:
α : Type u
b₀ b₁ : α
⊢ ![b₀, b₁] = ![b₀, b₁]

Proof state:
α : Type u
b₀ b₁ : α
⊢ ![b₀, b₁] = ![b₀, b₁]

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
lemma pmap_eq_map {P : α → Prop} (f : α → β) (z : Sym2 α) (h : ∀ a ∈ z, P a) :
    z.pmap (fun a _ => f a) h = z.map f

Proof state:
case h
α : Type u_1
β : Type u_2
P : α → Prop
f : α → β
x y : α
h : ∀ a ∈ s(x, y), P a
⊢ pmap (fun a x => f a) s(x, y) h = map f s(x, y)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
P : α → Prop
f : α → β
z : Sym2 α
h : ∀ a ∈ z, P a
⊢ pmap (fun a x => f a) z h = map f z

Tactic:
induction' z with x y

Result:
case h
α : Type u_1
β : Type u_2
P : α → Prop
f : α → β
x y : α
h : ∀ a ∈ s(x, y), P a
⊢ pmap (fun a x => f a) s(x, y) h = map f s(x, y)
-- Mathlib/SetTheory/Game/PGame.lean
theorem le_or_gf (x y : PGame) : x ≤ y ∨ y ⧏ x

Proof state:
x y : PGame
⊢ x ≤ y ∨ ¬x ≤ y

Tactic:
apply em

Result:
no goals

Proof state:
x y : PGame
⊢ x ≤ y ∨ y ⧏ x

Tactic:
rw [← PGame.not_le]

Result:
x y : PGame
⊢ x ≤ y ∨ ¬x ≤ y
-- Mathlib/CategoryTheory/Abelian/GrothendieckCategory/ColimCoyoneda.lean
lemma epi_f [IsFiltered J] : Epi (f y)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
inst✝ : IsFiltered J
⊢ Epi (f y)

Tactic:
exact (colim.exact_mapShortComplex
  ((ShortComplex.mk _ _ (kernel.condition (g y))).exact_of_f_is_kernel
    (kernelIsKernel (g y)))
  (colimit.isColimit _) (isColimitConstCocone _ _)
  ((Functor.Final.isColimitWhiskerEquiv (Under.forget j₀) c).symm hc) (f y) 0
  (fun j ↦ by simpa using hf y j)
  (fun _ ↦ by simpa using hy.symm)).epi_f rfl

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
inst✝ : IsFiltered J
j : Under j₀
⊢ (colimit.cocone (ShortComplex.mk (kernel.ι (g y)) (g y) ⋯).X₁).ι.app j ≫ f y =
    (ShortComplex.mk (kernel.ι (g y)) (g y) ⋯).f.app j ≫ (constCocone (Under j₀) X).ι.app j

Tactic:
simpa using hf y j

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : IsGrothendieckAbelian.{w, v, u} C
X : C
J : Type w
inst✝¹ : SmallCategory J
Y : J ⥤ C
c : Cocone Y
hc : IsColimit c
j₀ : J
y : X ⟶ Y.obj j₀
hy : y ≫ c.ι.app j₀ = 0
inst✝ : IsFiltered J
x✝ : Under j₀
⊢ (constCocone (Under j₀) X).ι.app x✝ ≫ 0 =
    (ShortComplex.mk (kernel.ι (g y)) (g y) ⋯).g.app x✝ ≫ (Cocone.whisker (Under.forget j₀) c).ι.app x✝

Tactic:
simpa using hy.symm

Result:
no goals
-- Mathlib/Data/ENNReal/Action.lean
theorem smul_top {R} [Zero R] [SMulWithZero R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞]
    [NoZeroSMulDivisors R ℝ≥0∞] [DecidableEq R] (c : R) :
    c • ∞ = if c = 0 then 0 else ∞

Proof state:
R : Type u_1
inst✝⁴ : Zero R
inst✝³ : SMulWithZero R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : NoZeroSMulDivisors R ℝ≥0∞
inst✝ : DecidableEq R
c : R
⊢ c • ⊤ = if c = 0 then 0 else ⊤

Tactic:
rw [← smul_one_mul, mul_top']

Result:
R : Type u_1
inst✝⁴ : Zero R
inst✝³ : SMulWithZero R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : NoZeroSMulDivisors R ℝ≥0∞
inst✝ : DecidableEq R
c : R
⊢ (if c • 1 = 0 then 0 else ⊤) = if c = 0 then 0 else ⊤

Proof state:
R : Type u_1
inst✝⁴ : Zero R
inst✝³ : SMulWithZero R ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : NoZeroSMulDivisors R ℝ≥0∞
inst✝ : DecidableEq R
c : R
⊢ (if c • 1 = 0 then 0 else ⊤) = if c = 0 then 0 else ⊤

Tactic:
simp_rw [smul_eq_zero, or_iff_left (one_ne_zero' ℝ≥0∞)]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem NormedCommGroup.nhds_basis_norm_lt (x : E) :
    (𝓝 x).HasBasis (fun ε : ℝ => 0 < ε) fun ε => { y | ‖y / x‖ < ε }

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x : E
⊢ (𝓝 x).HasBasis (fun ε => 0 < ε) fun ε => ball x ε

Tactic:
exact Metric.nhds_basis_ball

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x : E
⊢ (𝓝 x).HasBasis (fun ε => 0 < ε) fun ε => {y | ‖y / x‖ < ε}

Tactic:
simp_rw [← ball_eq']

Result:
E : Type u_5
inst✝ : SeminormedGroup E
x : E
⊢ (𝓝 x).HasBasis (fun ε => 0 < ε) fun ε => ball x ε
-- Mathlib/Data/List/Indexes.lean
theorem foldlIdx_eq_foldl_enum (f : ℕ → α → β → α) (a : α) (bs : List β) :
    foldlIdx f a bs = foldl (fun a p ↦ f p.fst a p.snd) a (enum bs)

Proof state:
α : Type u
β : Type v
f : ℕ → α → β → α
a : α
bs : List β
⊢ foldlIdx f a bs = foldl (fun a p => f p.fst a p.snd) a bs.enum

Tactic:
simp only [foldlIdx, foldlIdxSpec, foldlIdx_eq_foldlIdxSpec, enum]

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
protected lemma existsUnique_congr' (h : ∀ b, p (e.symm b) ↔ q b) : (∃! a, p a) ↔ ∃! b, q b :=
  e.existsUnique_congr_left.trans <| by simp [h]

Proof state:
α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (b : β), p (e.symm b) ↔ q b
⊢ (∃! b, p (e.symm b)) ↔ ∃! b, q b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem rel_bind {r : α → β → Prop} {p : γ → δ → Prop} {s t} {f : α → Multiset γ}
    {g : β → Multiset δ} (h : (r ⇒ Rel p) f g) (hst : Rel r s t) :
    Rel p (s.bind f) (t.bind g)

Proof state:
case h
α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (Rel p) (map f s) (map g t)

Tactic:
rw [rel_map]

Result:
case h
α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (fun a b => Rel p (f a) (g b)) s t

Proof state:
case h
α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (fun a b => Rel p (f a) (g b)) s t

Tactic:
exact hst.mono fun a _ b _ hr => h hr

Result:
no goals

Proof state:
α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel p (s.bind f) (t.bind g)

Tactic:
apply rel_join

Result:
case h
α : Type u_1
β : Type v
γ : Type u_2
δ : Type u_3
r : α → β → Prop
p : γ → δ → Prop
s : Multiset α
t : Multiset β
f : α → Multiset γ
g : β → Multiset δ
h : (r ⇒ Rel p) f g
hst : Rel r s t
⊢ Rel (Rel p) (map f s) (map g t)
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem add_lt_of_lt {a b c : Cardinal} (hc : ℵ₀ ≤ c) (h1 : a < c) (h2 : b < c) : a + b < c :=
  (add_le_add (le_max_left a b) (le_max_right a b)).trans_lt <|
    (lt_or_le (max a b) ℵ₀).elim (fun h => (add_lt_aleph0 h h).trans_le hc) fun h => by
      rw [add_eq_self h]; exact max_lt h1 h2

Proof state:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
h1 : a < c
h2 : b < c
h : ℵ₀ ≤ a ⊔ b
⊢ a ⊔ b + a ⊔ b < c

Tactic:
rw [add_eq_self h]

Result:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
h1 : a < c
h2 : b < c
h : ℵ₀ ≤ a ⊔ b
⊢ a ⊔ b < c

Proof state:
a b c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
h1 : a < c
h2 : b < c
h : ℵ₀ ≤ a ⊔ b
⊢ a ⊔ b < c

Tactic:
exact max_lt h1 h2

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplexSymmetry.lean
@[reassoc (attr := simp)]
lemma ιTotal_totalFlipIso_f_inv
    (i₁ : I₁) (i₂ : I₂) (j : J) (h : ComplexShape.π c₁ c₂ c (i₁, i₂) = j) :
    K.ιTotal c i₁ i₂ j h ≫ (K.totalFlipIso c).inv.f j =
      ComplexShape.σ c₁ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j
        (by rw [ComplexShape.π_symm c₁ c₂ c i₁ i₂, h])

Proof state:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{u_5, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
i₁ : I₁
i₂ : I₂
j : J
h : c₁.π c₂ c (i₁, i₂) = j
⊢ K.ιTotal c i₁ i₂ j h ≫ (K.totalFlipIso c).inv.f j = c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯

Tactic:
simp [totalFlipIso, totalFlipIsoX]

Result:
no goals

Proof state:
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{?u.44019, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
i₁ : I₁
i₂ : I₂
j : J
h : c₁.π c₂ c (i₁, i₂) = j
⊢ c₂.π c₁ c (i₂, i₁) = j

Tactic:
rw [ComplexShape.π_symm c₁ c₂ c i₁ i₂, h]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
lemma lTensor.inverse_of_rightInverse_comp_lTensor
    {h : P → N} (hgh : Function.RightInverse h g) :
    (lTensor.inverse_of_rightInverse Q hfg hgh).comp (lTensor Q g) =
      Submodule.mkQ (p := LinearMap.range (lTensor Q f))

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
⊢ (inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g) y = (range (lTensor Q f)).mkQ y

Tactic:
simp only [coe_comp, Function.comp_apply, Submodule.mkQ_apply,
  lTensor.inverse_of_rightInverse_apply]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
⊢ ∀ (x : Q ⊗[R] N), (inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g) x = (range (lTensor Q f)).mkQ x

Tactic:
intro y

Result:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
y : Q ⊗[R] N
⊢ (inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g) y = (range (lTensor Q f)).mkQ y

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
⊢ inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g = (range (lTensor Q f)).mkQ

Tactic:
rw [LinearMap.ext_iff]

Result:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
h : P → N
hgh : RightInverse h ⇑g
⊢ ∀ (x : Q ⊗[R] N), (inverse_of_rightInverse Q hfg hgh ∘ₗ lTensor Q g) x = (range (lTensor Q f)).mkQ x
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_lt_logb_iff_of_base_lt_one (hx : 0 < x) (hy : 0 < y) :
    logb b x < logb b y ↔ y < x

Proof state:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hy : 0 < y
⊢ log y < log x ↔ y < x

Tactic:
exact log_lt_log_iff hy hx

Result:
no goals

Proof state:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hy : 0 < y
⊢ logb b x < logb b y ↔ y < x

Tactic:
rw [logb, logb, div_lt_div_right_of_neg (log_neg b_pos b_lt_one)]

Result:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hy : 0 < y
⊢ log y < log x ↔ y < x
-- Mathlib/RingTheory/MvPolynomial/Homogeneous.lean
theorem isHomogeneous_monomial {d : σ →₀ ℕ} (r : R) {n : ℕ} (hn : d.degree = n) :
    IsHomogeneous (monomial d r) n

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : d.degree = n
⊢ ((monomial d) r).IsHomogeneous n

Tactic:
rw [degree_eq_weight_one] at hn

Result:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : (weight fun x => 1) d = n
⊢ ((monomial d) r).IsHomogeneous n

Proof state:
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : (weight fun x => 1) d = n
⊢ ((monomial d) r).IsHomogeneous n

Tactic:
exact isWeightedHomogeneous_monomial 1 d r hn

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem intCast_comp_cast : ((↑) : ℤ → R) ∘ (cast : ZMod n → ℤ) = cast

Proof state:
n : ℕ
R : Type u_1
inst✝ : Ring R
⊢ Int.cast ∘ cast = cast

Tactic:
cases n

Result:
case zero
R : Type u_1
inst✝ : Ring R
⊢ Int.cast ∘ cast = cast

case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
⊢ Int.cast ∘ cast = cast

Proof state:
case succ
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
⊢ Int.cast ∘ cast = cast

Tactic:
ext

Result:
case succ.h
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
x✝ : ZMod (n✝ + 1)
⊢ (Int.cast ∘ cast) x✝ = x✝.cast

Proof state:
case succ.h
R : Type u_1
inst✝ : Ring R
n✝ : ℕ
x✝ : ZMod (n✝ + 1)
⊢ (Int.cast ∘ cast) x✝ = x✝.cast

Tactic:
simp [ZMod, ZMod.cast]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
@[to_additive]
protected lemma div_eq_div_iff (hb : IsUnit b) (hd : IsUnit d) :
    a / b = c / d ↔ a * d = c * b

Proof state:
α : Type u
inst✝ : DivisionCommMonoid α
a b c d : α
hb : IsUnit b
hd : IsUnit d
⊢ a / b = c / d ↔ a * d = c * b

Tactic:
rw [← (hb.mul hd).mul_left_inj, ← mul_assoc, hb.div_mul_cancel, ← mul_assoc, mul_right_comm,
  hd.div_mul_cancel]

Result:
no goals