harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatten_ne_nil_iff {xs : List (List α)} : xs.flatten ≠ [] ↔ ∃ x, x ∈ xs ∧ x ≠ []

Proof state:
α : Type u_1
xs : List (List α)
⊢ xs.flatten ≠ [] ↔ ∃ x, x ∈ xs ∧ x ≠ []

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_univ (α : Type*) :
    encard (univ : Set α) = ENat.card α

Proof state:
α : Type u_3
⊢ univ.encard = ENat.card α

Tactic:
rw [encard, ENat.card_congr (Equiv.Set.univ α)]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Balance.lean
@[simp] lemma expect_balance (f : ι → G) : 𝔼 x, balance f x = 0

Proof state:
ι : Type u_1
G : Type u_4
inst✝² : Fintype ι
inst✝¹ : AddCommGroup G
inst✝ : Module ℚ≥0 G
f : ι → G
⊢ 𝔼 x : ι, balance f x = 0

Tactic:
simp [expect]

Result:
no goals
-- Mathlib/Data/Fin/Parity.lean
lemma even_iff_imp {n : ℕ} {k : Fin n} : Even k ↔ (Even n → Even k.val)

Proof state:
n : ℕ
k : Fin n
⊢ Even k ↔ Odd n ∨ Even ↑k

Tactic:
exact even_iff

Result:
no goals

Proof state:
n : ℕ
k : Fin n
⊢ Even k ↔ Even n → Even ↑k

Tactic:
rw [imp_iff_not_or, Nat.not_even_iff_odd]

Result:
n : ℕ
k : Fin n
⊢ Even k ↔ Odd n ∨ Even ↑k
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem continuousAt_logb_iff (hb₀ : 0 < b) (hb : b ≠ 1) : ContinuousAt (logb b) x ↔ x ≠ 0

Proof state:
b : ℝ
hb₀ : 0 < b
hb : b ≠ 1
h : ContinuousAt (logb b) 0
⊢ False

Tactic:
cases lt_or_gt_of_ne hb with
| inl hb₁ =>
    exact not_tendsto_nhds_of_tendsto_atTop (tendsto_logb_nhdsWithin_zero_of_base_lt_one hb₀ hb₁)
      _ (h.tendsto.mono_left inf_le_left)
| inr hb₁ =>
    exact not_tendsto_nhds_of_tendsto_atBot (tendsto_logb_nhdsWithin_zero hb₁)
      _ (h.tendsto.mono_left inf_le_left)

Result:
no goals

Proof state:
case inr
b : ℝ
hb₀ : 0 < b
hb : b ≠ 1
h : ContinuousAt (logb b) 0
hb₁ : b > 1
⊢ False

Tactic:
exact not_tendsto_nhds_of_tendsto_atBot (tendsto_logb_nhdsWithin_zero hb₁)
  _ (h.tendsto.mono_left inf_le_left)

Result:
no goals

Proof state:
b x : ℝ
hb₀ : 0 < b
hb : b ≠ 1
⊢ ContinuousAt (logb b) x → x ≠ 0

Tactic:
rintro h rfl

Result:
b : ℝ
hb₀ : 0 < b
hb : b ≠ 1
h : ContinuousAt (logb b) 0
⊢ False

Proof state:
b x : ℝ
hb₀ : 0 < b
hb : b ≠ 1
⊢ ContinuousAt (logb b) x ↔ x ≠ 0

Tactic:
refine ⟨?_, continuousAt_logb⟩

Result:
b x : ℝ
hb₀ : 0 < b
hb : b ≠ 1
⊢ ContinuousAt (logb b) x → x ≠ 0

Proof state:
case inl
b : ℝ
hb₀ : 0 < b
hb : b ≠ 1
h : ContinuousAt (logb b) 0
hb₁ : b < 1
⊢ False

Tactic:
exact not_tendsto_nhds_of_tendsto_atTop (tendsto_logb_nhdsWithin_zero_of_base_lt_one hb₀ hb₁)
  _ (h.tendsto.mono_left inf_le_left)

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem support_sum [DecidableEq β] [Zero M] [AddCommMonoid N] {f : α →₀ M} {g : α → M → β →₀ N} :
    (f.sum g).support ⊆ f.support.biUnion fun a => (g a (f a)).support

