harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/MellinInversion.lean
theorem rexp_cexp_aux (x : ℝ) (s : ℂ) (f : E) :
    rexp (-x) • cexp (-↑x) ^ (s - 1) • f = cexp (-s * ↑x) • f

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ 0 < π

Tactic:
exact pi_pos

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ (-↑x).im ≤ π

Tactic:
simpa using pi_nonneg

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ cexp (-↑x * (1 + (s - 1))) • f = cexp (-s * ↑x) • f

Tactic:
ring_nf

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ (↑(rexp (-x)) * cexp (-↑x) ^ (s - 1)) • f = cexp (-s * ↑x) • f

Tactic:
push_cast

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ (cexp (-↑x) * cexp (-↑x) ^ (s - 1)) • f = cexp (-s * ↑x) • f

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ -π < (-↑x).im

Tactic:
norm_num

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ 0 < π

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ ↑(rexp (-x)) • cexp (-↑x) ^ (s - 1) • f = cexp (-s * ↑x) • f

Tactic:
rw [← smul_assoc, smul_eq_mul]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ (↑(rexp (-x)) * cexp (-↑x) ^ (s - 1)) • f = cexp (-s * ↑x) • f

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ rexp (-x) • cexp (-↑x) ^ (s - 1) • f = cexp (-s * ↑x) • f

Tactic:
show (rexp (-x) : ℂ) • _ = _ • f

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ ↑(rexp (-x)) • cexp (-↑x) ^ (s - 1) • f = cexp (-s * ↑x) • f

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ (cexp (-↑x) ^ 1 * cexp (-↑x) ^ (s - 1)) • f = cexp (-s * ↑x) • f

Tactic:
rw [← cpow_add _ _ (Complex.exp_ne_zero _), cpow_def_of_ne_zero (Complex.exp_ne_zero _),
  Complex.log_exp (by norm_num; exact pi_pos) (by simpa using pi_nonneg)]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ cexp (-↑x * (1 + (s - 1))) • f = cexp (-s * ↑x) • f

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ (cexp (-↑x) * cexp (-↑x) ^ (s - 1)) • f = cexp (-s * ↑x) • f

Tactic:
conv in cexp _ * _ => lhs; rw [← cpow_one (cexp _)]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ (cexp (-↑x) ^ 1 * cexp (-↑x) ^ (s - 1)) • f = cexp (-s * ↑x) • f
-- Mathlib/Order/Filter/AtTopBot/Finset.lean
theorem atTop_finset_eq_iInf : (atTop : Filter (Finset α)) = ⨅ x : α, 𝓟 (Ici {x})

Proof state:
α : Type u_3
⊢ ⨅ x, 𝓟 (Ici {x}) ≤ atTop

Tactic:
refine
  le_iInf fun s =>
    le_principal_iff.2 <| mem_iInf_of_iInter s.finite_toSet (fun i => mem_principal_self _) ?_

Result:
α : Type u_3
s : Finset α
⊢ ⋂ i, Ici {↑i} ⊆ Ici s

Proof state:
α : Type u_3
s : Finset α
⊢ ⋂ i, Ici {↑i} ⊆ Ici s

Tactic:
simp only [subset_def, mem_iInter, SetCoe.forall, mem_Ici, Finset.le_iff_subset,
  Finset.mem_singleton, Finset.subset_iff, forall_eq]

Result:
α : Type u_3
s : Finset α
⊢ ∀ (x : Finset α), (∀ x_1 ∈ ↑s, x_1 ∈ x) → ∀ ⦃x_1 : α⦄, x_1 ∈ s → x_1 ∈ x

Proof state:
α : Type u_3
s : Finset α
⊢ ∀ (x : Finset α), (∀ x_1 ∈ ↑s, x_1 ∈ x) → ∀ ⦃x_1 : α⦄, x_1 ∈ s → x_1 ∈ x

Tactic:
exact fun t => id

Result:
no goals

Proof state:
α : Type u_3
⊢ atTop = ⨅ x, 𝓟 (Ici {x})

Tactic:
refine le_antisymm (le_iInf fun i => le_principal_iff.2 <| mem_atTop ({i} : Finset α)) ?_

