harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Ostrowski.lean
private lemma list_geom {T : Type*} {F : Type*} [Field F] (l : List T) {y : F} (hy : y ≠ 1) :
    (l.mapIdx fun i _ => y ^ i).sum = (y ^ l.length - 1) / (y - 1)

Proof state:
T : Type u_1
F : Type u_2
inst✝ : Field F
l : List T
y : F
hy : y ≠ 1
e : Fin l.zipIdx.length ≃ Fin l.length := finCongr ⋯
⊢ ∑ x : Fin l.zipIdx.length, y ^ (l.zipIdx.get ⟨↑x, ⋯⟩).2 = ∑ i : Fin l.length, y ^ ↑i

Tactic:
exact Fintype.sum_bijective e e.bijective _ _ fun _ ↦ by simp [e]

Result:
no goals

Proof state:
T : Type u_1
F : Type u_2
inst✝ : Field F
l : List T
y : F
hy : y ≠ 1
⊢ (List.mapIdx (fun i x => y ^ i) l).sum = (y ^ l.length - 1) / (y - 1)

Tactic:
rw [← geom_sum_eq hy l.length, List.mapIdx_eq_zipIdx_map, Finset.sum_range, ← Fin.sum_univ_get']

Result:
T : Type u_1
F : Type u_2
inst✝ : Field F
l : List T
y : F
hy : y ≠ 1
⊢ (∑ i : Fin l.zipIdx.length,
      match l.zipIdx[↑i] with
      | (a, i) => y ^ i) =
    ∑ i : Fin l.length, y ^ ↑i

Proof state:
T : Type u_1
F : Type u_2
inst✝ : Field F
l : List T
y : F
hy : y ≠ 1
⊢ ∑ x : Fin l.zipIdx.length, y ^ (l.zipIdx.get ⟨↑x, ⋯⟩).2 = ∑ i : Fin l.length, y ^ ↑i

Tactic:
let e : Fin l.zipIdx.length ≃ Fin l.length := finCongr List.length_zipIdx

Result:
T : Type u_1
F : Type u_2
inst✝ : Field F
l : List T
y : F
hy : y ≠ 1
e : Fin l.zipIdx.length ≃ Fin l.length := finCongr ⋯
⊢ ∑ x : Fin l.zipIdx.length, y ^ (l.zipIdx.get ⟨↑x, ⋯⟩).2 = ∑ i : Fin l.length, y ^ ↑i

Proof state:
T : Type u_1
F : Type u_2
inst✝ : Field F
l : List T
y : F
hy : y ≠ 1
e : Fin l.zipIdx.length ≃ Fin l.length := finCongr ⋯
x✝ : Fin l.zipIdx.length
⊢ y ^ (l.zipIdx.get ⟨↑x✝, ⋯⟩).2 = y ^ ↑(e x✝)

Tactic:
simp [e]

Result:
no goals

Proof state:
T : Type u_1
F : Type u_2
inst✝ : Field F
l : List T
y : F
hy : y ≠ 1
⊢ (∑ i : Fin l.zipIdx.length,
      match l.zipIdx[↑i] with
      | (a, i) => y ^ i) =
    ∑ i : Fin l.length, y ^ ↑i

Tactic:
simp only [List.getElem_zipIdx, Function.uncurry_apply_pair]

Result:
T : Type u_1
F : Type u_2
inst✝ : Field F
l : List T
y : F
hy : y ≠ 1
⊢ ∑ x : Fin l.zipIdx.length, y ^ (l.zipIdx.get ⟨↑x, ⋯⟩).2 = ∑ i : Fin l.length, y ^ ↑i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem bit_not_testBit (x : BitVec w) (i : Fin w) :
  getLsbD (((iunfoldr (fun (i : Fin w) c => (c, !(x.getLsbD i)))) ()).snd) i.val = !(getLsbD x i.val)

Proof state:
w : Nat
x : BitVec w
i : Fin w
⊢ (iunfoldr (fun i c => (c, !x.getLsbD ↑i)) ()).snd.getLsbD ↑i = !x.getLsbD ↑i

Tactic:
apply iunfoldr_getLsbD (fun _ => ()) i (by simp)

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Fin w
⊢ ∀ (i : Fin w), ((fun x => ()) ↑i, !x.getLsbD ↑i).fst = (fun x => ()) (↑i + 1)

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ToNat.lean
theorem toNat_eq_one : toNat c = 1 ↔ c = 1

Proof state:
c : Cardinal.{u}
⊢ toNat c = 1 ↔ c = 1

Tactic:
rw [toNat_eq_iff one_ne_zero, Nat.cast_one]

Result:
no goals
-- Mathlib/Data/Sym/Basic.lean
theorem ofVector_cons (a : α) (v : List.Vector α n) :
    ↑(Vector.cons a v) = a ::ₛ (↑v : Sym α n)

Proof state:
α : Type u_1
n : ℕ
a : α
v : List.Vector α n
⊢ ofVector (a ::ᵥ v) = a ::ₛ ofVector v

Tactic:
cases v

Result:
case mk
α : Type u_1
n : ℕ
a : α
val✝ : List α
property✝ : val✝.length = n
⊢ ofVector (a ::ᵥ ⟨val✝, property✝⟩) = a ::ₛ ofVector ⟨val✝, property✝⟩

Proof state:
case mk
α : Type u_1
n : ℕ
a : α
val✝ : List α
property✝ : val✝.length = n
⊢ ofVector (a ::ᵥ ⟨val✝, property✝⟩) = a ::ₛ ofVector ⟨val✝, property✝⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean
theorem subset_balancedCore (ht : (0 : E) ∈ t) (hst : ∀ a : 𝕜, ‖a‖ ≤ 1 → a • s ⊆ t) :
    s ⊆ balancedCore 𝕜 t

Proof state:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ ‖a⁻¹‖ ≤ 1

Tactic:
rw [norm_inv]

Result:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ ‖a‖⁻¹ ≤ 1

Proof state:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ ‖a‖⁻¹ ≤ 1

Tactic:
exact inv_le_one_of_one_le₀ ha

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ s ⊆ a • t

Tactic:
rw [subset_smul_set_iff₀ (norm_pos_iff.mp <| zero_lt_one.trans_le ha)]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ a⁻¹ • s ⊆ t

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
⊢ s ⊆ balancedCore 𝕜 t

Tactic:
rw [balancedCore_eq_iInter ht]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
⊢ s ⊆ ⋂ r, ⋂ (_ : 1 ≤ ‖r‖), r • t

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
⊢ s ⊆ ⋂ r, ⋂ (_ : 1 ≤ ‖r‖), r • t

Tactic:
refine subset_iInter₂ fun a ha ↦ ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ s ⊆ a • t

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ a⁻¹ • s ⊆ t

Tactic:
apply hst

Result:
case a
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ht : 0 ∈ t
hst : ∀ (a : 𝕜), ‖a‖ ≤ 1 → a • s ⊆ t
a : 𝕜
ha : 1 ≤ ‖a‖
⊢ ‖a⁻¹‖ ≤ 1
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem IsBigO.sum (h : ∀ i ∈ s, A i =O[l] g) : (fun x => ∑ i ∈ s, A i x) =O[l] g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_17
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, ∃ c, IsBigOWith c l (A i) g
⊢ ∃ c, IsBigOWith c l (fun x => ∑ i ∈ s, A i x) g

Tactic:
choose! C hC using h

Result:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_17
A : ι → α → E'
s : Finset ι
C : ι → ℝ
hC : ∀ i ∈ s, IsBigOWith (C i) l (A i) g
⊢ ∃ c, IsBigOWith c l (fun x => ∑ i ∈ s, A i x) g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_17
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, A i =O[l] g
⊢ (fun x => ∑ i ∈ s, A i x) =O[l] g

Tactic:
simp only [IsBigO_def] at *

Result:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_17
A : ι → α → E'
s : Finset ι
h : ∀ i ∈ s, ∃ c, IsBigOWith c l (A i) g
⊢ ∃ c, IsBigOWith c l (fun x => ∑ i ∈ s, A i x) g

Proof state:
α : Type u_1
F : Type u_4
E' : Type u_6
inst✝¹ : Norm F
inst✝ : SeminormedAddCommGroup E'
g : α → F
l : Filter α
ι : Type u_17
A : ι → α → E'
s : Finset ι
C : ι → ℝ
hC : ∀ i ∈ s, IsBigOWith (C i) l (A i) g
⊢ ∃ c, IsBigOWith c l (fun x => ∑ i ∈ s, A i x) g

Tactic:
exact ⟨_, IsBigOWith.sum hC⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem listTransvecCol_mul_mul_listTransvecRow_last_col (hM : M (inr unit) (inr unit) ≠ 0)
    (i : Fin r) :
    ((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inr unit) (inl i) = 0

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)
⊢ ((listTransvecCol M).prod * M * (listTransvecRow ((listTransvecCol M).prod * M)).prod) (inr ()) (inl i) = 0

Tactic:
apply mul_listTransvecRow_last_row

Result:
case hM
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)
⊢ ((listTransvecCol M).prod * M) (inr ()) (inr ()) ≠ 0

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
⊢ listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)