Proof state:
α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst✝² : DecidableEq β
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
f : α →₀ M
g : α → M → β →₀ N
this : ∀ (c : β), (f.sum fun a b => (g a b) c) ≠ 0 → ∃ a, f a ≠ 0 ∧ ¬(g a (f a)) c = 0
⊢ (f.sum g).support ⊆ f.support.biUnion fun a => (g a (f a)).support

Tactic:
simpa only [Finset.subset_iff, mem_support_iff, Finset.mem_biUnion, sum_apply, exists_prop]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst✝² : DecidableEq β
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
f : α →₀ M
g : α → M → β →₀ N
⊢ (f.sum g).support ⊆ f.support.biUnion fun a => (g a (f a)).support

Tactic:
have : ∀ c, (f.sum fun a b => g a b c) ≠ 0 → ∃ a, f a ≠ 0 ∧ ¬(g a (f a)) c = 0 := fun a₁ h =>
  let ⟨a, ha, ne⟩ := Finset.exists_ne_zero_of_sum_ne_zero h
  ⟨a, mem_support_iff.mp ha, ne⟩

Result:
α : Type u_1
β : Type u_7
M : Type u_8
N : Type u_10
inst✝² : DecidableEq β
inst✝¹ : Zero M
inst✝ : AddCommMonoid N
f : α →₀ M
g : α → M → β →₀ N
this : ∀ (c : β), (f.sum fun a b => (g a b) c) ≠ 0 → ∃ a, f a ≠ 0 ∧ ¬(g a (f a)) c = 0
⊢ (f.sum g).support ⊆ f.support.biUnion fun a => (g a (f a)).support
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem limit.post_post {E : Type u''} [Category.{v''} E] (H : D ⥤ E) [h : HasLimit ((F ⋙ G) ⋙ H)] :
    -- H G (limit F) ⟶ H (limit (F ⋙ G)) ⟶ limit ((F ⋙ G) ⋙ H) equals
    -- H G (limit F) ⟶ limit (F ⋙ (G ⋙ H))
    haveI : HasLimit (F ⋙ G ⋙ H) := h
    H.map (limit.post F G) ≫ limit.post (F ⋙ G) H = limit.post F (G ⋙ H)

Proof state:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
⊢ H.map (post F G) ≫ post (F ⋙ G) H = post F (G ⋙ H)

Tactic:
haveI : HasLimit (F ⋙ G ⋙ H) := h

Result:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
⊢ H.map (post F G) ≫ post (F ⋙ G) H = post F (G ⋙ H)

Proof state:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
j✝ : J
⊢ H.map (G.map (π F j✝)) = (G ⋙ H).map (π F j✝)

Tactic:
rfl

Result:
no goals

Proof state:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
j✝ : J
⊢ (H.map (post F G) ≫ post (F ⋙ G) H) ≫ π ((F ⋙ G) ⋙ H) j✝ = post F (G ⋙ H) ≫ π ((F ⋙ G) ⋙ H) j✝

Tactic:
erw [assoc, limit.post_π, ← H.map_comp, limit.post_π, limit.post_π]

Result:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
j✝ : J
⊢ H.map (G.map (π F j✝)) = (G ⋙ H).map (π F j✝)

Proof state:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
⊢ H.map (post F G) ≫ post (F ⋙ G) H = post F (G ⋙ H)

Tactic:
ext

Result:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
j✝ : J
⊢ (H.map (post F G) ≫ post (F ⋙ G) H) ≫ π ((F ⋙ G) ⋙ H) j✝ = post F (G ⋙ H) ≫ π ((F ⋙ G) ⋙ H) j✝
-- Mathlib/Data/Set/Image.lean
theorem image_insert_eq {f : α → β} {a : α} {s : Set α} :
    f '' insert a s = insert (f a) (f '' s)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
a : α
s : Set α
⊢ f '' insert a s = insert (f a) (f '' s)

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
f : α → β
a : α
s : Set α
x✝ : β
⊢ x✝ ∈ f '' insert a s ↔ x✝ ∈ insert (f a) (f '' s)

Proof state:
case h
α : Type u_1
β : Type u_2
f : α → β
a : α
s : Set α
x✝ : β
⊢ x✝ ∈ f '' insert a s ↔ x✝ ∈ insert (f a) (f '' s)