Result:
α : Type u_3
⊢ ⨅ x, 𝓟 (Ici {x}) ≤ atTop
-- Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
/-- The composition of the derivative of `extChartAt` with the derivative of the inverse of
`extChartAt` gives the identity.
Version where the basepoint belongs to `(extChartAt I x).target`. -/
lemma mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm {x : M}
    {y : E} (hy : y ∈ (extChartAt I x).target) :
    (mfderiv I 𝓘(𝕜, E) (extChartAt I x) ((extChartAt I x).symm y)) ∘L
      (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) y) = ContinuousLinearMap.id _ _

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range ↑I) y
⊢ (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y)).comp
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) y) =
    ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y)

Tactic:
have h'y : (extChartAt I x).symm y ∈ (extChartAt I x).source := (extChartAt I x).map_target hy

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_3
inst✝³ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range ↑I) y
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
⊢ (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y)).comp
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) y) =
    ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y)
-- Mathlib/Data/Real/Sqrt.lean
theorem sqrt_div_self : √x / x = (√x)⁻¹

Proof state:
x : ℝ
⊢ √x / x = (√x)⁻¹

Tactic:
rw [sqrt_div_self', one_div]

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem uniqueBaseOn_isBase_iff (hIE : I ⊆ E) : (uniqueBaseOn I E).IsBase B ↔ B = I

Proof state:
α : Type u_1
E B I : Set α
hIE : I ⊆ E
⊢ (uniqueBaseOn I E).IsBase B ↔ B = I

Tactic:
rw [uniqueBaseOn, isBase_restrict_iff', freeOn_isBasis'_iff, inter_eq_self_of_subset_right hIE]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Opposites.lean
theorem opRingEquiv_op_C_mul_X_pow (r : R) (n : ℕ) :
    opRingEquiv R (op (C r * X ^ n : R[X])) = C (op r) * X ^ n

Proof state:
R : Type u_1
inst✝ : Semiring R
r : R
n : ℕ
⊢ (opRingEquiv R) (op (C r * X ^ n)) = C (op r) * X ^ n

Tactic:
simp only [X_pow_mul, op_mul, op_pow, map_mul, map_pow, opRingEquiv_op_X, opRingEquiv_op_C]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
@[simp] lemma iSup_lt_eq_self (a : ℝ≥0∞) : ⨆ b, ⨆ _ : b < a, b = a

Proof state:
case intro.intro
a c : ℝ≥0∞
hca : c < a
d : ℝ≥0∞
hcd : c < d
hdb : d < a
⊢ c < ⨆ b, ⨆ (_ : b < a), b

Tactic:
exact hcd.trans_le <| le_iSup₂_of_le d hdb le_rfl

Result:
no goals

Proof state:
a : ℝ≥0∞
⊢ a ≤ ⨆ b, ⨆ (_ : b < a), b

Tactic:
refine le_of_forall_lt fun c hca ↦ ?_

Result:
a c : ℝ≥0∞
hca : c < a
⊢ c < ⨆ b, ⨆ (_ : b < a), b

Proof state:
a c : ℝ≥0∞
hca : c < a
⊢ c < ⨆ b, ⨆ (_ : b < a), b

Tactic:
obtain ⟨d, hcd, hdb⟩ := exists_between hca

Result:
case intro.intro
a c : ℝ≥0∞
hca : c < a
d : ℝ≥0∞
hcd : c < d
hdb : d < a
⊢ c < ⨆ b, ⨆ (_ : b < a), b

Proof state:
a : ℝ≥0∞
⊢ ⨆ b, ⨆ (_ : b < a), b = a

Tactic:
refine le_antisymm (iSup₂_le fun b hb ↦ hb.le) ?_

Result:
a : ℝ≥0∞
⊢ a ≤ ⨆ b, ⨆ (_ : b < a), b
-- Mathlib/Combinatorics/Additive/Corner/Defs.lean
/-- Corners are preserved under `2`-Freiman homomorphisms. -/
lemma IsCorner.image (hf : IsAddFreimanHom 2 s t f) (hAs : (A : Set (G × G)) ⊆ s ×ˢ s)
    (hA : IsCorner A x₁ y₁ x₂ y₂) : IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂)

Proof state:
G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanHom 2 s t f
hAs : A ⊆ s ×ˢ s
hA : IsCorner A x₁ y₁ x₂ y₂
⊢ IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂)

Tactic:
obtain ⟨hx₁y₁, hx₁y₂, hx₂y₁, hxy⟩ := hA

