harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Analytic/Basic.lean
theorem isLittleO_of_lt_radius (h : ↑r < p.radius) :
    ∃ a ∈ Ioo (0 : ℝ) 1, (fun n => ‖p n‖ * (r : ℝ) ^ n) =o[atTop] (a ^ ·)

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this✝ :
  (∃ a ∈ Ioo 0 1, (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r < ↑t
this : 0 < ↑t
⊢ ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n

Tactic:
rw [← div_lt_one this] at rt

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this✝ :
  (∃ a ∈ Ioo 0 1, (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r / ↑t < 1
this : 0 < ↑t
⊢ ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this✝ :
  (∃ a ∈ Ioo 0 1, (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r / ↑t < 1
this : 0 < ↑t
n : ℕ
⊢ ‖p n‖ * ↑t ^ n ≤ C

Tactic:
apply hC

Result:
no goals

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this :
  (∃ a ∈ Ioo 0 1, (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r < ↑t
⊢ ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n

Tactic:
have : 0 < (t : ℝ) := r.coe_nonneg.trans_lt rt

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
this✝ :
  (∃ a ∈ Ioo 0 1, (fun n => ‖p n‖ * ↑r ^ n) =o[atTop] fun x => a ^ x) ↔
    ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
t : ℝ≥0
C : ℝ
hC : ∀ (n : ℕ), ‖p n‖ * ↑t ^ n ≤ C
rt : ↑r < ↑t
this : 0 < ↑t
⊢ ∃ a < 1, ∃ C, (0 < C ∨ 0 < 1) ∧ ∀ (n : ℕ), |‖p n‖ * ↑r ^ n| ≤ C * a ^ n
-- Mathlib/Order/PartialSups.lean
theorem ciSup_partialSups_eq' [ConditionallyCompleteLinearOrder α] (f : ι → α) :
    ⨆ i, partialSups f i = ⨆ i, f i

Proof state:
case pos
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
h : BddAbove (Set.range f)
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
exact ciSup_partialSups_eq h

Result:
no goals

Proof state:
case neg
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
h : ¬BddAbove (Set.range f)
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
rw [iSup, iSup, ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _ h,
  ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove _
    (bddAbove_range_partialSups.not.mpr h)]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
by_cases h : BddAbove (Set.range f)

Result:
case pos
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
h : BddAbove (Set.range f)
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

case neg
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLinearOrder α
f : ι → α
h : ¬BddAbove (Set.range f)
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem min_add_left {a b : Nat} : min a (b + a) = a

Proof state:
a b : Nat
⊢ min a (b + a) = a

Tactic:
rw [Nat.min_def]

Result:
a b : Nat
⊢ (if a ≤ b + a then a else b + a) = a

Proof state:
a b : Nat
⊢ (if a ≤ b + a then a else b + a) = a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/ComplexDeriv.lean
theorem deriv_tan (x : ℂ) : deriv tan x = 1 / cos x ^ 2 :=
  if h : cos x = 0 then by
    have : ¬DifferentiableAt ℂ tan x := mt differentiableAt_tan.1 (Classical.not_not.2 h)
    simp [deriv_zero_of_not_differentiableAt this, h, sq]
  else (hasDerivAt_tan h).deriv

Proof state:
x : ℂ
h : cos x = 0
this : ¬DifferentiableAt ℂ tan x
⊢ deriv tan x = 1 / cos x ^ 2

Tactic:
simp [deriv_zero_of_not_differentiableAt this, h, sq]

Result:
no goals

Proof state:
x : ℂ
h : cos x = 0
⊢ deriv tan x = 1 / cos x ^ 2

Tactic:
have : ¬DifferentiableAt ℂ tan x := mt differentiableAt_tan.1 (Classical.not_not.2 h)

Result:
x : ℂ
h : cos x = 0
this : ¬DifferentiableAt ℂ tan x
⊢ deriv tan x = 1 / cos x ^ 2
-- Mathlib/Analysis/Convex/Segment.lean
theorem image_update_openSegment (i : ι) (x₁ x₂ : π i) (y : ∀ i, π i) :
    update y i '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (update y i x₁) (update y i x₂)

Proof state:
𝕜 : Type u_1
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y : (i : ι) → π i
a : 𝕜 × 𝕜
ha : a ∈ {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}
⊢ update y i (a.1 • x₁ + a.2 • x₂) = a.1 • update y i x₁ + a.2 • update y i x₂

Tactic:
simp only [← update_smul, ← update_add, Convex.combo_self ha.2.2]

Result:
no goals

Proof state:
𝕜 : Type u_1
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y : (i : ι) → π i
⊢ (fun x => update y i (x.1 • x₁ + x.2 • x₂)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    (fun p => p.1 • update y i x₁ + p.2 • update y i x₂) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}

Tactic:
refine EqOn.image_eq fun a ha ↦ ?_

Result:
𝕜 : Type u_1
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y : (i : ι) → π i
a : 𝕜 × 𝕜
ha : a ∈ {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}
⊢ update y i (a.1 • x₁ + a.2 • x₂) = a.1 • update y i x₁ + a.2 • update y i x₂

Proof state:
𝕜 : Type u_1
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y : (i : ι) → π i
⊢ update y i '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (update y i x₁) (update y i x₂)

Tactic:
rw [openSegment_eq_image₂, openSegment_eq_image₂, image_image]

Result:
𝕜 : Type u_1
ι : Type u_5
π : ι → Type u_6
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y : (i : ι) → π i
⊢ (fun x => update y i (x.1 • x₁ + x.2 • x₂)) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1} =
    (fun p => p.1 • update y i x₁ + p.2 • update y i x₂) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}
-- Mathlib/CategoryTheory/IsConnected.lean
theorem induct_on_objects [IsPreconnected J] (p : Set J) {j₀ : J} (h0 : j₀ ∈ p)
    (h1 : ∀ {j₁ j₂ : J} (_ : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) (j : J) : j ∈ p

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
aux : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → { down := j₁ ∈ p } = { down := j₂ ∈ p } :=
  fun j₁ j₂ f => congrArg ULift.up (Iff.eq (h1 f))
i : (j ∈ p) = (j₀ ∈ p)
⊢ j ∈ p

Tactic:
rwa [i]

Result:
no goals

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
aux : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → { down := j₁ ∈ p } = { down := j₂ ∈ p } :=
  fun j₁ j₂ f => congrArg ULift.up (Iff.eq (h1 f))
⊢ j ∈ p

Tactic:
injection constant_of_preserves_morphisms (fun k => ULift.up.{u₁} (k ∈ p)) aux j j₀ with i

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
aux : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → { down := j₁ ∈ p } = { down := j₂ ∈ p } :=
  fun j₁ j₂ f => congrArg ULift.up (Iff.eq (h1 f))
i : (j ∈ p) = (j₀ ∈ p)
⊢ j ∈ p

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
⊢ j ∈ p

Tactic:
let aux (j₁ j₂ : J) (f : j₁ ⟶ j₂) := congrArg ULift.up <| (h1 f).eq

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
inst✝ : IsPreconnected J
p : Set J
j₀ : J
h0 : j₀ ∈ p
h1 : ∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : J
aux : ∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → { down := j₁ ∈ p } = { down := j₂ ∈ p } :=
  fun j₁ j₂ f => congrArg ULift.up (Iff.eq (h1 f))
⊢ j ∈ p
-- Mathlib/Analysis/Convex/Function.lean
theorem concaveOn_id {s : Set β} (hs : Convex 𝕜 s) : ConcaveOn 𝕜 s _root_.id :=
  ⟨hs, by
    intros
    rfl⟩

Proof state:
𝕜 : Type u_1
β : Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
s : Set β
hs : Convex 𝕜 s
x✝ : β
a✝⁵ : x✝ ∈ s
y✝ : β
a✝⁴ : y✝ ∈ s
a✝³ b✝ : 𝕜
a✝² : 0 ≤ a✝³
a✝¹ : 0 ≤ b✝
a✝ : a✝³ + b✝ = 1
⊢ a✝³ • _root_.id x✝ + b✝ • _root_.id y✝ ≤ _root_.id (a✝³ • x✝ + b✝ • y✝)

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
β : Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
s : Set β
hs : Convex 𝕜 s
⊢ ∀ ⦃x : β⦄,
    x ∈ s →
      ∀ ⦃y : β⦄,
        y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • _root_.id x + b • _root_.id y ≤ _root_.id (a • x + b • y)

Tactic:
intros

Result:
𝕜 : Type u_1
β : Type u_5
inst✝² : OrderedSemiring 𝕜
inst✝¹ : OrderedAddCommMonoid β
inst✝ : SMul 𝕜 β
s : Set β
hs : Convex 𝕜 s
x✝ : β
a✝⁵ : x✝ ∈ s
y✝ : β
a✝⁴ : y✝ ∈ s
a✝³ b✝ : 𝕜
a✝² : 0 ≤ a✝³
a✝¹ : 0 ≤ b✝
a✝ : a✝³ + b✝ = 1
⊢ a✝³ • _root_.id x✝ + b✝ • _root_.id y✝ ≤ _root_.id (a✝³ • x✝ + b✝ • y✝)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem lookup_eq_findSome? (l : List (α × β)) (k : α) :
    l.lookup k = l.findSome? fun p => if k == p.1 then some p.2 else none

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
l : List (α × β)
k : α
⊢ lookup k l = findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l

Tactic:
induction l with
| nil => rfl
| cons p l ih =>
  match p with
  | (k', v) =>
    simp only [lookup_cons, findSome?_cons]
    split <;> simp_all

Result:
no goals

Proof state:
case nil
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
⊢ lookup k [] = findSome? (fun p => if (k == p.fst) = true then some p.snd else none) []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
p : α × β
l : List (α × β)
ih : lookup k l = findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l
⊢ lookup k (p :: l) = findSome? (fun p => if (k == p.fst) = true then some p.snd else none) (p :: l)

Tactic:
match p with
| (k', v) =>
  simp only [lookup_cons, findSome?_cons]
  split <;> simp_all

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
p : α × β
l : List (α × β)
ih : lookup k l = findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l
k' : α
v : β
⊢ (match k == k' with
    | true => some v
    | false => lookup k l) =
    match if (k == k') = true then some v else none with
    | some b => some b
    | none => findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
p : α × β
l : List (α × β)
ih : lookup k l = findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l
k' : α
v : β
⊢ lookup k ((k', v) :: l) = findSome? (fun p => if (k == p.fst) = true then some p.snd else none) ((k', v) :: l)

Tactic:
simp only [lookup_cons, findSome?_cons]

Result:
α : Type u_2
inst✝¹ : BEq α
inst✝ : LawfulBEq α
β : Type u_1
k : α
p : α × β
l : List (α × β)
ih : lookup k l = findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l
k' : α
v : β
⊢ (match k == k' with
    | true => some v
    | false => lookup k l) =
    match if (k == k') = true then some v else none with
    | some b => some b
    | none => findSome? (fun p => if (k == p.fst) = true then some p.snd else none) l
-- Mathlib/Data/Matroid/Sum.lean
@[simp] lemma sum'_indep_iff {I} :
    (Matroid.sum' M).Indep I ↔ ∀ i, (M i).Indep (Prod.mk i ⁻¹' I)

Proof state:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I : Set (ι × α)
⊢ (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' I))) ↔ ∀ (i : ι), (M i).Indep (Prod.mk i ⁻¹' I)

Tactic:
convert Iff.rfl

Result:
case h.e'_2.h.h.e'_3
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I : Set (ι × α)
a✝ : ι
⊢ Prod.mk a✝ ⁻¹' I = Sigma.mk a✝ ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' I)

Proof state:
case h.e'_2.h.h.e'_3.h
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I : Set (ι × α)
a✝ : ι
x✝ : α
⊢ x✝ ∈ Prod.mk a✝ ⁻¹' I ↔ x✝ ∈ Sigma.mk a✝ ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' I)

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_2.h.h.e'_3
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I : Set (ι × α)
a✝ : ι
⊢ Prod.mk a✝ ⁻¹' I = Sigma.mk a✝ ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' I)

Tactic:
ext

Result:
case h.e'_2.h.h.e'_3.h
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I : Set (ι × α)
a✝ : ι
x✝ : α
⊢ x✝ ∈ Prod.mk a✝ ⁻¹' I ↔ x✝ ∈ Sigma.mk a✝ ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' I)

Proof state:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I : Set (ι × α)
⊢ (Matroid.sum' M).Indep I ↔ ∀ (i : ι), (M i).Indep (Prod.mk i ⁻¹' I)

Tactic:
simp only [Matroid.sum', mapEquiv_indep_iff, Equiv.sigmaEquivProd_symm_apply, sigma_indep_iff]

Result:
α : Type u_1
ι : Type u_2
M : ι → Matroid α
I : Set (ι × α)
⊢ (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' ((fun a => ⟨a.1, a.2⟩) '' I))) ↔ ∀ (i : ι), (M i).Indep (Prod.mk i ⁻¹' I)
-- Mathlib/Probability/Independence/Basic.lean
theorem indepFun_iff_map_prod_eq_prod_map_map {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'}
    [IsFiniteMeasure μ] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
    IndepFun f g μ ↔ μ.map (fun ω ↦ (f ω, g ω)) = (μ.map f).prod (μ.map g)

Proof state:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsFiniteMeasure μ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ IndepFun f g μ ↔ Measure.map (fun ω => (f ω, g ω)) μ = (Measure.map f μ).prod (Measure.map g μ)

Tactic:
rw [indepFun_iff_measure_inter_preimage_eq_mul]

Result:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsFiniteMeasure μ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ (∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → μ (f ⁻¹' s ∩ g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t)) ↔
    Measure.map (fun ω => (f ω, g ω)) μ = (Measure.map f μ).prod (Measure.map g μ)

Proof state:
case mp
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsFiniteMeasure μ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h₀ :
  ∀ {s : Set β} {t : Set β'},
    MeasurableSet s →
      MeasurableSet t →
        μ (f ⁻¹' s) * μ (g ⁻¹' t) = (Measure.map f μ) s * (Measure.map g μ) t ∧
          μ (f ⁻¹' s ∩ g ⁻¹' t) = (Measure.map (fun ω => (f ω, g ω)) μ) (s ×ˢ t)
h : ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → μ (f ⁻¹' s ∩ g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t)
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (Measure.map (fun ω => (f ω, g ω)) μ) (s ×ˢ t) = (Measure.map f μ) s * (Measure.map g μ) t

Tactic:
rw [← (h₀ hs ht).1, ← (h₀ hs ht).2, h s t hs ht]

Result:
no goals

Proof state:
Ω : Type u_1
β : Type u_6
β' : Type u_7
_mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝ : IsFiniteMeasure μ
hf : AEMeasurable f μ
hg : AEMeasurable g μ
s : Set β
t : Set β'
hs : MeasurableSet s
ht : MeasurableSet t
⊢ μ (f ⁻¹' s) * μ (g ⁻¹' t) = (Measure.map f μ) s * (Measure.map g μ) t

Tactic:
rw [Measure.map_apply_of_aemeasurable hf hs, Measure.map_apply_of_aemeasurable hg ht]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem cos_pi_div_two_sub (x : ℂ) : cos (π / 2 - x) = sin x

Proof state:
x : ℂ
⊢ cos (↑π / 2 - x) = sin x

Tactic:
rw [← cos_neg, neg_sub, cos_sub_pi_div_two]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Prod.lean
theorem measure_mul_measure_eq (s t : Set G) (h2s : ν' s ≠ 0) (h3s : ν' s ≠ ∞) :
    μ' s * ν' t = ν' s * μ' t

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
hs : MeasurableSet s
t : Set G
ht : MeasurableSet t
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
have h1 := measure_lintegral_div_measure ν' ν' hs h2s h3s (t.indicator fun _ => 1)
  (measurable_const.indicator ht)

Result:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
hs : MeasurableSet s
t : Set G
ht : MeasurableSet t
h1 :
  ν' s * ∫⁻ (y : G), t.indicator (fun x => 1) y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s) ∂ν' =
    ∫⁻ (x : G), t.indicator (fun x => 1) x ∂ν'
⊢ μ' s * ν' t = ν' s * μ' t

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
hs : MeasurableSet s
t : Set G
ht : MeasurableSet t
h1 :
  ν' s * ∫⁻ (y : G), t.indicator (fun x => 1) y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s) ∂ν' =
    ∫⁻ (x : G), t.indicator (fun x => 1) x ∂ν'
⊢ μ' s * ν' t = ν' s * μ' t

Tactic:
have h2 := measure_lintegral_div_measure μ' ν' hs h2s h3s (t.indicator fun _ => 1)
  (measurable_const.indicator ht)

Result:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
inst✝⁴ : MeasurableInv G
μ' ν' : Measure G
inst✝³ : SigmaFinite μ'
inst✝² : SigmaFinite ν'
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : ν'.IsMulLeftInvariant
s : Set G
h2s : ν' s ≠ 0
h3s : ν' s ≠ ⊤
hs : MeasurableSet s
t : Set G
ht : MeasurableSet t
h1 :
  ν' s * ∫⁻ (y : G), t.indicator (fun x => 1) y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s) ∂ν' =
    ∫⁻ (x : G), t.indicator (fun x => 1) x ∂ν'
h2 :
  μ' s * ∫⁻ (y : G), t.indicator (fun x => 1) y⁻¹ / ν' ((fun x => x * y⁻¹) ⁻¹' s) ∂ν' =
    ∫⁻ (x : G), t.indicator (fun x => 1) x ∂μ'
⊢ μ' s * ν' t = ν' s * μ' t
-- Mathlib/Analysis/Complex/AbelLimit.lean
lemma nhdsWithin_stolzCone_le_nhdsWithin_stolzSet {s : ℝ} (hs : 0 < s) :
    ∃ M, 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1

Proof state:
case h
s : ℝ
hs : 0 < s
M ε : ℝ
left✝ : 0 < M
hε : 0 < ε
H : {z | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
⊢ ∃ u, IsOpen u ∧ 1 ∈ u ∧ u ∩ stolzCone s ⊆ stolzSet M

Tactic:
refine ⟨{w | 1 - ε < w.re}, isOpen_lt continuous_const continuous_re, ?_, H⟩

Result:
case h
s : ℝ
hs : 0 < s
M ε : ℝ
left✝ : 0 < M
hε : 0 < ε
H : {z | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
⊢ 1 ∈ {w | 1 - ε < w.re}

Proof state:
case h
s : ℝ
hs : 0 < s
M ε : ℝ
left✝ : 0 < M
hε : 0 < ε
H : {z | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
⊢ 1 ∈ {w | 1 - ε < w.re}

Tactic:
simp only [Set.mem_setOf_eq, one_re, sub_lt_self_iff, hε]

Result:
no goals

Proof state:
case h
s : ℝ
hs : 0 < s
M ε : ℝ
left✝ : 0 < M
hε : 0 < ε
H : {z | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
⊢ 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1

Tactic:
rw [nhdsWithin_le_iff, mem_nhdsWithin]

Result:
case h
s : ℝ
hs : 0 < s
M ε : ℝ
left✝ : 0 < M
hε : 0 < ε
H : {z | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
⊢ ∃ u, IsOpen u ∧ 1 ∈ u ∧ u ∩ stolzCone s ⊆ stolzSet M

Proof state:
s : ℝ
hs : 0 < s
⊢ ∃ M, 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1

Tactic:
obtain ⟨M, ε, _, hε, H⟩ := stolzCone_subset_stolzSet_aux hs

Result:
case intro.intro.intro.intro
s : ℝ
hs : 0 < s
M ε : ℝ
left✝ : 0 < M
hε : 0 < ε
H : {z | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
⊢ ∃ M, 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1

Proof state:
case intro.intro.intro.intro
s : ℝ
hs : 0 < s
M ε : ℝ
left✝ : 0 < M
hε : 0 < ε
H : {z | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
⊢ ∃ M, 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1

Tactic:
use M

Result:
case h
s : ℝ
hs : 0 < s
M ε : ℝ
left✝ : 0 < M
hε : 0 < ε
H : {z | 1 - ε < z.re} ∩ stolzCone s ⊆ stolzSet M
⊢ 𝓝[stolzCone s] 1 ≤ 𝓝[stolzSet M] 1
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem sum_nat_eq_add_sum_succ (f : ℕ → Cardinal.{u}) :
    Cardinal.sum f = f 0 + Cardinal.sum fun i => f (i + 1)

Proof state:
f : ℕ → Cardinal.{u}
⊢ sum f = f 0 + sum fun i => f (i + 1)

Tactic:
refine (Equiv.sigmaNatSucc fun i => Quotient.out (f i)).cardinal_eq.trans ?_

Result:
f : ℕ → Cardinal.{u}
⊢ #(Quotient.out (f 0) ⊕ (n : ℕ) × Quotient.out (f (n + 1))) = f 0 + sum fun i => f (i + 1)

Proof state:
f : ℕ → Cardinal.{u}
⊢ #(Quotient.out (f 0) ⊕ (n : ℕ) × Quotient.out (f (n + 1))) = f 0 + sum fun i => f (i + 1)

Tactic:
simp only [mk_sum, mk_out, lift_id, mk_sigma]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/SubMulAction.lean
theorem val_preimage_orbit {p : SubMulAction R M} (m : p) :
    Subtype.val ⁻¹' MulAction.orbit R (m : M) = MulAction.orbit R m

Proof state:
R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ Subtype.val ⁻¹' MulAction.orbit R ↑m = MulAction.orbit R m

Tactic:
rw [← val_image_orbit, Subtype.val_injective.preimage_image]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueFinset_map_of_equiv (e : α ≃ β) (n : ℕ) :
    (G.map e.toEmbedding).cliqueFinset n =
      (G.cliqueFinset n).map ⟨map e.toEmbedding, Finset.map_injective _⟩ :=
  coe_injective <| by push_cast; exact cliqueSet_map_of_equiv _ _ _

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype β
inst✝ : DecidableEq β
e : α ≃ β
n : ℕ
⊢ (SimpleGraph.map e.toEmbedding G).cliqueSet n = ⇑{ toFun := map e.toEmbedding, inj' := ⋯ } '' G.cliqueSet n

Tactic:
exact cliqueSet_map_of_equiv _ _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype β
inst✝ : DecidableEq β
e : α ≃ β
n : ℕ
⊢ ↑((SimpleGraph.map e.toEmbedding G).cliqueFinset n) =
    ↑(map { toFun := map e.toEmbedding, inj' := ⋯ } (G.cliqueFinset n))

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
inst✝⁴ : Fintype α
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype β
inst✝ : DecidableEq β
e : α ≃ β
n : ℕ
⊢ (SimpleGraph.map e.toEmbedding G).cliqueSet n = ⇑{ toFun := map e.toEmbedding, inj' := ⋯ } '' G.cliqueSet n