harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem map_one_div (I : FractionalIdeal R₁⁰ K) (h : K ≃ₐ[R₁] K') :
    (1 / I).map (h : K →ₐ[R₁] K') = 1 / I.map h

Proof state:
R₁ : Type u_3
inst✝⁷ : CommRing R₁
K : Type u_4
inst✝⁶ : Field K
inst✝⁵ : Algebra R₁ K
inst✝⁴ : IsFractionRing R₁ K
inst✝³ : IsDomain R₁
K' : Type u_5
inst✝² : Field K'
inst✝¹ : Algebra R₁ K'
inst✝ : IsFractionRing R₁ K'
I : FractionalIdeal R₁⁰ K
h : K ≃ₐ[R₁] K'
⊢ map (↑h) (1 / I) = 1 / map (↑h) I

Tactic:
rw [map_div, map_one]

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem map_toSubmodule (h : ↑(map f I) = f '' I) :
    LieSubmodule.toSubmodule (map f I) = (LieSubmodule.toSubmodule I).map (f : L →ₗ[R] L')

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : ↑(map f I) = ⇑f '' ↑I
⊢ ↑(map f I) = Submodule.map ↑f ↑I

Tactic:
rw [SetLike.ext'_iff, LieSubmodule.coe_toSubmodule, h, Submodule.map_coe]

Result:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : ↑(map f I) = ⇑f '' ↑I
⊢ ⇑f '' ↑I = ⇑↑f '' ↑↑I

Proof state:
R : Type u
L : Type v
L' : Type w₂
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieRing L'
inst✝¹ : LieAlgebra R L'
inst✝ : LieAlgebra R L
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
h : ↑(map f I) = ⇑f '' ↑I
⊢ ⇑f '' ↑I = ⇑↑f '' ↑↑I

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Height.lean
theorem le_chainHeight_TFAE (n : ℕ) :
    TFAE [↑n ≤ s.chainHeight, ∃ l ∈ s.subchain, length l = n, ∃ l ∈ s.subchain, n ≤ length l]

Proof state:
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
⊢ [↑n ≤ s.chainHeight, ∃ l ∈ s.subchain, l.length = n, ∃ l ∈ s.subchain, n ≤ l.length].TFAE

Tactic:
tfae_have 1 → 2 := s.exists_chain_of_le_chainHeight

Result:
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
tfae_1_to_2 : ↑n ≤ s.chainHeight → ∃ l ∈ s.subchain, l.length = n
⊢ [↑n ≤ s.chainHeight, ∃ l ∈ s.subchain, l.length = n, ∃ l ∈ s.subchain, n ≤ l.length].TFAE

Proof state:
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
tfae_1_to_2 : ↑n ≤ s.chainHeight → ∃ l ∈ s.subchain, l.length = n
tfae_2_to_3 : (∃ l ∈ s.subchain, l.length = n) → ∃ l ∈ s.subchain, n ≤ l.length
tfae_3_to_1 : (∃ l ∈ s.subchain, n ≤ l.length) → ↑n ≤ s.chainHeight
⊢ [↑n ≤ s.chainHeight, ∃ l ∈ s.subchain, l.length = n, ∃ l ∈ s.subchain, n ≤ l.length].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
tfae_1_to_2 : ↑n ≤ s.chainHeight → ∃ l ∈ s.subchain, l.length = n
tfae_2_to_3 : (∃ l ∈ s.subchain, l.length = n) → ∃ l ∈ s.subchain, n ≤ l.length
⊢ [↑n ≤ s.chainHeight, ∃ l ∈ s.subchain, l.length = n, ∃ l ∈ s.subchain, n ≤ l.length].TFAE

Tactic:
tfae_have 3 → 1 := fun ⟨l, hs, hn⟩ ↦ le_iSup₂_of_le l hs (WithTop.coe_le_coe.2 hn)

Result:
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
tfae_1_to_2 : ↑n ≤ s.chainHeight → ∃ l ∈ s.subchain, l.length = n
tfae_2_to_3 : (∃ l ∈ s.subchain, l.length = n) → ∃ l ∈ s.subchain, n ≤ l.length
tfae_3_to_1 : (∃ l ∈ s.subchain, n ≤ l.length) → ↑n ≤ s.chainHeight
⊢ [↑n ≤ s.chainHeight, ∃ l ∈ s.subchain, l.length = n, ∃ l ∈ s.subchain, n ≤ l.length].TFAE

Proof state:
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
tfae_1_to_2 : ↑n ≤ s.chainHeight → ∃ l ∈ s.subchain, l.length = n
⊢ [↑n ≤ s.chainHeight, ∃ l ∈ s.subchain, l.length = n, ∃ l ∈ s.subchain, n ≤ l.length].TFAE

Tactic:
tfae_have 2 → 3 := fun ⟨l, hls, he⟩ ↦ ⟨l, hls, he.ge⟩

Result:
α : Type u_1
inst✝ : LT α
s : Set α
n : ℕ
tfae_1_to_2 : ↑n ≤ s.chainHeight → ∃ l ∈ s.subchain, l.length = n
tfae_2_to_3 : (∃ l ∈ s.subchain, l.length = n) → ∃ l ∈ s.subchain, n ≤ l.length
⊢ [↑n ≤ s.chainHeight, ∃ l ∈ s.subchain, l.length = n, ∃ l ∈ s.subchain, n ≤ l.length].TFAE
-- Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
@[reassoc (attr := simp)]
lemma inr_f_triangle_mor₃_f (p : ℤ) : (inr φ).f p ≫ (triangle φ).mor₃.f p = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
p : ℤ
⊢ (inr φ).f p ≫ ((-↑(fst φ)).rightShift 1 0 triangle.proof_3).v p p ⋯ = 0

Tactic:
simp only [Cochain.rightShift_neg, Cochain.neg_v, shiftFunctor_obj_X',
  Cochain.rightShift_v _ 1 0 _ p p (add_zero p) (p + 1) rfl, shiftFunctor_obj_X,
  shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_inv, comp_id,
  Preadditive.comp_neg, inr_f_fst_v, neg_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
p : ℤ
⊢ (inr φ).f p ≫ (triangle φ).mor₃.f p = 0

Tactic:
dsimp [triangle]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
p : ℤ
⊢ (inr φ).f p ≫ ((-↑(fst φ)).rightShift 1 0 triangle.proof_3).v p p ⋯ = 0
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma finsetSup_mem (hC : IsSetRing C) {ι : Type*} {s : ι → Set α} {t : Finset ι}
    (hs : ∀ i ∈ t, s i ∈ C) :
    t.sup s ∈ C

Proof state:
case empty
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
ι : Type u_2
s : ι → Set α
hs : ∀ i ∈ ∅, s i ∈ C
⊢ ∅.sup s ∈ C

Tactic:
exact hC.empty_mem

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
ι : Type u_2
s : ι → Set α
t : Finset ι
hs : ∀ i ∈ t, s i ∈ C
⊢ t.sup s ∈ C

Tactic:
classical
induction t using Finset.induction_on with
| empty => exact hC.empty_mem
| @insert m t hm ih =>
  simpa only [sup_insert] using
    hC.union_mem (hs m <| mem_insert_self m t) (ih <| fun i hi ↦ hs _ <| mem_insert_of_mem hi)

Result:
no goals

Proof state:
case insert
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
ι : Type u_2
s : ι → Set α
m : ι
t : Finset ι
hm : m ∉ t
ih : (∀ i ∈ t, s i ∈ C) → t.sup s ∈ C
hs : ∀ i ∈ insert m t, s i ∈ C
⊢ (insert m t).sup s ∈ C

Tactic:
simpa only [sup_insert] using
  hC.union_mem (hs m <| mem_insert_self m t) (ih <| fun i hi ↦ hs _ <| mem_insert_of_mem hi)

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
ι : Type u_2
s : ι → Set α
t : Finset ι
hs : ∀ i ∈ t, s i ∈ C
⊢ t.sup s ∈ C

Tactic:
induction t using Finset.induction_on with
| empty => exact hC.empty_mem
| @insert m t hm ih =>
  simpa only [sup_insert] using
    hC.union_mem (hs m <| mem_insert_self m t) (ih <| fun i hi ↦ hs _ <| mem_insert_of_mem hi)

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem hasBasis_self {l : Filter α} {P : Set α → Prop} :
    HasBasis l (fun s => s ∈ l ∧ P s) id ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t

Proof state:
α : Type u_1
l : Filter α
P : Set α → Prop
⊢ (∀ (t : Set α), t ∈ l ↔ ∃ i ∈ l, P i ∧ i ⊆ t) ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t

Tactic:
exact forall_congr' fun s =>
  ⟨fun h => h.1, fun h => ⟨h, fun ⟨t, hl, _, hts⟩ => mem_of_superset hl hts⟩⟩

Result:
no goals

Proof state:
α : Type u_1
l : Filter α
P : Set α → Prop
⊢ l.HasBasis (fun s => s ∈ l ∧ P s) id ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t

Tactic:
simp only [hasBasis_iff, id, and_assoc]

Result:
α : Type u_1
l : Filter α
P : Set α → Prop
⊢ (∀ (t : Set α), t ∈ l ↔ ∃ i ∈ l, P i ∧ i ⊆ t) ↔ ∀ t ∈ l, ∃ r ∈ l, P r ∧ r ⊆ t
-- Mathlib/Probability/Independence/Kernel.lean
theorem iIndepSets.indepSets {s : ι → Set (Set Ω)} {_mΩ : MeasurableSpace Ω}
    {κ : Kernel α Ω} {μ : Measure α} (h_indep : iIndepSets s κ μ) {i j : ι} (hij : i ≠ j) :
    IndepSets (s i) (s j) κ μ

Proof state:
case h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
hf_m : ∀ x ∈ {i, j}, (if x = i then t₁ else t₂) ∈ s x
h1 : t₁ = if i = i then t₁ else t₂
h2 : t₂ = if j = i then t₁ else t₂
h_inter : (⋂ t ∈ {i, j}, if t = i then t₁ else t₂) = (if i = i then t₁ else t₂) ∩ if j = i then t₁ else t₂
a : α
h_indep' : (κ a) (⋂ i_1 ∈ {i, j}, if i_1 = i then t₁ else t₂) = ∏ i_1 ∈ {i, j}, (κ a) (if i_1 = i then t₁ else t₂)
⊢ (κ a) (t₁ ∩ t₂) = (κ a) t₁ * (κ a) t₂

Tactic:
have h_prod : (∏ t ∈ ({i, j} : Finset ι), κ a (ite (t = i) t₁ t₂))
    = κ a (ite (i = i) t₁ t₂) * κ a (ite (j = i) t₁ t₂) := by
  simp only [hij, Finset.prod_singleton, Finset.prod_insert, not_false_iff,
    Finset.mem_singleton]

Result:
case h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
hf_m : ∀ x ∈ {i, j}, (if x = i then t₁ else t₂) ∈ s x
h1 : t₁ = if i = i then t₁ else t₂
h2 : t₂ = if j = i then t₁ else t₂
h_inter : (⋂ t ∈ {i, j}, if t = i then t₁ else t₂) = (if i = i then t₁ else t₂) ∩ if j = i then t₁ else t₂
a : α
h_indep' : (κ a) (⋂ i_1 ∈ {i, j}, if i_1 = i then t₁ else t₂) = ∏ i_1 ∈ {i, j}, (κ a) (if i_1 = i then t₁ else t₂)
h_prod :
  ∏ t ∈ {i, j}, (κ a) (if t = i then t₁ else t₂) = (κ a) (if i = i then t₁ else t₂) * (κ a) (if j = i then t₁ else t₂)
⊢ (κ a) (t₁ ∩ t₂) = (κ a) t₁ * (κ a) t₂

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
hf_m : ∀ x ∈ {i, j}, (if x = i then t₁ else t₂) ∈ s x
h1 : t₁ = if i = i then t₁ else t₂
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t₁ ∩ t₂) = (κ a) t₁ * (κ a) t₂

Tactic:
have h2 : t₂ = ite (j = i) t₁ t₂ := by simp only [hij.symm, if_false]

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h_indep : iIndepSets s κ μ
i j : ι
hij : i ≠ j
t₁ t₂ : Set Ω
ht₁ : t₁ ∈ s i
ht₂ : t₂ ∈ s j
hf_m : ∀ x ∈ {i, j}, (if x = i then t₁ else t₂) ∈ s x
h1 : t₁ = if i = i then t₁ else t₂
h2 : t₂ = if j = i then t₁ else t₂
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t₁ ∩ t₂) = (κ a) t₁ * (κ a) t₂
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_natCast (a : Ordinal) (n : ℕ) : a ^ (n : Ordinal) = a ^ n

Proof state:
a : Ordinal.{u_1}
n : ℕ
⊢ a ^ ↑n = a ^ n

Tactic:
induction n with
| zero => rw [Nat.cast_zero, opow_zero, pow_zero]
| succ n IH => rw [Nat.cast_succ, add_one_eq_succ, opow_succ, pow_succ, IH]

Result:
no goals

Proof state:
case succ
a : Ordinal.{u_1}
n : ℕ
IH : a ^ ↑n = a ^ n
⊢ a ^ ↑(n + 1) = a ^ (n + 1)

Tactic:
rw [Nat.cast_succ, add_one_eq_succ, opow_succ, pow_succ, IH]

Result:
no goals

Proof state:
case zero
a : Ordinal.{u_1}
⊢ a ^ ↑0 = a ^ 0

Tactic:
rw [Nat.cast_zero, opow_zero, pow_zero]

Result:
no goals
-- Mathlib/Data/Sum/Interval.lean
theorem mem_sumLift₂ :
    c ∈ sumLift₂ f g a b ↔
      (∃ a₁ b₁ c₁, a = inl a₁ ∧ b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
        ∃ a₂ b₂ c₂, a = inr a₂ ∧ b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂

Proof state:
case mp.inl.inl.intro.intro
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
a : α₁
b : β₁
c : γ₁
hc : c ∈ f a b
⊢ (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inl b = inl b₁ ∧ Embedding.inl c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
    ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inl b = inr b₂ ∧ Embedding.inl c = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
exact Or.inl ⟨a, b, c, rfl, rfl, rfl, hc⟩

Result:
no goals

Proof state:
case mp.inl.inr
α₁ : Type u_1
α₂ : Type u_2
β₁ : Type u_3
β₂ : Type u_4
γ₁ : Type u_5
γ₂ : Type u_6
f : α₁ → β₁ → Finset γ₁
g : α₂ → β₂ → Finset γ₂
c : γ₁ ⊕ γ₂
a : α₁
b : β₂
⊢ c ∈ sumLift₂ f g (inl a) (inr b) →
    (∃ a₁ b₁ c₁, inl a = inl a₁ ∧ inr b = inl b₁ ∧ c = inl c₁ ∧ c₁ ∈ f a₁ b₁) ∨
      ∃ a₂ b₂ c₂, inl a = inr a₂ ∧ inr b = inr b₂ ∧ c = inr c₂ ∧ c₂ ∈ g a₂ b₂

Tactic:
refine fun h ↦ (not_mem_empty _ h).elim

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem formPerm_apply_mem_eq_next (hl : Nodup l) (x : α) (hx : x ∈ l) :
    formPerm l x = next l x hx

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
x : α
hx : x ∈ l
⊢ l.formPerm x = l.next x hx

Tactic:
obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ l.formPerm l[k] = l.next l[k] hx

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
l : List α
hl : l.Nodup
k : ℕ
hk : k < l.length
hx : l[k] ∈ l
⊢ l.formPerm l[k] = l.next l[k] hx

Tactic:
rw [next_getElem _ hl, formPerm_apply_getElem _ hl]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem continuousWithinAt_congr_set' [TopologicalSpace Y] [T1Space X]
    {x : X} {s t : Set X} {f : X → Y} (y : X) (h : s =ᶠ[𝓝[{y}ᶜ] x] t) :
    ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x : X
s t : Set X
f : X → Y
y : X
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x

Tactic:
rw [← continuousWithinAt_insert_self (s := s), ← continuousWithinAt_insert_self (s := t)]

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x : X
s t : Set X
f : X → Y
y : X
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f (insert x t) x

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x : X
s t : Set X
f : X → Y
y : X
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f (insert x t) x

Tactic:
exact continuousWithinAt_congr_set (eventuallyEq_insert h)

Result:
no goals
-- Mathlib/Tactic/CancelDenoms/Core.lean
theorem cancel_factors_eq_div {α} [Field α] {n e e' : α}
    (h : n * e = e') (h2 : n ≠ 0) : e = e' / n :=
  eq_div_of_mul_eq h2 <| by rwa [mul_comm] at h

Proof state:
α : Type u_1
inst✝ : Field α
n e e' : α
h : n * e = e'
h2 : n ≠ 0
⊢ e * n = e'

Tactic:
rwa [mul_comm] at h

Result:
no goals
-- Mathlib/Order/Interval/Set/SuccPred.lean
lemma Ioi_pred_eq_Ici_of_not_isMin (ha : ¬ IsMin a) : Ioi (pred a) = Ici a

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
x : α
⊢ x ∈ Ioi (pred a) ↔ x ∈ Ici a

Tactic:
rw [mem_Ioi, mem_Ici, pred_lt_iff_of_not_isMin ha]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
⊢ Ioi (pred a) = Ici a

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a : α
ha : ¬IsMin a
x : α
⊢ x ∈ Ioi (pred a) ↔ x ∈ Ici a
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem image_coe_closedBall (z : ℍ) (r : ℝ) :
    ((↑) : ℍ → ℂ) '' closedBall (α := ℍ) z r = closedBall ↑(z.center r) (z.im * Real.sinh r)

Proof state:
case h.mpr
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ closedBall (↑(z.center r)) (z.im * Real.sinh r) → w ∈ UpperHalfPlane.coe '' closedBall z r

Tactic:
intro hw

Result:
case h.mpr
z : ℍ
r : ℝ
w : ℂ
hw : w ∈ closedBall (↑(z.center r)) (z.im * Real.sinh r)
⊢ w ∈ UpperHalfPlane.coe '' closedBall z r

Proof state:
case h.mpr.intro
z : ℍ
r : ℝ
w : ℍ
hw : ↑w ∈ closedBall (↑(z.center r)) (z.im * Real.sinh r)
⊢ ↑w ∈ UpperHalfPlane.coe '' closedBall z r

Tactic:
exact mem_image_of_mem _ (dist_le_iff_dist_coe_center_le.2 hw)

Result:
no goals

Proof state:
case h
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' closedBall z r ↔ w ∈ closedBall (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
constructor

Result:
case h.mp
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' closedBall z r → w ∈ closedBall (↑(z.center r)) (z.im * Real.sinh r)

case h.mpr
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ closedBall (↑(z.center r)) (z.im * Real.sinh r) → w ∈ UpperHalfPlane.coe '' closedBall z r

Proof state:
case h.mpr
z : ℍ
r : ℝ
w : ℂ
hw : w ∈ closedBall (↑(z.center r)) (z.im * Real.sinh r)
⊢ w ∈ UpperHalfPlane.coe '' closedBall z r

Tactic:
lift w to ℍ using im_pos_of_dist_center_le hw

Result:
case h.mpr.intro
z : ℍ
r : ℝ
w : ℍ
hw : ↑w ∈ closedBall (↑(z.center r)) (z.im * Real.sinh r)
⊢ ↑w ∈ UpperHalfPlane.coe '' closedBall z r

Proof state:
z : ℍ
r : ℝ
⊢ UpperHalfPlane.coe '' closedBall z r = closedBall (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
ext w

Result:
case h
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' closedBall z r ↔ w ∈ closedBall (↑(z.center r)) (z.im * Real.sinh r)

Proof state:
case h.mp
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' closedBall z r → w ∈ closedBall (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
rintro ⟨w, hw, rfl⟩

Result:
case h.mp.intro.intro
z : ℍ
r : ℝ
w : ℍ
hw : w ∈ closedBall z r
⊢ ↑w ∈ closedBall (↑(z.center r)) (z.im * Real.sinh r)

Proof state:
case h.mp.intro.intro
z : ℍ
r : ℝ
w : ℍ
hw : w ∈ closedBall z r
⊢ ↑w ∈ closedBall (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
exact dist_le_iff_dist_coe_center_le.1 hw

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.mul [Add α] [Mul β] (hf : Periodic f c) (hg : Periodic g c) :
    Periodic (f * g) c

Proof state:
α : Type u_1
β : Type u_2
f g : α → β
c : α
inst✝¹ : Add α
inst✝ : Mul β
hf : Periodic f c
hg : Periodic g c
⊢ Periodic (f * g) c

Tactic:
simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filterMap_append {α β : Type _} (l l' : List α) (f : α → Option β) :
    filterMap f (l ++ l') = filterMap f l ++ filterMap f l'

Proof state:
case cons
α : Type u_1
β : Type u_2
l' : List α
f : α → Option β
head✝ : α
tail✝ : List α
tail_ih✝ : filterMap f (tail✝ ++ l') = filterMap f tail✝ ++ filterMap f l'
⊢ (match f head✝ with
    | none => filterMap f (tail✝ ++ l')
    | some b => b :: filterMap f (tail✝ ++ l')) =
    (match f head✝ with
      | none => filterMap f tail✝
      | some b => b :: filterMap f tail✝) ++
      filterMap f l'

Tactic:
split <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l l' : List α
f : α → Option β
⊢ filterMap f (l ++ l') = filterMap f l ++ filterMap f l'

Tactic:
induction l <;> simp [filterMap_cons]

Result:
case cons
α : Type u_1
β : Type u_2
l' : List α
f : α → Option β
head✝ : α
tail✝ : List α
tail_ih✝ : filterMap f (tail✝ ++ l') = filterMap f tail✝ ++ filterMap f l'
⊢ (match f head✝ with
    | none => filterMap f (tail✝ ++ l')
    | some b => b :: filterMap f (tail✝ ++ l')) =
    (match f head✝ with
      | none => filterMap f tail✝
      | some b => b :: filterMap f tail✝) ++
      filterMap f l'
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma CFC.eq_algebraMap_of_spectrum_subset_singleton (r : R) (h_spec : spectrum R a ⊆ {r})
    (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
r : R
h_spec : spectrum R a ⊆ {r}
ha : autoParam (p a) _auto✝
x : R
hx : x ∈ spectrum R a
⊢ id x = (fun x => r) x

Tactic:
simpa using h_spec hx

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
a : A
r : R
h_spec : spectrum R a ⊆ {r}
ha : autoParam (p a) _auto✝
⊢ a = (algebraMap R A) r

Tactic:
simpa [cfc_id R a, cfc_const r a] using
  cfc_congr (f := id) (g := fun _ : R ↦ r) (a := a) fun x hx ↦ by simpa using h_spec hx

Result:
no goals
-- Mathlib/Data/Finmap.lean
theorem mem_list_toFinmap (a : α) (xs : List (Sigma β)) :
    a ∈ xs.toFinmap ↔ ∃ b : β a, Sigma.mk a b ∈ xs

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ a ∈ [].toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ []

Tactic:
simp only [toFinmap_nil, not_mem_empty, find?, not_mem_nil, exists_false]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
⊢ a ∈ (x :: xs).toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ x :: xs

Tactic:
obtain ⟨fst_i, snd_i⟩ := x

Result:
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
fst_i : α
snd_i : β fst_i
⊢ a ∈ (⟨fst_i, snd_i⟩ :: xs).toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ ⟨fst_i, snd_i⟩ :: xs

Proof state:
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
fst_i : α
snd_i : β fst_i
⊢ a ∈ (⟨fst_i, snd_i⟩ :: xs).toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ ⟨fst_i, snd_i⟩ :: xs

Tactic:
simp only [toFinmap_cons, *, exists_or, mem_cons, mem_insert, exists_and_left, Sigma.mk.inj_iff]

Result:
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
fst_i : α
snd_i : β fst_i
⊢ (a = fst_i ∨ ∃ b, ⟨a, b⟩ ∈ xs) ↔ (a = fst_i ∧ ∃ x, HEq x snd_i) ∨ ∃ x, ⟨a, x⟩ ∈ xs

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
⊢ a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs

Tactic:
induction' xs with x xs

Result:
case nil
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ a ∈ [].toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ []

case cons
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
x : Sigma β
xs : List (Sigma β)
tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
⊢ a ∈ (x :: xs).toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ x :: xs

Proof state:
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
snd_i : β a
⊢ ∃ x, HEq x snd_i

Tactic:
simp only [exists_eq, heq_iff_eq]

Result:
no goals

Proof state:
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
fst_i : α
snd_i : β fst_i
⊢ (a = fst_i ∨ ∃ b, ⟨a, b⟩ ∈ xs) ↔ (a = fst_i ∧ ∃ x, HEq x snd_i) ∨ ∃ x, ⟨a, x⟩ ∈ xs

Tactic:
refine (or_congr_left <| and_iff_left_of_imp ?_).symm

Result:
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
fst_i : α
snd_i : β fst_i
⊢ a = fst_i → ∃ x, HEq x snd_i

Proof state:
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
fst_i : α
snd_i : β fst_i
⊢ a = fst_i → ∃ x, HEq x snd_i

Tactic:
rintro rfl

Result:
case cons.mk
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih✝ : a ∈ xs.toFinmap ↔ ∃ b, ⟨a, b⟩ ∈ xs
snd_i : β a
⊢ ∃ x, HEq x snd_i
-- Mathlib/CategoryTheory/Groupoid/FreeGroupoid.lean
theorem lift_spec (φ : V ⥤q V') : of V ⋙q (lift φ).toPrefunctor = φ

Proof state:
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
⊢ Quiver.Symmetrify.of ⋙q (Paths.of ⋙q (Quotient.functor redStep ⋙ lift φ).toPrefunctor) = φ

Tactic:
dsimp [lift]

Result:
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
⊢ Quiver.Symmetrify.of ⋙q
      (Paths.of ⋙q
        (Quotient.functor redStep ⋙ Quotient.lift redStep (Paths.lift (Quiver.Symmetrify.lift φ)) ⋯).toPrefunctor) =
    φ

Proof state:
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
⊢ of V ⋙q (lift φ).toPrefunctor = φ

Tactic:
rw [of_eq, Prefunctor.comp_assoc, Prefunctor.comp_assoc, Functor.toPrefunctor_comp]

Result:
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
⊢ Quiver.Symmetrify.of ⋙q (Paths.of ⋙q (Quotient.functor redStep ⋙ lift φ).toPrefunctor) = φ

Proof state:
V : Type u
inst✝¹ : Quiver V
V' : Type u'
inst✝ : Groupoid V'
φ : V ⥤q V'
⊢ Quiver.Symmetrify.of ⋙q
      (Paths.of ⋙q
        (Quotient.functor redStep ⋙ Quotient.lift redStep (Paths.lift (Quiver.Symmetrify.lift φ)) ⋯).toPrefunctor) =
    φ

Tactic:
rw [Quotient.lift_spec, Paths.lift_spec, Quiver.Symmetrify.lift_spec]

Result:
no goals