Tactic:
simp [and_or_left, exists_or, eq_comm, or_comm, and_comm]

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
theorem mul_assoc : a * b * c = a * (b * c) :=
  numDenCasesOn' a fun n₁ d₁ h₁ =>
    numDenCasesOn' b fun n₂ d₂ h₂ =>
      numDenCasesOn' c fun n₃ d₃ h₃ => by
        simp [h₁, h₂, h₃, Int.mul_comm, Nat.mul_assoc, Int.mul_left_comm]

Proof state:
a b c : ℚ
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
n₃ : ℤ
d₃ : ℕ
h₃ : d₃ ≠ 0
⊢ n₁ /. ↑d₁ * (n₂ /. ↑d₂) * (n₃ /. ↑d₃) = n₁ /. ↑d₁ * (n₂ /. ↑d₂ * (n₃ /. ↑d₃))

Tactic:
simp [h₁, h₂, h₃, Int.mul_comm, Nat.mul_assoc, Int.mul_left_comm]

Result:
no goals
-- Mathlib/Algebra/Group/NatPowAssoc.lean
theorem neg_npow_assoc {R : Type*} [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] (a b : R) (k : ℕ) :
    (-1)^k * a * b = (-1)^k * (a * b)

Proof state:
case succ
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
a b : R
k : ℕ
ih : (-1) ^ k * a * b = (-1) ^ k * (a * b)
⊢ -(-1) ^ k * a * b = -(-1) ^ k * (a * b)

Tactic:
simp only [neg_mul, ih]

Result:
no goals

Proof state:
case zero
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
a b : R
⊢ (-1) ^ 0 * a * b = (-1) ^ 0 * (a * b)

Tactic:
simp only [npow_zero, one_mul]

Result:
no goals

Proof state:
case succ
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
a b : R
k : ℕ
ih : (-1) ^ k * a * b = (-1) ^ k * (a * b)
⊢ (-1) ^ (k + 1) * a * b = (-1) ^ (k + 1) * (a * b)

Tactic:
rw [npow_add, npow_one, ← neg_mul_comm, mul_one]

Result:
case succ
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
a b : R
k : ℕ
ih : (-1) ^ k * a * b = (-1) ^ k * (a * b)
⊢ -(-1) ^ k * a * b = -(-1) ^ k * (a * b)

Proof state:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
a b : R
k : ℕ
⊢ (-1) ^ k * a * b = (-1) ^ k * (a * b)

Tactic:
induction k with
| zero => simp only [npow_zero, one_mul]
| succ k ih =>
  rw [npow_add, npow_one, ← neg_mul_comm, mul_one]
  simp only [neg_mul, ih]

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem intCast_modEq_intCast {a b z : ℤ} : a ≡ b [PMOD (z : α)] ↔ a ≡ b [PMOD z]

Proof state:
α : Type u_1
inst✝¹ : AddCommGroupWithOne α
inst✝ : CharZero α
a b z : ℤ
⊢ (∃ z_1, ↑b - ↑a = ↑(z_1 * z)) ↔ ∃ z_1, b - a = z_1 • z

Tactic:
norm_cast

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : AddCommGroupWithOne α
inst✝ : CharZero α
a b z : ℤ
⊢ ↑a ≡ ↑b [PMOD ↑z] ↔ a ≡ b [PMOD z]

Tactic:
simp_rw [ModEq, ← Int.cast_mul_eq_zsmul_cast]

Result:
α : Type u_1
inst✝¹ : AddCommGroupWithOne α
inst✝ : CharZero α
a b z : ℤ
⊢ (∃ z_1, ↑b - ↑a = ↑(z_1 * z)) ↔ ∃ z_1, b - a = z_1 • z
-- Mathlib/Topology/DerivedSet.lean
/-- In a `T1Space`, the `derivedSet` of the closure of a set is equal to the derived set of the
set itself.

Note: this doesn't hold in a space with the indiscrete topology. For example, if `X` is a type with
two elements, `x` and `y`, and `A := {x}`, then `closure A = Set.univ` and `derivedSet A = {y}`,
but `derivedSet Set.univ = Set.univ`. -/
lemma derivedSet_closure [T1Space X] (A : Set X) : derivedSet (closure A) = derivedSet A

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
⊢ derivedSet (closure A) = derivedSet A

Tactic:
refine le_antisymm (fun x hx => ?_) (derivedSet_mono _ _ subset_closure)

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
x : X
hx : x ∈ derivedSet (closure A)
⊢ x ∈ derivedSet A

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
x : X
hx : ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen i → (i ∩ {x}ᶜ ∩ closure A).Nonempty
⊢ ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen i → (i ∩ {x}ᶜ ∩ A).Nonempty

