harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem supp_injective :
    Function.Injective (ConnectedComponent.supp : G.ConnectedComponent → Set V)

Proof state:
V : Type u
G : SimpleGraph V
v w : V
h : ∀ (x : V), G.Reachable x v ↔ G.Reachable x w
⊢ G.Reachable v w

Tactic:
rw [reachable_comm, h]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
⊢ ∀ (v w : V),
    (G.connectedComponentMk v).supp = (G.connectedComponentMk w).supp →
      G.connectedComponentMk v = G.connectedComponentMk w

Tactic:
intro v w

Result:
V : Type u
G : SimpleGraph V
v w : V
⊢ (G.connectedComponentMk v).supp = (G.connectedComponentMk w).supp →
    G.connectedComponentMk v = G.connectedComponentMk w

Proof state:
V : Type u
G : SimpleGraph V
v w : V
⊢ (∀ (x : V), G.Reachable x v ↔ G.Reachable x w) → G.Reachable v w

Tactic:
intro h

Result:
V : Type u
G : SimpleGraph V
v w : V
h : ∀ (x : V), G.Reachable x v ↔ G.Reachable x w
⊢ G.Reachable v w

Proof state:
V : Type u
G : SimpleGraph V
v w : V
⊢ (G.connectedComponentMk v).supp = (G.connectedComponentMk w).supp →
    G.connectedComponentMk v = G.connectedComponentMk w

Tactic:
simp only [ConnectedComponent.supp, Set.ext_iff, ConnectedComponent.eq, Set.mem_setOf_eq]

Result:
V : Type u
G : SimpleGraph V
v w : V
⊢ (∀ (x : V), G.Reachable x v ↔ G.Reachable x w) → G.Reachable v w

Proof state:
V : Type u
G : SimpleGraph V
⊢ Injective supp

Tactic:
refine ConnectedComponent.ind₂ ?_

Result:
V : Type u
G : SimpleGraph V
⊢ ∀ (v w : V),
    (G.connectedComponentMk v).supp = (G.connectedComponentMk w).supp →
      G.connectedComponentMk v = G.connectedComponentMk w
-- Mathlib/Data/List/Nodup.lean
theorem Nodup.sigma {σ : α → Type*} {l₂ : ∀ a , List (σ a)} (d₁ : Nodup l₁)
    (d₂ : ∀ a , Nodup (l₂ a)) : (l₁.sigma l₂).Nodup :=
  nodup_flatMap.2
    ⟨fun a _ => (d₂ a).map fun b b' h => by injection h with _ h,
      d₁.imp fun {a₁ a₂} n x h₁ h₂ => by
        rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩
        rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩
        exact n rfl⟩

Proof state:
case intro.intro
α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : σ a₁
left✝ : b₁ ∈ l₂ a₁
h₁ : ⟨a₁, b₁⟩ ∈ (fun a => map (Sigma.mk a) (l₂ a)) a₁
h₂ : ⟨a₁, b₁⟩ ∈ (fun a => map (Sigma.mk a) (l₂ a)) a₂
⊢ False

Tactic:
rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩

Result:
case intro.intro.intro.intro.refl
α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ : α
b₁ : σ a₁
left✝ : b₁ ∈ l₂ a₁
h₁ : ⟨a₁, b₁⟩ ∈ (fun a => map (Sigma.mk a) (l₂ a)) a₁
n : a₁ ≠ a₁
h₂ : ⟨a₁, b₁⟩ ∈ (fun a => map (Sigma.mk a) (l₂ a)) a₁
mb₂ : b₁ ∈ l₂ a₁
⊢ False

Proof state:
α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
x : (a : α) × σ a
h₁ : x ∈ (fun a => map (Sigma.mk a) (l₂ a)) a₁
h₂ : x ∈ (fun a => map (Sigma.mk a) (l₂ a)) a₂
⊢ False

Tactic:
rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩

Result:
case intro.intro
α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ a₂ : α
n : a₁ ≠ a₂
b₁ : σ a₁
left✝ : b₁ ∈ l₂ a₁
h₁ : ⟨a₁, b₁⟩ ∈ (fun a => map (Sigma.mk a) (l₂ a)) a₁
h₂ : ⟨a₁, b₁⟩ ∈ (fun a => map (Sigma.mk a) (l₂ a)) a₂
⊢ False

Proof state:
case intro.intro.intro.intro.refl
α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a₁ : α
b₁ : σ a₁
left✝ : b₁ ∈ l₂ a₁
h₁ : ⟨a₁, b₁⟩ ∈ (fun a => map (Sigma.mk a) (l₂ a)) a₁
n : a₁ ≠ a₁
h₂ : ⟨a₁, b₁⟩ ∈ (fun a => map (Sigma.mk a) (l₂ a)) a₁
mb₂ : b₁ ∈ l₂ a₁
⊢ False

Tactic:
exact n rfl

Result:
no goals

Proof state:
α : Type u
l₁ : List α
σ : α → Type u_1
l₂ : (a : α) → List (σ a)
d₁ : l₁.Nodup
d₂ : ∀ (a : α), (l₂ a).Nodup
a : α
x✝ : a ∈ l₁
b b' : σ a
h : ⟨a, b⟩ = ⟨a, b'⟩
⊢ b = b'

Tactic:
injection h with _ h

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem get_map {β : Type*} (v : Vector α n) (f : α → β) (i : Fin n) :
    (v.map f).get i = f (v.get i)

Proof state:
case mk
α : Type u_1
n : ℕ
β : Type u_6
f : α → β
i : Fin n
val✝ : List α
property✝ : val✝.length = n
⊢ (map f ⟨val✝, property✝⟩).get i = f (get ⟨val✝, property✝⟩ i)

Tactic:
simp [Vector.map, get_eq_get_toList]

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α n
f : α → β
i : Fin n
⊢ (map f v).get i = f (v.get i)

Tactic:
cases v

Result:
case mk
α : Type u_1
n : ℕ
β : Type u_6
f : α → β
i : Fin n
val✝ : List α
property✝ : val✝.length = n
⊢ (map f ⟨val✝, property✝⟩).get i = f (get ⟨val✝, property✝⟩ i)
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem toMatrix_reindexEquiv (e : n ≃ p) (t : TransvectionStruct n R) :
    (t.reindexEquiv e).toMatrix = reindexAlgEquiv R _ e t.toMatrix

Proof state:
case mk
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
⊢ (reindexEquiv e { i := t_i, j := t_j, hij := hij✝, c := c✝ }).toMatrix =
    (reindexAlgEquiv R R e) { i := t_i, j := t_j, hij := hij✝, c := c✝ }.toMatrix

Tactic:
ext a b

Result:
case mk.a
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
⊢ (reindexEquiv e { i := t_i, j := t_j, hij := hij✝, c := c✝ }).toMatrix a b =
    (reindexAlgEquiv R R e) { i := t_i, j := t_j, hij := hij✝, c := c✝ }.toMatrix a b

Proof state:
case mk.a
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
⊢ (1 + stdBasisMatrix (e t_i) (e t_j) c✝) a b = (1 + stdBasisMatrix t_i t_j c✝) (e.symm a) (e.symm b)

Tactic:
by_cases ha : e t_i = a <;> by_cases hb : e t_j = b <;> by_cases hab : a = b <;>
  simp [ha, hb, hab, ← e.apply_eq_iff_eq_symm_apply, stdBasisMatrix]

Result:
no goals

Proof state:
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t : TransvectionStruct n R
⊢ (reindexEquiv e t).toMatrix = (reindexAlgEquiv R R e) t.toMatrix

Tactic:
rcases t with ⟨t_i, t_j, _⟩

