harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/ByteArray.lean
theorem size_extract (a : ByteArray) (start stop) :
    (a.extract start stop).size = min stop a.size - start

Proof state:
a : ByteArray
start stop : Nat
⊢ (a.extract start stop).size = min stop a.size - start

Tactic:
simp [size]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/GetElem.lean
theorem get_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom]
    (c : cont) (i : idx) [Decidable (dom c i)] (h) :
    c[i]?.get h = c[i]'(by simp only [getElem?_def] at h; split at h <;> simp_all)

Proof state:
cont : Type ?u.7821
idx : Type ?u.7820
elem : Type ?u.7819
dom : cont → idx → Prop
inst✝² : GetElem? cont idx elem dom
inst✝¹ : LawfulGetElem cont idx elem dom
c : cont
i : idx
inst✝ : Decidable (dom c i)
h : (if h : dom c i then some (getElem c i h) else none).isSome = true
⊢ dom c i

Tactic:
split at h <;> simp_all

Result:
no goals

Proof state:
cont : Type ?u.7821
idx : Type ?u.7820
elem : Type ?u.7819
dom : cont → idx → Prop
inst✝² : GetElem? cont idx elem dom
inst✝¹ : LawfulGetElem cont idx elem dom
c : cont
i : idx
inst✝ : Decidable (dom c i)
h : (getElem? c i).isSome = true
⊢ dom c i

Tactic:
simp only [getElem?_def] at h

Result:
cont : Type ?u.7821
idx : Type ?u.7820
elem : Type ?u.7819
dom : cont → idx → Prop
inst✝² : GetElem? cont idx elem dom
inst✝¹ : LawfulGetElem cont idx elem dom
c : cont
i : idx
inst✝ : Decidable (dom c i)
h : (if h : dom c i then some (getElem c i h) else none).isSome = true
⊢ dom c i

Proof state:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝² : GetElem? cont idx elem dom
inst✝¹ : LawfulGetElem cont idx elem dom
c : cont
i : idx
inst✝ : Decidable (dom c i)
h✝ : (getElem? c i).isSome = true
h : (if h : dom c i then some (getElem c i h) else none).isSome = true
⊢ (if h : dom c i then some (getElem c i h) else none).get ⋯ = getElem c i ⋯

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝² : GetElem? cont idx elem dom
inst✝¹ : LawfulGetElem cont idx elem dom
c : cont
i : idx
inst✝ : Decidable (dom c i)
h : (getElem? c i).isSome = true
⊢ (getElem? c i).get h = getElem c i ⋯

Tactic:
simp only [getElem?_def] at h ⊢

Result:
cont : Type u_1
idx : Type u_2
elem : Type u_3
dom : cont → idx → Prop
inst✝² : GetElem? cont idx elem dom
inst✝¹ : LawfulGetElem cont idx elem dom
c : cont
i : idx
inst✝ : Decidable (dom c i)
h✝ : (getElem? c i).isSome = true
h : (if h : dom c i then some (getElem c i h) else none).isSome = true
⊢ (if h : dom c i then some (getElem c i h) else none).get ⋯ = getElem c i ⋯
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The Dirichlet character mod `0` corresponds to `δ`. -/
lemma modZero_eq_delta {χ : DirichletCharacter ℂ 0} : ↗χ = δ

Proof state:
case h
χ : DirichletCharacter ℂ 0
n : ℕ
⊢ χ ↑n = δ n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Result:
case h.inl
χ : DirichletCharacter ℂ 0
⊢ χ ↑0 = δ 0

case h.inr
χ : DirichletCharacter ℂ 0
n : ℕ
hn : n ≠ 0
⊢ χ ↑n = δ n

Proof state:
case h.inr
χ : DirichletCharacter ℂ 0
n : ℕ
hn : n ≠ 0
⊢ χ ↑n = δ n

Tactic:
rcases eq_or_ne n 1 with rfl | hn'

Result:
case h.inr.inl
χ : DirichletCharacter ℂ 0
hn : 1 ≠ 0
⊢ χ ↑1 = δ 1