Tactic:
peel hx with u hu _

Result:
case h.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
x : X
hx : ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen i → (i ∩ {x}ᶜ ∩ closure A).Nonempty
u : Set X
hu : x ∈ u ∧ IsOpen u
this : (u ∩ {x}ᶜ ∩ closure A).Nonempty
⊢ (u ∩ {x}ᶜ ∩ A).Nonempty

Proof state:
case h.h.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
x : X
hx : ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen i → (i ∩ {x}ᶜ ∩ closure A).Nonempty
u : Set X
this : (u ∩ {x}ᶜ ∩ closure A).Nonempty
hu_open : IsOpen u
⊢ (u ∩ {x}ᶜ ∩ A).Nonempty

Tactic:
exact mem_closure_iff.mp this.some_mem.2 (u ∩ {x}ᶜ) (hu_open.inter isOpen_compl_singleton)
  this.some_mem.1

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
x : X
hx : x ∈ derivedSet (closure A)
⊢ x ∈ derivedSet A

Tactic:
rw [mem_derivedSet, AccPt, (nhdsWithin_basis_open x {x}ᶜ).inf_principal_neBot_iff] at hx ⊢

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
x : X
hx : ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen i → (i ∩ {x}ᶜ ∩ closure A).Nonempty
⊢ ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen i → (i ∩ {x}ᶜ ∩ A).Nonempty

Proof state:
case h.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
x : X
hx : ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen i → (i ∩ {x}ᶜ ∩ closure A).Nonempty
u : Set X
hu : x ∈ u ∧ IsOpen u
this : (u ∩ {x}ᶜ ∩ closure A).Nonempty
⊢ (u ∩ {x}ᶜ ∩ A).Nonempty

Tactic:
obtain ⟨-, hu_open⟩ := hu

Result:
case h.h.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
x : X
hx : ∀ ⦃i : Set X⦄, x ∈ i ∧ IsOpen i → (i ∩ {x}ᶜ ∩ closure A).Nonempty
u : Set X
this : (u ∩ {x}ᶜ ∩ closure A).Nonempty
hu_open : IsOpen u
⊢ (u ∩ {x}ᶜ ∩ A).Nonempty
-- Mathlib/Algebra/Order/BigOperators/Group/LocallyFinite.lean
@[to_additive]
lemma prod_Ioc_mul_left (h : a ≤ b) : (∏ x ∈ Ioc a b, f x) * f a = ∏ x ∈ Icc a b, f x

Proof state:
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : CommMonoid β
f : α → β
a b : α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ (∏ x ∈ Ioc a b, f x) * f a = ∏ x ∈ Icc a b, f x

Tactic:
rw [mul_comm, left_mul_prod_Ioc h]

Result:
no goals
-- Mathlib/Logic/Equiv/Fin.lean
theorem finSuccEquiv'_last_apply {i : Fin (n + 1)} (h : i ≠ Fin.last n) :
    finSuccEquiv' (Fin.last n) i = Fin.castLT i (Fin.val_lt_last h)