Result:
case mk
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
⊢ (reindexEquiv e { i := t_i, j := t_j, hij := hij✝, c := c✝ }).toMatrix =
    (reindexAlgEquiv R R e) { i := t_i, j := t_j, hij := hij✝, c := c✝ }.toMatrix

Proof state:
case mk.a
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
⊢ (reindexEquiv e { i := t_i, j := t_j, hij := hij✝, c := c✝ }).toMatrix a b =
    (reindexAlgEquiv R R e) { i := t_i, j := t_j, hij := hij✝, c := c✝ }.toMatrix a b

Tactic:
simp only [reindexEquiv, transvection, mul_boole, Algebra.id.smul_eq_mul, toMatrix_mk,
  submatrix_apply, reindex_apply, DMatrix.add_apply, Pi.smul_apply, reindexAlgEquiv_apply]

Result:
case mk.a
n : Type u_1
p : Type u_2
R : Type u₂
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
inst✝¹ : Fintype n
inst✝ : Fintype p
e : n ≃ p
t_i t_j : n
hij✝ : t_i ≠ t_j
c✝ : R
a b : p
⊢ (1 + stdBasisMatrix (e t_i) (e t_j) c✝) a b = (1 + stdBasisMatrix t_i t_j c✝) (e.symm a) (e.symm b)
-- Mathlib/Order/PiLex.lean
theorem toLex_strictMono : StrictMono (@toLex (∀ i, β i)) := fun a b h =>
  let ⟨i, hi, hl⟩ := IsWellFounded.wf.has_min (r := (· < ·)) { i | a i ≠ b i }
    (Function.ne_iff.1 h.ne)
  ⟨i, fun j hj => by
    contrapose! hl
    exact ⟨j, hl, hj⟩, (h.le i).lt_of_ne hi⟩

Proof state:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
a b : (i : ι) → β i
h : a < b
i : ι
hi : i ∈ {i | a i ≠ b i}
hl : ∀ x ∈ {i | a i ≠ b i}, ¬x < i
j : ι
hj : (fun x1 x2 => x1 < x2) j i
⊢ toLex a j = toLex b j

Tactic:
contrapose! hl

Result:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
a b : (i : ι) → β i
h : a < b
i : ι
hi : i ∈ {i | a i ≠ b i}
j : ι
hj : (fun x1 x2 => x1 < x2) j i
hl : toLex a j ≠ toLex b j
⊢ ∃ x ∈ {i | a i ≠ b i}, x < i

Proof state:
ι : Type u_1
β : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : (i : ι) → PartialOrder (β i)
a b : (i : ι) → β i
h : a < b
i : ι
hi : i ∈ {i | a i ≠ b i}
j : ι
hj : (fun x1 x2 => x1 < x2) j i
hl : toLex a j ≠ toLex b j
⊢ ∃ x ∈ {i | a i ≠ b i}, x < i

Tactic:
exact ⟨j, hl, hj⟩

Result:
no goals
-- Mathlib/Analysis/Convex/EGauge.lean
lemma le_egauge_smul_left (c : 𝕜) (s : Set E) (x : E) :
    egauge 𝕜 s x / ‖c‖ₑ ≤ egauge 𝕜 (c • s) x

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
a : 𝕜
x : E
hx : x ∈ s
⊢ egauge 𝕜 s ((fun x => (a * c) • x) x) / ‖c‖ₑ ≤ ‖a‖ₑ

Tactic:
apply ENNReal.div_le_of_le_mul

Result:
case intro.intro.h
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
a : 𝕜
x : E
hx : x ∈ s
⊢ egauge 𝕜 s ((fun x => (a * c) • x) x) ≤ ‖a‖ₑ * ‖c‖ₑ

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
⊢ egauge 𝕜 s x / ‖c‖ₑ ≤ egauge 𝕜 (c • s) x

Tactic:
simp_rw [le_egauge_iff, smul_smul]