Result:
case mk
G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanHom 2 s t f
hAs : A ⊆ s ×ˢ s
hx₁y₁ : (x₁, y₁) ∈ A
hx₁y₂ : (x₁, y₂) ∈ A
hx₂y₁ : (x₂, y₁) ∈ A
hxy : x₁ + y₂ = x₂ + y₁
⊢ IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂)

Proof state:
case mk
G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanHom 2 s t f
hAs : A ⊆ s ×ˢ s
hx₁y₁ : (x₁, y₁) ∈ A
hx₁y₂ : (x₁, y₂) ∈ A
hx₂y₁ : (x₂, y₁) ∈ A
hxy : x₁ + y₂ = x₂ + y₁
⊢ IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂)

Tactic:
exact ⟨mem_image_of_mem _ hx₁y₁, mem_image_of_mem _ hx₁y₂, mem_image_of_mem _ hx₂y₁,
  hf.add_eq_add (hAs hx₁y₁).1 (hAs hx₁y₂).2 (hAs hx₂y₁).1 (hAs hx₁y₁).2 hxy⟩

Result:
no goals
-- Mathlib/Combinatorics/Schnirelmann.lean
/--
If the Schnirelmann density is `0`, there is a positive natural for which
`|A ∩ {1, ..., n}| / n < ε`, for any positive `ε`.
Note this cannot be improved to `∃ᶠ n : ℕ in atTop`, as can be seen by `A = {1}ᶜ`.
-/
lemma exists_of_schnirelmannDensity_eq_zero {ε : ℝ} (hε : 0 < ε) (hA : schnirelmannDensity A = 0) :
    ∃ n, 0 < n ∧ #{a ∈ Ioc 0 n | a ∈ A} / n < ε

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
ε : ℝ
hε : 0 < ε
hA : schnirelmannDensity A = 0
⊢ ∃ n, 0 < n ∧ ↑(#(filter (fun a => a ∈ A) (Ioc 0 n))) / ↑n < ε

Tactic:
by_contra! h

Result:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
ε : ℝ
hε : 0 < ε
hA : schnirelmannDensity A = 0
h : ∀ (n : ℕ), 0 < n → ε ≤ ↑(#(filter (fun a => a ∈ A) (Ioc 0 n))) / ↑n
⊢ False

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
ε : ℝ
hε : 0 < ε
hA : schnirelmannDensity A = 0
h : ∀ (n : ℕ), 0 < n → ε ≤ ↑(#(filter (fun a => a ∈ A) (Ioc 0 n))) / ↑n
⊢ False

Tactic:
rw [← le_schnirelmannDensity_iff] at h

Result:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
ε : ℝ
hε : 0 < ε
hA : schnirelmannDensity A = 0
h : ε ≤ schnirelmannDensity A
⊢ False

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
ε : ℝ
hε : 0 < ε
hA : schnirelmannDensity A = 0
h : ε ≤ schnirelmannDensity A
⊢ False

Tactic:
linarith

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean
theorem abs_mulExpNegMulSq_comp_le_norm {E : Type*} [TopologicalSpace E] {x : E}
    (g : BoundedContinuousFunction E ℝ) (hε : 0 ≤ ε) :
    |(mulExpNegMulSq ε ∘ g) x| ≤ ‖g‖

Proof state:
ε : ℝ
E : Type u_1
inst✝ : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ rexp (-(ε * g x * g x)) ≤ 1

Tactic:
rw [exp_le_one_iff, Left.neg_nonpos_iff, mul_assoc]

Result:
ε : ℝ
E : Type u_1
inst✝ : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ 0 ≤ ε * (g x * g x)

Proof state:
ε : ℝ
E : Type u_1
inst✝ : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ |(ε.mulExpNegMulSq ∘ ⇑g) x| ≤ ‖g‖

Tactic:
simp only [Function.comp_apply, mulExpNegMulSq, abs_mul, abs_exp]

Result:
ε : ℝ
E : Type u_1
inst✝ : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ |g x| * rexp (-(ε * g x * g x)) ≤ ‖g‖

Proof state:
ε : ℝ
E : Type u_1
inst✝ : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ 0 ≤ ε * (g x * g x)

Tactic:
exact mul_nonneg hε (mul_self_nonneg (g x))

Result:
no goals

Proof state:
ε : ℝ
E : Type u_1
inst✝ : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ |g x| * rexp (-(ε * g x * g x)) ≤ ‖g‖

Tactic:
apply le_trans (mul_le_of_le_one_right (abs_nonneg (g x)) _) (g.norm_coe_le_norm x)

Result:
ε : ℝ
E : Type u_1
inst✝ : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ rexp (-(ε * g x * g x)) ≤ 1
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem continuous_integral : Continuous fun f : α →₁[μ] G => ∫ a, f a ∂μ

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
hG : ¬CompleteSpace G
⊢ Continuous fun f => ∫ (a : α), ↑↑f a ∂μ

Tactic:
simp [integral, hG, continuous_const]

Result:
no goals

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
hG : CompleteSpace G
⊢ Continuous fun f =>
    if h : True then
      if hf : Integrable (fun a => ↑↑f a) μ then L1.integralCLM (Integrable.toL1 (fun a => ↑↑f a) hf) else 0
    else 0

Tactic:
exact continuous_setToFun (dominatedFinMeasAdditive_weightedSMul μ)

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
⊢ Continuous fun f => ∫ (a : α), ↑↑f a ∂μ

Tactic:
by_cases hG : CompleteSpace G

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
hG : CompleteSpace G
⊢ Continuous fun f => ∫ (a : α), ↑↑f a ∂μ

case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
hG : ¬CompleteSpace G
⊢ Continuous fun f => ∫ (a : α), ↑↑f a ∂μ

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
hG : CompleteSpace G
⊢ Continuous fun f => ∫ (a : α), ↑↑f a ∂μ

Tactic:
simp only [integral, hG, L1.integral]

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
hG : CompleteSpace G
⊢ Continuous fun f =>
    if h : True then
      if hf : Integrable (fun a => ↑↑f a) μ then L1.integralCLM (Integrable.toL1 (fun a => ↑↑f a) hf) else 0
    else 0
-- Mathlib/Probability/Independence/ZeroOne.lean
theorem measure_zero_or_one_of_measurableSet_limsup_atBot
    (h_le : ∀ n, s n ≤ m0) (h_indep : iIndep s μ) {t : Set Ω}
    (ht_tail : MeasurableSet[limsup s atBot] t) :
    μ t = 0 ∨ μ t = 1

Proof state:
Ω : Type u_2
ι : Type u_3
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : SemilatticeInf ι
inst✝¹ : NoMinOrder ι
inst✝ : Nonempty ι
h_le : ∀ (n : ι), s n ≤ m0
h_indep : iIndep s μ
t : Set Ω
ht_tail : MeasurableSet t
⊢ μ t = 0 ∨ μ t = 1

Tactic:
simpa only [ae_dirac_eq, Filter.eventually_pure]
  using Kernel.measure_zero_or_one_of_measurableSet_limsup_atBot h_le h_indep ht_tail

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
lemma filter_biUnion (s : Finset α) (f : α → Finset β) (p : β → Prop) [DecidablePred p] :
    (s.biUnion f).filter p = s.biUnion fun a ↦ (f a).filter p

Proof state:
case h.mpr.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
a : α
ha : a ∈ s
hba : b ∈ f a
hb : p b
⊢ (∃ a ∈ s, b ∈ f a) ∧ p b

Tactic:
exact ⟨⟨a, ha, hba⟩, hb⟩

Result:
no goals

Proof state:
case h.mp.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
hb : p b
a : α
ha : a ∈ s
hba : b ∈ f a
⊢ ∃ a ∈ s, b ∈ f a ∧ p b

Tactic:
exact ⟨a, ha, hba, hb⟩

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ b ∈ filter p (s.biUnion f) ↔ b ∈ s.biUnion fun a => filter p (f a)

Tactic:
simp only [mem_biUnion, exists_prop, mem_filter]

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a ∈ s, b ∈ f a) ∧ p b ↔ ∃ a ∈ s, b ∈ f a ∧ p b

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
⊢ filter p (s.biUnion f) = s.biUnion fun a => filter p (f a)

Tactic:
ext b

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ b ∈ filter p (s.biUnion f) ↔ b ∈ s.biUnion fun a => filter p (f a)

Proof state:
case h.mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a ∈ s, b ∈ f a) ∧ p b → ∃ a ∈ s, b ∈ f a ∧ p b

Tactic:
rintro ⟨⟨a, ha, hba⟩, hb⟩

Result:
case h.mp.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
hb : p b
a : α
ha : a ∈ s
hba : b ∈ f a
⊢ ∃ a ∈ s, b ∈ f a ∧ p b

Proof state:
case h.mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a ∈ s, b ∈ f a ∧ p b) → (∃ a ∈ s, b ∈ f a) ∧ p b