Tactic:
simp [listTransvecRow, listTransvecCol_mul_last_row]

Result:
no goals

Proof state:
case hM
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)
⊢ ((listTransvecCol M).prod * M) (inr ()) (inr ()) ≠ 0

Tactic:
simpa [listTransvecCol_mul_last_row] using hM

Result:
no goals

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inr ()) (inl i) = 0

Tactic:
rw [this]

Result:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)
⊢ ((listTransvecCol M).prod * M * (listTransvecRow ((listTransvecCol M).prod * M)).prod) (inr ()) (inl i) = 0

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inr ()) (inl i) = 0

Tactic:
have : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M) := by
  simp [listTransvecRow, listTransvecCol_mul_last_row]

Result:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M)
⊢ ((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inr ()) (inl i) = 0
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem IsRoot.dvd {R : Type*} [CommSemiring R] {p q : R[X]} {x : R} (h : p.IsRoot x)
    (hpq : p ∣ q) : q.IsRoot x

Proof state:
R : Type u_1
inst✝ : CommSemiring R
p q : R[X]
x : R
h : p.IsRoot x
hpq : p ∣ q
⊢ q.IsRoot x

Tactic:
rwa [IsRoot, eval, eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _ hpq]

Result:
no goals
-- Mathlib/Data/Multiset/MapFold.lean
theorem map_surjective_of_surjective {f : α → β} (hf : Function.Surjective f) :
    Function.Surjective (map f)

Proof state:
case empty
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
⊢ ∃ a, map f a = 0

Tactic:
exact ⟨0, map_zero _⟩

Result:
no goals

Proof state:
case cons.intro.intro
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
y : α
t : Multiset α
⊢ ∃ a, map f a = f y ::ₘ map f t

Tactic:
exact ⟨y ::ₘ t, map_cons _ _ _⟩

Result:
no goals

Proof state:
case cons.intro
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
s : Multiset β
ih : ∃ a, map f a = s
y : α
⊢ ∃ a, map f a = f y ::ₘ s

Tactic:
obtain ⟨t, rfl⟩ := ih

Result:
case cons.intro.intro
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
y : α
t : Multiset α
⊢ ∃ a, map f a = f y ::ₘ map f t

Proof state:
case cons
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
x : β
s : Multiset β
ih : ∃ a, map f a = s
⊢ ∃ a, map f a = x ::ₘ s

Tactic:
obtain ⟨y, rfl⟩ := hf x

Result:
case cons.intro
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
s : Multiset β
ih : ∃ a, map f a = s
y : α
⊢ ∃ a, map f a = f y ::ₘ s

Proof state:
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
s : Multiset β
⊢ ∃ a, map f a = s

Tactic:
induction' s using Multiset.induction_on with x s ih

Result:
case empty
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
⊢ ∃ a, map f a = 0

case cons
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
x : β
s : Multiset β
ih : ∃ a, map f a = s
⊢ ∃ a, map f a = x ::ₘ s

Proof state:
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
⊢ Surjective (map f)

Tactic:
intro s

Result:
α : Type u_1
β : Type v
f : α → β
hf : Surjective f
s : Multiset β
⊢ ∃ a, map f a = s
-- Mathlib/Analysis/Convex/Strict.lean
theorem DirectedOn.strictConvex_sUnion {S : Set (Set E)} (hdir : DirectedOn (· ⊆ ·) S)
    (hS : ∀ s ∈ S, StrictConvex 𝕜 s) : StrictConvex 𝕜 (⋃₀ S)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
S : Set (Set E)
hdir : DirectedOn (fun x1 x2 => x1 ⊆ x2) S
hS : ∀ s ∈ S, StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (⋃₀ S)

Tactic:
rw [sUnion_eq_iUnion]

Result:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
S : Set (Set E)
hdir : DirectedOn (fun x1 x2 => x1 ⊆ x2) S
hS : ∀ s ∈ S, StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (⋃ i, ↑i)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
S : Set (Set E)
hdir : DirectedOn (fun x1 x2 => x1 ⊆ x2) S
hS : ∀ s ∈ S, StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (⋃ i, ↑i)

Tactic:
exact (directedOn_iff_directed.1 hdir).strictConvex_iUnion fun s => hS _ s.2

Result:
no goals
-- Mathlib/Algebra/Divisibility/Prod.lean
theorem prod_dvd_iff {x y : G₁ × G₂} :
    x ∣ y ↔ x.1 ∣ y.1 ∧ x.2 ∣ y.2

Proof state:
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Semigroup G₁
inst✝ : Semigroup G₂
x y : G₁ × G₂
⊢ x ∣ y ↔ x.1 ∣ y.1 ∧ x.2 ∣ y.2

Tactic:
cases x

Result:
case mk
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Semigroup G₁
inst✝ : Semigroup G₂
y : G₁ × G₂
fst✝ : G₁
snd✝ : G₂
⊢ (fst✝, snd✝) ∣ y ↔ (fst✝, snd✝).1 ∣ y.1 ∧ (fst✝, snd✝).2 ∣ y.2

Proof state:
case mk.mk
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Semigroup G₁
inst✝ : Semigroup G₂
fst✝¹ : G₁
snd✝¹ : G₂
fst✝ : G₁
snd✝ : G₂
⊢ (fst✝¹, snd✝¹) ∣ (fst✝, snd✝) ↔ (fst✝¹, snd✝¹).1 ∣ (fst✝, snd✝).1 ∧ (fst✝¹, snd✝¹).2 ∣ (fst✝, snd✝).2

Tactic:
simp only [dvd_def, Prod.exists, Prod.mk_mul_mk, Prod.mk.injEq,
  exists_and_left, exists_and_right, and_self, true_and]

Result:
no goals

Proof state:
case mk
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Semigroup G₁
inst✝ : Semigroup G₂
y : G₁ × G₂
fst✝ : G₁
snd✝ : G₂
⊢ (fst✝, snd✝) ∣ y ↔ (fst✝, snd✝).1 ∣ y.1 ∧ (fst✝, snd✝).2 ∣ y.2

Tactic:
cases y

Result:
case mk.mk
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Semigroup G₁
inst✝ : Semigroup G₂
fst✝¹ : G₁
snd✝¹ : G₂
fst✝ : G₁
snd✝ : G₂
⊢ (fst✝¹, snd✝¹) ∣ (fst✝, snd✝) ↔ (fst✝¹, snd✝¹).1 ∣ (fst✝, snd✝).1 ∧ (fst✝¹, snd✝¹).2 ∣ (fst✝, snd✝).2
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic {K : Type*} [Field K] (f : K[X]) {a : K}
    (hf : (X - C a) ∣ f /ₘ (X - C a)) : X - C a ∣ derivative f

Proof state:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - C a ∣ f /ₘ (X - C a)
key : f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
u : K[X]
hu : f /ₘ (X - C a) = (X - C a) * u
⊢ X - C a ∣ (X - C a) * (u + derivative ((X - C a) * u))

Tactic:
use (u + derivative ((X - C a) * u))

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - C a ∣ f /ₘ (X - C a)
key : f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
⊢ X - C a ∣ derivative f

Tactic:
have ⟨u,hu⟩ := hf

Result:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - C a ∣ f /ₘ (X - C a)
key : f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
u : K[X]
hu : f /ₘ (X - C a) = (X - C a) * u
⊢ X - C a ∣ derivative f

Proof state:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - C a ∣ f /ₘ (X - C a)
key : f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
u : K[X]
hu : f /ₘ (X - C a) = (X - C a) * u
⊢ X - C a ∣ derivative f

Tactic:
rw [← key, hu, ← mul_add (X - C a) u _]

Result:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - C a ∣ f /ₘ (X - C a)
key : f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
u : K[X]
hu : f /ₘ (X - C a) = (X - C a) * u
⊢ X - C a ∣ (X - C a) * (u + derivative ((X - C a) * u))

Proof state:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - C a ∣ f /ₘ (X - C a)
⊢ X - C a ∣ derivative f

Tactic:
have key := divByMonic_add_X_sub_C_mul_derivate_divByMonic_eq_derivative f a

Result:
K : Type u_1
inst✝ : Field K
f : K[X]
a : K
hf : X - C a ∣ f /ₘ (X - C a)
key : f /ₘ (X - C a) + (X - C a) * derivative (f /ₘ (X - C a)) = derivative f
⊢ X - C a ∣ derivative f
-- Mathlib/CategoryTheory/GradedObject/Unitor.lean
@[reassoc]
lemma mapBifunctorLeftUnitor_inv_naturality :
    φ ≫ (mapBifunctorLeftUnitor F X e p hp Y').inv =
      (mapBifunctorLeftUnitor F X e p hp Y).inv ≫ mapBifunctorMapMap F p (𝟙 _) φ

Proof state:
case h
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{u_6, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝² : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p
j : J
⊢ (φ ≫ (mapBifunctorLeftUnitor F X e p hp Y').inv) j =
    ((mapBifunctorLeftUnitor F X e p hp Y).inv ≫ mapBifunctorMapMap F p (𝟙 ((single₀ I).obj X)) φ) j

Tactic:
dsimp

Result:
case h
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁷ : Category.{u_6, u_1} C
inst✝⁶ : Category.{u_5, u_2} D
inst✝⁵ : Zero I
inst✝⁴ : DecidableEq I
inst✝³ : HasInitial C
F : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝² : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y Y' : GradedObject J D
φ : Y ⟶ Y'
inst✝¹ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y').HasMap p
j : J
⊢ φ j ≫ (mapBifunctorLeftUnitor F X e p hp Y').inv j =
    (mapBifunctorLeftUnitor F X e p hp Y).inv j ≫ mapBifunctorMapMap F p (𝟙 ((single₀ I).obj X)) φ j
-- Mathlib/Data/ENNReal/Basic.lean
theorem toNNReal_natCast (n : ℕ) : (n : ℝ≥0∞).toNNReal = n

Proof state:
n : ℕ
⊢ (↑n).toNNReal = ↑n

Tactic:
rw [← ENNReal.coe_natCast n, ENNReal.toNNReal_coe]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem lt_mul_iff_one_lt_right' [MulLeftStrictMono α]
    [MulLeftReflectLT α] (a : α) {b : α} :
    a < a * b ↔ 1 < b :=
  Iff.trans (by rw [mul_one]) (mul_lt_mul_iff_left a)

Proof state:
α : Type u_1
inst✝³ : MulOneClass α
inst✝² : LT α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulLeftReflectLT α
a b : α
⊢ a < a * b ↔ a * 1 < a * b

Tactic:
rw [mul_one]

Result:
no goals
-- Mathlib/Deprecated/Cardinal/Finite.lean
theorem _root_.Cardinal.toPartENat_eq_natCast_iff {c : Cardinal} {n : ℕ} :
    Cardinal.toPartENat c = n ↔ c = n

Proof state:
c : Cardinal.{u_1}
n : ℕ
⊢ toPartENat c = ↑n ↔ c = ↑n

Tactic:
rw [eq_comm, Cardinal.natCast_eq_toPartENat_iff, eq_comm]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Prod.lean
theorem tendsto_atBot_diagonal [Preorder α] : Tendsto (fun a : α => (a, a)) atBot atBot

Proof state:
α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a => (a, a)) atBot atBot

Tactic:
rw [← prod_atBot_atBot_eq]

Result:
α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a => (a, a)) atBot (atBot ×ˢ atBot)

Proof state:
α : Type u_3
inst✝ : Preorder α
⊢ Tendsto (fun a => (a, a)) atBot (atBot ×ˢ atBot)

Tactic:
exact tendsto_id.prod_mk tendsto_id

Result:
no goals
-- Mathlib/Order/RelClasses.lean
lemma subset_of_eq_of_subset (hab : a = b) (hbc : b ⊆ c) : a ⊆ c

Proof state:
α : Type u
inst✝ : HasSubset α
a b c : α
hab : a = b
hbc : b ⊆ c
⊢ a ⊆ c

Tactic:
rwa [hab]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive (attr := simp)] lemma pow_eq_empty : s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Proof state:
case mpr
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
rintro ⟨rfl, hn⟩

Result:
case mpr.intro
α : Type u_2
inst✝ : Monoid α
n : ℕ
hn : n ≠ 0
⊢ ∅ ^ n = ∅

Proof state:
case mpr.intro
α : Type u_2
inst✝ : Monoid α
n : ℕ
hn : n ≠ 0
⊢ ∅ ^ n = ∅

Tactic:
exact empty_pow hn

Result:
no goals

Proof state:
case mp.inl
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
hs : s.Nonempty
⊢ (s ^ n).Nonempty

Tactic:
exact hs.pow

Result:
no goals

Proof state:
case mp
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

Tactic:
contrapose!

Result:
case mp
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s.Nonempty ∨ n = 0 → (s ^ n).Nonempty

Proof state:
case mp.inr
α : Type u_2
inst✝ : Monoid α
s : Set α
⊢ (s ^ 0).Nonempty

Tactic:
simp

Result:
no goals

Proof state:
case mp
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s.Nonempty ∨ n = 0 → (s ^ n).Nonempty

Tactic:
rintro (hs | rfl)

Result:
case mp.inl
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
hs : s.Nonempty
⊢ (s ^ n).Nonempty

case mp.inr
α : Type u_2
inst✝ : Monoid α
s : Set α
⊢ (s ^ 0).Nonempty

Proof state:
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Tactic:
constructor

Result:
case mp
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

case mpr
α : Type u_2
inst✝ : Monoid α
s : Set α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅
-- Mathlib/Data/Set/Card.lean
theorem Finite.exists_bijOn_of_encard_eq [Nonempty β] (hs : s.Finite) (h : s.encard = t.encard) :
    ∃ (f : α → β), BijOn f s t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst✝ : Nonempty β
hs : s.Finite
h : s.encard = t.encard
⊢ ∃ f, BijOn f s t

Tactic:
obtain ⟨f, hf, hinj⟩ := hs.exists_injOn_of_encard_le h.le

Result:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst✝ : Nonempty β
hs : s.Finite
h : s.encard = t.encard
f : α → β
hf : s ⊆ f ⁻¹' t
hinj : InjOn f s
⊢ ∃ f, BijOn f s t

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst✝ : Nonempty β
hs : s.Finite
h : s.encard = t.encard
f : α → β
hf : s ⊆ f ⁻¹' t
hinj : InjOn f s
⊢ ∃ f, BijOn f s t

Tactic:
use f

Result:
case h
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst✝ : Nonempty β
hs : s.Finite
h : s.encard = t.encard
f : α → β
hf : s ⊆ f ⁻¹' t
hinj : InjOn f s
⊢ BijOn f s t

Proof state:
case h
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst✝ : Nonempty β
hs : s.Finite
h : s.encard = t.encard
f : α → β
hf : s ⊆ f ⁻¹' t
hinj : InjOn f s
⊢ BijOn f s t

Tactic:
convert hinj.bijOn_image

Result:
case h.e'_5
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst✝ : Nonempty β
hs : s.Finite
h : s.encard = t.encard
f : α → β
hf : s ⊆ f ⁻¹' t
hinj : InjOn f s
⊢ t = f '' s

Proof state:
case h.e'_5
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst✝ : Nonempty β
hs : s.Finite
h : s.encard = t.encard
f : α → β
hf : s ⊆ f ⁻¹' t
hinj : InjOn f s
⊢ t = f '' s

Tactic:
rw [(hs.image f).eq_of_subset_of_encard_le' (image_subset_iff.mpr hf)
  (h.symm.trans hinj.encard_image.symm).le]

Result:
no goals