Result:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
⊢ ∀ (c_1 : 𝕜), x ∈ (c_1 * c) • s → egauge 𝕜 s x / ‖c‖ₑ ≤ ‖c_1‖ₑ

Proof state:
case intro.intro.h
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
a : 𝕜
x : E
hx : x ∈ s
⊢ egauge 𝕜 s ((fun x => (a * c) • x) x) ≤ ‖a‖ₑ * ‖c‖ₑ

Tactic:
rw [← enorm_mul]

Result:
case intro.intro.h
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
a : 𝕜
x : E
hx : x ∈ s
⊢ egauge 𝕜 s ((fun x => (a * c) • x) x) ≤ ‖a * c‖ₑ

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
x : E
⊢ ∀ (c_1 : 𝕜), x ∈ (c_1 * c) • s → egauge 𝕜 s x / ‖c‖ₑ ≤ ‖c_1‖ₑ

Tactic:
rintro a ⟨x, hx, rfl⟩

Result:
case intro.intro
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
a : 𝕜
x : E
hx : x ∈ s
⊢ egauge 𝕜 s ((fun x => (a * c) • x) x) / ‖c‖ₑ ≤ ‖a‖ₑ

Proof state:
case intro.intro.h
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
c : 𝕜
s : Set E
a : 𝕜
x : E
hx : x ∈ s
⊢ egauge 𝕜 s ((fun x => (a * c) • x) x) ≤ ‖a * c‖ₑ

Tactic:
exact egauge_le_of_mem_smul <| smul_mem_smul_set hx

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Bisect.lean
theorem le_add_one_of_avg_eq_left (h : avg a b = a) : b ≤ a + 1

Proof state:
case inr
a b : Nat
h : a.avg b = a
hge : b ≥ a + 2
⊢ a < a

Tactic:
conv => rhs; rw [← h]

Result:
case inr
a b : Nat
h : a.avg b = a
hge : b ≥ a + 2
⊢ a < a.avg b

Proof state:
case inr
a b : Nat
h : a.avg b = a
hge : b ≥ a + 2
⊢ (a + 1) * 2 ≤ a + b

Tactic:
omega

Result:
no goals

Proof state:
case inr
a b : Nat
h : a.avg b = a
hge : b ≥ a + 2
⊢ b ≤ a + 1

Tactic:
absurd Nat.lt_irrefl a

Result:
case inr
a b : Nat
h : a.avg b = a
hge : b ≥ a + 2
⊢ a < a

Proof state:
case inl
a b : Nat
h : a.avg b = a
hlt : b < a + 2
⊢ b ≤ a + 1

Tactic:
exact Nat.le_of_lt_add_one hlt

Result:
no goals

Proof state:
a b : Nat
h : a.avg b = a
⊢ b ≤ a + 1

Tactic:
cases Nat.lt_or_ge b (a+2) with
| inl hlt => exact Nat.le_of_lt_add_one hlt
| inr hge =>
  absurd Nat.lt_irrefl a
  conv => rhs; rw [← h]
  rw [← Nat.add_one_le_iff, Nat.le_div_iff_mul_le Nat.zero_lt_two]
  omega

Result:
no goals

Proof state:
case inr
a b : Nat
h : a.avg b = a
hge : b ≥ a + 2
⊢ a < a.avg b

Tactic:
rw [← Nat.add_one_le_iff, Nat.le_div_iff_mul_le Nat.zero_lt_two]