Tactic:
rintro ⟨a, ha, hba, hb⟩

Result:
case h.mpr.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
a : α
ha : a ∈ s
hba : b ∈ f a
hb : p b
⊢ (∃ a ∈ s, b ∈ f a) ∧ p b

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a ∈ s, b ∈ f a) ∧ p b ↔ ∃ a ∈ s, b ∈ f a ∧ p b

Tactic:
constructor

Result:
case h.mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a ∈ s, b ∈ f a) ∧ p b → ∃ a ∈ s, b ∈ f a ∧ p b

case h.mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
s : Finset α
f : α → Finset β
p : β → Prop
inst✝ : DecidablePred p
b : β
⊢ (∃ a ∈ s, b ∈ f a ∧ p b) → (∃ a ∈ s, b ∈ f a) ∧ p b
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioo_inter_Ioc_of_right_lt (h : b₂ < b₁) : Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (max a₁ a₂) b₂

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h : b₂ < b₁
⊢ Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioc (a₁ ⊔ a₂) b₂

Tactic:
rw [inter_comm, Ioc_inter_Ioo_of_left_lt h, max_comm]

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem mem_closure_iff {s : Set R} {x} :
    x ∈ closure s ↔ x ∈ AddSubgroup.closure (Submonoid.closure s : Set R) :=
  ⟨fun h => by
    induction h using closure_induction with
    | mem _ hx => exact AddSubgroup.subset_closure (Submonoid.subset_closure hx)
    | zero => exact zero_mem _
    | one => exact AddSubgroup.subset_closure (one_mem _)
    | add _ _ _ _ hx hy => exact add_mem hx hy
    | neg _ _ hx => exact neg_mem hx
    | mul _ _ _hx _hy hx hy =>
      clear _hx _hy
      induction hx, hy using AddSubgroup.closure_induction₂ with
      | mem _ _ hx hy => exact AddSubgroup.subset_closure (mul_mem hx hy)
      | one_left => simpa using zero_mem _
      | one_right => simpa using zero_mem _
      | mul_left _ _ _ _ _ _ h₁ h₂ => simpa [add_mul] using add_mem h₁ h₂
      | mul_right _ _ _ _ _ _ h₁ h₂ => simpa [mul_add] using add_mem h₁ h₂
      | inv_left _ _ _ _ h => simpa [neg_mul] using neg_mem h
      | inv_right _ _ _ _ h => simpa [mul_neg] using neg_mem h,
    fun h => by
      induction h using AddSubgroup.closure_induction with
      | mem x hx =>
        induction hx using Submonoid.closure_induction with
        | mem _ h => exact subset_closure h
        | one => exact one_mem _
        | mul _ _ _ _ h₁ h₂ => exact mul_mem h₁ h₂
      | one => exact zero_mem _
      | mul _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
      | inv _ _ h => exact neg_mem h⟩

