harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ShortComplex/ExactFunctor.lean
/--
For an additive functor `F : C ⥤ D` between abelian categories, the following are equivalent:
- `F` preserves short exact sequences, i.e. if `0 ⟶ A ⟶ B ⟶ C ⟶ 0` is exact then
  `0 ⟶ F(A) ⟶ F(B) ⟶ F(C) ⟶ 0` is exact.
- `F` preserves exact sequences, i.e. if `A ⟶ B ⟶ C` is exact then `F(A) ⟶ F(B) ⟶ F(C)` is exact.
- `F` preserves homology.
- `F` preserves both finite limits and finite colimits.
-/
lemma exact_tfae : List.TFAE
    [
      ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact,
      ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact,
      PreservesHomology F,
      PreservesFiniteLimits F ∧ PreservesFiniteColimits F
    ]

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
x✝ : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact := x✝
⊢ F.PreservesHomology

Tactic:
refine ⟨fun {X Y} f ↦ ?_, fun {X Y} f ↦ ?_⟩

Result:
case refine_1
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
x✝ : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact := x✝
X Y : C
f : X ⟶ Y
⊢ PreservesLimit (parallelPair f 0) F

case refine_2
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
x✝ : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact
hF : ∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact := x✝
X Y : C
f : X ⟶ Y
⊢ PreservesColimit (parallelPair f 0) F
-- Mathlib/Algebra/Group/Center.lean
theorem div_mem_center (ha : a ∈ Set.center M) (hb : b ∈ Set.center M) : a / b ∈ Set.center M

Proof state:
M : Type u_1
inst✝ : DivisionMonoid M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a / b ∈ center M

Tactic:
rw [div_eq_mul_inv]

Result:
M : Type u_1
inst✝ : DivisionMonoid M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a * b⁻¹ ∈ center M

Proof state:
M : Type u_1
inst✝ : DivisionMonoid M
a b : M
ha : a ∈ center M
hb : b ∈ center M
⊢ a * b⁻¹ ∈ center M

Tactic:
exact mul_mem_center ha (inv_mem_center hb)

Result:
no goals
-- Mathlib/Data/Nat/Choose/Sum.lean
theorem add_pow (h : Commute x y) (n : ℕ) :
    (x + y) ^ n = ∑ m ∈ range (n + 1), x ^ m * y ^ (n - m) * n.choose m

Proof state:
case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) = y * (x ^ i.succ * y ^ (n - i.succ) * ↑(n.choose i.succ))

Tactic:
rw [← mul_assoc y, ← mul_assoc y, (h.symm.pow_right i.succ).eq]

Result:
case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem size_eraseP {l : Array α} : (l.eraseP p).size = if l.any p then l.size - 1 else l.size

Proof state:
case isFalse
α : Type u_1
p : α → Bool
l : Array α
h : ¬∃ i x, p l[i] = true
⊢ ∀ (i : Nat) (h : i < l.size), ¬p l[i] = true

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : Array α
i : Nat
h : i < l.size
w : p l[i] = true
⊢ l[i] ∈ l

Tactic:
simp

Result:
no goals

Proof state:
case isTrue.intro.intro
α : Type u_1
p : α → Bool
l : Array α
i : Nat
h : i < l.size
w : p l[i] = true
⊢ (l.eraseP p).size = l.size - 1

Tactic:
simp [size_eraseP_of_mem (l := l) (by simp) w]

Result:
no goals

Proof state:
case isTrue
α : Type u_1
p : α → Bool
l : Array α
h : l.any p = true
⊢ (l.eraseP p).size = l.size - 1

Tactic:
simp only [any_eq_true] at h

Result:
case isTrue
α : Type u_1
p : α → Bool
l : Array α
h : ∃ i x, p l[i] = true
⊢ (l.eraseP p).size = l.size - 1

Proof state:
case isFalse
α : Type u_1
p : α → Bool
l : Array α
h : ¬l.any p = true
⊢ (l.eraseP p).size = l.size

Tactic:
simp only [any_eq_true] at h

Result:
case isFalse
α : Type u_1
p : α → Bool
l : Array α
h : ¬∃ i x, p l[i] = true
⊢ (l.eraseP p).size = l.size