case h.inr.inr
χ : DirichletCharacter ℂ 0
n : ℕ
hn : n ≠ 0
hn' : n ≠ 1
⊢ χ ↑n = δ n

Proof state:
χ : DirichletCharacter ℂ 0
⊢ (fun n => χ ↑n) = δ

Tactic:
ext n

Result:
case h
χ : DirichletCharacter ℂ 0
n : ℕ
⊢ χ ↑n = δ n

Proof state:
case h.inr.inr
χ : DirichletCharacter ℂ 0
n : ℕ
hn : n ≠ 0
hn' : n ≠ 1
⊢ χ ↑n = δ n

Tactic:
have : ¬ IsUnit (n : ZMod 0) := fun h ↦ hn' <| ZMod.eq_one_of_isUnit_natCast h

Result:
case h.inr.inr
χ : DirichletCharacter ℂ 0
n : ℕ
hn : n ≠ 0
hn' : n ≠ 1
this : ¬IsUnit ↑n
⊢ χ ↑n = δ n

Proof state:
case h.inl
χ : DirichletCharacter ℂ 0
⊢ χ ↑0 = δ 0

Tactic:
simp_rw [cast_zero, χ.map_nonunit not_isUnit_zero, delta, reduceCtorEq, if_false]

Result:
no goals

Proof state:
case h.inr.inr
χ : DirichletCharacter ℂ 0
n : ℕ
hn : n ≠ 0
hn' : n ≠ 1
this : ¬IsUnit ↑n
⊢ χ ↑n = δ n

Tactic:
simp_all [χ.map_nonunit this, delta]

Result:
no goals

Proof state:
case h.inr.inl
χ : DirichletCharacter ℂ 0
hn : 1 ≠ 0
⊢ χ ↑1 = δ 1

Tactic:
simp [delta]

Result:
no goals
-- Mathlib/Data/Rat/Lemmas.lean
theorem num_div_eq_of_coprime {a b : ℤ} (hb0 : 0 < b) (h : Nat.Coprime a.natAbs b.natAbs) :
    (a / b : ℚ).num = a

Proof state:
a b : ℤ
hb0 : 0 < b
h : a.natAbs.Coprime b.natAbs
⊢ (↑a / ↑b).num = a