Proof state:
R : Type u
inst✝ : Ring R
s : Set R
x : R
h : x ∈ closure s
⊢ x ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
induction h using closure_induction with
| mem _ hx => exact AddSubgroup.subset_closure (Submonoid.subset_closure hx)
| zero => exact zero_mem _
| one => exact AddSubgroup.subset_closure (one_mem _)
| add _ _ _ _ hx hy => exact add_mem hx hy
| neg _ _ hx => exact neg_mem hx
| mul _ _ _hx _hy hx hy =>
  clear _hx _hy
  induction hx, hy using AddSubgroup.closure_induction₂ with
  | mem _ _ hx hy => exact AddSubgroup.subset_closure (mul_mem hx hy)
  | one_left => simpa using zero_mem _
  | one_right => simpa using zero_mem _
  | mul_left _ _ _ _ _ _ h₁ h₂ => simpa [add_mul] using add_mem h₁ h₂
  | mul_right _ _ _ _ _ _ h₁ h₂ => simpa [mul_add] using add_mem h₁ h₂
  | inv_left _ _ _ _ h => simpa [neg_mul] using neg_mem h
  | inv_right _ _ _ _ h => simpa [mul_neg] using neg_mem h

Result:
no goals

Proof state:
case mem.one
R : Type u
inst✝ : Ring R
s : Set R
x✝ x : R
⊢ 1 ∈ closure s

Tactic:
exact one_mem _

Result:
no goals