Result:
case inr
a b : Nat
h : a.avg b = a
hge : b ≥ a + 2
⊢ (a + 1) * 2 ≤ a + b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem getElem_unattach
    {p : α → Prop} {l : Array { x // p x }} (i : Nat) (h : i < l.unattach.size) :
    l.unattach[i] = (l[i]'(by simpa using h)).1

Proof state:
α : Type ?u.148186
p : α → Prop
l : Array { x // p x }
i : Nat
h : i < l.unattach.size
⊢ i < l.size

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
l : Array { x // p x }
i : Nat
h : i < l.unattach.size
⊢ l.unattach[i] = l[i].val

Tactic:
simp [unattach]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem pow_rpow_inv_natCast (x : ℝ≥0) {n : ℕ} (hn : n ≠ 0) : (x ^ n) ^ (n⁻¹ : ℝ) = x

Proof state:
x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ (↑x ^ n) ^ (↑n)⁻¹ = ↑x

Tactic:
exact Real.pow_rpow_inv_natCast x.2 hn

Result:
no goals

Proof state:
x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ (x ^ n) ^ (↑n)⁻¹ = x

Tactic:
rw [← NNReal.coe_inj, coe_rpow, NNReal.coe_pow]

Result:
x : ℝ≥0
n : ℕ
hn : n ≠ 0
⊢ (↑x ^ n) ^ (↑n)⁻¹ = ↑x
-- Mathlib/CategoryTheory/Limits/Preserves/Opposites.lean
/-- If `F : C ⥤ D` preserves finite products, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite
    coproducts. -/
lemma preservesFiniteCoproducts_op (F : C ⥤ D) [PreservesFiniteProducts F] :
    PreservesFiniteCoproducts F.op where
  preserves _

Proof state:
case inst
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝))ᵒᵖ F

Tactic:
exact preservesLimitsOfShape_of_equiv (Discrete.opposite _).symm _

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝)) F.op

Tactic:
apply (config := { allowSynthFailures := true }) preservesColimitsOfShape_op

Result:
case inst
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesFiniteProducts F
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝))ᵒᵖ F
-- Mathlib/Data/List/Cycle.lean
theorem chain_of_pairwise : (∀ a ∈ s, ∀ b ∈ s, r a b) → Chain r s

Proof state:
case HI.p.refine_1.inl
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l
⊢ r a b

Tactic:
exact hs a Ha b (Hl hb)

Result:
no goals

Proof state:
case HI.p
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ List.Pairwise r (a :: (l ++ [a]))

Tactic:
rw [pairwise_cons]

Result:
case HI.p
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
⊢ (∀ a' ∈ l ++ [a], r a a') ∧ List.Pairwise r (l ++ [a])

Proof state:
case HI.p.refine_2
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l
c : α
hc : c = a
⊢ r b c

Tactic:
rw [hc]

Result:
case HI.p.refine_2
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ l
c : α
hc : c = a
⊢ r b a

Proof state:
case HI.p.refine_1.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b ∈ [a]
⊢ r a b

Tactic:
rw [mem_singleton] at hb

Result:
case HI.p.refine_1.inr
α : Type u_1
r : α → α → Prop
s : Cycle α
a : α
l : List α
a✝ : (∀ a ∈ ↑l, ∀ b ∈ ↑l, r a b) → Chain r ↑l
hs : ∀ a_1 ∈ ↑(a :: l), ∀ b ∈ ↑(a :: l), r a_1 b
Ha : a ∈ ↑(a :: l)
Hl : ∀ {b : α}, b ∈ l → b ∈ ↑(a :: l)
b : α
hb : b = a
⊢ r a b
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem exists_pos_mul_lt {a : α} (h : 0 < a) (b : α) : ∃ c : α, 0 < c ∧ b * c < a

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a : α
h : 0 < a
b : α
this : 0 < a / ((b + 1) ⊔ 1)
⊢ b < (b + 1) ⊔ 1

Tactic:
exact lt_max_iff.2 (Or.inl <| lt_add_one _)

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a : α
h : 0 < a
b : α
this : 0 < a / ((b + 1) ⊔ 1)
⊢ b * (a / ((b + 1) ⊔ 1)) < a