Proof state:
case isTrue
α : Type u_1
p : α → Bool
l : Array α
h : ∃ i x, p l[i] = true
⊢ (l.eraseP p).size = l.size - 1

Tactic:
obtain ⟨i, h, w⟩ := h

Result:
case isTrue.intro.intro
α : Type u_1
p : α → Bool
l : Array α
i : Nat
h : i < l.size
w : p l[i] = true
⊢ (l.eraseP p).size = l.size - 1

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ (l.eraseP p).size = if l.any p = true then l.size - 1 else l.size

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
p : α → Bool
l : Array α
h : l.any p = true
⊢ (l.eraseP p).size = l.size - 1

case isFalse
α : Type u_1
p : α → Bool
l : Array α
h : ¬l.any p = true
⊢ (l.eraseP p).size = l.size

Proof state:
case isFalse
α : Type u_1
p : α → Bool
l : Array α
h : ¬∃ i x, p l[i] = true
⊢ (l.eraseP p).size = l.size

Tactic:
rw [eraseP_of_forall_getElem_not]

Result:
case isFalse
α : Type u_1
p : α → Bool
l : Array α
h : ¬∃ i x, p l[i] = true
⊢ ∀ (i : Nat) (h : i < l.size), ¬p l[i] = true
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem sum_eq_iSup_lift {f : ι → Cardinal.{max u v}} (hι : ℵ₀ ≤ #ι)
    (h : lift.{v} #ι ≤ iSup f) : sum f = iSup f

Proof state:
case h.e'_4
ι : Type u
f : ι → Cardinal.{max u v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ iSup f
⊢ iSup f = lift.{v, u} #ι * iSup f

Tactic:
rw [mul_eq_max (aleph0_le_lift.mpr hι) ((aleph0_le_lift.mpr hι).trans h), max_eq_right h]

Result:
no goals

Proof state:
ι : Type u
f : ι → Cardinal.{max u v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ iSup f
⊢ sum f ≤ iSup f

Tactic:
convert sum_le_iSup_lift f

Result:
case h.e'_4
ι : Type u
f : ι → Cardinal.{max u v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ iSup f
⊢ iSup f = lift.{v, u} #ι * iSup f

Proof state:
ι : Type u
f : ι → Cardinal.{max u v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ iSup f
⊢ sum f = iSup f

Tactic:
apply (iSup_le_sum f).antisymm'

Result:
ι : Type u
f : ι → Cardinal.{max u v}
hι : ℵ₀ ≤ #ι
h : lift.{v, u} #ι ≤ iSup f
⊢ sum f ≤ iSup f
-- Mathlib/Data/Int/Cast/Lemmas.lean
@[simp] lemma cast_eq_zero : (n : α) = 0 ↔ n = 0 where
  mp h

Proof state:
case negSucc
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑-[a✝+1] = 0
⊢ -[a✝+1] = 0

Tactic:
rw [cast_negSucc, neg_eq_zero, Nat.cast_eq_zero] at h

Result:
case negSucc
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : a✝ + 1 = 0
⊢ -[a✝+1] = 0

Proof state:
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
n : ℤ
h : ↑n = 0
⊢ n = 0

Tactic:
cases n

Result:
case ofNat
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑(ofNat a✝) = 0
⊢ ofNat a✝ = 0

case negSucc
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑-[a✝+1] = 0
⊢ -[a✝+1] = 0

Proof state:
case negSucc
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : a✝ + 1 = 0
⊢ -[a✝+1] = 0

Tactic:
contradiction

Result:
no goals

Proof state:
case ofNat
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑(ofNat a✝) = 0
⊢ ofNat a✝ = 0

Tactic:
erw [Int.cast_natCast] at h

Result:
case ofNat
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑a✝ = 0
⊢ ofNat a✝ = 0

Proof state:
case ofNat
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
a✝ : ℕ
h : ↑a✝ = 0
⊢ ofNat a✝ = 0

Tactic:
exact congr_arg _ (Nat.cast_eq_zero.1 h)

Result:
no goals

Proof state:
α : Type u_3
inst✝¹ : AddGroupWithOne α
inst✝ : CharZero α
n : ℤ
h : n = 0
⊢ ↑n = 0

Tactic:
rw [h, cast_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem getLast_drop {l : List α} (h : l.drop n ≠ []) :
    (l.drop n).getLast h = l.getLast (ne_nil_of_length_pos (by simp at h; omega))

Proof state:
α : Type ?u.31935
n : Nat
l : List α
h : drop n l ≠ []
⊢ 0 < l.length

Tactic:
simp at h

Result:
α : Type ?u.31935
n : Nat
l : List α
h : n < l.length
⊢ 0 < l.length

Proof state:
α : Type u_1
n : Nat
l : List α
h : drop n l ≠ []
⊢ (drop n l).getLast h = l.getLast ⋯

Tactic:
simp only [ne_eq, drop_eq_nil_iff] at h

Result:
α : Type u_1
n : Nat
l : List α
h✝ : drop n l ≠ []
h : ¬l.length ≤ n
⊢ (drop n l).getLast h✝ = l.getLast ⋯

Proof state:
α : Type u_1
n : Nat
l : List α
h✝ : drop n l ≠ []
h : ¬l.length ≤ n
⊢ some ((drop n l).getLast h✝) = some (l.getLast ⋯)

Tactic:
simp only [← getLast?_eq_getLast, getLast?_drop, ite_eq_right_iff]

Result:
α : Type u_1
n : Nat
l : List α
h✝ : drop n l ≠ []
h : ¬l.length ≤ n
⊢ l.length ≤ n → none = l.getLast?

Proof state:
α : Type u_1
n : Nat
l : List α
h✝ : drop n l ≠ []
h : ¬l.length ≤ n
⊢ l.length ≤ n → none = l.getLast?

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.31935
n : Nat
l : List α
h : n < l.length
⊢ 0 < l.length

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
h✝ : drop n l ≠ []
h : ¬l.length ≤ n
⊢ (drop n l).getLast h✝ = l.getLast ⋯

Tactic:
apply Option.some_inj.1

Result:
α : Type u_1
n : Nat
l : List α
h✝ : drop n l ≠ []
h : ¬l.length ≤ n
⊢ some ((drop n l).getLast h✝) = some (l.getLast ⋯)
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem coeffs_monomial (n : ℕ) {c : R} (hc : c ≠ 0) : (monomial n c).coeffs = {c}

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
c : R
hc : c ≠ 0
⊢ image (fun n_1 => ((monomial n) c).coeff n_1) {n} = {c}

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
c : R
hc : c ≠ 0
⊢ ((monomial n) c).coeffs = {c}

Tactic:
rw [coeffs, support_monomial n hc]

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
c : R
hc : c ≠ 0
⊢ image (fun n_1 => ((monomial n) c).coeff n_1) {n} = {c}
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive]
lemma IsOfFinOrder.finite_powers (ha : IsOfFinOrder a) : (powers a : Set G).Finite

Proof state:
G : Type u_1
inst✝ : Monoid G
a : G
ha : IsOfFinOrder a
⊢ (↑(Finset.image (fun x => a ^ x) (Finset.range (orderOf a)))).Finite

Tactic:
exact Finset.finite_toSet _

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Monoid G
a : G
ha : IsOfFinOrder a
⊢ (↑(powers a)).Finite

Tactic:
classical rw [ha.powers_eq_image_range_orderOf]; exact Finset.finite_toSet _

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Monoid G
a : G
ha : IsOfFinOrder a
⊢ (↑(powers a)).Finite

Tactic:
rw [ha.powers_eq_image_range_orderOf]

Result:
G : Type u_1
inst✝ : Monoid G
a : G
ha : IsOfFinOrder a
⊢ (↑(Finset.image (fun x => a ^ x) (Finset.range (orderOf a)))).Finite
-- Mathlib/MeasureTheory/PiSystem.lean
theorem measurableSet_iSup_of_mem_piiUnionInter (m : ι → MeasurableSpace α) (S : Set ι) (t : Set α)
    (ht : t ∈ piiUnionInter (fun n => { s | MeasurableSet[m n] s }) S) :
    MeasurableSet[⨆ i ∈ S, m i] t

Proof state:
case intro.intro.intro.intro
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ x ∈ pt, ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
⊢ m i ≤ ⨆ i ∈ S, m i

Tactic:
have hi' : i ∈ S := hpt hi

Result:
case intro.intro.intro.intro
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ x ∈ pt, ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
hi' : i ∈ S
⊢ m i ≤ ⨆ i ∈ S, m i

Proof state:
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
t : Set α
ht : t ∈ piiUnionInter (fun n => {s | MeasurableSet s}) S
⊢ MeasurableSet t

Tactic:
rcases ht with ⟨pt, hpt, ft, ht_m, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ x ∈ pt, ft x ∈ (fun n => {s | MeasurableSet s}) x
⊢ MeasurableSet (⋂ x ∈ pt, ft x)

Proof state:
case intro.intro.intro.intro
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ x ∈ pt, ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
hi' : i ∈ S
⊢ m i ≤ ⨆ i ∈ S, m i

Tactic:
exact le_iSup₂ (f := fun i (_ : i ∈ S) => m i) i hi'

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ x ∈ pt, ft x ∈ (fun n => {s | MeasurableSet s}) x
⊢ MeasurableSet (⋂ x ∈ pt, ft x)

Tactic:
refine pt.measurableSet_biInter fun i hi => ?_

Result:
case intro.intro.intro.intro
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ x ∈ pt, ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
⊢ MeasurableSet (ft i)

Proof state:
case intro.intro.intro.intro
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ x ∈ pt, ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
⊢ MeasurableSet (ft i)

Tactic:
suffices h_le : m i ≤ ⨆ i ∈ S, m i from h_le (ft i) (ht_m i hi)

Result:
case intro.intro.intro.intro
α : Type u_3
ι : Type u_4
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ x ∈ pt, ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
⊢ m i ≤ ⨆ i ∈ S, m i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_lt_sub_left : ∀ {k m n : Nat}, k < m → k < n → m - n < m - k
  | 0, m+1, n+1, _, _ => by rw [Nat.add_sub_add_right]; exact lt_succ_of_le (Nat.sub_le _ _)
  | k+1, m+1, n+1, h1, h2 => by
    rw [Nat.add_sub_add_right, Nat.add_sub_add_right]
    exact Nat.sub_lt_sub_left (Nat.lt_of_succ_lt_succ h1) (Nat.lt_of_succ_lt_succ h2)

Proof state:
k m n : Nat
h1 : k + 1 < m + 1
h2 : k + 1 < n + 1
⊢ m + 1 - (n + 1) < m + 1 - (k + 1)

Tactic:
rw [Nat.add_sub_add_right, Nat.add_sub_add_right]

Result:
k m n : Nat
h1 : k + 1 < m + 1
h2 : k + 1 < n + 1
⊢ m - n < m - k

Proof state:
m n : Nat
x✝¹ : 0 < m + 1
x✝ : 0 < n + 1
⊢ m + 1 - (n + 1) < m + 1 - 0

Tactic:
rw [Nat.add_sub_add_right]

Result:
m n : Nat
x✝¹ : 0 < m + 1
x✝ : 0 < n + 1
⊢ m - n < m + 1 - 0

Proof state:
m n : Nat
x✝¹ : 0 < m + 1
x✝ : 0 < n + 1
⊢ m - n < m + 1 - 0

Tactic:
exact lt_succ_of_le (Nat.sub_le _ _)

Result:
no goals

Proof state:
k m n : Nat
h1 : k + 1 < m + 1
h2 : k + 1 < n + 1
⊢ m - n < m - k

Tactic:
exact Nat.sub_lt_sub_left (Nat.lt_of_succ_lt_succ h1) (Nat.lt_of_succ_lt_succ h2)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/CardPowDegree.lean
theorem cardPowDegree_apply [DecidableEq Fq] (p : Fq[X]) :
    cardPowDegree p = if p = 0 then 0 else (Fintype.card Fq : ℤ) ^ natDegree p

Proof state:
Fq : Type u_1
inst✝² : Field Fq
inst✝¹ : Fintype Fq
inst✝ : DecidableEq Fq
p : Fq[X]
⊢ cardPowDegree p = if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree

Tactic:
rw [cardPowDegree]

Result:
Fq : Type u_1
inst✝² : Field Fq
inst✝¹ : Fintype Fq
inst✝ : DecidableEq Fq
p : Fq[X]
⊢ { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯,
        add_le' := ⋯ }
      p =
    if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree

Proof state:
Fq : Type u_1
inst✝² : Field Fq
inst✝¹ : Fintype Fq
inst✝ : DecidableEq Fq
p : Fq[X]
⊢ { toFun := fun p => if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯,
        add_le' := ⋯ }
      p =
    if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree

Tactic:
dsimp

Result:
Fq : Type u_1
inst✝² : Field Fq
inst✝¹ : Fintype Fq
inst✝ : DecidableEq Fq
p : Fq[X]
⊢ (if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree) = if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree

Proof state:
Fq : Type u_1
inst✝² : Field Fq
inst✝¹ : Fintype Fq
inst✝ : DecidableEq Fq
p : Fq[X]
⊢ (if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree) = if p = 0 then 0 else ↑(Fintype.card Fq) ^ p.natDegree

Tactic:
convert rfl

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem Iso.inv_inv (f : X ≅ Y) : inv f.inv = f.hom

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ≅ Y
⊢ inv f.inv = f.hom

Tactic:
apply inv_eq_of_hom_inv_id

Result:
case hom_inv_id
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ≅ Y
⊢ f.inv ≫ f.hom = 𝟙 Y

Proof state:
case hom_inv_id
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ≅ Y
⊢ f.inv ≫ f.hom = 𝟙 Y

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal_apply (M : o → Matrix m n α) (ik jk) :
    blockDiagonal M ik jk = if ik.2 = jk.2 then M ik.2 ik.1 jk.1 else 0

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
ik : m × o
jk : n × o
⊢ blockDiagonal M ik jk = if ik.2 = jk.2 then M ik.2 ik.1 jk.1 else 0

Tactic:
cases ik

Result:
case mk
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
jk : n × o
fst✝ : m
snd✝ : o
⊢ blockDiagonal M (fst✝, snd✝) jk = if (fst✝, snd✝).2 = jk.2 then M (fst✝, snd✝).2 (fst✝, snd✝).1 jk.1 else 0

Proof state:
case mk.mk
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
fst✝¹ : m
snd✝¹ : o
fst✝ : n
snd✝ : o
⊢ blockDiagonal M (fst✝¹, snd✝¹) (fst✝, snd✝) =
    if (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2 then M (fst✝¹, snd✝¹).2 (fst✝¹, snd✝¹).1 (fst✝, snd✝).1 else 0

Tactic:
rfl

Result:
no goals

Proof state:
case mk
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
jk : n × o
fst✝ : m
snd✝ : o
⊢ blockDiagonal M (fst✝, snd✝) jk = if (fst✝, snd✝).2 = jk.2 then M (fst✝, snd✝).2 (fst✝, snd✝).1 jk.1 else 0

Tactic:
cases jk

Result:
case mk.mk
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
fst✝¹ : m
snd✝¹ : o
fst✝ : n
snd✝ : o
⊢ blockDiagonal M (fst✝¹, snd✝¹) (fst✝, snd✝) =
    if (fst✝¹, snd✝¹).2 = (fst✝, snd✝).2 then M (fst✝¹, snd✝¹).2 (fst✝¹, snd✝¹).1 (fst✝, snd✝).1 else 0
-- Mathlib/Topology/Instances/Rat.lean
theorem Int.isClosedEmbedding_coe_rat : IsClosedEmbedding ((↑) : ℤ → ℚ) :=
  isClosedEmbedding_of_pairwise_le_dist zero_lt_one <| by simpa using Int.pairwise_one_le_dist

Proof state:
⊢ Pairwise fun x y => 1 ≤ dist ↑x ↑y

Tactic:
simpa using Int.pairwise_one_le_dist

Result:
no goals
-- Mathlib/NumberTheory/AbelSummation.lean
theorem ineqofmemIco {k : ℕ} (hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊) :
    a ≤ k ∧ k + 1 ≤ b

Proof state:
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ a ≤ ↑k ∧ ↑k + 1 ≤ b

Tactic:
constructor

Result:
case left
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ a ≤ ↑k

case right
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ ↑k + 1 ≤ b

Proof state:
case right
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ k.succ ≤ ⌊b⌋₊

Tactic:
exact (Set.mem_Ico.mp hk).2

Result:
no goals

Proof state:
case right
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ ↑k + 1 ≤ b

Tactic:
rw [← Nat.cast_add_one, ← Nat.le_floor_iff' (Nat.succ_ne_zero k)]

Result:
case right
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ k.succ ≤ ⌊b⌋₊

Proof state:
case left
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
this : ⌊a⌋₊ + 1 ≤ k
⊢ a ≤ ↑k

Tactic:
exact le_of_lt <| (Nat.floor_lt' (by omega)).mp this

Result:
no goals

Proof state:
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
this : ⌊a⌋₊ + 1 ≤ k
⊢ k ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
case left
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ a ≤ ↑k

Tactic:
have := (Set.mem_Ico.mp hk).1

Result:
case left
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
this : ⌊a⌋₊ + 1 ≤ k
⊢ a ≤ ↑k
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem LinearIndependent.maximal_iff {ι : Type w} {R : Type u} [Semiring R] [Nontrivial R]
    {M : Type v} [AddCommMonoid M] [Module R M] {v : ι → M} (i : LinearIndependent R v) :
    i.Maximal ↔
      ∀ (κ : Type v) (w : κ → M) (_i' : LinearIndependent R w) (j : ι → κ) (_h : w ∘ j = v),
        Surjective j

Proof state:
case mpr
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M), LinearIndependent R w → ∀ (j : ι → κ), w ∘ j = v → Surjective j
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ≤ w
⊢ range v = w

Tactic:
specialize
  p w ((↑) : w → M) i' (fun i => ⟨v i, range_subset_iff.mp h i⟩)
    (by
      ext
      simp)

Result:
case mpr
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ≤ w
p : Surjective fun i => ⟨v i, ⋯⟩
⊢ range v = w

Proof state:
case mpr
ι : Type w
R : Type u
inst✝³ : Semiring R
inst✝² : Nontrivial R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent R Subtype.val
h : range v ≤ w
p : Surjective fun i => ⟨v i, ⋯⟩
q : (fun x => ↑⟨v x, ⋯⟩) '' univ = Subtype.val '' univ
⊢ range v = w

Tactic:
simpa using q

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_def [DecidableEq R] (p : R[X]) [Decidable (p = 0)] :
    p.roots = if h : p = 0 then ∅ else Classical.choose (exists_multiset_roots h)

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
ip0 : Decidable (p = 0)
⊢ p.roots = if h : p = 0 then ∅ else Classical.choose ⋯

Tactic:
obtain rfl := Subsingleton.elim ip0 (Classical.dec (p = 0))

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ p.roots = if h : p = 0 then ∅ else Classical.choose ⋯

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
⊢ p.roots = if h : p = 0 then ∅ else Classical.choose ⋯

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
iR : DecidableEq R
p : R[X]
ip0 : Decidable (p = 0)
⊢ p.roots = if h : p = 0 then ∅ else Classical.choose ⋯

Tactic:
obtain rfl := Subsingleton.elim iR (Classical.decEq R)

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
ip0 : Decidable (p = 0)
⊢ p.roots = if h : p = 0 then ∅ else Classical.choose ⋯

Proof state:
R : Type u
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
p : R[X]
inst✝ : Decidable (p = 0)
⊢ p.roots = if h : p = 0 then ∅ else Classical.choose ⋯

Tactic:
rename_i iR ip0

Result:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
iR : DecidableEq R
p : R[X]
ip0 : Decidable (p = 0)
⊢ p.roots = if h : p = 0 then ∅ else Classical.choose ⋯