Proof state:
case add
R : Type u
inst✝ : Ring R
s : Set R
x x✝ y✝ : R
hx✝ : x✝ ∈ closure s
hy✝ : y✝ ∈ closure s
hx : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x✝ + y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
exact add_mem hx hy

Result:
no goals

Proof state:
case inv
R : Type u
inst✝ : Ring R
s : Set R
x x✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h : x✝ ∈ closure s
⊢ -x✝ ∈ closure s

Tactic:
exact neg_mem h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem cos_pos_iff_abs_toReal_lt_pi_div_two {θ : Angle} : 0 < cos θ ↔ |θ.toReal| < π / 2

Proof state:
θ : Angle
⊢ |θ.toReal| ≤ π / 2 → (|θ.toReal| ≠ π / 2 ↔ 0 ≠ θ.cos)

Tactic:
rintro -

Result:
θ : Angle
⊢ |θ.toReal| ≠ π / 2 ↔ 0 ≠ θ.cos

Proof state:
θ : Angle
⊢ 0 < θ.cos ↔ |θ.toReal| < π / 2

Tactic:
rw [lt_iff_le_and_ne, lt_iff_le_and_ne, cos_nonneg_iff_abs_toReal_le_pi_div_two, ←
  and_congr_right]

Result:
θ : Angle
⊢ |θ.toReal| ≤ π / 2 → (|θ.toReal| ≠ π / 2 ↔ 0 ≠ θ.cos)

Proof state:
θ : Angle
⊢ |θ.toReal| ≠ π / 2 ↔ 0 ≠ θ.cos

Tactic:
rw [Ne, Ne, not_iff_not, @eq_comm ℝ 0, abs_toReal_eq_pi_div_two_iff, cos_eq_zero_iff]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem two_dvd_card_support {σ : Perm α} (hσ : σ ^ 2 = 1) : 2 ∣ σ.support.card :=
  (congr_arg (Dvd.dvd 2) σ.sum_cycleType).mp
    (Multiset.dvd_sum fun n hn => by
      rw [_root_.le_antisymm
          (Nat.le_of_dvd zero_lt_two <|
            (dvd_of_mem_cycleType hn).trans <| orderOf_dvd_of_pow_eq_one hσ)
          (two_le_of_mem_cycleType hn)])

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ^ 2 = 1
n : ℕ
hn : n ∈ σ.cycleType
⊢ 2 ∣ n

Tactic:
rw [_root_.le_antisymm
    (Nat.le_of_dvd zero_lt_two <|
      (dvd_of_mem_cycleType hn).trans <| orderOf_dvd_of_pow_eq_one hσ)
    (two_le_of_mem_cycleType hn)]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/IsSheafFor.lean
theorem FamilyOfElements.Compatible.compPresheafMap (f : P ⟶ Q) {x : FamilyOfElements P R}
    (h : x.Compatible) : (x.compPresheafMap f).Compatible

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible
Z₁ Z₂ W : C
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ X
f₂ : Z₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Q.map g₁.op (FamilyOfElements.compPresheafMap f x f₁ h₁) = Q.map g₂.op (FamilyOfElements.compPresheafMap f x f₂ h₂)

Tactic:
unfold FamilyOfElements.compPresheafMap

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible
Z₁ Z₂ W : C
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ X
f₂ : Z₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Q.map g₁.op (f.app (op Z₁) (x f₁ h₁)) = Q.map g₂.op (f.app (op Z₂) (x f₂ h₂))

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible
Z₁ Z₂ W : C
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ X
f₂ : Z₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Q.map g₁.op (f.app (op Z₁) (x f₁ h₁)) = Q.map g₂.op (f.app (op Z₂) (x f₂ h₂))

Tactic:
rwa [← FunctorToTypes.naturality, ← FunctorToTypes.naturality, h]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible
⊢ (FamilyOfElements.compPresheafMap f x).Compatible

Tactic:
intro Z₁ Z₂ W g₁ g₂ f₁ f₂ h₁ h₂ eq

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
f : P ⟶ Q
x : FamilyOfElements P R
h : x.Compatible
Z₁ Z₂ W : C
g₁ : W ⟶ Z₁
g₂ : W ⟶ Z₂
f₁ : Z₁ ⟶ X
f₂ : Z₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
eq : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ Q.map g₁.op (FamilyOfElements.compPresheafMap f x f₁ h₁) = Q.map g₂.op (FamilyOfElements.compPresheafMap f x f₂ h₂)