Tactic:
rw [← lt_div_iff₀ this, div_div_cancel₀ h.ne']

Result:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a : α
h : 0 < a
b : α
this : 0 < a / ((b + 1) ⊔ 1)
⊢ b < (b + 1) ⊔ 1

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a : α
h : 0 < a
b : α
⊢ ∃ c, 0 < c ∧ b * c < a

Tactic:
have : 0 < a / max (b + 1) 1 := div_pos h (lt_max_iff.2 (Or.inr zero_lt_one))

Result:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a : α
h : 0 < a
b : α
this : 0 < a / ((b + 1) ⊔ 1)
⊢ ∃ c, 0 < c ∧ b * c < a

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a : α
h : 0 < a
b : α
this : 0 < a / ((b + 1) ⊔ 1)
⊢ ∃ c, 0 < c ∧ b * c < a

Tactic:
refine ⟨a / max (b + 1) 1, this, ?_⟩

Result:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a : α
h : 0 < a
b : α
this : 0 < a / ((b + 1) ⊔ 1)
⊢ b * (a / ((b + 1) ⊔ 1)) < a
-- Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean
@[stacks 04XU]
lemma Scheme.Hom.isProperMap (f : X.Hom Y) [UniversallyClosed f] : IsProperMap f.base

Proof state:
case refine_1
X Y : Scheme
f : X.Hom Y
inst✝ : UniversallyClosed f
⊢ IsClosedMap ⇑(ConcreteCategory.hom f.base)

Tactic:
exact MorphismProperty.universally_le (P := topologically @IsClosedMap) _ UniversallyClosed.out

Result:
no goals

Proof state:
case refine_2
X Y : Scheme
f : X.Hom Y
inst✝ : UniversallyClosed f
y : ↑↑Y.toPresheafedSpace
this : CompactSpace ↑↑(pullback f (Y.fromSpecResidueField y)).toPresheafedSpace
⊢ IsCompact (Set.range ⇑(ConcreteCategory.hom (pullback.fst f (Y.fromSpecResidueField y)).base))

Tactic:
exact isCompact_range (Scheme.Hom.continuous _)

Result:
no goals

Proof state:
case refine_2
X Y : Scheme
f : X.Hom Y
inst✝ : UniversallyClosed f
y : ↑↑Y.toPresheafedSpace
this : CompactSpace ↑↑(pullback f (Y.fromSpecResidueField y)).toPresheafedSpace
⊢ IsCompact (⇑(ConcreteCategory.hom f.base) ⁻¹' {y})

Tactic:
rw [← Scheme.range_fromSpecResidueField, ← Scheme.Pullback.range_fst]

Result:
case refine_2
X Y : Scheme
f : X.Hom Y
inst✝ : UniversallyClosed f
y : ↑↑Y.toPresheafedSpace
this : CompactSpace ↑↑(pullback f (Y.fromSpecResidueField y)).toPresheafedSpace
⊢ IsCompact (Set.range ⇑(ConcreteCategory.hom (pullback.fst f (Y.fromSpecResidueField y)).base))

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝ : UniversallyClosed f
⊢ Continuous ⇑(ConcreteCategory.hom f.base) ∧
    IsClosedMap ⇑(ConcreteCategory.hom f.base) ∧
      ∀ (y : ↑↑Y.toPresheafedSpace), IsCompact (⇑(ConcreteCategory.hom f.base) ⁻¹' {y})

Tactic:
refine ⟨Scheme.Hom.continuous f, ?_, ?_⟩

Result:
case refine_1
X Y : Scheme
f : X.Hom Y
inst✝ : UniversallyClosed f
⊢ IsClosedMap ⇑(ConcreteCategory.hom f.base)

case refine_2
X Y : Scheme
f : X.Hom Y
inst✝ : UniversallyClosed f
⊢ ∀ (y : ↑↑Y.toPresheafedSpace), IsCompact (⇑(ConcreteCategory.hom f.base) ⁻¹' {y})

Proof state:
case refine_2
X Y : Scheme
f : X.Hom Y
inst✝ : UniversallyClosed f
y : ↑↑Y.toPresheafedSpace
⊢ IsCompact (⇑(ConcreteCategory.hom f.base) ⁻¹' {y})

Tactic:
have := compactSpace_of_universallyClosed (pullback.snd f (Y.fromSpecResidueField y))

Result:
case refine_2
X Y : Scheme
f : X.Hom Y
inst✝ : UniversallyClosed f
y : ↑↑Y.toPresheafedSpace
this : CompactSpace ↑↑(pullback f (Y.fromSpecResidueField y)).toPresheafedSpace
⊢ IsCompact (⇑(ConcreteCategory.hom f.base) ⁻¹' {y})

Proof state:
case refine_2
X Y : Scheme
f : X.Hom Y
inst✝ : UniversallyClosed f
⊢ ∀ (y : ↑↑Y.toPresheafedSpace), IsCompact (⇑(ConcreteCategory.hom f.base) ⁻¹' {y})

Tactic:
intro y

Result:
case refine_2
X Y : Scheme
f : X.Hom Y
inst✝ : UniversallyClosed f
y : ↑↑Y.toPresheafedSpace
⊢ IsCompact (⇑(ConcreteCategory.hom f.base) ⁻¹' {y})

Proof state:
X Y : Scheme
f : X.Hom Y
inst✝ : UniversallyClosed f
⊢ IsProperMap ⇑(ConcreteCategory.hom f.base)

Tactic:
rw [isProperMap_iff_isClosedMap_and_compact_fibers]

Result:
X Y : Scheme
f : X.Hom Y
inst✝ : UniversallyClosed f
⊢ Continuous ⇑(ConcreteCategory.hom f.base) ∧
    IsClosedMap ⇑(ConcreteCategory.hom f.base) ∧
      ∀ (y : ↑↑Y.toPresheafedSpace), IsCompact (⇑(ConcreteCategory.hom f.base) ⁻¹' {y})
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsBasis'.encard_eq_encard (hI : M.IsBasis' I X) (hJ : M.IsBasis' J X) :
    I.encard = J.encard

Proof state:
α : Type u_1
M : Matroid α
I X J : Set α
hI : M.IsBasis' I X
hJ : M.IsBasis' J X
⊢ I.encard = J.encard

Tactic:
rw [← isBase_restrict_iff'] at hI hJ

Result:
α : Type u_1
M : Matroid α
I X J : Set α
hI : (M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
⊢ I.encard = J.encard

Proof state:
α : Type u_1
M : Matroid α
I X J : Set α
hI : (M ↾ X).IsBase I
hJ : (M ↾ X).IsBase J
⊢ I.encard = J.encard

Tactic:
exact hI.encard_eq_encard_of_isBase hJ

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
theorem charpoly_degree_eq_dim [Nontrivial R] (M : Matrix n n R) :
    M.charpoly.degree = Fintype.card n

Proof state:
case pos
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ M.charmatrix.det.degree = ↑0

Tactic:
rw [det_of_card_zero]

Result:
case pos
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ degree 1 = ↑0

case pos.h
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ Fintype.card n = 0

Proof state:
case h
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
⊢ ∏ x : n, 1 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
case pos.h
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ Fintype.card n = 0

Tactic:
assumption

Result:
no goals

Proof state:
case pos
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ M.charpoly.degree = ↑0

Tactic:
unfold charpoly

Result:
case pos
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : Fintype.card n = 0
⊢ M.charmatrix.det.degree = ↑0

Proof state:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ Fintype.card n - 1 < Fintype.card n

Tactic:
rw [← Nat.pred_eq_sub_one]

Result:
case neg
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ (Fintype.card n).pred < Fintype.card n

Proof state:
case neg.a
R : Type u
inst✝³ : CommRing R
n : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Nontrivial R
M : Matrix n n R
h : ¬Fintype.card n = 0
h1 : (∏ i : n, (X - C (M i i))).degree = ↑(Fintype.card n)
⊢ Fintype.card n ≠ 0

Tactic:
apply h

Result:
no goals