harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
theorem closure_toSubmonoid (S : Set G) :
    (closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹)

Proof state:
case refine_2
G : Type u_2
inst✝ : Group G
S : Set G
⊢ S ∪ S⁻¹ ⊆ ↑(closure S).toSubmonoid

Tactic:
simp only [true_and, coe_toSubmonoid, union_subset_iff, subset_closure, inv_subset_closure]

Result:
no goals

Proof state:
G : Type u_2
inst✝ : Group G
S : Set G
⊢ (closure S).toSubmonoid = Submonoid.closure (S ∪ S⁻¹)

Tactic:
refine le_antisymm (fun x hx => ?_) (Submonoid.closure_le.2 ?_)

Result:
case refine_1
G : Type u_2
inst✝ : Group G
S : Set G
x : G
hx : x ∈ (closure S).toSubmonoid
⊢ x ∈ Submonoid.closure (S ∪ S⁻¹)

case refine_2
G : Type u_2
inst✝ : Group G
S : Set G
⊢ S ∪ S⁻¹ ⊆ ↑(closure S).toSubmonoid

Proof state:
case refine_1
G : Type u_2
inst✝ : Group G
S : Set G
x✝¹ : G
hx✝ : x✝¹ ∈ (closure S).toSubmonoid
x : G
x✝ : x ∈ closure S
hx : x ∈ Submonoid.closure (S ∪ S⁻¹)
⊢ x⁻¹ ∈ Submonoid.closure (S ∪ S⁻¹)

Tactic:
rwa [← Submonoid.mem_closure_inv, Set.union_inv, inv_inv, Set.union_comm]

Result:
no goals

Proof state:
case refine_1
G : Type u_2
inst✝ : Group G
S : Set G
x : G
hx : x ∈ (closure S).toSubmonoid
⊢ x ∈ Submonoid.closure (S ∪ S⁻¹)

Tactic:
refine
  closure_induction
    (fun x hx => Submonoid.closure_mono subset_union_left (Submonoid.subset_closure hx))
    (Submonoid.one_mem _) (fun x y _ _ hx hy => Submonoid.mul_mem _ hx hy) (fun x _ hx => ?_) hx

