harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/Embedding/IsSupported.lean
lemma isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside :
    IsZero K ↔ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e

Proof state:
case mpr.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{u_4, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
⊢ 𝟙 K = 0

Tactic:
ext n

Result:
case mpr.intro.h
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{u_4, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
⊢ (𝟙 K).f n = Hom.f 0 n

Proof state:
case mpr.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{u_4, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
⊢ IsZero K

Tactic:
rw [IsZero.iff_id_eq_zero]

Result:
case mpr.intro
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{u_4, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
⊢ 𝟙 K = 0

Proof state:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝¹ : Category.{u_4, u_3} C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
hn : ¬∃ i, e.f i = n
⊢ IsZero (K.X n)

Tactic:
exact K.isZero_X_of_isStrictlySupported e _ (by simpa using hn)

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem toBlock_mul_eq_add {m n k : Type*} [Fintype n] (p : m → Prop) (q : n → Prop)
    [DecidablePred q] (r : k → Prop) (A : Matrix m n R) (B : Matrix n k R) : (A * B).toBlock p r =
    A.toBlock p q * B.toBlock q r + (A.toBlock p fun i => ¬q i) * B.toBlock (fun i => ¬q i) r

Proof state:
R : Type u_10
inst✝² : CommRing R
m : Type u_14
n : Type u_15
k : Type u_16
inst✝¹ : Fintype n
p : m → Prop
q : n → Prop
inst✝ : DecidablePred q
r : k → Prop
A : Matrix m n R
B : Matrix n k R
⊢ (A * B).toBlock p r = A.toBlock p q * B.toBlock q r + (A.toBlock p fun i => ¬q i) * B.toBlock (fun i => ¬q i) r

Tactic:
ext i k

Result:
case a
R : Type u_10
inst✝² : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝¹ : Fintype n
p : m → Prop
q : n → Prop
inst✝ : DecidablePred q
r : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // r a }
⊢ (A * B).toBlock p r i k =
    (A.toBlock p q * B.toBlock q r + (A.toBlock p fun i => ¬q i) * B.toBlock (fun i => ¬q i) r) i k

Proof state:
case a
R : Type u_10
inst✝² : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝¹ : Fintype n
p : m → Prop
q : n → Prop
inst✝ : DecidablePred q
r : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // r a }
⊢ (A * B).toBlock p r i k =
    (A.toBlock p q * B.toBlock q r + (A.toBlock p fun i => ¬q i) * B.toBlock (fun i => ¬q i) r) i k

Tactic:
simp only [toBlock_apply, mul_apply, Pi.add_apply]

Result:
case a
R : Type u_10
inst✝² : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝¹ : Fintype n
p : m → Prop
q : n → Prop
inst✝ : DecidablePred q
r : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // r a }
⊢ ∑ j : n, A (↑i) j * B j ↑k =
    (A.toBlock p q * B.toBlock q r + (A.toBlock p fun i => ¬q i) * B.toBlock (fun i => ¬q i) r) i k

Proof state:
R : Type u_10
inst✝² : CommRing R
m : Type u_14
n : Type u_15
k : Type u_16
inst✝¹ : Fintype n
p : m → Prop
q : n → Prop
inst✝ : DecidablePred q
r : k → Prop
A : Matrix m n R
B : Matrix n k R
⊢ (A * B).toBlock p r = A.toBlock p q * B.toBlock q r + (A.toBlock p fun i => ¬q i) * B.toBlock (fun i => ¬q i) r

Tactic:
classical
  ext i k
  simp only [toBlock_apply, mul_apply, Pi.add_apply]
  exact (Fintype.sum_subtype_add_sum_subtype q fun x => A (↑i) x * B x ↑k).symm

Result:
no goals

Proof state:
case a
R : Type u_10
inst✝² : CommRing R
m : Type u_14
n : Type u_15
k✝ : Type u_16
inst✝¹ : Fintype n
p : m → Prop
q : n → Prop
inst✝ : DecidablePred q
r : k✝ → Prop
A : Matrix m n R
B : Matrix n k✝ R
i : { a // p a }
k : { a // r a }
⊢ ∑ j : n, A (↑i) j * B j ↑k =
    (A.toBlock p q * B.toBlock q r + (A.toBlock p fun i => ¬q i) * B.toBlock (fun i => ¬q i) r) i k

Tactic:
exact (Fintype.sum_subtype_add_sum_subtype q fun x => A (↑i) x * B x ↑k).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem IsPrefix.find?_eq_some {l₁ l₂ : List α} {p : α → Bool} (h : l₁ <+: l₂) :
    List.find? p l₁ = some b → List.find? p l₂ = some b

Proof state:
α : Type u_1
b : α
l₁ l₂ : List α
p : α → Bool
h : l₁ <+: l₂
⊢ find? p l₁ = some b → find? p l₂ = some b

Tactic:
rw [IsPrefix] at h

Result:
α : Type u_1
b : α
l₁ l₂ : List α
p : α → Bool
h : ∃ t, l₁ ++ t = l₂
⊢ find? p l₁ = some b → find? p l₂ = some b

Proof state:
α : Type u_1
b : α
l₁ l₂ : List α
p : α → Bool
h : ∃ t, l₁ ++ t = l₂
⊢ find? p l₁ = some b → find? p l₂ = some b

Tactic:
obtain ⟨t, rfl⟩ := h

Result:
case intro
α : Type u_1
b : α
l₁ : List α
p : α → Bool
t : List α
⊢ find? p l₁ = some b → find? p (l₁ ++ t) = some b

Proof state:
case intro
α : Type u_1
b : α
l₁ : List α
p : α → Bool
t : List α
⊢ find? p l₁ = some b → find? p (l₁ ++ t) = some b

Tactic:
simp +contextual [find?_append]

Result:
no goals
-- Mathlib/ModelTheory/Encoding.lean
theorem listDecode_encode_list (l : List (L.Term α)) :
    listDecode (l.flatMap listEncode) = l

Proof state:
case func
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
h : listDecode (flatMap (fun i => (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
⊢ (fun i => (List.map ts (finRange n) ++ listDecode l)[↑i]) = ts ∧
    drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l

Tactic:
refine ⟨funext (fun i => ?_), ?_⟩

Result:
case func.refine_1
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
h : listDecode (flatMap (fun i => (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
i : Fin n
⊢ (List.map ts (finRange n) ++ listDecode l)[↑i] = ts i

case func.refine_2
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
h : listDecode (flatMap (fun i => (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
⊢ drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l

Proof state:
L : Language
α : Type u'
l : List (L.Term α)
t : L.Term α
⊢ ∀ (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode (t.listEncode ++ l) = t :: listDecode l

Tactic:
induction' t with a n f ts ih <;> intro l

Result:
case var
L : Language
α : Type u'
l✝ : List (L.Term α)
a : α
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ listDecode ((var a).listEncode ++ l) = var a :: listDecode l

case func
L : Language
α : Type u'
l✝ : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n) (l : List (α ⊕ (i : ℕ) × L.Functions i)), listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (α ⊕ (i : ℕ) × L.Functions i)
⊢ listDecode ((func f ts).listEncode ++ l) = func f ts :: listDecode l
-- Mathlib/Analysis/Convex/Segment.lean
theorem mem_openSegment_translate (a : E) {x b c : E} :
    a + x ∈ openSegment 𝕜 (a + b) (a + c) ↔ x ∈ openSegment 𝕜 b c

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a x b c : E
⊢ a + x ∈ openSegment 𝕜 (a + b) (a + c) ↔ x ∈ openSegment 𝕜 b c

Tactic:
simp_rw [← vadd_eq_add, ← vadd_openSegment, vadd_mem_vadd_set_iff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Lemmas.lean
theorem equiv_rootD : Equiv self (self.rootD a) a

Proof state:
self : UnionFind
a : Nat
⊢ self.Equiv (self.rootD a) a

Tactic:
simp [Equiv, rootD_rootD]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem hausdorffMeasure_segment {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [MeasurableSpace E] [BorelSpace E] (x y : E) : μH[1] (segment ℝ x y) = edist x y

Proof state:
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
x y : E
⊢ μH[1] (segment ℝ x y) = edist x y

Tactic:
rw [← affineSegment_eq_segment, hausdorffMeasure_affineSegment]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Localization.lean
private lemma auxHom_auxInv : (auxHom S r).toRingHom.comp (auxInv S r) = RingHom.id S

Proof state:
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
⊢ (IsLocalization.Away.auxHom S r).comp (IsLocalization.Away.auxInv S r) = RingHom.id S

Tactic:
apply IsLocalization.ringHom_ext (Submonoid.powers r)

Result:
case h
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
⊢ ((IsLocalization.Away.auxHom S r).comp (IsLocalization.Away.auxInv S r)).comp (algebraMap R S) =
    (RingHom.id S).comp (algebraMap R S)

Proof state:
case h
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
⊢ ((IsLocalization.Away.auxHom S r).comp (IsLocalization.Away.auxInv S r)).comp (algebraMap R S) =
    (RingHom.id S).comp (algebraMap R S)

Tactic:
ext x

Result:
case h.a
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : R
⊢ (((IsLocalization.Away.auxHom S r).comp (IsLocalization.Away.auxInv S r)).comp (algebraMap R S)) x =
    ((RingHom.id S).comp (algebraMap R S)) x

Proof state:
case h.a
R : Type u_2
inst✝³ : CommRing R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
x : R
⊢ (((IsLocalization.Away.auxHom S r).comp (IsLocalization.Away.auxInv S r)).comp (algebraMap R S)) x =
    ((RingHom.id S).comp (algebraMap R S)) x

Tactic:
simp [auxInv]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem contractRight_comm (x : CliffordAlgebra Q) : x⌊d⌊d' = -(x⌊d'⌊d)

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d d' : Module.Dual R M
x : CliffordAlgebra Q
⊢ (contractRight ((contractRight x) d)) d' = -(contractRight ((contractRight x) d')) d

Tactic:
rw [contractRight_eq, contractRight_eq, contractRight_eq, contractRight_eq, reverse_reverse,
  reverse_reverse, contractLeft_comm, map_neg]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem _root_.MeasurableEmbedding.integrableAtFilter_map_iff [MeasurableSpace β] {e : α → β}
    (he : MeasurableEmbedding e) {f : β → E} :
    IntegrableAtFilter f (l.map e) (μ.map e) ↔ IntegrableAtFilter (f ∘ e) l μ

Proof state:
case mp.intro
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
s : Set β
hs : s ∈ map e l ∧ IntegrableOn (f ∘ e) (e ⁻¹' s) μ
⊢ ∃ s ∈ l, IntegrableOn (f ∘ e) s μ

Tactic:
exact ⟨_, hs⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
⊢ IntegrableAtFilter f (map e l) (Measure.map e μ) ↔ IntegrableAtFilter (f ∘ e) l μ

Tactic:
simp_rw [IntegrableAtFilter, he.integrableOn_map_iff]

Result:
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
⊢ (∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ) ↔ ∃ s ∈ l, IntegrableOn (f ∘ e) s μ

Proof state:
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
s : Set α
hs : s ∈ l ∧ IntegrableOn (f ∘ e) s μ
⊢ e '' s ∈ map e l ∧ IntegrableOn (f ∘ e) (e ⁻¹' (e '' s)) μ

Tactic:
rwa [mem_map, he.injective.preimage_image]

Result:
no goals

Proof state:
case mpr.intro
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
s : Set α
hs : s ∈ l ∧ IntegrableOn (f ∘ e) s μ
⊢ ∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ

Tactic:
exact ⟨e '' s, by rwa [mem_map, he.injective.preimage_image]⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
⊢ (∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ) ↔ ∃ s ∈ l, IntegrableOn (f ∘ e) s μ

Tactic:
constructor <;> rintro ⟨s, hs⟩

Result:
case mp.intro
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
s : Set β
hs : s ∈ map e l ∧ IntegrableOn (f ∘ e) (e ⁻¹' s) μ
⊢ ∃ s ∈ l, IntegrableOn (f ∘ e) s μ

case mpr.intro
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
l : Filter α
inst✝ : MeasurableSpace β
e : α → β
he : MeasurableEmbedding e
f : β → E
s : Set α
hs : s ∈ l ∧ IntegrableOn (f ∘ e) s μ
⊢ ∃ s ∈ map e l, IntegrableOn (f ∘ e) (e ⁻¹' s) μ
-- Mathlib/Topology/Bases.lean
theorem IsSeparable.univ_pi {ι : Type*} [Countable ι] {X : ι → Type*} {s : ∀ i, Set (X i)}
    [∀ i, TopologicalSpace (X i)] (h : ∀ i, IsSeparable (s i)) :
    IsSeparable (univ.pi s)

Proof state:
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f : (i : ι) → X i
hf : f ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen (u a) ∧ f a ∈ u a
hI : (↑I).pi u ⊆ o
⊢ ∃ f, g ⟨I, f⟩ ∈ (↑I).pi u

Tactic:
suffices H : ∀ i ∈ I, (u i ∩ c i).Nonempty by
  choose f hfu hfc using H
  refine ⟨fun i ↦ ⟨f i i.2, hfc i i.2⟩, fun i (hi : i ∈ I) ↦ ?_⟩
  simpa only [g, dif_pos hi] using hfu i hi

Result:
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : { x // x ∈ I }) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i =>
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f : (i : ι) → X i
hf : f ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen (u a) ∧ f a ∈ u a
hI : (↑I).pi u ⊆ o
⊢ ∀ i ∈ I, (u i ∩ c i).Nonempty

Proof state:
case inr.intro
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure (c i)
⊢ IsSeparable (univ.pi s)

Tactic:
haveI := fun i ↦ (c_count i).to_subtype

Result:
case inr.intro
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure (c i)
this : ∀ (i : ι), Countable ↑(c i)
⊢ IsSeparable (univ.pi s)
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem kahler_apply_self (x : E) : o.kahler x x = ‖x‖ ^ 2

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x : E
⊢ (o.kahler x) x = ↑‖x‖ ^ 2

Tactic:
simp [kahler_apply_apply, real_inner_self_eq_norm_sq]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
@[to_additive]
protected lemma div_mul_right (h : IsUnit a) (b : α) : a / (a * b) = 1 / b

Proof state:
α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a / (a * b) = 1 / b

Tactic:
rw [mul_comm, h.div_mul_left]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Abs.lean
theorem abs_cases (a : α) : |a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0

Proof state:
case pos
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : α
h : 0 ≤ a
⊢ |a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0

Tactic:
left

Result:
case pos.h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : α
h : 0 ≤ a
⊢ |a| = a ∧ 0 ≤ a

Proof state:
case neg.h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : α
h : ¬0 ≤ a
⊢ |a| = -a ∧ a < 0

Tactic:
push_neg at h

Result:
case neg.h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : α
h : a < 0
⊢ |a| = -a ∧ a < 0

Proof state:
case pos.h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : α
h : 0 ≤ a
⊢ |a| = a ∧ 0 ≤ a

Tactic:
exact ⟨abs_eq_self.mpr h, h⟩

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : α
h : ¬0 ≤ a
⊢ |a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0

Tactic:
right

Result:
case neg.h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : α
h : ¬0 ≤ a
⊢ |a| = -a ∧ a < 0

Proof state:
case neg.h
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : α
h : a < 0
⊢ |a| = -a ∧ a < 0

Tactic:
exact ⟨abs_eq_neg_self.mpr (le_of_lt h), h⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : α
⊢ |a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0

Tactic:
by_cases h : 0 ≤ a

Result:
case pos
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : α
h : 0 ≤ a
⊢ |a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0

case neg
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a : α
h : ¬0 ≤ a
⊢ |a| = a ∧ 0 ≤ a ∨ |a| = -a ∧ a < 0
-- Mathlib/Algebra/Polynomial/HasseDeriv.lean
theorem factorial_smul_hasseDeriv : ⇑(k ! • @hasseDeriv R _ k) = (@derivative R _)^[k]

Proof state:
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ (((k + 1)! • hasseDeriv (k + 1)) f).coeff n = (derivative ((k ! • hasseDeriv k) f)).coeff n

Tactic:
simp only [LinearMap.smul_apply, coeff_smul, LinearMap.map_smul_of_tower, coeff_derivative,
  hasseDeriv_coeff, ← @choose_symm_add _ k]

Result:
case succ.h.a
R : Type u_1
inst✝ : Semiring R
k✝ k : ℕ
ih : ⇑(k ! • hasseDeriv k) = (⇑derivative)^[k]
f : R[X]
n : ℕ
⊢ (k + 1)! • (↑((n + (k + 1)).choose (k + 1)) * f.coeff (n + (k + 1))) =
    k ! • (↑((n + 1 + k).choose (n + 1)) * f.coeff (n + 1 + k) * (↑n + 1))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem insertIfNew_val [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} {b : β a} :
    m.val.insertIfNew a b = m.insertIfNew a b

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
⊢ m.val.insertIfNew a b = (m.insertIfNew a b).val

Tactic:
simp [Raw.insertIfNew, m.2]

Result:
no goals
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem Iic_coatomic_of_compact_element {k : α} (h : IsCompactElement k) :
    IsCoatomic (Set.Iic k)

Proof state:
case eq_top_or_exists_le_coatom
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
⊢ ∀ (b : ↑(Iic k)), b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

Tactic:
rintro ⟨b, hbk⟩

Result:
case eq_top_or_exists_le_coatom.mk
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
⊢ ⟨b, hbk⟩ = ⊤ ∨ ∃ a, IsCoatom a ∧ ⟨b, hbk⟩ ≤ a

Proof state:
case neg
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
S : Set α
SC : S ⊆ Iio k
cC : IsChain (fun x1 x2 => x1 ≤ x2) S
I : α
a✝ : I ∈ S
hS : ¬S.Nonempty
⊢ ∃ ub ∈ Iio k, ∀ z ∈ S, z ≤ ub

Tactic:
exact
  ⟨b, lt_of_le_of_ne hbk H, by
    simp only [Set.not_nonempty_iff_eq_empty.mp hS, Set.mem_empty_iff_false, forall_const,
      forall_prop_of_false, not_false_iff]⟩

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Covering.lean
theorem Prefunctor.pathStar_surjective (hφ : ∀ u, Surjective (φ.star u)) (u : U) :
    Surjective (φ.pathStar u)

Proof state:
case mk.cons.intro.mk.refl.intro.mk
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v c✝ : V
u' : U
q' : Path u u'
ev : φ.obj u' ⟶ c✝
u'' : U
eu : u' ⟶ u''
k : φ.star u' ⟨u'', eu⟩ = ⟨c✝, ev⟩
⊢ ∃ a, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, (φ.mapPath q').cons ev⟩

Tactic:
simp only [star_apply, Sigma.mk.inj_iff] at k

Result:
case mk.cons.intro.mk.refl.intro.mk
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v c✝ : V
u' : U
q' : Path u u'
ev : φ.obj u' ⟶ c✝
u'' : U
eu : u' ⟶ u''
k : φ.obj u'' = c✝ ∧ HEq (φ.map eu) ev
⊢ ∃ a, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, (φ.mapPath q').cons ev⟩

Proof state:
case mk.cons
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v b✝ c✝ : V
p' : Path (φ.obj u) b✝
ev : b✝ ⟶ c✝
ih : ∃ a, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨b✝, p'⟩
⊢ ∃ a, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, p'.cons ev⟩

Tactic:
obtain ⟨⟨u', q'⟩, h⟩ := ih

Result:
case mk.cons.intro.mk
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v b✝ c✝ : V
p' : Path (φ.obj u) b✝
ev : b✝ ⟶ c✝
u' : U
q' : Path u u'
h : (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨u', q'⟩ = ⟨b✝, p'⟩
⊢ ∃ a, (fun p => ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, p'.cons ev⟩
-- Mathlib/FieldTheory/IsAlgClosed/Basic.lean
theorem exists_eval₂_eq_zero_of_injective {R : Type*} [Ring R] [IsAlgClosed k] (f : R →+* k)
    (hf : Function.Injective f) (p : R[X]) (hp : p.degree ≠ 0) : ∃ x, p.eval₂ f x = 0 :=
  let ⟨x, hx⟩ := exists_root (p.map f) (by rwa [degree_map_eq_of_injective hf])
  ⟨x, by rwa [eval₂_eq_eval_map, ← IsRoot]⟩

Proof state:
k : Type u
inst✝² : Field k
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsAlgClosed k
f : R →+* k
hf : Function.Injective ⇑f
p : R[X]
hp : p.degree ≠ 0
x : k
hx : (map f p).IsRoot x
⊢ eval₂ f x p = 0

Tactic:
rwa [eval₂_eq_eval_map, ← IsRoot]

Result:
no goals

Proof state:
k : Type u
inst✝² : Field k
R : Type u_1
inst✝¹ : Ring R
inst✝ : IsAlgClosed k
f : R →+* k
hf : Function.Injective ⇑f
p : R[X]
hp : p.degree ≠ 0
⊢ (map f p).degree ≠ 0

Tactic:
rwa [degree_map_eq_of_injective hf]

Result:
no goals