Tactic:
rw [← Int.natAbs_of_nonneg hb0.le, ← Rat.divInt_eq_div,
  ← mk_eq_divInt _ _ (Int.natAbs_ne_zero.mpr hb0.ne') h]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
lemma in₁₂_iff' :
    (graph t).Adj (in₁ b) (in₂ c) ↔ ∃ x : α × β × γ, x ∈ t ∧ x.2.1 = b ∧ x.2.2 = c where
  mp

Proof state:
case intro.mk.mk.intro.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (?intro.mk.mk.intro.intro.a, (a, b, c).2.1, (a, b, c).2.2) ∈ t

case intro.mk.mk.intro.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ α

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ (a✝¹, b, c).2.1 = b ∧ (a✝¹, b, c).2.2 = c

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
⊢ (∃ x ∈ t, x.2.1 = b ∧ x.2.2 = c) → (graph t).Adj (in₁ b) (in₂ c)

Tactic:
rintro ⟨⟨a, b, c⟩, h, rfl, rfl⟩

Result:
case intro.mk.mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₁ (a, b, c).2.1) (in₂ (a, b, c).2.2)

Proof state:
case in₁₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ ∃ x ∈ t, x.2.1 = b ∧ x.2.2 = c

Tactic:
exact ⟨_, ‹_›, by simp⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
⊢ (graph t).Adj (in₁ b) (in₂ c) → ∃ x ∈ t, x.2.1 = b ∧ x.2.2 = c

Tactic:
rintro ⟨⟩

Result:
case in₁₂
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
b : β
c : γ
a✝¹ : α
a✝ : (a✝¹, b, c) ∈ t
⊢ ∃ x ∈ t, x.2.1 = b ∧ x.2.2 = c

Proof state:
case intro.mk.mk.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (graph t).Adj (in₁ (a, b, c).2.1) (in₂ (a, b, c).2.2)

Tactic:
constructor

Result:
case intro.mk.mk.intro.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ (?intro.mk.mk.intro.intro.a, (a, b, c).2.1, (a, b, c).2.2) ∈ t

case intro.mk.mk.intro.intro.a
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
b : β
c : γ
h : (a, b, c) ∈ t
⊢ α
-- Mathlib/LinearAlgebra/Matrix/Determinant/TotallyUnimodular.lean
/-- If `A` is totally unimodular and each row of `B` is all zeros except for at most a single `1` or
a single `-1` then `fromRows A B` is totally unimodular. -/
lemma IsTotallyUnimodular.fromRows_unitlike [DecidableEq n] {A : Matrix m n R} {B : Matrix m' n R}
    (hA : A.IsTotallyUnimodular)
    (hB : Nonempty n → ∀ i : m', ∃ j : n, ∃ s : SignType, B i = Pi.single j s.cast) :
    (fromRows A B).IsTotallyUnimodular

Proof state:
case neg
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
j' : n
s : SignType
hj' : B j = Pi.single j' ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x : Fin k.succ,
      (-1) ^ (↑i + ↑x) * Pi.single j' (↑s) (g x) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
hj'' : ∀ (x : Fin (k + 1)), ¬g x = j'
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast

Tactic:
use 0

Result:
case h
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
k : ℕ
ih :
  ∀ (f : Fin k → m ⊕ m') (g : Fin k → n),
    Function.Injective f → Function.Injective g → ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
f : Fin (k + 1) → m ⊕ m'
g : Fin (k + 1) → n
hf : Function.Injective f
hg : Function.Injective g
hB : ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
i : Fin (k + 1)
j : m'
hfi : f i = Sum.inr j
j' : n
s : SignType
hj' : B j = Pi.single j' ↑s
hAB :
  ((A.fromRows B).submatrix f g).det =
    ∑ x : Fin k.succ,
      (-1) ^ (↑i + ↑x) * Pi.single j' (↑s) (g x) *
        (((A.fromRows B).submatrix f g).submatrix i.succAbove x.succAbove).det
hj'' : ∀ (x : Fin (k + 1)), ¬g x = j'
⊢ ↑0 = ((A.fromRows B).submatrix f g).det

Proof state:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : Nonempty n → ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
⊢ (A.fromRows B).IsTotallyUnimodular

Tactic:
intro k f g hf hg

Result:
m : Type u_1
m' : Type u_2
n : Type u_3
R : Type u_5
inst✝¹ : CommRing R
inst✝ : DecidableEq n
A : Matrix m n R
B : Matrix m' n R
hA : A.IsTotallyUnimodular
hB : Nonempty n → ∀ (i : m'), ∃ j s, B i = Pi.single j ↑s
k : ℕ
f : Fin k → m ⊕ m'
g : Fin k → n
hf : Function.Injective f
hg : Function.Injective g
⊢ ((A.fromRows B).submatrix f g).det ∈ Set.range SignType.cast
-- Mathlib/RingTheory/Trace/Basic.lean
theorem PowerBasis.trace_gen_eq_nextCoeff_minpoly [Nontrivial S] (pb : PowerBasis K S) :
    Algebra.trace K S pb.gen = -(minpoly K pb.gen).nextCoeff

Proof state:
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
⊢ 0 < (minpoly K pb.gen).natDegree

Tactic:
simpa

Result:
no goals

Proof state:
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
⊢ (Algebra.trace K S) pb.gen = -(minpoly K pb.gen).nextCoeff

Tactic:
have d_pos' : 0 < (minpoly K pb.gen).natDegree := by simpa

Result:
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
d_pos' : 0 < (minpoly K pb.gen).natDegree
⊢ (Algebra.trace K S) pb.gen = -(minpoly K pb.gen).nextCoeff

Proof state:
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
d_pos' : 0 < (minpoly K pb.gen).natDegree
this : Nonempty (Fin pb.dim)
⊢ (Algebra.trace K S) pb.gen = -(minpoly K pb.gen).nextCoeff

Tactic:
rw [trace_eq_matrix_trace pb.basis, trace_eq_neg_charpoly_coeff, charpoly_leftMulMatrix, ←
  pb.natDegree_minpoly, Fintype.card_fin, ← nextCoeff_of_natDegree_pos d_pos']

Result:
no goals

Proof state:
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
d_pos' : 0 < (minpoly K pb.gen).natDegree
⊢ (Algebra.trace K S) pb.gen = -(minpoly K pb.gen).nextCoeff

Tactic:
haveI : Nonempty (Fin pb.dim) := ⟨⟨0, d_pos⟩⟩

Result:
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
d_pos' : 0 < (minpoly K pb.gen).natDegree
this : Nonempty (Fin pb.dim)
⊢ (Algebra.trace K S) pb.gen = -(minpoly K pb.gen).nextCoeff

Proof state:
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : Nontrivial S
pb : PowerBasis K S
⊢ (Algebra.trace K S) pb.gen = -(minpoly K pb.gen).nextCoeff

Tactic:
have d_pos : 0 < pb.dim := PowerBasis.dim_pos pb

Result:
S : Type u_2
inst✝³ : CommRing S
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra K S
inst✝ : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
⊢ (Algebra.trace K S) pb.gen = -(minpoly K pb.gen).nextCoeff
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma epi_homologyMap_of_epi_cyclesMap'
    [S₁.HasHomology] [S₂.HasHomology] (h : Epi (cyclesMap φ)) :
    Epi (homologyMap φ)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h : Epi (cyclesMap φ)
⊢ Epi (homologyMap φ)

Tactic:
have : Epi (S₁.homologyπ ≫ homologyMap φ) := by
  rw [homologyπ_naturality φ]
  apply epi_comp

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h : Epi (cyclesMap φ)
this : Epi (S₁.homologyπ ≫ homologyMap φ)
⊢ Epi (homologyMap φ)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h : Epi (cyclesMap φ)
this : Epi (S₁.homologyπ ≫ homologyMap φ)
⊢ Epi (homologyMap φ)

Tactic:
exact epi_of_epi S₁.homologyπ (homologyMap φ)

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h : Epi (cyclesMap φ)
⊢ Epi (S₁.homologyπ ≫ homologyMap φ)

Tactic:
rw [homologyπ_naturality φ]

Result:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h : Epi (cyclesMap φ)
⊢ Epi (cyclesMap φ ≫ S₂.homologyπ)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h : Epi (cyclesMap φ)
⊢ Epi (cyclesMap φ ≫ S₂.homologyπ)

Tactic:
apply epi_comp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
lemma inl_eq_inr_iff [Mono f] (x₁ : X₁) (x₂ : X₂) :
    (inl f g x₁ = inr f g x₂) ↔
      ∃ (s : S), f s = x₁ ∧ g s = x₂

Proof state:
case mpr.intro.intro
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
⊢ Rel' f g (Sum.inl (f s)) (Sum.inr (g s))

Tactic:
apply Rel'.inl_inr

Result:
no goals

Proof state:
case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₁ : X₁
x₂ : X₂
⊢ Rel' f g (Sum.inl x₁) (Sum.inr x₂) → ∃ s, f s = x₁ ∧ g s = x₂

Tactic:
rintro ⟨⟩

Result:
case mp.inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
⊢ ∃ s, f s = f s✝ ∧ g s = g s✝

Proof state:
case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₁ : X₁
x₂ : X₂
⊢ (∃ s, f s = x₁ ∧ g s = x₂) → Rel' f g (Sum.inl x₁) (Sum.inr x₂)

Tactic:
rintro ⟨s, rfl, rfl⟩

Result:
case mpr.intro.intro
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
⊢ Rel' f g (Sum.inl (f s)) (Sum.inr (g s))

Proof state:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₁ : X₁
x₂ : X₂
⊢ inl f g x₁ = inr f g x₂ ↔ ∃ s, f s = x₁ ∧ g s = x₂

Tactic:
refine (Pushout.quot_mk_eq_iff f g (Sum.inl x₁) (Sum.inr x₂)).trans ?_

Result:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₁ : X₁
x₂ : X₂
⊢ Rel' f g (Sum.inl x₁) (Sum.inr x₂) ↔ ∃ s, f s = x₁ ∧ g s = x₂

Proof state:
case mp.inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
⊢ ∃ s, f s = f s✝ ∧ g s = g s✝

Tactic:
exact ⟨_, rfl, rfl⟩

Result:
no goals

Proof state:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₁ : X₁
x₂ : X₂
⊢ Rel' f g (Sum.inl x₁) (Sum.inr x₂) ↔ ∃ s, f s = x₁ ∧ g s = x₂

Tactic:
constructor

Result:
case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₁ : X₁
x₂ : X₂
⊢ Rel' f g (Sum.inl x₁) (Sum.inr x₂) → ∃ s, f s = x₁ ∧ g s = x₂

case mpr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₁ : X₁
x₂ : X₂
⊢ (∃ s, f s = x₁ ∧ g s = x₂) → Rel' f g (Sum.inl x₁) (Sum.inr x₂)
-- Mathlib/Data/Fintype/Fin.lean
theorem card_filter_univ_succ (p : Fin (n + 1) → Prop) [DecidablePred p] :
    #{x | p x} = if p 0 then #{x | p (.succ x)} + 1 else #{x | p (.succ x)}

Proof state:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ #(filter (fun x => p x) univ) =
    if p 0 then #(filter (fun x => p x.succ) univ) + 1 else #(filter (fun x => p x.succ) univ)

Tactic:
rw [Fin.univ_succ, filter_cons, apply_ite Finset.card, card_cons, filter_map, card_map]

Result:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ (if p 0 then #(filter ((fun x => p x) ∘ ⇑{ toFun := succ, inj' := ⋯ }) univ) + 1
    else #(filter ((fun x => p x) ∘ ⇑{ toFun := succ, inj' := ⋯ }) univ)) =
    if p 0 then #(filter (fun x => p x.succ) univ) + 1 else #(filter (fun x => p x.succ) univ)

Proof state:
n : ℕ
p : Fin (n + 1) → Prop
inst✝ : DecidablePred p
⊢ (if p 0 then #(filter ((fun x => p x) ∘ ⇑{ toFun := succ, inj' := ⋯ }) univ) + 1
    else #(filter ((fun x => p x) ∘ ⇑{ toFun := succ, inj' := ⋯ }) univ)) =
    if p 0 then #(filter (fun x => p x.succ) univ) + 1 else #(filter (fun x => p x.succ) univ)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get_insertMany_empty_list_of_mem [LawfulBEq α]
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l)
    {h} :
    (insertMany empty l).1.get k' h = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v

Proof state:
case e_a
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h : (empty.insertMany l).val.contains k' = true
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h : (empty.insertMany l).val.contains k' = true
⊢ (empty.insertMany l).val.get k' h = cast ⋯ v

Tactic:
rw [get_insertMany_list_of_mem _ Raw.WF.empty₀ k_beq distinct mem]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h : (empty.insertMany l).val.contains k' = true
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
h : (empty.insertMany l).val.contains k' = true
⊢ k = k'
-- Mathlib/Data/Finset/Card.lean
theorem one_lt_card_iff : 1 < #s ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Proof state:
α : Type u_1
s : Finset α
⊢ 1 < #s ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
rw [one_lt_card]

Result:
α : Type u_1
s : Finset α
⊢ (∃ a ∈ s, ∃ b ∈ s, a ≠ b) ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Proof state:
α : Type u_1
s : Finset α
⊢ (∃ a ∈ s, ∃ b ∈ s, a ≠ b) ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠ b

Tactic:
simp only [exists_prop, exists_and_left]

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem prod_mk {m : MeasurableSpace α} [TopologicalSpace β] [TopologicalSpace γ]
    {f : α → β} {g : α → γ} (hf : StronglyMeasurable f) (hg : StronglyMeasurable g) :
    StronglyMeasurable fun x => (f x, g x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun n => ((fun n => (hf.approx n).pair (hg.approx n)) n) x) atTop (𝓝 ((fun x => (f x, g x)) x))

Tactic:
rw [nhds_prod_eq]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun n => ((fun n => (hf.approx n).pair (hg.approx n)) n) x) atTop (𝓝 (f x) ×ˢ 𝓝 (g x))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun n => ((fun n => (hf.approx n).pair (hg.approx n)) n) x) atTop (𝓝 (f x) ×ˢ 𝓝 (g x))

Tactic:
exact Tendsto.prod_mk (hf.tendsto_approx x) (hg.tendsto_approx x)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable fun x => (f x, g x)

Tactic:
refine ⟨fun n => SimpleFunc.pair (hf.approx n) (hg.approx n), fun x => ?_⟩

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
g : α → γ
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto (fun n => ((fun n => (hf.approx n).pair (hg.approx n)) n) x) atTop (𝓝 ((fun x => (f x, g x)) x))
-- Mathlib/Order/Atoms.lean
theorem isCoatom_iff (s : Set α) : IsCoatom s ↔ ∃ x, s = {x}ᶜ

Proof state:
α : Type u_2
s : Set α
⊢ (∃ x, sᶜ = {x}) ↔ ∃ x, s = {x}ᶜ

Tactic:
simp_rw [@eq_comm _ s, compl_eq_comm]

Result:
no goals

Proof state:
α : Type u_2
s : Set α
⊢ IsCoatom s ↔ ∃ x, s = {x}ᶜ

Tactic:
rw [isCompl_compl.isCoatom_iff_isAtom, isAtom_iff]

Result:
α : Type u_2
s : Set α
⊢ (∃ x, sᶜ = {x}) ↔ ∃ x, s = {x}ᶜ
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk'_sec (z : N) : f.mk' (f.sec z).1 (f.sec z).2 = z :=
  show _ * _ = _ by rw [← sec_spec, mul_inv_left, mul_comm]

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
z : N
⊢ f.toMap (f.sec z).1 * ↑((IsUnit.liftRight (f.toMap.restrict S) ⋯) (f.sec z).2)⁻¹ = z

Tactic:
rw [← sec_spec, mul_inv_left, mul_comm]

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Finite.lean
lemma IsRkFinite.subset (h : M.IsRkFinite X) (hXY : Y ⊆ X) : M.IsRkFinite Y

Proof state:
α : Type u_1
M : Matroid α
X Y : Set α
h : M.IsRkFinite X
hXY : Y ⊆ X
⊢ M.IsRkFinite Y

Tactic:
obtain ⟨I, hI⟩ := M.exists_isBasis' Y

Result:
case intro
α : Type u_1
M : Matroid α
X Y : Set α
h : M.IsRkFinite X
hXY : Y ⊆ X
I : Set α
hI : M.IsBasis' I Y
⊢ M.IsRkFinite Y

Proof state:
case intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
h : M.IsRkFinite X
hXY : Y ⊆ X
I : Set α
hI : M.IsBasis' I Y
J : Set α
hJ : M.IsBasis' J X
hIJ : I ⊆ J
⊢ M.IsRkFinite Y

Tactic:
exact hI.isRkFinite_of_finite <| (hJ.finite_of_isRkFinite h).subset hIJ

Result:
no goals

Proof state:
case intro
α : Type u_1
M : Matroid α
X Y : Set α
h : M.IsRkFinite X
hXY : Y ⊆ X
I : Set α
hI : M.IsBasis' I Y
⊢ M.IsRkFinite Y

Tactic:
obtain ⟨J, hJ, hIJ⟩ := hI.indep.subset_isBasis'_of_subset (hI.subset.trans hXY)

Result:
case intro.intro.intro
α : Type u_1
M : Matroid α
X Y : Set α
h : M.IsRkFinite X
hXY : Y ⊆ X
I : Set α
hI : M.IsBasis' I Y
J : Set α
hJ : M.IsBasis' J X
hIJ : I ⊆ J
⊢ M.IsRkFinite Y