Proof state:
case intro
n : ℕ
i : Fin n
h : i.castSucc ≠ Fin.last n
⊢ (finSuccEquiv' (Fin.last n)) i.castSucc = some (i.castSucc.castLT ⋯)

Tactic:
rw [finSuccEquiv'_last_apply_castSucc]

Result:
case intro
n : ℕ
i : Fin n
h : i.castSucc ≠ Fin.last n
⊢ some i = some (i.castSucc.castLT ⋯)

Proof state:
case intro
n : ℕ
i : Fin n
h : i.castSucc ≠ Fin.last n
⊢ some i = some (i.castSucc.castLT ⋯)

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
i : Fin (n + 1)
h : i ≠ Fin.last n
⊢ (finSuccEquiv' (Fin.last n)) i = some (i.castLT ⋯)

Tactic:
rcases Fin.exists_castSucc_eq.2 h with ⟨i, rfl⟩

Result:
case intro
n : ℕ
i : Fin n
h : i.castSucc ≠ Fin.last n
⊢ (finSuccEquiv' (Fin.last n)) i.castSucc = some (i.castSucc.castLT ⋯)
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem colimit.pre_pre [h : HasColimit (D ⋙ E ⋙ F)] :
    haveI : HasColimit ((D ⋙ E) ⋙ F) := h
    colimit.pre (E ⋙ F) D ≫ colimit.pre F E = colimit.pre F (D ⋙ E)

Proof state:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimit F
E : K ⥤ J
inst✝¹ : HasColimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ ι F (E.obj (D.obj j)) = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)

Tactic:
haveI : HasColimit ((D ⋙ E) ⋙ F) := h

Result:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimit F
E : K ⥤ J
inst✝¹ : HasColimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasColimit (D ⋙ E ⋙ F)
j : L
this : HasColimit ((D ⋙ E) ⋙ F)
⊢ ι F (E.obj (D.obj j)) = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)

Proof state:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimit F
E : K ⥤ J
inst✝¹ : HasColimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasColimit (D ⋙ E ⋙ F)
j : L
this : HasColimit ((D ⋙ E) ⋙ F)
⊢ ι F (E.obj (D.obj j)) = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)

Tactic:
exact (colimit.ι_pre F (D ⋙ E) j).symm

Result:
no goals

Proof state:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimit F
E : K ⥤ J
inst✝¹ : HasColimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasColimit (D ⋙ E ⋙ F)
⊢ pre (E ⋙ F) D ≫ pre F E = pre F (D ⋙ E)

Tactic:
ext j

Result:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimit F
E : K ⥤ J
inst✝¹ : HasColimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ ι (D ⋙ E ⋙ F) j ≫ pre (E ⋙ F) D ≫ pre F E = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)

Proof state:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimit F
E : K ⥤ J
inst✝¹ : HasColimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ ι (D ⋙ E ⋙ F) j ≫ pre (E ⋙ F) D ≫ pre F E = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)

Tactic:
rw [← assoc, colimit.ι_pre, colimit.ι_pre]

Result:
case w
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u
inst✝³ : Category.{v, u} C
F : J ⥤ C
inst✝² : HasColimit F
E : K ⥤ J
inst✝¹ : HasColimit (E ⋙ F)
L : Type u₃
inst✝ : Category.{v₃, u₃} L
D : L ⥤ K
h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ ι F (E.obj (D.obj j)) = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)
-- Mathlib/LinearAlgebra/FreeModule/Finite/Basic.lean
theorem Module.Finite.of_basis {R M ι : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
    [_root_.Finite ι] (b : Basis ι R M) : Module.Finite R M

Proof state:
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
b : Basis ι R M
⊢ Module.Finite R M

Tactic:
cases nonempty_fintype ι

Result:
case intro
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ Module.Finite R M

Proof state:
case intro
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ Submodule.span R ↑(Finset.image (⇑b) Finset.univ) = ⊤

Tactic:
simp only [Set.image_univ, Finset.coe_univ, Finset.coe_image, Basis.span_eq]

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ Module.Finite R M

Tactic:
refine ⟨⟨Finset.univ.image b, ?_⟩⟩

Result:
case intro
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ Submodule.span R ↑(Finset.image (⇑b) Finset.univ) = ⊤

Proof state:
case intro
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ Module.Finite R M

Tactic:
classical
  refine ⟨⟨Finset.univ.image b, ?_⟩⟩
  simp only [Set.image_univ, Finset.coe_univ, Finset.coe_image, Basis.span_eq]

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem insertionSort_cons {a : α} {l : List α} (h : ∀ b ∈ l, r a b) :
    insertionSort r (a :: l) = a :: insertionSort r l

Proof state:
case cons
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ b ∈ l, r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ orderedInsert r a (b :: m) = a :: b :: m

Tactic:
rw [orderedInsert_of_le]

Result:
case cons.h
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ b ∈ l, r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ r a b

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ b ∈ l, r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ b ∈ insertionSort r l

Tactic:
rw [hi]

Result:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ b ∈ l, r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ b ∈ b :: m

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ b ∈ l, r a b
⊢ insertionSort r (a :: l) = a :: insertionSort r l

Tactic:
rw [insertionSort]

Result:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ b ∈ l, r a b
⊢ orderedInsert r a (insertionSort r l) = a :: insertionSort r l

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ b ∈ l, r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ b ∈ b :: m

Tactic:
exact mem_cons_self b m

Result:
no goals

Proof state:
case cons.h
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ b ∈ l, r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ r a b

Tactic:
apply h b <| (mem_insertionSort r).1 _

Result:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ b ∈ l, r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ b ∈ insertionSort r l

Proof state:
case nil
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ b ∈ l, r a b
hi : insertionSort r l = []
⊢ orderedInsert r a [] = [a]

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a : α
l : List α
h : ∀ b ∈ l, r a b
⊢ orderedInsert r a (insertionSort r l) = a :: insertionSort r l

Tactic:
cases hi : insertionSort r l with
| nil => rfl
| cons b m =>
  rw [orderedInsert_of_le]
  apply h b <| (mem_insertionSort r).1 _
  rw [hi]
  exact mem_cons_self b m

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem prod_cyclotomic_eq_geom_sum {n : ℕ} (h : 0 < n) (R) [CommRing R] :
    ∏ i ∈ n.divisors.erase 1, cyclotomic i R = ∑ i ∈ Finset.range n, X ^ i

Proof state:
n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
this : ∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ = ∑ i ∈ range n, X ^ i
⊢ ∏ i ∈ n.divisors.erase 1, cyclotomic i R = ∑ i ∈ range n, X ^ i

Tactic:
simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow,
  Polynomial.map_X] using congr_arg (map (Int.castRingHom R)) this