Result:
case refine_1
G : Type u_2
inst✝ : Group G
S : Set G
x✝¹ : G
hx✝ : x✝¹ ∈ (closure S).toSubmonoid
x : G
x✝ : x ∈ closure S
hx : x ∈ Submonoid.closure (S ∪ S⁻¹)
⊢ x⁻¹ ∈ Submonoid.closure (S ∪ S⁻¹)
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem cos_angle_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2) :
    Real.cos (∠ p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ Real.cos (∠ p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃

Tactic:
rw [angle, dist_eq_norm_vsub' V p₃ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
  add_comm, cos_angle_add_of_inner_eq_zero h]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
⊢ Real.cos (∠ p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
  inner_neg_left, neg_vsub_eq_vsub_rev] at h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ Real.cos (∠ p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃
-- Mathlib/MeasureTheory/Measure/Restrict.lean
lemma AbsolutelyContinuous.restrict (h : μ ≪ ν) (s : Set α) : μ.restrict s ≪ ν.restrict s

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
s t : Set α
ht : MeasurableSet t
htν : ν (t ∩ s) = 0
⊢ μ (t ∩ s) = 0

Tactic:
exact h htν

Result:
no goals

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
s t : Set α
ht : MeasurableSet t
htν : (ν.restrict s) t = 0
⊢ (μ.restrict s) t = 0

Tactic:
rw [restrict_apply ht] at htν ⊢

Result:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
s t : Set α
ht : MeasurableSet t
htν : ν (t ∩ s) = 0
⊢ μ (t ∩ s) = 0

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
s : Set α
⊢ μ.restrict s ≪ ν.restrict s

Tactic:
refine Measure.AbsolutelyContinuous.mk (fun t ht htν ↦ ?_)

Result:
α : Type u_2
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
s t : Set α
ht : MeasurableSet t
htν : (ν.restrict s) t = 0
⊢ (μ.restrict s) t = 0
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
theorem closure_induction_right {p : (x : G) → x ∈ closure s → Prop} (one : p 1 (one_mem _))
    (mul_right : ∀ (x) hx, ∀ y (hy : y ∈ s), p x hx → p (x * y) (mul_mem hx (subset_closure hy)))
    (mul_inv_cancel : ∀ (x) hx, ∀ y (hy : y ∈ s), p x hx →
      p (x * y⁻¹) (mul_mem hx (inv_mem (subset_closure hy))))
    {x : G} (h : x ∈ closure s) : p x h :=
  closure_induction_left (s := MulOpposite.unop ⁻¹' s)
    (p := fun m hm => p m.unop <| by rwa [← op_closure] at hm)
    one
    (fun _x hx _y _ => mul_right _ _ _ hx)
    (fun _x hx _y _ => mul_inv_cancel _ _ _ hx)
    (by rwa [← op_closure])

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
mul_right : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯
mul_inv_cancel : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯
x : G
h : x ∈ closure s
⊢ { unop' := x } ∈ closure (MulOpposite.unop ⁻¹' s)

Tactic:
rwa [← op_closure]

Result:
no goals

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
mul_right : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯
mul_inv_cancel : ∀ (x : G) (hx : x ∈ closure s) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯
x : G
h : x ∈ closure s
m : Gᵐᵒᵖ
hm : m ∈ closure (MulOpposite.unop ⁻¹' s)
⊢ MulOpposite.unop m ∈ closure s

Tactic:
rwa [← op_closure] at hm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/SOM.lean
theorem Poly.add_denote (ctx : Context) (p₁ p₂ : Poly) : (p₁.add p₂).denote ctx = p₁.denote ctx + p₂.denote ctx :=
  go hugeFuel p₁ p₂
where
  go (fuel : Nat) (p₁ p₂ : Poly) : (Poly.add.go fuel p₁ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx

Proof state:
case neg
ctx : Context
p₁✝¹ p₂✝¹ : Poly
n✝ : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (add.go n✝ p₁ p₂) = denote ctx p₁ + denote ctx p₂
p₁✝ p₂✝ : Poly
k₁ : Nat
m₁ : Mon
p₁ : List (Nat × Mon)
k₂ : Nat
m₂ : Mon
p₂ : List (Nat × Mon)
hlt : ¬m₁ < m₂
⊢ denote ctx
      (bif decide (m₂ < m₁) then (k₂, m₂) :: add.go n✝ ((k₁, m₁) :: p₁) p₂
      else bif k₁ + k₂ == 0 then add.go n✝ p₁ p₂ else (k₁ + k₂, m₁) :: add.go n✝ p₁ p₂) =
    k₁ * Mon.denote ctx m₁ + (denote ctx p₁ + (k₂ * Mon.denote ctx m₂ + denote ctx p₂))

Tactic:
by_cases hgt : m₂ < m₁ <;> simp! [hgt, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, ih]

Result:
case neg
ctx : Context
p₁✝¹ p₂✝¹ : Poly
n✝ : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (add.go n✝ p₁ p₂) = denote ctx p₁ + denote ctx p₂
p₁✝ p₂✝ : Poly
k₁ : Nat
m₁ : Mon
p₁ : List (Nat × Mon)
k₂ : Nat
m₂ : Mon
p₂ : List (Nat × Mon)
hlt : ¬m₁ < m₂
hgt : ¬m₂ < m₁
⊢ denote ctx (bif k₁ + k₂ == 0 then add.go n✝ p₁ p₂ else (k₁ + k₂, m₁) :: add.go n✝ p₁ p₂) =
    k₁ * Mon.denote ctx m₁ + (k₂ * Mon.denote ctx m₂ + (denote ctx p₁ + denote ctx p₂))
-- Mathlib/RingTheory/WittVector/Complete.lean
theorem mem_span_p_iff_coeff_zero_eq_zero (x : 𝕎 k) :
    x ∈ (Ideal.span {(p : 𝕎 k)}) ↔ x.coeff 0 = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
⊢ x ∈ Ideal.span {↑p} ↔ x.coeff 0 = 0

Tactic:
simp_rw [Ideal.mem_span_singleton, dvd_def, mul_comm]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
⊢ (∃ c, x = c * ↑p) ↔ x.coeff 0 = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
⊢ (∃ c, x = c * ↑p) ↔ x.coeff 0 = 0

Tactic:
refine ⟨fun ⟨u, hu⟩ ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
x✝ : ∃ c, x = c * ↑p
u : 𝕎 k
hu : x = u * ↑p
⊢ x.coeff 0 = 0

case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
h : x.coeff 0 = 0
⊢ ∃ c, x = c * ↑p

Proof state:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
h : x.coeff 0 = 0
⊢ ∃ c, x = c * ↑p

Tactic:
use (frobeniusEquiv p k).symm (x.shift 1)

Result:
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
h : x.coeff 0 = 0
⊢ x = (frobeniusEquiv p k).symm (x.shift 1) * ↑p

Proof state:
case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
h : x.coeff 0 = 0
⊢ x = (frobeniusEquiv p k).symm (x.shift 1) * ↑p

Tactic:
calc
_ = verschiebung (x.shift 1) := by
  simpa using eq_iterate_verschiebung (n := 1) (by simp [h])
_ = _ := by
  rw [← verschiebung_frobenius, ← frobeniusEquiv_apply,
      RingEquiv.apply_symm_apply (frobeniusEquiv p k) _]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
h : x.coeff 0 = 0
⊢ ∀ i < 1, x.coeff i = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
h : x.coeff 0 = 0
⊢ verschiebung (x.shift 1) = (frobeniusEquiv p k).symm (x.shift 1) * ↑p

Tactic:
rw [← verschiebung_frobenius, ← frobeniusEquiv_apply,
    RingEquiv.apply_symm_apply (frobeniusEquiv p k) _]

Result:
no goals

Proof state:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
x✝ : ∃ c, x = c * ↑p
u : 𝕎 k
hu : x = u * ↑p
⊢ x.coeff 0 = 0

Tactic:
rw [hu, mul_charP_coeff_zero]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
h : x.coeff 0 = 0
⊢ x = verschiebung (x.shift 1)

Tactic:
simpa using eq_iterate_verschiebung (n := 1) (by simp [h])

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma div_mul_div_comm (a b c d : EReal) : a / b * (c / d) = a * c / (b * d)

Proof state:
a b c d : EReal
⊢ a / b * (c / d) = a * c / (b * d)

Tactic:
rw [← mul_div a, mul_comm b d, ← div_div c, ← mul_div_left_comm (c / d), mul_comm (a / b)]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem typein_ordinal (o : Ordinal.{u}) :
    @typein Ordinal (· < ·) _ o = Ordinal.lift.{u + 1} o

Proof state:
o : Ordinal.{u}
⊢ (typein fun x1 x2 => x1 < x2).toRelEmbedding o = lift.{u + 1, u} o

Tactic:
refine Quotient.inductionOn o ?_

Result:
o : Ordinal.{u}
⊢ ∀ (a : WellOrder), (typein fun x1 x2 => x1 < x2).toRelEmbedding ⟦a⟧ = lift.{u + 1, u} ⟦a⟧

Proof state:
case mk
o : Ordinal.{u}
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
⊢ (typein fun x1 x2 => x1 < x2).toRelEmbedding ⟦{ α := α, r := r, wo := wo }⟧ =
    lift.{u + 1, u} ⟦{ α := α, r := r, wo := wo }⟧

Tactic:
apply Quotient.sound

Result:
case mk.a
o : Ordinal.{u}
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
⊢ { α := { x // (fun x1 x2 => x1 < x2) x ⟦{ α := α, r := r, wo := wo }⟧ },
      r := Subrel (fun x1 x2 => x1 < x2) fun x => (fun x1 x2 => x1 < x2) x ⟦{ α := α, r := r, wo := wo }⟧, wo := ⋯ } ≈
    { α := ULift.{u + 1, u} { α := α, r := r, wo := wo }.α, r := ULift.down ⁻¹'o { α := α, r := r, wo := wo }.r,
      wo := ⋯ }

Proof state:
case mk.a
o : Ordinal.{u}
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
⊢ { α := { x // (fun x1 x2 => x1 < x2) x ⟦{ α := α, r := r, wo := wo }⟧ },
      r := Subrel (fun x1 x2 => x1 < x2) fun x => (fun x1 x2 => x1 < x2) x ⟦{ α := α, r := r, wo := wo }⟧, wo := ⋯ } ≈
    { α := ULift.{u + 1, u} { α := α, r := r, wo := wo }.α, r := ULift.down ⁻¹'o { α := α, r := r, wo := wo }.r,
      wo := ⋯ }

Tactic:
constructor

Result:
case mk.a.val
o : Ordinal.{u}
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
⊢ (Subrel (fun x1 x2 => x1 < x2) fun x => (fun x1 x2 => x1 < x2) x ⟦{ α := α, r := r, wo := wo }⟧) ≃r
    ULift.down ⁻¹'o { α := α, r := r, wo := wo }.r

Proof state:
o : Ordinal.{u}
⊢ ∀ (a : WellOrder), (typein fun x1 x2 => x1 < x2).toRelEmbedding ⟦a⟧ = lift.{u + 1, u} ⟦a⟧

Tactic:
rintro ⟨α, r, wo⟩

Result:
case mk
o : Ordinal.{u}
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
⊢ (typein fun x1 x2 => x1 < x2).toRelEmbedding ⟦{ α := α, r := r, wo := wo }⟧ =
    lift.{u + 1, u} ⟦{ α := α, r := r, wo := wo }⟧

Proof state:
case mk.a.val
o : Ordinal.{u}
α : Type u
r : α → α → Prop
wo : IsWellOrder α r
⊢ (Subrel (fun x1 x2 => x1 < x2) fun x => (fun x1 x2 => x1 < x2) x ⟦{ α := α, r := r, wo := wo }⟧) ≃r
    ULift.down ⁻¹'o { α := α, r := r, wo := wo }.r

Tactic:
refine ((RelIso.preimage Equiv.ulift r).trans (enum r).symm).symm

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem lintegral_withDensity_le_lintegral_mul (μ : Measure α) {f : α → ℝ≥0∞}
    (f_meas : Measurable f) (g : α → ℝ≥0∞) : (∫⁻ a, g a ∂μ.withDensity f) ≤ ∫⁻ a, (f * g) a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
⊢ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f ≤
    ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ

Tactic:
refine iSup₂_le fun i i_meas => iSup_le fun hi => ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ g
⊢ ∫⁻ (a : α), i a ∂μ.withDensity f ≤ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ g
A : f * i ≤ f * g
⊢ ∫⁻ (a : α), i a ∂μ.withDensity f ≤ ⨆ (_ : f * i ≤ f * g), ∫⁻ (a : α), (f * i) a ∂μ

Tactic:
exact le_iSup_of_le A (le_of_eq (lintegral_withDensity_eq_lintegral_mul _ f_meas i_meas))

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
⊢ ∫⁻ (a : α), g a ∂μ.withDensity f ≤ ∫⁻ (a : α), (f * g) a ∂μ

Tactic:
rw [← iSup_lintegral_measurable_le_eq_lintegral, ← iSup_lintegral_measurable_le_eq_lintegral]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g : α → ℝ≥0∞
⊢ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ g), ∫⁻ (a : α), g_1 a ∂μ.withDensity f ≤
    ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ g
⊢ ∫⁻ (a : α), i a ∂μ.withDensity f ≤ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ

Tactic:
have A : f * i ≤ f * g := fun x => mul_le_mul_left' (hi x) _

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ g
A : f * i ≤ f * g
⊢ ∫⁻ (a : α), i a ∂μ.withDensity f ≤ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ g
A : f * i ≤ f * g
⊢ ∫⁻ (a : α), i a ∂μ.withDensity f ≤ ⨆ g_1, ⨆ (_ : Measurable g_1), ⨆ (_ : g_1 ≤ f * g), ∫⁻ (a : α), g_1 a ∂μ

Tactic:
refine le_iSup₂_of_le (f * i) (f_meas.mul i_meas) ?_

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
f_meas : Measurable f
g i : α → ℝ≥0∞
i_meas : Measurable i
hi : i ≤ g
A : f * i ≤ f * g
⊢ ∫⁻ (a : α), i a ∂μ.withDensity f ≤ ⨆ (_ : f * i ≤ f * g), ∫⁻ (a : α), (f * i) a ∂μ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lex.lean
theorem lt_iff_exists [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : Vector α n} :
    l₁ < l₂ ↔
      (∃ (i : Nat) (h : i < n), (∀ j, (hj : j < i) → l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i])

Proof state:
α : Type u_1
n : Nat
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₁ l₂ : Vector α n
⊢ l₁ < l₂ ↔ ∃ i h, (∀ (j : Nat) (hj : j < i), l₁[j] = l₂[j]) ∧ l₁[i] < l₂[i]

Tactic:
cases l₁

Result:
case mk
α : Type u_1
n : Nat
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₂ : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ } < l₂ ↔
    ∃ i h,
      (∀ (j : Nat) (hj : j < i), { toArray := toArray✝, size_toArray := size_toArray✝ }[j] = l₂[j]) ∧
        { toArray := toArray✝, size_toArray := size_toArray✝ }[i] < l₂[i]

Proof state:
case mk
α : Type u_1
n : Nat
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
l₂ : Vector α n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ } < l₂ ↔
    ∃ i h,
      (∀ (j : Nat) (hj : j < i), { toArray := toArray✝, size_toArray := size_toArray✝ }[j] = l₂[j]) ∧
        { toArray := toArray✝, size_toArray := size_toArray✝ }[i] < l₂[i]

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
n : Nat
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } < { toArray := toArray✝, size_toArray := size_toArray✝ } ↔
    ∃ i h,
      (∀ (j : Nat) (hj : j < i),
          { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }[j] =
            { toArray := toArray✝, size_toArray := size_toArray✝ }[j]) ∧
        { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }[i] <
          { toArray := toArray✝, size_toArray := size_toArray✝ }[i]

Proof state:
case mk.mk
α : Type u_1
n : Nat
inst✝² : DecidableEq α
inst✝¹ : LT α
inst✝ : DecidableLT α
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } < { toArray := toArray✝, size_toArray := size_toArray✝ } ↔
    ∃ i h,
      (∀ (j : Nat) (hj : j < i),
          { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }[j] =
            { toArray := toArray✝, size_toArray := size_toArray✝ }[j]) ∧
        { toArray := toArray✝¹, size_toArray := size_toArray✝¹ }[i] <
          { toArray := toArray✝, size_toArray := size_toArray✝ }[i]

Tactic:
simp_all [Array.lt_iff_exists]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean
theorem Presieve.isSheaf_iff_preservesFiniteProducts (F : Cᵒᵖ ⥤ Type w) :
    Presieve.IsSheaf (extensiveTopology C) F ↔ PreservesFiniteProducts F

Proof state:
case refine_1.refine_1.a.refine_2
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).covering X, IsSheafFor F R
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
Z : Fin n → C := fun i => unop (K.obj { as := i })
this✝ : (ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).hasPullbacks
this : ∀ (i : Fin n), Mono ((Cofan.mk (∐ Z) (Sigma.ι Z)).inj i)
i : K ≅ Discrete.functor fun i => op (Z i) := Discrete.natIsoFunctor
⊢ (default ≫ Sigma.desc fun a => ⋯.elim a) = 𝟙 (⊥_ C)

Tactic:
simp only [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
case refine_1
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : IsSheaf (extensiveTopology C) F
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
⊢ PreservesLimit K F

Tactic:
rw [extensiveTopology, isSheaf_coverage] at hF

Result:
case refine_1
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).covering X, IsSheafFor F R
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
⊢ PreservesLimit K F

Proof state:
case refine_2
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : PreservesFiniteProducts F
X : C
R : Presieve X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (Sigma.desc π)
this : IsIso (Sigma.desc (Cofan.mk X π).inj)
⊢ IsSheafFor F R

Tactic:
have : R.Extensive := ⟨Y, α, Z, π, hR, ⟨Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X π)⟩⟩

Result:
case refine_2
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : PreservesFiniteProducts F
X : C
R : Presieve X
Y : Type
α : Finite Y
Z : Y → C
π : (a : Y) → Z a ⟶ X
hR : R = ofArrows Z π
hi : IsIso (Sigma.desc π)
this✝ : IsIso (Sigma.desc (Cofan.mk X π).inj)
this : R.Extensive
⊢ IsSheafFor F R
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem IsPrime.prod_mem_iff {s : Finset ι} {x : ι → R} {p : Ideal R} [hp : p.IsPrime] :
    ∏ i ∈ s, x i ∈ p ↔ ∃ i ∈ s, x i ∈ p

Proof state:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
s : Finset ι
x : ι → R
p : Ideal R
hp : p.IsPrime
⊢ ∏ i ∈ s, span {x i} ≤ p ↔ ∃ i ∈ s, span {x i} ≤ p

Tactic:
exact hp.prod_le

Result:
no goals

Proof state:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
s : Finset ι
x : ι → R
p : Ideal R
hp : p.IsPrime
⊢ ∏ i ∈ s, x i ∈ p ↔ ∃ i ∈ s, x i ∈ p

Tactic:
simp_rw [← span_singleton_le_iff_mem, ← prod_span_singleton]

Result:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
s : Finset ι
x : ι → R
p : Ideal R
hp : p.IsPrime
⊢ ∏ i ∈ s, span {x i} ≤ p ↔ ∃ i ∈ s, span {x i} ≤ p
-- Mathlib/GroupTheory/GroupAction/SubMulAction.lean
lemma orbitRel_nonZero_iff (x y : { v : M // v ≠ 0 }) :
    MulAction.orbitRel Rˣ { v // v ≠ 0 } x y ↔ MulAction.orbitRel Rˣ M x y :=
  ⟨by rintro ⟨a, rfl⟩; exact ⟨a, by simp⟩, by intro ⟨a, ha⟩; exact ⟨a, by ext; simpa⟩⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
x y : { v // v ≠ 0 }
a : Rˣ
ha : (fun m => m • ↑y) a = ↑x
⊢ (fun m => m • y) a = x

Tactic:
ext

Result:
case a
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
x y : { v // v ≠ 0 }
a : Rˣ
ha : (fun m => m • ↑y) a = ↑x
⊢ ↑((fun m => m • y) a) = ↑x

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
y : { v // v ≠ 0 }
a : Rˣ
⊢ (MulAction.orbitRel Rˣ M) ↑((fun m => m • y) a) ↑y

Tactic:
exact ⟨a, by simp⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
x y : { v // v ≠ 0 }
⊢ (MulAction.orbitRel Rˣ M) ↑x ↑y → (MulAction.orbitRel Rˣ { v // v ≠ 0 }) x y

Tactic:
intro ⟨a, ha⟩

Result:
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
x y : { v // v ≠ 0 }
a : Rˣ
ha : (fun m => m • ↑y) a = ↑x
⊢ (MulAction.orbitRel Rˣ { v // v ≠ 0 }) x y

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
x y : { v // v ≠ 0 }
a : Rˣ
ha : (fun m => m • ↑y) a = ↑x
⊢ (MulAction.orbitRel Rˣ { v // v ≠ 0 }) x y

Tactic:
exact ⟨a, by ext; simpa⟩

Result:
no goals

Proof state:
case a
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
x y : { v // v ≠ 0 }
a : Rˣ
ha : (fun m => m • ↑y) a = ↑x
⊢ ↑((fun m => m • y) a) = ↑x

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
x y : { v // v ≠ 0 }
⊢ (MulAction.orbitRel Rˣ { v // v ≠ 0 }) x y → (MulAction.orbitRel Rˣ M) ↑x ↑y

Tactic:
rintro ⟨a, rfl⟩

Result:
case intro
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
y : { v // v ≠ 0 }
a : Rˣ
⊢ (MulAction.orbitRel Rˣ M) ↑((fun m => m • y) a) ↑y

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Monoid R
inst✝¹ : AddCommMonoid M
inst✝ : DistribMulAction R M
y : { v // v ≠ 0 }
a : Rˣ
⊢ (fun m => m • ↑y) a = ↑((fun m => m • y) a)

Tactic:
simp

Result:
no goals