Result:
no goals

Proof state:
n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ = ∑ i ∈ range n, X ^ i

Tactic:
rw [← mul_left_inj' (cyclotomic_ne_zero 1 ℤ), prod_erase_mul _ _ (Nat.one_mem_divisors.2 h.ne'),
  cyclotomic_one, geom_sum_mul, prod_cyclotomic_eq_X_pow_sub_one h]

Result:
no goals

Proof state:
n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i ∈ n.divisors.erase 1, cyclotomic i R = ∑ i ∈ range n, X ^ i

Tactic:
suffices (∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ) = ∑ i ∈ Finset.range n, X ^ i by
  simpa only [Polynomial.map_prod, map_cyclotomic_int, Polynomial.map_sum, Polynomial.map_pow,
    Polynomial.map_X] using congr_arg (map (Int.castRingHom R)) this

Result:
n : ℕ
h : 0 < n
R : Type u_1
inst✝ : CommRing R
⊢ ∏ i ∈ n.divisors.erase 1, cyclotomic i ℤ = ∑ i ∈ range n, X ^ i
-- Mathlib/NumberTheory/NumberField/Units/Basic.lean
theorem coe_zpow (x : (𝓞 K)ˣ) (n : ℤ) : (↑(x ^ n) : K) = (x : K) ^ n

Proof state:
K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
n : ℤ
⊢ ((coeHom K).comp (map ↑(algebraMap (𝓞 K) K))) (x ^ n) = (algebraMap (𝓞 K) K) ↑x ^ n

Tactic:
exact map_zpow _ x n

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
n : ℤ
⊢ (algebraMap (𝓞 K) K) ↑(x ^ n) = (algebraMap (𝓞 K) K) ↑x ^ n

Tactic:
change ((Units.coeHom K).comp (map (algebraMap (𝓞 K) K))) (x ^ n) = _

Result:
K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
n : ℤ
⊢ ((coeHom K).comp (map ↑(algebraMap (𝓞 K) K))) (x ^ n) = (algebraMap (𝓞 K) K) ↑x ^ n
-- Mathlib/RingTheory/Congruence/Basic.lean
theorem coe_sInf (S : Set (RingCon R)) : ⇑(sInf S) = sInf ((⇑) '' S)

Proof state:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
⊢ ⇑(sInf S) = sInf (DFunLike.coe '' S)

Tactic:
ext

Result:
case h.h.a
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x✝¹ x✝ : R
⊢ (sInf S) x✝¹ x✝ ↔ sInf (DFunLike.coe '' S) x✝¹ x✝

Proof state:
case h.h.a
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x✝¹ x✝ : R
⊢ (sInf S) x✝¹ x✝ ↔ sInf (DFunLike.coe '' S) x✝¹ x✝

Tactic:
simp only [sInf_image, iInf_apply, iInf_Prop_eq]

Result:
case h.h.a
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x✝¹ x✝ : R
⊢ (sInf S) x✝¹ x✝ ↔ ∀ i ∈ S, i x✝¹ x✝

Proof state:
case h.h.a
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x✝¹ x✝ : R
⊢ (sInf S) x✝¹ x✝ ↔ ∀ i ∈ S, i x✝¹ x✝

Tactic:
rfl

Result:
no goals